Ideal

Results named in Tau Ceti's TauCeti.RingTheory.Ideal modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremArtin–Rees for a finitely generated submodule#

If N₀ is a finitely generated submodule over a noetherian ring, there is a shift k such that I ^ (n + k) • N₀ ⊓ L equals I ^ n • (I ^ k • N₀ ⊓ L) for every submodule L and every n. The ambient module need not be finite: only N₀ is, so Mathlib's Ideal.exists_pow_inf_eq_pow_smul is applied inside N₀. In particular I ^ (n + k) • N₀ ⊓ L ≤ I ^ n • L; when L ≤ N₀, this shows that the filtration N₀ induces on L is cofinal in the I-adic filtration of L.

Ideal.exists_pow_add_smul_inf_eq_pow_smul.{u_1, u_2} {R : Type u_1} [CommRing R] {M : Type u_2}
  [AddCommGroup M] [_root_.Module R M] [IsNoetherianRing R] (I : Ideal R) {N₀ : Submodule R M}
  (hN₀ : N₀.FG) (L : Submodule R M) :
  ∃ k, ∀ (n : ℕ), I ^ (n + k) • N₀ ⊓ L = I ^ n • (I ^ k • N₀ ⊓ L)
Lean

Formalized in Tau Ceti as Ideal.exists_pow_add_smul_inf_eq_pow_smul.

Sources
LeanIdeal.exists_pow_add_smul_inf_eq_pow_smul
Used by 1
Used byLinear maps of finite modules over a Huber ring with a noetherian ring of definition are strict (Huber, Lemma 2.3(i))

TheoremThe Golod–Shafarevich inequality for finite-dimensional algebras#

Let A be a finite-dimensional algebra over a field k and I a proper two-sided ideal of A, generated as a left ideal by a nonempty finite family x. If every relation ∑ aᵢ xᵢ = 0 among the generators is an A-linear combination of a finite family y of vectors in A^ι with all entries in I, then (#x)² < 4 · #y.

TauCeti.card_sq_lt_four_mul_card_of_relations_le_span.{u_1, u_2, u_3, u_4} {A : Type u_1} [Ring A]
  {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] (k : Type u_4) [Field k] [Algebra k A]
  [FiniteDimensional k A] [Nonempty ι] (I : Ideal A) [I.IsTwoSided] (hI : I ≠ ⊤) (x : ι → A)
  (hx : Submodule.span A (Set.range x) = I) (y : κ → ι → A) (hy : ∀ (j : κ) (i : ι), y j i ∈ I)
  (hker : ∀ (a : ι → A), ∑ i, a i * x i = 0 → a ∈ Submodule.span A (Set.range y)) :
  Fintype.card ι ^ 2 < 4 * Fintype.card κ
Lean

Formalized in Tau Ceti as TauCeti.card_sq_lt_four_mul_card_of_relations_le_span.

Sources
LeanTauCeti.card_sq_lt_four_mul_card_of_relations_le_span
Used by 1
Used byThe Golod–Shafarevich inequality

TheoremThe Krull intersection theorem for an extended ideal#

If R is Noetherian and A is a finite R-module, an element of every power of the two-sided ideal of A generated by I is fixed by multiplication by some scalar in I.

Ideal.mem_iInf_map_algebraMap_pow_iff.{u_1, u_2} {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A]
  [Algebra R A] [IsNoetherianRing R] [Module.Finite R A] (I : Ideal R) (x : A) :
  x ∈ ⨅ n, Ideal.map (algebraMap R A) I ^ n ↔ ∃ r ∈ I, (algebraMap R A) r * x = x
Lean

Formalized in Tau Ceti as Ideal.mem_iInf_map_algebraMap_pow_iff.

Sources
LeanIdeal.mem_iInf_map_algebraMap_pow_iff
Used by 2
Used byAdo's theorem in characteristic zero · Hochschild's strengthening of the Ado–Iwasawa theorem

TheoremSerre's criterion#

When S is generated over R by a set s and G acts by R-algebra automorphisms, membership in the inertia subgroup of a two-sided ideal I is decided on s alone: the elements moved into I form an R-subalgebra.

TauCeti.Ideal.mem_inertia_iff_of_adjoin_eq_top.{u_1, u_2, u_3} {G : Type u_1} [Group G]
  {S : Type u_2} [Ring S] [MulSemiringAction G S] {R : Type u_3} [CommSemiring R] [Algebra R S]
  [SMulCommClass G R S] {I : Ideal S} [I.IsTwoSided] {s : Set S} (hs : Algebra.adjoin R s = ⊤)
  {σ : G} : σ ∈ Ideal.inertia G I ↔ ∀ x ∈ s, σ • x - x ∈ I
Lean

Formalized in Tau Ceti as TauCeti.Ideal.mem_inertia_iff_of_adjoin_eq_top.

Sources
LeanTauCeti.Ideal.mem_inertia_iff_of_adjoin_eq_top
Used by 4
Used byTauCeti.DyadicCyclotomicEight.map_restrictSqrtTwo_lowerRamificationGroup_three_ne · Serre's quotient formula for the lower index · Hilbert's counting identity · Serre's criterion for the ramification filtration

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.