10.44 Separable extensions… to 10.63 Associated primes

Section10.44 Separable extensions, continued#

Section 10.44 of the Stacks Project, Tag 05DT. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 030W, a lemma

Tag 030W in the Stacks Project.

Algebra.isSeparableExtension_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/Separable/TFAE.lean, line 194. The attribute's comment: “Stated for the exponential characteristic, so that characteristic zero is the case p = 1, where all four conditions hold; the source assumes p > 0. Condition (2) quantifies over arbitrary, not just finite, linearly independent subsets. See the module docstring.”.

Stacks 030W. Let k be a field of exponential characteristic p and let K/k be a field extension. The following are equivalent: K is separable over k (Definition Stacks 030O); for every k-linearly independent subset s of K the set of p-th powers of elements of s is k-linearly independent; the ring K ⊗_k k^{1/p} is reduced; and K is geometrically reduced over k.

public theorem Algebra.isSeparableExtension_tfae (k K : Type*) [Field k] [Field K] [Algebra k K]
    (p : ℕ) [ExpChar k p] :
    List.TFAE
      [Algebra.IsSeparableExtension k K,
        ∀ s : Set K, LinearIndepOn k _root_.id s → LinearIndepOn k (· ^ p) s,
        IsReduced (K ⊗[k] AdjoinPthRoots k),
        Algebra.IsGeometricallyReduced k K]
Tag 030X, a lemma

Tag 030X in the Stacks Project.

exists_isTranscendenceBasis_and_isSeparable_of_isSeparable_adjoin_of_essFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/Separable/Basic.lean, line 88.

A separably generated field extension is separable. Let K/k be a field extension with a separating transcendence basis s, that is, a transcendence basis of K/k such that K is separable algebraic over k(s). Then every subextension k ⊆ L ⊆ K which is finitely generated over k again has a separating transcendence basis: there is a finite transcendence basis t of L/k such that L is separable algebraic over k(t).

public theorem exists_isTranscendenceBasis_and_isSeparable_of_isSeparable_adjoin_of_essFiniteType
    {k K L : Type*} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] [Algebra L K]
    [IsScalarTower k L K] [Algebra.EssFiniteType k L] {s : Set K}
    (hs : IsTranscendenceBasis k ((↑) : s → K))
    (hsep : Algebra.IsSeparable (IntermediateField.adjoin k s) K) :
    ∃ t : Finset L,
      IsTranscendenceBasis k ((↑) : t → L) ∧
        Algebra.IsSeparable (IntermediateField.adjoin k (t : Set L)) L
Tag 030V, a lemma

Tag 030V in the Stacks Project.

Algebra.isGeometricallyReduced_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyReduced/TFAE.lean, line 198. The attribute's comment: “The source's five conditions in its order, with its definition of geometric reducedness spelled out as item (5), plus item (6), Mathlib's Algebra.IsGeometricallyReduced; k^{1/p} is AdjoinPthRoots k, and the perfect and algebraic closures are taken abstractly, as IsPerfectClosure and IsAlgClosure.”.

Let k be a field of exponential characteristic p and let S be a commutative k-algebra. The following are equivalent: (1) k' ⊗[k] S is reduced for every finite purely inseparable extension k'/k; (2) k^{1/p} ⊗[k] S is reduced, where k^{1/p} = AdjoinPthRoots k; (3) k^{perf} ⊗[k] S is reduced for a perfect closure k^{perf} of k; (4) K ⊗[k] S is reduced for an algebraic closure K of k; (5) L ⊗[k] S is reduced for every field extension L/k; (6) Algebra.IsGeometricallyReduced k S.

public theorem isGeometricallyReduced_tfae
    (k : Type u) [Field k] (p : ℕ) [ExpChar k p] (S : Type v) [CommRing S] [Algebra k S]
    (kperf : Type w) [Field kperf] [Algebra k kperf] [ExpChar kperf p] [PerfectRing kperf p]
    [IsPerfectClosure (algebraMap k kperf) p]
    (K : Type w') [Field K] [Algebra k K] [IsAlgClosure k K] :
    [∀ (k' : Type u) [Field k'] [Algebra k k'] [FiniteDimensional k k']
        [IsPurelyInseparable k k'], IsReduced (k' ⊗[k] S),
      IsReduced (AdjoinPthRoots k ⊗[k] S),
      IsReduced (kperf ⊗[k] S),
      IsReduced (K ⊗[k] S),
      ∀ (L : Type u) [Field L] [Algebra k L], IsReduced (L ⊗[k] S),
      IsGeometricallyReduced k S].TFAE
Sources
LeanAlgebra.isSeparableExtension_tfae · exists_isTranscendenceBasis_and_isSeparable_of_isSeparable_adjoin_of_essFiniteType · Algebra.isGeometricallyReduced_tfae

Section10.45 Perfect fields#

Section 10.45 of the Stacks Project, Tag 05DU. 4 tags here are carried by 2 declarations of the repository (all in StacksFrontier) and 6 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 030R, a lemma

Tag 030R in the Stacks Project.

exists_isPurelyInseparable_and_isSeparableExtension_of_essFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/PurelyInseparable/BaseChange.lean, line 979. References: EGA 0 (19.6.6).

Let K/k be a finitely generated field extension and let Ω/K be a perfect field extension. Then inside Ω there is a diagram 

K  →  K'
↑     ↑
k  →  k'
with k'/k and K'/K finite purely inseparable and K'/k' separable in the sense of [stacks, 030O](2), in which moreover K' is the compositum k'K and the canonical map k' ⊗[k] K → K' is surjective with kernel the nilradical, i.e. K' = (k' ⊗[k] K)_red.

public theorem exists_isPurelyInseparable_and_isSeparableExtension_of_essFiniteType
    (k K Ω : Type*) [Field k] [Field K] [Field Ω] [Algebra k K] [Algebra k Ω] [Algebra K Ω]
    [IsScalarTower k K Ω] [PerfectField Ω] [Algebra.EssFiniteType k K] :
    ∃ (K' : IntermediateField K Ω) (k' : IntermediateField k ↥K'),
      Module.Finite K ↥K' ∧ IsPurelyInseparable K ↥K' ∧
      Module.Finite k ↥k' ∧ IsPurelyInseparable k ↥k' ∧
      Algebra.IsSeparableExtension ↥k' ↥K' ∧
      IntermediateField.adjoin K (k' : Set ↥K') = ⊤ ∧
      Function.Surjective (Algebra.TensorProduct.productMap
        (IsScalarTower.toAlgHom k ↥k' ↥K') (IsScalarTower.toAlgHom k K ↥K')) ∧
      RingHom.ker (Algebra.TensorProduct.productMap
        (IsScalarTower.toAlgHom k ↥k' ↥K') (IsScalarTower.toAlgHom k K ↥K')) =
        nilradical (↥k' ⊗[k] K)
Tag 046W, a lemma

Tag 046W in the Stacks Project.

Declarations registered for the tag:

Tag 046X, a definition

Tag 046X in the Stacks Project.

Declarations registered for the tag:

Tag 00I4, a lemma

Tag 00I4 in the Stacks Project.

isReduced_tensorProduct_baseField_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorProduct/Reduced.lean, line 188. The attribute's comment: “Only the degenerate R = k case of clause (2); clause (1) and the general clause (2) are not formalized.”.

Stacks 00I4, the degenerate R = k case of clause (2): the tensor product k ⊗[k] S of k with a reduced k-algebra S is reduced.

theorem isReduced_tensorProduct_baseField_left (k : Type*) [Field k] (S : Type*)
    [CommRing S] [Algebra k S] [IsReduced S] : IsReduced (k ⊗[k] S)
Sources
Leanexists_isPurelyInseparable_and_isSeparableExtension_of_essFiniteType · perfectClosure.isPurelyInseparable · perfectClosure.perfectField · IsPurelyInseparable.instNonemptyAlgHomOfPerfectField · instSubsingletonAlgHomOfIsPurelyInseparable · perfectClosure · isReduced_tensorProduct_baseField_left

Section10.46 Universal homeomorphisms#

Section 10.46 of the Stacks Project, Tag 0BR5. 11 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BR6, a lemma

Tag 0BR6 in the Stacks Project.

Algebra.IsPushout.surjective_and_ker_eq_map_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversalHomeomorphism/Examples/BaseChange.lean, line 113. The attribute's comment: “The base change assertion.”.

Let R → S be a surjective ring map and let S' be the base change of S along an arbitrary ring map R → R', i.e. R', S' complete R, S to a pushout square of R-algebras. Then R' → S' is surjective and its kernel is the ideal of R' generated by the image of the kernel of R → S.

public theorem surjective_and_ker_eq_map_of_surjective
    {R S R' S' : Type*} [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R S]
    [Algebra R R'] [Algebra R S'] [Algebra S S'] [Algebra R' S'] [IsScalarTower R S S']
    [IsScalarTower R R' S'] [IsPushout R S R' S']
    (hsurj : Function.Surjective (algebraMap R S)) :
    Function.Surjective (algebraMap R' S') ∧
      RingHom.ker (algebraMap R' S') = (RingHom.ker (algebraMap R S)).map (algebraMap R R')
Tag 0BR7, a lemma

Tag 0BR7 in the Stacks Project.

forall_exists_pow_mem_iff_isPurelyInseparable_or_isAlgebraic_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversalHomeomorphism/Examples/PowerConditions.lean, line 613.

Let k'/k be a field extension. Then every element of k' has a positive power lying in k if and only if either k'/k is purely inseparable — which in characteristic zero means k' = k — or k' has positive characteristic and is algebraic over its prime field 𝐅_p.

public theorem forall_exists_pow_mem_iff_isPurelyInseparable_or_isAlgebraic_bot
    {k k' : Type*} [Field k] [Field k'] [Algebra k k'] :
    (∀ x : k', ∃ n > 0, x ^ n ∈ (algebraMap k k').range) ↔
      IsPurelyInseparable k k' ∨
        (ringChar k' ≠ 0 ∧ Algebra.IsAlgebraic (⊥ : Subfield k') k')
Tag 0BR8, a lemma

Tag 0BR8 in the Stacks Project.

Ideal.ResidueField.exists_pow_mem_range_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversalHomeomorphism/Examples/BaseChange.lean, line 168. The attribute's comment: “The residue field extensions.”.

Let f : R →+* S be a ring map such that every element of S has a positive power in the image of f, let q be a prime of S and let p = f⁻¹(q). Then every element of the residue field κ(q) has a positive power in the image of the canonical embedding κ(p) → κ(q); that is, the induced residue field extensions satisfy the equivalent conditions of forall_exists_pow_mem_iff_isPurelyInseparable_or_isAlgebraic_bot.

public theorem Ideal.ResidueField.exists_pow_mem_range_map {R S : Type*} [CommRing R] [CommRing S]
    {f : R →+* S} (H : ∀ x : S, ∃ n > 0, x ^ n ∈ f.range) (p : Ideal R) [p.IsPrime] (q : Ideal S)
    [q.IsPrime] (hpq : p = q.comap f) (x : q.ResidueField) :
    ∃ n > 0, x ^ n ∈ (Ideal.ResidueField.map p q f hpq).range
Tag 0EUH, a lemma

Tag 0EUH in the Stacks Project.

PrimeSpectrum.isHomeomorph_comap_and_residueFieldMap_bijective_of_adjoin_sq_cube_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversalHomeomorphism/Examples/GenerationCriteria.lean, line 765.

Let R → S be a ring map with locally nilpotent kernel such that S is generated as an R-algebra by elements whose square and cube lie in the image of R. Then Spec S → Spec R is a homeomorphism, the induced residue field extensions κ(𝔭) → κ(𝔮) are isomorphisms, and both hypotheses again hold for the base change R' → S' of R → S along any ring map R → R'.

public theorem isHomeomorph_comap_and_residueFieldMap_bijective_of_adjoin_sq_cube_eq_top
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    (hgen : Algebra.adjoin R
      {x : S | x ^ 2 ∈ (⊥ : Subalgebra R S) ∧ x ^ 3 ∈ (⊥ : Subalgebra R S)} = ⊤)
    (hker : RingHom.ker (algebraMap R S) ≤ nilradical R) :
    IsHomeomorph (comap (algebraMap R S)) ∧
      (∀ (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime]
        (hpq : p = q.comap (algebraMap R S)),
          Function.Bijective (Ideal.ResidueField.map p q (algebraMap R S) hpq)) ∧
      ∀ (R' : Type v) (S' : Type w) [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra R S']
        [Algebra S S'] [Algebra R' S'] [IsScalarTower R S S'] [IsScalarTower R R' S']
        [Algebra.IsPushout R S R' S'],
          Algebra.adjoin R'
            {x : S' | x ^ 2 ∈ (⊥ : Subalgebra R' S') ∧ x ^ 3 ∈ (⊥ : Subalgebra R' S')} = ⊤ ∧
            RingHom.ker (algebraMap R' S') ≤ nilradical R'
Tag 0545, a lemma

Tag 0545 in the Stacks Project.

Stacks.UniversalHomeomorphism.FrobeniusPowerSubring.exists_pow_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversalHomeomorphism/Examples/PowerConditions.lean, line 163.

Let p be a prime number and n, m > 0. Then there is an a such that both (x + y) ^ p ^ a and p ^ a (x + y) lie in R = ℤ[x ^ p ^ n, p ^ n x, y ^ p ^ m, p ^ m y], where x = X 0 and y = X 1.

theorem exists_pow_mem (p : ℕ) (hp : p.Prime) (n m : ℕ) (hn : 0 < n) (hm : 0 < m) :
    ∃ a : ℕ, (X 0 + X 1 : MvPolynomial (Fin 2) ℤ) ^ p ^ a ∈ subringR p n m ∧
      (p ^ a : ℤ) • (X 0 + X 1 : MvPolynomial (Fin 2) ℤ) ∈ subringR p n m
Tag 0BR9, a lemma

Tag 0BR9 in the Stacks Project.

satisfiesGeneratingCondition_iff_structuralCondition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversalHomeomorphism/Examples/PowerConditions.lean, line 230.

Let K / k be a field extension and p a prime. Then K is generated as a field extension of k by the elements x admitting an n > 0 with x ^ p ^ n ∈ k and p ^ n • x ∈ k — the generating condition of the source — if and only if either k = K, or the characteristic is p and K / k is purely inseparable, which is the source's structural condition.

The two directions are the two halves of the perfect closure: in characteristic p the generators lie in the perfect closure of k, which is therefore all of K; away from p the multiple p ^ n • x of a generator is x times a unit of k, so the generators lie in k already.

public theorem satisfiesGeneratingCondition_iff_structuralCondition
    {K : Type*} [Field K] (k : Subfield K) (p : ℕ) (hp : p.Prime) :
    Subfield.closure ((k : Set K) ∪ {x : K | ∃ n > 0, x ^ p ^ n ∈ k ∧ (p ^ n : ℕ) • x ∈ k}) = ⊤ ↔
      k = ⊤ ∨ (ringChar K = p ∧ IsPurelyInseparable k K)
Tag 0BRA, a lemma

Tag 0BRA in the Stacks Project.

PrimeSpectrum.isHomeomorph_comap_and_isPurelyInseparable_and_baseChange_of_adjoin_pow_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversalHomeomorphism/Examples/GenerationCriteria.lean, line 526.

Let p be a prime number and let φ : R → S be a ring map whose kernel is locally nilpotent and such that S is generated as an R-algebra by elements x for which there is an n > 0 with x ^ p ^ n and p ^ n • x in the image of φ. Then Spec(S) → Spec(R) is a homeomorphism, every induced residue field extension κ(𝔭) → κ(𝔮) is either surjective or of characteristic p and purely inseparable — the equivalent conditions of satisfiesGeneratingCondition_iff_structuralCondition — and both hypotheses hold again for every base change R' → S' of R → S along an arbitrary ring map R → R', i.e. for every pushout square of R-algebras completing R, S by R', S'.

public theorem isHomeomorph_comap_and_isPurelyInseparable_and_baseChange_of_adjoin_pow_eq_top
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (p : ℕ) (hp : p.Prime)
    (hker : RingHom.ker (algebraMap R S) ≤ nilradical R)
    (hgen : Algebra.adjoin R {x : S | ∃ n > 0, x ^ p ^ n ∈ (algebraMap R S).range ∧
      p ^ n • x ∈ (algebraMap R S).range} = ⊤) :
    IsHomeomorph (comap (algebraMap R S)) ∧
      (∀ (𝔭 : Ideal R) [𝔭.IsPrime] (𝔮 : Ideal S) [𝔮.IsPrime]
        (h : 𝔭 = 𝔮.comap (algebraMap R S)),
        Function.Surjective (Ideal.ResidueField.map 𝔭 𝔮 (algebraMap R S) h) ∨
          ringChar 𝔮.ResidueField = p ∧
            (Ideal.ResidueField.map 𝔭 𝔮 (algebraMap R S) h).IsPurelyInseparable) ∧
      ∀ (R' : Type u') (S' : Type v') [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S']
        [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
        [Algebra.IsPushout R S R' S'],
        RingHom.ker (algebraMap R' S') ≤ nilradical R' ∧
          Algebra.adjoin R' {x : S' | ∃ n > 0, x ^ p ^ n ∈ (algebraMap R' S').range ∧
            p ^ n • x ∈ (algebraMap R' S').range} = ⊤
Tag 0BRB, a lemma

Tag 0BRB in the Stacks Project.

Algebra.IsPushout.injective_comap_and_residueFieldMap_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversalHomeomorphism/Examples/BaseChange.lean, line 333.

Let R → S be a ring map which induces an injective map of spectra and purely inseparable residue field extensions, and let S' be the base change of S along an arbitrary ring map R → R', i.e. R', S' complete R, S to a pushout square of R-algebras. Then R' → S' also induces an injective map of spectra and purely inseparable residue field extensions.

public theorem Algebra.IsPushout.injective_comap_and_residueFieldMap_isPurelyInseparable
    {R S R' S' : Type*} [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R S]
    [Algebra R R'] [Algebra R S'] [Algebra S S'] [Algebra R' S'] [IsScalarTower R S S']
    [IsScalarTower R R' S'] [IsPushout R S R' S']
    (hinj : Function.Injective (PrimeSpectrum.comap (algebraMap R S)))
    (hins : ∀ (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime]
      (hpq : p = q.comap (algebraMap R S)),
      (Ideal.ResidueField.map p q (algebraMap R S) hpq).IsPurelyInseparable) :
    Function.Injective (PrimeSpectrum.comap (algebraMap R' S')) ∧
      ∀ (p' : Ideal R') [p'.IsPrime] (q' : Ideal S') [q'.IsPrime]
        (hpq : p' = q'.comap (algebraMap R' S')),
        (Ideal.ResidueField.map p' q' (algebraMap R' S') hpq).IsPurelyInseparable
Tag 0BRC, a lemma

Tag 0BRC in the Stacks Project.

PrimeSpectrum.isClosedEmbedding_comap_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversalHomeomorphism/Examples/BaseChange.lean, line 358.

An integral ring map f : R → S whose induced map of spectra is injective induces a homeomorphism from Spec(S) onto a closed subset of Spec(R).

public theorem isClosedEmbedding_comap_of_isIntegral {R : Type u} {S : Type v} [CommRing R]
    [CommRing S] (f : R →+* S) (hf : f.IsIntegral) (hinj : Function.Injective (comap f)) :
    Topology.IsClosedEmbedding (comap f)

PrimeSpectrum.isClosedEmbedding_comap_and_baseChange_of_injective_comap_of_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversalHomeomorphism/Examples/BaseChange.lean, line 371.

Let R → S be an integral ring map which induces an injective map of spectra and purely inseparable residue field extensions. Then Spec(S) → Spec(R) is a homeomorphism onto a closed subset of Spec(R), and for every base change R' → S' of R → S along an arbitrary ring map R → R', i.e. for every pushout square of R-algebras completing R, S by R', S', the map R' → S' is again integral and again induces an injective map of spectra and purely inseparable residue field extensions.

public theorem isClosedEmbedding_comap_and_baseChange_of_injective_comap_of_isPurelyInseparable
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S]
    (hinj : Function.Injective (comap (algebraMap R S)))
    (hins : ∀ (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime]
      (hpq : p = q.comap (algebraMap R S)),
      (Ideal.ResidueField.map p q (algebraMap R S) hpq).IsPurelyInseparable) :
    Topology.IsClosedEmbedding (comap (algebraMap R S)) ∧
      ∀ (R' : Type u') (S' : Type v') [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S']
        [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
        [Algebra.IsPushout R S R' S'],
        Algebra.IsIntegral R' S' ∧ Function.Injective (comap (algebraMap R' S')) ∧
          ∀ (p' : Ideal R') [p'.IsPrime] (q' : Ideal S') [q'.IsPrime]
            (hpq : p' = q'.comap (algebraMap R' S')),
            (Ideal.ResidueField.map p' q' (algebraMap R' S') hpq).IsPurelyInseparable
Tag 0BRD, a lemma

Tag 0BRD in the Stacks Project.

PrimeSpectrum.isHomeomorph_comap_and_baseChange_of_bijective_comap_of_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversalHomeomorphism/Examples/BaseChange.lean, line 450. References: EGA IV (2.4.5), “(i), affine case”; EGA 0 (23.2.2), “more general”.

Let R → S be an integral ring map which induces a bijective map of spectra and purely inseparable residue field extensions. Then Spec(S) → Spec(R) is a homeomorphism, and for every base change R' → S' of R → S along an arbitrary ring map R → R', i.e. for every pushout square of R-algebras completing R, S by R', S', the map R' → S' is again integral and again induces a bijective map of spectra and purely inseparable residue field extensions.

public theorem isHomeomorph_comap_and_baseChange_of_bijective_comap_of_isPurelyInseparable
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S]
    (hbij : Function.Bijective (comap (algebraMap R S)))
    (hins : ∀ (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime]
      (hpq : p = q.comap (algebraMap R S)),
      (Ideal.ResidueField.map p q (algebraMap R S) hpq).IsPurelyInseparable) :
    IsHomeomorph (comap (algebraMap R S)) ∧
      ∀ (R' : Type u') (S' : Type v') [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S']
        [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
        [Algebra.IsPushout R S R' S'],
        Algebra.IsIntegral R' S' ∧ Function.Bijective (comap (algebraMap R' S')) ∧
          ∀ (p' : Ideal R') [p'.IsPrime] (q' : Ideal S') [q'.IsPrime]
            (hpq : p' = q'.comap (algebraMap R' S')),
            (Ideal.ResidueField.map p' q' (algebraMap R' S') hpq).IsPurelyInseparable
Tag 09EF, a lemma

Tag 09EF in the Stacks Project.

PrimeSpectrum.isHomeomorph_comap_and_isPurelyInseparable_and_baseChange_of_adjoin_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversalHomeomorphism/Examples/GenerationCriteria.lean, line 272.

Let φ : R → S be a ring map whose kernel is locally nilpotent and such that S is generated as an R-algebra by elements x for which there are an n > 0 and a polynomial P(T) ∈ R[T] whose image in S[T] is (T - x) ^ n. Then Spec(S) → Spec(R) is a homeomorphism, the induced residue field extensions κ(p) → κ(q) are purely inseparable, and both hypotheses hold again for every base change R' → S' of R → S along an arbitrary ring map R → R', i.e. for every pushout square of R-algebras completing R, S by R', S'.

public theorem isHomeomorph_comap_and_isPurelyInseparable_and_baseChange_of_adjoin_eq_top
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    (hker : RingHom.ker (algebraMap R S) ≤ nilradical R)
    (hgen : Algebra.adjoin R
      {x : S | ∃ n > 0, ((X : S[X]) - C x) ^ n ∈ lifts (algebraMap R S)} = ⊤) :
    IsHomeomorph (comap (algebraMap R S)) ∧
      (∀ (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime]
        (hpq : p = q.comap (algebraMap R S)),
        (Ideal.ResidueField.map p q (algebraMap R S) hpq).IsPurelyInseparable) ∧
      ∀ (R' : Type u') (S' : Type v') [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S']
        [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
        [Algebra.IsPushout R S R' S'],
        RingHom.ker (algebraMap R' S') ≤ nilradical R' ∧
          Algebra.adjoin R'
            {x : S' | ∃ n > 0, ((X : S'[X]) - C x) ^ n ∈ lifts (algebraMap R' S')} = ⊤
Sources
LeanAlgebra.IsPushout.surjective_and_ker_eq_map_of_surjective · forall_exists_pow_mem_iff_isPurelyInseparable_or_isAlgebraic_bot · Ideal.ResidueField.exists_pow_mem_range_map · PrimeSpectrum.isHomeomorph_comap_and_residueFieldMap_bijective_of_adjoin_sq_cube_eq_top · Stacks.UniversalHomeomorphism.FrobeniusPowerSubring.exists_pow_mem · satisfiesGeneratingCondition_iff_structuralCondition · PrimeSpectrum.isHomeomorph_comap_and_isPurelyInseparable_and_baseChange_of_adjoin_pow_eq_top · Algebra.IsPushout.injective_comap_and_residueFieldMap_isPurelyInseparable

Section10.47 Geometrically irreducible algebras#

Section 10.47 of the Stacks Project, Tag 00I2. 14 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00I6, a lemma

Tag 00I6 in the Stacks Project.

irreducibleSpace_primeSpectrum_of_isOpenMap_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/IrreducibleFibres.lean, line 122. The attribute's comment: “general form”. References: EGA IV (2.3.5), “(iii), special case”; EGA IV (4.4.2), “special case”.

Stacks 00I6 (algebraic form, more general statement). Let R → S be a ring map. Assume: * Spec R is irreducible; * the induced map Spec S → Spec R is open; * the topological fibres of Spec S → Spec R are irreducible for p in a dense subset of Spec R.

Then Spec S is irreducible.

theorem irreducibleSpace_primeSpectrum_of_isOpenMap_comap
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    [IrreducibleSpace (PrimeSpectrum R)]
    (hopen : IsOpenMap (PrimeSpectrum.comap (algebraMap R S)))
    (D : Set (PrimeSpectrum R)) (hD : Dense D)
    (hfib : ∀ p ∈ D,
      IrreducibleSpace
        {q : PrimeSpectrum S // PrimeSpectrum.comap (algebraMap R S) q = p}) :
    IrreducibleSpace (PrimeSpectrum S)

irreducibleSpace_primeSpectrum_of_flat_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/IrreducibleFibres.lean, line 140.

Stacks 00I6 (flat + finite-presentation form). Let R → S be a flat ring map of finite presentation. If Spec R is irreducible and the topological fibres of Spec S → Spec R are irreducible for p in a dense subset of Spec R, then Spec S is irreducible.

theorem irreducibleSpace_primeSpectrum_of_flat_finitePresentation
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    [IrreducibleSpace (PrimeSpectrum R)]
    [Module.Flat R S] [Algebra.FinitePresentation R S]
    (D : Set (PrimeSpectrum R)) (hD : Dense D)
    (hfib : ∀ p ∈ D,
      IrreducibleSpace
        {q : PrimeSpectrum S // PrimeSpectrum.comap (algebraMap R S) q = p}) :
    IrreducibleSpace (PrimeSpectrum S)
Tag 00I7, a lemma

Tag 00I7 in the Stacks Project.

tensorProduct_unique_minimalPrime_of_isSepClosed_right_base, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/IrreducibleFibres.lean, line 227. The attribute's comment: “Only the degenerate S = k case; the general R ⊗_k S statement is not formalized.”.

Stacks Tag 00I7 (right-factor-is-the-base-field special case). Let k be a field and let R be a k-algebra with a unique minimal prime. Then R ⊗_k k has a unique minimal prime.

The full Stacks lemma asserts the same conclusion for R ⊗_k S for any pair of k-algebras R, S each with a unique minimal prime; that proof requires the algebraic closure of k, generic-fibre irreducibility for the flat finite-type map R → R ⊗_k S (Hilbert Nullstellensatz, Jacobson), and a limit argument over finitely generated subalgebras.

Only the degenerate S = k case is formalized here, and it does not use separable closedness of k: it is Algebra.TensorProduct.rid transported along unique_minimalPrime_of_ringEquiv. Accordingly no [IsSepClosed k] hypothesis is assumed, and the @[stacks 00I7] attribute is qualified -- tag 00I7 is still open in the generality Stacks states.

alias tensorProduct_unique_minimalPrime_of_isSepClosed_right_base
Tag 037K, a lemma

Tag 037K in the Stacks Project.

AlgebraicGeometry.geometricallyIrreducible_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/Criteria.lean, line 403.

Stacks 037K. Let k be a field, R a commutative k-algebra, k^{sep} a separable closure of k and k̄ an algebraic closure of k. The following are equivalent: 1. the spectrum of R ⊗[k] k' is irreducible for every field extension k'/k; 2. the spectrum of R ⊗[k] k' is irreducible for every finite separable field extension k'/k; 3. the spectrum of R ⊗[k] k^{sep} is irreducible; 4. the spectrum of R ⊗[k] k̄ is irreducible; 5. Spec R ⟶ Spec k is geometrically irreducible.

public theorem AlgebraicGeometry.geometricallyIrreducible_tfae (k R : Type u) [Field k]
    [CommRing R] [Algebra k R] (ksep kbar : Type u) [Field ksep] [Algebra k ksep]
    [IsSepClosure k ksep] [Field kbar] [Algebra k kbar] [IsAlgClosure k kbar] :
    List.TFAE
      [∀ (k' : Type u) [Field k'] [Algebra k k'], IrreducibleSpace (PrimeSpectrum (R ⊗[k] k')),
        ∀ (k' : Type u) [Field k'] [Algebra k k'] [FiniteDimensional k k']
          [Algebra.IsSeparable k k'], IrreducibleSpace (PrimeSpectrum (R ⊗[k] k')),
        IrreducibleSpace (PrimeSpectrum (R ⊗[k] ksep)),
        IrreducibleSpace (PrimeSpectrum (R ⊗[k] kbar)),
        GeometricallyIrreducible (Spec.map (ofHom (algebraMap k R)))]
Tag 037L, a definition

Tag 037L in the Stacks Project.

Algebra.IsGeometricallyIrreducible, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/Defs.lean, line 133. References: EGA IV (4.5.2), “special case”; EGA IV (4.5.9).

A k-algebra S is geometrically irreducible over k if every base change of Spec S ⟶ Spec k along a field-valued point of Spec k is an irreducible space, equivalently if for every field extension k'/k the spectrum of S ⊗[k] k' is irreducible (Algebra.isGeometricallyIrreducible_iff_irreducibleSpace_primeSpectrum_tensorProduct). An irreducible space is nonempty, so this forces every such S ⊗[k] k' to be nonzero.

public abbrev Algebra.IsGeometricallyIrreducible (k S : Type u) [Field k] [CommRing S]
    [Algebra k S] : Prop
Tag 037M, a lemma

Tag 037M in the Stacks Project.

Algebra.isGeometricallyIrreducible_iff_irreducibleSpace_primeSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/Criteria.lean, line 528.

Stacks 037M. Let k be a separably algebraically closed field and let R be a k-algebra. Then R is geometrically irreducible over k if and only if the spectrum of R is irreducible.

public theorem Algebra.isGeometricallyIrreducible_iff_irreducibleSpace_primeSpectrum
    (k R : Type u) [Field k] [IsSepClosed k] [CommRing R] [Algebra k R] :
    Algebra.IsGeometricallyIrreducible k R ↔ IrreducibleSpace (PrimeSpectrum R)
Tag 037N, a lemma

Tag 037N in the Stacks Project.

isGeometricallyIrreducible_of_subalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/Subalgebra.lean, line 189. The attribute's comment: “(1)”.

Statement 1 (Subalgebras). If S is geometrically irreducible over k, then every k-subalgebra S' ⊆ S is geometrically irreducible over k.

theorem isGeometricallyIrreducible_of_subalgebra
    (k : Type u) [Field k] (S : Type u) [CommRing S] [Algebra k S]
    (hS : Algebra.IsGeometricallyIrreducible k S)
    (S' : Subalgebra k S) :
    Algebra.IsGeometricallyIrreducible k S'

isGeometricallyIrreducible_of_forall_fg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/Subalgebra.lean, line 278. The attribute's comment: “(2)”.

Statement 2 (Detection by finitely generated subalgebras). If every finitely generated k-subalgebra of S is geometrically irreducible over k, then S is geometrically irreducible over k.

Proof outline: for each field extension k'/k, reduce IrreducibleSpace (PrimeSpectrum (S ⊗[k] k')) to (nilradical (S ⊗[k] k')).IsPrime via irreducibleSpace_primeSpectrum_iff_nilradical_isPrime, then build IsPrime from its two pieces: ne_top (from nontrivial_tensorProduct_of_forall_fg) and mem_or_mem (from nilradical_tensorProduct_mem_or_mem_of_forall_fg).

theorem isGeometricallyIrreducible_of_forall_fg
    (k : Type u) [Field k] (S : Type u) [CommRing S] [Algebra k S]
    (hS : ∀ (S' : Subalgebra k S), S'.FG →
      Algebra.IsGeometricallyIrreducible k S') :
    Algebra.IsGeometricallyIrreducible k S

isGeometricallyIrreducible_directLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/Subalgebra.lean, line 708. The attribute's comment: “(3)”.

Statement 3 (Directed colimits). A directed colimit of geometrically irreducible k-algebras is geometrically irreducible over k.

The directed system is given by a directed preorder ι, k-algebras G i, and transition ring homomorphisms f i j : G i →+* G j (for i ≤ j) that commute with the structure maps from k (hf) and form a DirectedSystem. The colimit is Ring.DirectLimit G f, equipped with the k-algebra structure dlAlg k G f.

Proof outline: for each field extension k'/k, reduce to (nilradical (DirectLimit ⊗ k')).IsPrime via irreducibleSpace_primeSpectrum_iff_nilradical_isPrime, then assemble IsPrime from nontrivial_directLimit_tensorProduct (nontriviality ⇒ ne_top) and nilradical_directLimit_tensorProduct_mem_or_mem (the prime implication).

theorem isGeometricallyIrreducible_directLimit
    (k : Type u) [Field k]
    {ι : Type u} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (G : ι → Type u) [∀ i, CommRing (G i)] [∀ i, Algebra k (G i)]
    (f : (i j : ι) → i ≤ j → G i →+* G j)
    (hf : ∀ (i j : ι) (h : i ≤ j) (x : k),
      f i j h (algebraMap k (G i) x) = algebraMap k (G j) x)
    [DirectedSystem G (fun i j h => (f i j h : G i → G j))]
    (hG : ∀ i, Algebra.IsGeometricallyIrreducible k (G i)) :
    letI := dlAlg k G (fun i j h => (f i j h : G i → G j))
    Algebra.IsGeometricallyIrreducible k
      (Ring.DirectLimit G (fun i j h => (f i j h : G i → G j)))
Tag 037O, a lemma

Tag 037O in the Stacks Project.

Algebra.IsGeometricallyIrreducible.bijOn_irreducibleComponents_primeSpectrum_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/IrreducibleComponents.lean, line 190.

Stacks 037O. Let k be a field, let S be a geometrically irreducible k-algebra and let R be any k-algebra. Then the map Spec (R ⊗[k] S) → Spec R induced by r ↦ r ⊗ₜ 1 induces a bijection on irreducible components: taking images along it is a bijection from the irreducible components of Spec (R ⊗[k] S) onto the irreducible components of Spec R.

public theorem
    Algebra.IsGeometricallyIrreducible.bijOn_irreducibleComponents_primeSpectrum_tensorProduct
    (k R S : Type u) [Field k] [CommRing R] [Algebra k R] [CommRing S] [Algebra k S]
    [Algebra.IsGeometricallyIrreducible k S] :
    Set.BijOn (fun Z ↦ PrimeSpectrum.comap (algebraMap R (R ⊗[k] S)) '' Z)
      (irreducibleComponents (PrimeSpectrum (R ⊗[k] S)))
      (irreducibleComponents (PrimeSpectrum R))
Tag 037P, a lemma

Tag 037P in the Stacks Project.

Algebra.IsGeometricallyIrreducible.of_algebraicClosure_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/Tower.lean, line 190.

Let K/k be a field extension. If k is algebraically closed in K, that is, if the relative algebraic closure algebraicClosure k K is trivial, then K is geometrically irreducible over k.

public theorem Algebra.IsGeometricallyIrreducible.of_algebraicClosure_eq_bot (k K : Type u)
    [Field k] [Field K] [Algebra k K] (h : algebraicClosure k K = ⊥) :
    Algebra.IsGeometricallyIrreducible k K
Tag 0G30, a lemma

Tag 0G30 in the Stacks Project.

Algebra.IsGeometricallyIrreducible.trans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/Tower.lean, line 96.

Let K/k be a geometrically irreducible field extension and let S be a geometrically irreducible K-algebra. Then S is geometrically irreducible over k.

public theorem Algebra.IsGeometricallyIrreducible.trans (k K S : Type u) [Field k] [Field K]
    [CommRing S] [Algebra k K] [Algebra K S] [Algebra k S] [IsScalarTower k K S]
    [Algebra.IsGeometricallyIrreducible k K] [Algebra.IsGeometricallyIrreducible K S] :
    Algebra.IsGeometricallyIrreducible k S
Tag 0G31, a lemma

Tag 0G31 in the Stacks Project.

AlgebraicGeometry.GeometricallyIrreducible.iff_ratFunc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/AdjoinTranscendental.lean, line 179.

An extension of fields K/k is geometrically irreducible if and only if the induced extension K(X)/k(X) of purely transcendental extensions in one variable is geometrically irreducible.

public theorem AlgebraicGeometry.GeometricallyIrreducible.iff_ratFunc (k K : Type u) [Field k]
    [Field K] [Algebra k K] :
    GeometricallyIrreducible (Spec.map (ofHom (algebraMap k K))) ↔
      GeometricallyIrreducible (Spec.map (ofHom (algebraMap k⟮X⟯ K⟮X⟯)))
Tag 0G32, a lemma

Tag 0G32 in the Stacks Project.

AlgebraicGeometry.geometricallyIrreducible_specMap_adjoin_of_transcendental, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/AdjoinTranscendental.lean, line 370.

Let K/L/M be a tower of fields with L geometrically irreducible over M, and let x : K be transcendental over L. Then L(x) is geometrically irreducible over M(x), where M(x) = M⟮x⟯ and L(x) is the M⟮x⟯-subfield of K generated by the image of L.

public theorem AlgebraicGeometry.geometricallyIrreducible_specMap_adjoin_of_transcendental
    {M L K : Type u} [Field M] [Field L] [Field K] [Algebra M L] [Algebra M K] [Algebra L K]
    [IsScalarTower M L K]
    [GeometricallyIrreducible (Spec.map (CommRingCat.ofHom (algebraMap M L)))]
    {x : K} (hx : Transcendental L x) :
    GeometricallyIrreducible (Spec.map (CommRingCat.ofHom
      (algebraMap ↥M⟮x⟯ ↥(adjoin ↥M⟮x⟯ (Set.range (algebraMap L K))))))
Tag 0G33, a lemma

Tag 0G33 in the Stacks Project.

separableClosure.eq_bot_iff_geometricallyIrreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/Tower.lean, line 328.

Let K/k be an extension of fields. The separable closure of k in K is trivial — every element of K separably algebraic over k lies in k — if and only if K is geometrically irreducible over k.

public theorem separableClosure.eq_bot_iff_geometricallyIrreducible (k K : Type u) [Field k]
    [Field K] [Algebra k K] :
    separableClosure k K = ⊥ ↔ GeometricallyIrreducible (Spec.map (ofHom (algebraMap k K)))
Tag 037Q, a lemma

Tag 037Q in the Stacks Project.

part2, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/SeparableClosure/SeparableTensor.lean, line 287. The attribute's comment: “(2)”.

Statement 2 (Finiteness of [k' : k]). If K/k is a finitely generated field extension (Definition 4 — finite generation as a field, encoded by (⊤ : IntermediateField k K).FG), then k' is finite over k, i.e. Module.Finite k k' (equivalently [k' : k] < ∞).

theorem part2 (k K : Type*) [Field k] [Field K] [Algebra k K]
    (hfg : (⊤ : IntermediateField k K).FG) :
    Module.Finite k (separableClosure k K)

part1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/SeparableClosure/SeparablyClosedBase.lean, line 806. The attribute's comment: “(1)”. References: EGA IV (4.3.2), “special case”; EGA IV (4.3.3), “special case”; EGA IV (4.4.4), “special case”; EGA IV (4.5.21), “special case”.

Statement 1 (Geometric irreducibility over k'). K is geometrically irreducible over k' = separableClosure k K: for every field extension L/k' the spectrum Spec(K ⊗\_\{k'} L) is irreducible.

theorem part1 (k K : Type*) [Field k] [Field K] [Algebra k K] :
    ∀ (L : Type) [Field L] [Algebra (separableClosure k K) L],
      IrreducibleSpace (PrimeSpectrum (K ⊗[separableClosure k K] L))
Tag 04KP, a lemma

Tag 04KP in the Stacks Project.

gal_acts_transitively_on_primes_of_isGalois, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIrreducible/GaloisAction.lean, line 317. References: SGA 1 V (1.1), “(ii), special case”.

Statement 1 (Stacks Tag 04KP). The Galois group Gal(kbar/k) of a Galois extension kbar/k acts transitively on the primes of kbar ⊗[k] K: for every pair of prime ideals P, Q there exists σ ∈ Gal(kbar/k) whose induced map on the prime spectrum (via comap of σ ⊗ id_K) carries Q to P. A separable algebraic closure of k, the case the source states, is Galois over k.

theorem gal_acts_transitively_on_primes_of_isGalois
    {k K kbar : Type*}
    [Field k] [Field K] [Field kbar]
    [Algebra k K] [Algebra k kbar] [IsGalois k kbar] :
    ∀ (P Q : PrimeSpectrum (kbar ⊗[k] K)),
      ∃ σ : kbar ≃ₐ[k] kbar,
        PrimeSpectrum.comap
          (Algebra.TensorProduct.congr σ (AlgEquiv.refl (R := k) (A₁ :=
              K))).toAlgHom.toRingHom Q = P
Sources
LeanirreducibleSpace_primeSpectrum_of_isOpenMap_comap · irreducibleSpace_primeSpectrum_of_flat_finitePresentation · tensorProduct_unique_minimalPrime_of_isSepClosed_right_base · AlgebraicGeometry.geometricallyIrreducible_tfae · Algebra.IsGeometricallyIrreducible · Algebra.isGeometricallyIrreducible_iff_irreducibleSpace_primeSpectrum · isGeometricallyIrreducible_of_subalgebra · isGeometricallyIrreducible_of_forall_fg

Section10.48 Geometrically connected algebras#

Section 10.48 of the Stacks Project, Tag 05DV. 6 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 037R, a lemma

Tag 037R in the Stacks Project.

Algebra.TensorProduct.connectedSpace_primeSpectrum, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorProduct/Connected.lean, line 332. The attribute's comment: “Connectedness of the spectra of two k-algebras over a separably closed field k is inherited by the spectrum of their tensor product over k. Stated as an instance, with Spec read as PrimeSpectrum and connected as ConnectedSpace, which includes nonemptiness as the source's notion of a connected space does.”. References: SGA 3 X (9.7.2), “affine case”; SGA 3 X (9.7.1), “affine case, i = 1”.

Connectedness of the spectrum of a tensor product over a separably closed field. Let k be a separably algebraically closed field and let R and S be k-algebras. If Spec R and Spec S are connected, then so is Spec (R ⊗[k] S).

public instance connectedSpace_primeSpectrum (k : Type u) (R : Type v) (S : Type w) [Field k]
    [IsSepClosed k] [CommRing R] [Algebra k R] [CommRing S] [Algebra k S]
    [ConnectedSpace (PrimeSpectrum R)] [ConnectedSpace (PrimeSpectrum S)] :
    ConnectedSpace (PrimeSpectrum (R ⊗[k] S))
Tag 037S, a lemma

Tag 037S in the Stacks Project.

Algebra.isGeometricallyConnected_iff_forall_finite_separable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyConnected/Criteria.lean, line 136. The attribute's comment: “Geometric connectedness of a k-algebra need only be tested on the finite separable extensions of k. Condition (1) of the lemma is Algebra.IsGeometricallyConnected (Stacks 037T), which is that condition verbatim; Spec is PrimeSpectrum and connected is ConnectedSpace, which includes nonemptiness as the source's notion does.”. References: EGA IV (8.4.5), “affine case”; EGA IV (8.4.5), “affine case”.

Geometric connectedness is detected by the finite separable extensions. Let k be a field and let R be a k-algebra. Then R is geometrically connected over k, that is, Spec (K ⊗[k] R) is connected for every field extension K/k, if and only if Spec (K ⊗[k] R) is connected for every finite separable field extension K/k.

public theorem isGeometricallyConnected_iff_forall_finite_separable (k : Type u) (R : Type v)
    [Field k] [CommRing R] [Algebra k R] :
    IsGeometricallyConnected k R ↔
      ∀ (K : Type u) [Field K] [Algebra k K] [FiniteDimensional k K] [Algebra.IsSeparable k K],
        ConnectedSpace (PrimeSpectrum (K ⊗[k] R))
Tag 037T, a definition

Tag 037T in the Stacks Project.

Algebra.IsGeometricallyConnected, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyConnected/Defs.lean, line 68.

A k-algebra S over a field k is geometrically connected over k if for every field extension K/k the spectrum of K ⊗[k] S is connected.

public class IsGeometricallyConnected (k : Type u) (S : Type v) [Field k] [CommRing S]
    [Algebra k S] : Prop
Tag 037U, a lemma

Tag 037U in the Stacks Project.

Algebra.isGeometricallyConnected_iff_connectedSpace_primeSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyConnected.lean, line 335.

Geometric connectedness over a separably closed field. Let k be a separably algebraically closed field and let R be a k-algebra. Then R is geometrically connected over k if and only if Spec R is connected.

public theorem Algebra.isGeometricallyConnected_iff_connectedSpace_primeSpectrum
    (k : Type u) (R : Type v) [Field k] [IsSepClosed k] [CommRing R] [Algebra k R] :
    Algebra.IsGeometricallyConnected k R ↔ ConnectedSpace (PrimeSpectrum R)
Tag 037V, a lemma

Tag 037V in the Stacks Project.

geometricallyConnected_of_subalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyConnected.lean, line 117. The attribute's comment: “(1)”.

If S is geometrically connected over k, then every k-subalgebra R ⊆ S is geometrically connected over k.

theorem geometricallyConnected_of_subalgebra
    (k : Type u) (S : Type v) [Field k] [CommRing S] [Algebra k S]
    (hS : Algebra.IsGeometricallyConnected k S) (R : Subalgebra k S) :
    Algebra.IsGeometricallyConnected k R

geometricallyConnected_of_forall_fg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyConnected.lean, line 131. The attribute's comment: “(2)”.

If every finitely generated k-subalgebra of S is geometrically connected over k, then S is geometrically connected over k.

theorem geometricallyConnected_of_forall_fg
    (k : Type u) (S : Type v) [Field k] [CommRing S] [Algebra k S]
    (h : ∀ R : Subalgebra k S, R.FG → Algebra.IsGeometricallyConnected k R) :
    Algebra.IsGeometricallyConnected k S

geometricallyConnected_of_directedColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyConnected.lean, line 192. The attribute's comment: “(3)”.

A directed colimit of geometrically connected k-algebras is geometrically connected over k. The colimit S of the directed system (S_i, φ_{ij}) with cocone maps ψ_i : S_i →ₐ[k] S is presented by its elementary universal property: the ψ_i are jointly surjective, and ψ_i y = ψ_i z holds only if y and z become equal after some transition map φ_{ij}.

theorem geometricallyConnected_of_directedColimit
    (k : Type u) [Field k]
    (ι : Type w) [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
    (Sfun : ι → Type v) [(i : ι) → CommRing (Sfun i)] [(i : ι) → Algebra k (Sfun i)]
    (φ : (i j : ι) → i ≤ j → (Sfun i →ₐ[k] Sfun j))
    (hφcomp : ∀ (i j l : ι) (hij : i ≤ j) (hjl : j ≤ l),
      (φ j l hjl).comp (φ i j hij) = φ i l (le_trans hij hjl))
    (S : Type v) [CommRing S] [Algebra k S]
    (ψ : (i : ι) → (Sfun i →ₐ[k] S))
    (hψ : ∀ (i j : ι) (hij : i ≤ j), (ψ j).comp (φ i j hij) = ψ i)
    (hsurj : ∀ x : S, ∃ (i : ι) (y : Sfun i), ψ i y = x)
    (hsep : ∀ (i : ι) (y z : Sfun i), ψ i y = ψ i z →
      ∃ (j : ι) (hij : i ≤ j), φ i j hij y = φ i j hij z)
    (hgc : ∀ i, Algebra.IsGeometricallyConnected k (Sfun i)) :
    Algebra.IsGeometricallyConnected k S
Tag 037W, a lemma

Tag 037W in the Stacks Project.

Algebra.TensorProduct.bijOn_isIdempotentElem_and_bijective_connectedComponentsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorProduct/Connected.lean, line 479. The attribute's comment: “Base change of an arbitrary k-algebra R along a geometrically connected k-algebra S induces a bijection on idempotents and a bijection on connected components of the spectra. Both assertions of the lemma; the second is stated as a bijection, as in the source, rather than as the homeomorphism of Varieties, Lemma 0385.”.

Base change along a geometrically connected algebra. Let k be a field, let S be a geometrically connected k-algebra and let R be any k-algebra. Then R → R ⊗[k] S, r ↦ r ⊗ 1, restricts to a bijection from the idempotents of R onto the idempotents of R ⊗[k] S, and the induced map Spec (R ⊗[k] S) → Spec R is a bijection on connected components.

public theorem bijOn_isIdempotentElem_and_bijective_connectedComponentsMap
    (k : Type u) [Field k] (S : Type v) [CommRing S] [Algebra k S]
    [IsGeometricallyConnected k S] (R : Type w) [CommRing R] [Algebra k R] :
    Set.BijOn (algebraMap R (R ⊗[k] S)) {e | IsIdempotentElem e} {e | IsIdempotentElem e} ∧
      Function.Bijective (PrimeSpectrum.continuous_comap
        (algebraMap R (R ⊗[k] S))).connectedComponentsMap
Sources
LeanAlgebra.TensorProduct.connectedSpace_primeSpectrum · Algebra.isGeometricallyConnected_iff_forall_finite_separable · Algebra.IsGeometricallyConnected · Algebra.isGeometricallyConnected_iff_connectedSpace_primeSpectrum · geometricallyConnected_of_subalgebra · geometricallyConnected_of_forall_fg · geometricallyConnected_of_directedColimit · Algebra.TensorProduct.bijOn_isIdempotentElem_and_bijective_connectedComponentsMap

Section10.49 Geometrically integral algebras#

Section 10.49 of the Stacks Project, Tag 05DW. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05DX, a definition

Tag 05DX in the Stacks Project.

Algebra.IsGeometricallyIntegral, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIntegral/Defs.lean, line 120. References: EGA IV (4.6.2), “affine, special case”; SGA 6 XII (1.2), “special case”.

A k-algebra S is geometrically integral over k if every base change of Spec S ⟶ Spec k along a field-valued point of Spec k is an integral scheme, equivalently if for every field extension k'/k the ring S ⊗[k] k' is a domain (Algebra.isGeometricallyIntegral_iff_isDomain_tensorProduct).

public abbrev Algebra.IsGeometricallyIntegral (k S : Type u) [Field k] [CommRing S]
    [Algebra k S] : Prop
Tag 05DY, a lemma

Tag 05DY in the Stacks Project.

geometricallyIntegral_iff_irreducible_and_reduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIntegral/Defs.lean, line 238. References: EGA IV (4.6.14), “special case”; EGA IV (4.6.2), “affine, special case”; SGA 3 XIX (2.1), “partial”.

A k-algebra S is geometrically integral over k if and only if it is both geometrically irreducible and geometrically reduced over k. This is Stacks tag 05DY.

GeometricallyReduced uses the convention IsReduced (k' ⊗[k] S) (extension on the left). The local statements about S ⊗[k] k' (algebra on the left) are interchanged with these via the canonical ring isomorphism Algebra.TensorProduct.comm.

theorem geometricallyIntegral_iff_irreducible_and_reduced
    (k : Type u) [Field k] (S : Type v) [CommRing S] [Algebra k S] :
    GeometricallyIntegral.{u, v, w} k S ↔
      GeometricallyIrreducible.{u, v, w} k S ∧ GeometricallyReduced.{u, v, w} k S
Tag 0FWF, a lemma

Tag 0FWF in the Stacks Project.

Algebra.isGeometricallyIntegral_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIntegral/TFAE.lean, line 124.

Stacks 0FWF. Let k be a field and let S be a k-algebra. The following are equivalent: (1) S is geometrically integral over k; (2) S ⊗[k] k' is a domain for every field extension k'/k; (3) S ⊗[k] k' is a domain for every finite extension k'/k; (4) S ⊗[k] AlgebraicClosure k is a domain.

public theorem Algebra.isGeometricallyIntegral_tfae (k S : Type u) [Field k] [CommRing S]
    [Algebra k S] :
    List.TFAE
      [ Algebra.IsGeometricallyIntegral k S,
        ∀ (k' : Type u) [Field k'] [Algebra k k'], IsDomain (S ⊗[k] k'),
        ∀ (k' : Type u) [Field k'] [Algebra k k'] [Module.Finite k k'], IsDomain (S ⊗[k] k'),
        IsDomain (S ⊗[k] AlgebraicClosure k) ]
Tag 09P9, a lemma

Tag 09P9 in the Stacks Project.

Algebra.IsGeometricallyIntegral.isDomain_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIntegral/TensorProduct.lean, line 100.

Let k be a field, let S be a geometrically integral k-algebra and let R be a k-algebra which is an integral domain. Then R ⊗[k] S is an integral domain.

public theorem Algebra.IsGeometricallyIntegral.isDomain_tensorProduct (k R S : Type u) [Field k]
    [CommRing R] [IsDomain R] [Algebra k R] [CommRing S] [Algebra k S]
    [Algebra.IsGeometricallyIntegral k S] : IsDomain (R ⊗[k] S)
Sources
LeanAlgebra.IsGeometricallyIntegral · geometricallyIntegral_iff_irreducible_and_reduced · Algebra.isGeometricallyIntegral_tfae · Algebra.IsGeometricallyIntegral.isDomain_tensorProduct

Section10.50 Valuation rings#

Section 10.50 of the Stacks Project, Tag 00I8. 15 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 28 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00I9, a definition

Tag 00I9 in the Stacks Project.

dominates_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Domination.lean, line 74. The attribute's comment: “(1)”. References: EGA I (8.1.1), “(i) ⇔ (ii)”.

Part (1). For local subrings A, B of a field K, the domination order A ≤ B of LocalSubring K holds iff A ⊆ B (as subrings) and, for every a ∈ A, the element a lies in the maximal ideal of A exactly when its image in B lies in the maximal ideal of B. The latter is the literal Stacks condition 𝔪_A = A ∩ 𝔪_B.

theorem dominates_iff {A B : LocalSubring K} :
    A ≤ B ↔ ∃ h : A.toSubring ≤ B.toSubring,
      ∀ a : A.toSubring,
        a ∈ maximalIdeal A.toSubring ↔
          Subring.inclusion h a ∈ maximalIdeal B.toSubring

IsValuationRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Domination.lean, line 90. The attribute's comment: “(2)”. References: EGA II (7.1.1), “definition”.

Part (2). A local domain A is a valuation ring when, viewed inside its fraction field, it is maximal for the domination order among the local subrings of FractionRing A.

def IsValuationRing (A : Type*) [CommRing A] [IsDomain A] [IsLocalRing A] : Prop

IsCenteredOn, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Domination.lean, line 110. The attribute's comment: “(3)”.

Part (3). A valuation ring A with fraction field K, represented as a ValuationSubring K, is centered on a subring R ⊆ K when R ⊆ A.

def IsCenteredOn (A : ValuationSubring K) (R : Subring K) : Prop
Tag 00IB, a lemma

Tag 00IB in the Stacks Project.

Declarations registered for the tag:

Tag 052K, a lemma

Tag 052K in the Stacks Project.

Declarations registered for the tag:

Tag 0AS4, a lemma

Tag 0AS4 in the Stacks Project.

valuationRing_directLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/DirectLimit.lean, line 62. References: EGA IV (5.13.3), “(i), special case”.

A filtered direct limit of valuation rings is a valuation ring: if (G i, f i j) is a directed system of commutative rings over a directed index set in which every G i is an integral domain and a valuation ring, then the colimit Ring.DirectLimit G f is an integral domain and a valuation ring.

The conclusion is phrased as an existential over an IsDomain instance together with ValuationRing, because ValuationRing is a typeclass whose statement presupposes [IsDomain _], and Mathlib does not automatically derive IsDomain for the colimit.

theorem valuationRing_directLimit
    {ι : Type*} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
    (G : ι → Type*) [∀ i, CommRing (G i)] [∀ i, IsDomain (G i)]
    (f : (i j : ι) → i ≤ j → G i →+* G j)
    [DirectedSystem G fun i j h => f i j h]
    [∀ i, ValuationRing (G i)] :
    ∃ _ : IsDomain (Ring.DirectLimit G fun i j h => f i j h),
      ValuationRing (Ring.DirectLimit G fun i j h => f i j h)
Tag 052L, a lemma

Tag 052L in the Stacks Project.

Declarations registered for the tag:

Tag 0AAV, a lemma

Tag 0AAV in the Stacks Project.

intersectionSubring_ne_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Restriction.lean, line 112.

Stacks Tag 0AAV. Let L / K be an algebraic extension of fields and let B be a valuation subring of L (so B is a valuation ring with Frac B = L) which is not a field (B ≠ ⊤). Then A = K ∩ B = B.comap (algebraMap K L) is a valuation subring of K (so a valuation ring with fraction field K, by its type) which is not a field (A ≠ ⊤).

theorem intersectionSubring_ne_top
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (halg : Algebra.IsAlgebraic K L)
    (B : ValuationSubring L) (hB : B ≠ ⊤) :
    intersectionSubring B ≠ (⊤ : ValuationSubring K)
Tag 088Y, a lemma

Tag 088Y in the Stacks Project.

valuationRing_quotient_of_prime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Constructions.lean, line 83.

For any prime ideal p ⊆ A, the quotient ring A ⧸ p is a valuation ring.

theorem valuationRing_quotient_of_prime (𝔭 : Ideal A) [𝔭.IsPrime] :
    ValuationRing (A ⧸ 𝔭)

valuationRing_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Constructions.lean, line 92. References: EGA II (7.1.1), “partial”.

Let M ⊆ A be a submonoid with M ≤ nonZeroDivisors A, and let S be any commutative ring that is a localization of A at M. Then S is a valuation ring. (S is an integral domain by IsLocalization.isDomain_of_le_nonZeroDivisors.)

theorem valuationRing_localization (M : Submonoid A) (hM : M ≤ nonZeroDivisors A)
    (S : Type*) [CommRing S] [Algebra A S] [IsLocalization M S] :
    haveI : IsDomain S := IsLocalization.isDomain_of_le_nonZeroDivisors (S := S) hM
    ValuationRing S

valuationRing_localization_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Constructions.lean, line 109. References: EGA II (7.1.1), “partial”.

For any prime ideal p ⊆ A, the localization A_p = Localization.AtPrime p is a valuation ring.

theorem valuationRing_localization_atPrime (𝔭 : Ideal A) [𝔭.IsPrime] :
    ValuationRing (Localization.AtPrime 𝔭)
Tag 088Z, a lemma

Tag 088Z in the Stacks Project.

residueValuationSubring_mem_or_inv_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Constructions.lean, line 201.

Stacks Tag 088Z. C satisfies the valuation criterion of tag 052K: for every x : L, either x ∈ C or x⁻¹ ∈ C. Via ValuationSubring.ofSubring this says exactly that C is a valuation ring with fraction field L.

theorem residueValuationSubring_mem_or_inv_mem (A' : ValuationSubring L)
    (A : ValuationSubring (IsLocalRing.ResidueField A')) (x : L) :
    x ∈ residueValuationSubring A' A ∨ x⁻¹ ∈ residueValuationSubring A' A
Tag 00ID, a lemma

Tag 00ID in the Stacks Project.

Declarations registered for the tag:

Tag 00IE, a definition

Tag 00IE in the Stacks Project.

Declarations registered for the tag:

Tag 00IF, a lemma

Tag 00IF in the Stacks Project.

Declarations registered for the tag:

Tag 090Q, a lemma

Tag 090Q in the Stacks Project.

Declarations registered for the tag:

Tag 00IG, a lemma

Tag 00IG in the Stacks Project.

StacksValuation.isValuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/ValueGroup.lean, line 234. The attribute's comment: “Valuation ring, unit group and maximal ideal only. The value-group clause Kˣ/A* ≅ Im(v) is NOT formalized: the fourth conjunct merely says Set.range v is a subgroup of Γ.”.

Stacks 00IG (lemma-valuation-valuation-ring). Let (Γ, ≥) be a totally ordered abelian group, K a field, and v : Kˣ → Γ a group homomorphism with v(a + b) ≥ min (v a) (v b) for a, b, a + b nonzero. Then A = {x ∈ K | x = 0 ∨ v x ≥ 0} is a valuation ring with value group Im(v) ⊆ Γ, with maximal ideal m = {x ∈ K | x = 0 ∨ v x > 0} and group of units A* = {x ∈ Kˣ | v x = 0}.

Formalized here: ValuationRing A, the unit-group description and the maximal-ideal description. The value-group clause is not formalized. The fourth conjunct below only records that Set.range v is an additive subgroup of Γ, which is a triviality about any group homomorphism; it does not relate A's own value group Kˣ/A* to Im(v). Stating that identification needs A as a ValuationSubring K (so that IsFractionRing A K and ValuationRing.valuation A K are available), whereas integerSubring is a bare Subring. The @[stacks 00IG] attribute is qualified accordingly.

theorem isValuationRing :
    -- `A` is a valuation ring.
    ValuationRing sv.integerSubring ∧
    -- The group of units of `A` is `{x | v x = 0}`.
    (∀ x : sv.integerSubring, IsUnit x ↔ sv.addVal (x : K) = 0) ∧
    -- The maximal ideal of `A` is `m = {x | v x > 0}`.
    (∀ x : sv.integerSubring,
      x ∈ IsLocalRing.maximalIdeal sv.integerSubring ↔ 0 < sv.addVal (x : K)) ∧
    -- The value group `Im(v) ⊆ Γ` is an additive subgroup of `Γ`.
    ((0 : Γ) ∈ Set.range sv.toFun ∧
      (∀ g ∈ Set.range sv.toFun, ∀ g' ∈ Set.range sv.toFun, g + g' ∈ Set.range sv.toFun) ∧
      (∀ g ∈ Set.range sv.toFun, -g ∈ Set.range sv.toFun))
Tag 00IH, a lemma

Tag 00IH in the Stacks Project.

ideals_correspond_to_valueGroupIdeals, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/ValueGroup.lean, line 535.

Stacks tag 00IH. Let A be a valuation ring with fraction field K and value group Γ = ValueGroup A K. The ideals of A are in inclusion-preserving bijection with the ideals of Γ (IsIdealGamma), via Φ(𝔞) = v(𝔞 \ {0}), and this bijection carries prime ideals to prime ideals (and reflects them).

theorem ideals_correspond_to_valueGroupIdeals :
    ∃ e : Ideal A ≃ {I : Set (Gamma A K) // IsIdealGamma A K I},
      (∀ 𝔞 𝔟 : Ideal A, 𝔞 ≤ 𝔟 ↔ (e 𝔞).1 ⊆ (e 𝔟).1) ∧
        (∀ 𝔞 : Ideal A, 𝔞.IsPrime ↔ IsPrimeIdealGamma A K (e 𝔞).1)
Tag 00II, a lemma

Tag 00II in the Stacks Project.

valuation_ring_noetherian_iff_dvr_or_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Criteria.lean, line 55. References: EGA II (7.1.6), “valuation ring ⇒ DVR”.

A valuation ring is Noetherian if and only if it is a discrete valuation ring or a field.

theorem valuation_ring_noetherian_iff_dvr_or_field
    (A : Type*) [CommRing A] [IsDomain A] [ValuationRing A] :
    IsNoetherianRing A ↔ IsDiscreteValuationRing A ∨ IsField A
Sources
Leandominates_iff · IsValuationRing · IsCenteredOn · ValuationRing.iff_isInteger_or_isInteger · ValuationSubring · ValuationSubring.instValuationRingSubtypeMem · ValuationSubring.instIsFractionRingSubtypeMem · valuationRing_directLimit

Section10.51 More Noetherian rings#

Section 10.51 of the Stacks Project, Tag 00IJ. 5 tags here are carried by 4 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00IK, a lemma

Tag 00IK in the Stacks Project.

Declarations registered for the tag:

Tag 00IN, a lemma

Tag 00IN in the Stacks Project.

artin_rees, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Noetherian/ArtinRees.lean, line 66. References: EGA 0 (7.3.2.1).

Artin–Rees lemma. For a Noetherian ring R, an ideal I ⊆ R and a submodule N of a finite R-module M, there is a constant c > 0 with I^n M ⊓ N = I^(n-c) • (I^c M ⊓ N) for every n ≥ c.

theorem artin_rees
    {R : Type*} {M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    [IsNoetherianRing R] [Module.Finite R M]
    (I : Ideal R) (N : Submodule R M) :
    ∃ c > 0, ∀ n ≥ c,
      (I ^ n • (⊤ : Submodule R M)) ⊓ N
        = I ^ (n - c) • ((I ^ c • (⊤ : Submodule R M)) ⊓ N)
Tag 00IO, a lemma

Tag 00IO in the Stacks Project.

exists_comap_smul_eq_and_range_inf_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Noetherian/ArtinRees.lean, line 158. References: EGA 0 (7.3.2.1), “more general”.

Map version of Artin–Rees. For an exact sequence 0 → K → M → N of finitely generated modules over a Noetherian ring R and an ideal I, there is a constant c such that for all n ≥ c, f⁻¹(IⁿN) = K + Iⁿ⁻ᶜ · f⁻¹(IᶜN) and f(M) ∩ IⁿN ⊆ f(Iⁿ⁻ᶜ M).

theorem exists_comap_smul_eq_and_range_inf_le
    {R : Type*} [CommRing R] [IsNoetherianRing R]
    {M N : Type*} [AddCommGroup M] [AddCommGroup N]
    [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N]
    (f : M →ₗ[R] N) (I : Ideal R) :
    ∃ c, ∀ n ≥ c,
      Submodule.comap f (I ^ n • (⊤ : Submodule R N)) =
        LinearMap.ker f +
          I ^ (n - c) • Submodule.comap f (I ^ c • (⊤ : Submodule R N)) ∧
      LinearMap.range f ⊓ (I ^ n • (⊤ : Submodule R N)) ≤
        Submodule.map f (I ^ (n - c) • (⊤ : Submodule R M))
Tag 00IP, a lemma

Tag 00IP in the Stacks Project.

Declarations registered for the tag:

Tag 00IQ, a lemma

Tag 00IQ in the Stacks Project.

exists_notMem_localized_krullIntersection_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Noetherian/ArtinRees.lean, line 206. References: EGA 0 (7.4.2), “more general”; SGA 3 VIB (6.5.3), “special case”.

For every prime ideal p containing I, there exists f ∈ R with f ∉ p such that the localization of N = ⋂_n I^n M at the submonoid generated by f is the zero submodule.

theorem exists_notMem_localized_krullIntersection_eq_bot
    {R : Type*} [CommRing R] [IsNoetherianRing R]
    {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M]
    (I : Ideal R) (p : Ideal R) [p.IsPrime] (hIp : I ≤ p) :
    ∃ f : R, f ∉ p ∧
      (krullIntersection M I).localized (Submonoid.powers f) = ⊥

krullIntersection_eq_bot_of_le_jacobson, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Noetherian/ArtinRees.lean, line 228. References: EGA 0 (7.3.5), “(a) => (c)”.

If I is contained in the Jacobson radical of R, then N = ⋂_n I^n M = 0.

theorem krullIntersection_eq_bot_of_le_jacobson
    {R : Type*} [CommRing R] [IsNoetherianRing R]
    {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M]
    (I : Ideal R) (hI : I ≤ Ideal.jacobson ⊥) :
    krullIntersection M I = ⊥
Sources
LeanModule.finitePresentation_of_finite · isNoetherian_of_isNoetherianRing_of_finite · IsNoetherian.noetherian · isNoetherian_iff' · artin_rees · exists_comap_smul_eq_and_range_inf_le · Ideal.iInf_pow_smul_eq_bot_of_isLocalRing · exists_notMem_localized_krullIntersection_eq_bot

Section10.52 Length#

Section 10.52 of the Stacks Project, Tag 00IU. 14 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 11 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02LY, a definition

Tag 02LY in the Stacks Project.

Declarations registered for the tag:

Tag 02LZ, a lemma

Tag 02LZ in the Stacks Project.

Declarations registered for the tag:

Tag 00IV, a lemma

Tag 00IV in the Stacks Project.

Declarations registered for the tag:

Tag 00IW, a lemma

Tag 00IW in the Stacks Project.

exists_pow_maximalIdeal_smul_eq_bot_of_length_lt_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/Finiteness.lean, line 103.

Stacks 00IW. For a local ring R with maximal ideal m, if the R-module M has finite length then m ^ n M = 0 for some n ≥ 0.

theorem exists_pow_maximalIdeal_smul_eq_bot_of_length_lt_top
    (R : Type*) [CommRing R] [IsLocalRing R]
    (M : Type*) [AddCommGroup M] [Module R M]
    (h : Module.length R M < ⊤) :
    ∃ n : ℕ, IsLocalRing.maximalIdeal R ^ n • (⊤ : Submodule R M) = ⊥
Tag 00IX, a lemma

Tag 00IX in the Stacks Project.

Module.length_le_length_restrictScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/Comparison.lean, line 67. The attribute's comment: “(1)”.

For a ring map φ : R → S and an S-module M, viewed as an R-module by restriction of scalars along φ, the length over R is at least the length over S.

theorem Module.length_le_length_restrictScalars
    (R S : Type*) [CommRing R] [CommRing S] (φ : R →+* S)
    (M : Type*) [AddCommGroup M] [Module S M] :
    letI : Module R M := Module.compHom M φ
    Module.length S M ≤ Module.length R M

length_restrictScalars_eq_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/Comparison.lean, line 78. The attribute's comment: “(2)”.

For a surjective ring map φ : R → S and an S-module M, viewed as an R-module by restriction of scalars along φ, the length over R equals the length over S.

theorem length_restrictScalars_eq_of_surjective
    (R S : Type*) [CommRing R] [CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective φ)
    (M : Type*) [AddCommGroup M] [Module S M] :
    letI : Module R M := Module.compHom M φ
    Module.length R M = Module.length S M
Tag 00IY, a lemma

Tag 00IY in the Stacks Project.

length_eq_rank_of_maximal_smul_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/Comparison.lean, line 129. The attribute's comment: “(1)”.

Length of M as an R-module equals the dimension of M as an R ⧸ m-vector space, when m M = 0 for a maximal ideal m.

theorem length_eq_rank_of_maximal_smul_eq_zero
    (R : Type*) [CommRing R] (m : Ideal R) [m.IsMaximal]
    (M : Type*) [AddCommGroup M] [Module R M]
    (hM : ∀ r ∈ m, ∀ x : M, r • x = 0) :
    letI hTors : Module.IsTorsionBySet R M (m : Set R) :=
      fun x a => hM a.1 a.2 x
    letI : Module (R ⧸ m) M := hTors.module
    Module.length R M = Cardinal.toENat (Module.rank (R ⧸ m) M)

length_lt_top_iff_finite_of_smul_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/Comparison.lean, line 145. The attribute's comment: “(2)”.

The length of M is finite if and only if M is a finite R-module, when m M = 0 for a maximal ideal m.

theorem length_lt_top_iff_finite_of_smul_eq_zero
    (R : Type*) [CommRing R] (m : Ideal R) [m.IsMaximal]
    (M : Type*) [AddCommGroup M] [Module R M]
    (hM : ∀ r ∈ m, ∀ x : M, r • x = 0) :
    Module.length R M < ⊤ ↔ Module.Finite R M
Tag 00IZ, a lemma

Tag 00IZ in the Stacks Project.

Module.length_localizedModule_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/Comparison.lean, line 194.

Stacks Tag 00IZ. Let R be a ring, M an R-module, and S ⊆ R a multiplicative subset. Then length_R(M) ≥ length_{S⁻¹R}(S⁻¹M).

theorem Module.length_localizedModule_le :
    Module.length (Localization S) (LocalizedModule S M) ≤ Module.length R M
Tag 00J0, a lemma

Tag 00J0 in the Stacks Project.

length_lt_top_of_pow_smul_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/Finiteness.lean, line 234.

Stacks 00J0. Let R be a commutative ring with finitely generated maximal ideal m. If M is a finite R-module with m ^ n • M = 0 for some n, then length_R M < ∞.

theorem length_lt_top_of_pow_smul_eq_bot
    {R : Type*} [CommRing R]
    (m : Ideal R) [m.IsMaximal] (hm : m.FG)
    {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M]
    (n : ℕ) (hn : m ^ n • (⊤ : Submodule R M) = ⊥) :
    Module.length R M < ⊤
Tag 00J1, a definition

Tag 00J1 in the Stacks Project.

Declarations registered for the tag:

Tag 00J2, a lemma

Tag 00J2 in the Stacks Project.

Declarations registered for the tag:

Tag 00J3, a lemma

Tag 00J3 in the Stacks Project.

length_eq_and_subQuot_isSimpleModule_and_exists_quot_maximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/CompositionSeries.lean, line 124.

Stacks 00J3 (parts 1, 2, 3). For a finite-length R-module M and a maximal chain 0 = M_0 ⊂ M_1 ⊂ … ⊂ M_n = M of submodules, we have

  • n = length_R(M) (length is well-defined on maximal chains);
  • each successive quotient M_{i+1}/M_i is simple;
  • each successive quotient is isomorphic to R/𝔪 for some maximal ideal 𝔪.

Part (4) of Stacks 00J3, which counts the indices i with 𝔪_i = 𝔪 in terms of the length of a localization, is not covered by this statement.

theorem length_eq_and_subQuot_isSimpleModule_and_exists_quot_maximal
    {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
    {n : ℕ} (M' : Fin (n + 1) → Submodule R M) (hchain : IsMaximalChainPrime M') :
    ((compositionSeriesOfMaximalChain M' hchain).length : ℕ∞)
        = Module.length R M ∧
      (∀ i : Fin n, IsSimpleModule R (subQuot M' i)) ∧
      (∀ i : Fin n, ∃ (𝔪 : Ideal R) (_ : 𝔪.IsMaximal),
        Nonempty (subQuot M' i ≃ₗ[R] R ⧸ 𝔪))
Tag 02M0, a lemma

Tag 02M0 in the Stacks Project.

length_eq_sum_residue_degree_mul_localized_length, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/SemiLocal.lean, line 200. References: EGA IV (21.10.11), “partial”; SGA 3 VIIB (1.2.6), “partial”.

Stacks 02M0. Length over a local ring A of a finite-length module M over a semi-local A-algebra B, expressed as a sum over the (finitely many) maximal ideals of B of the residue degrees times the lengths of the localizations.

theorem length_eq_sum_residue_degree_mul_localized_length
    {A B : Type*} [CommRing A] [CommRing B] [IsLocalRing A] [Algebra A B]
    {M : Type*} [AddCommGroup M] [Module B M] [Module A M] [IsScalarTower A B M]
    (n : ℕ) (𝔪 : Fin n → Ideal B)
    -- `B` is semi-local with the `𝔪 i` being exactly its maximal ideals:
    (hmax : ∀ i, (𝔪 i).IsMaximal)
    (hinj : Function.Injective 𝔪)
    (hsurj : ∀ I : Ideal B, I.IsMaximal → ∃ i, 𝔪 i = I)
    -- each `𝔪 i` lies over the maximal ideal of `A`:
    (hlies : ∀ i, IsLocalRing.maximalIdeal A = (𝔪 i).comap (algebraMap A B))
    -- `M` has finite length over `B`:
    (hM : IsFiniteLength B M) :
    -- introduce the residue-field algebra structures and the primality of the `𝔪 i`:
    letI : ∀ i, (𝔪 i).IsMaximal := hmax
    letI : ∀ i, Algebra (IsLocalRing.maximalIdeal A).ResidueField (𝔪 i).ResidueField :=
      fun i => residueFieldAlgebra (𝔪 i) (hlies i)
    -- finiteness of residue degrees `[κ(𝔪 i) : κ(𝔪)] < ∞`:
    (∀ i, Module.Finite (IsLocalRing.maximalIdeal A).ResidueField (𝔪 i).ResidueField) →
      -- `M` has finite length over `A`, and the length formula holds in `ℕ∞`:
      IsFiniteLength A M ∧
        Module.length A M
          = ∑ i : Fin n,
              (Module.finrank (IsLocalRing.maximalIdeal A).ResidueField (𝔪 i).ResidueField : ℕ∞)
                * Module.length (Localization.AtPrime (𝔪 i))
                    (LocalizedModule (𝔪 i).primeCompl M)
Tag 02M1, a lemma

Tag 02M1 in the Stacks Project.

length_baseChange_eq_length_mul_length_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/FlatLocalHom.lean, line 57. References: EGA IV (2.5.5.3); EGA IV (2.5.5.2), “case N = B”; EGA IV (2.5.5.1), “F = structure sheaf”; EGA IV (4.7.1), “more general”; EGA IV (4.7.2), “more general”.

For a flat local homomorphism A → B of local rings and every A-module M, the length of M over A times the length of B / m_A B over B equals the length of the base change B ⊗[A] M over B, as an identity in ℕ∞.

theorem length_baseChange_eq_length_mul_length_quotient
    (A B : Type*) [CommRing A] [CommRing B] [Algebra A B] [IsLocalRing A] [IsLocalRing B]
    [IsLocalHom (algebraMap A B)] [Module.Flat A B]
    (M : Type*) [AddCommGroup M] [Module A M] :
    Module.length A M *
      Module.length B (B ⧸ extendedMaximalIdeal A B) =
      Module.length B (B ⊗[A] M)

finite_length_iff_finite_length_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/FlatLocalHom.lean, line 70. References: EGA IV (2.5.5.3), “in particular”; EGA IV (4.7.1).

For a flat local homomorphism A → B of local rings such that B / m_A B has finite length over B, an A-module M has finite length over A if and only if its base change B ⊗[A] M has finite length over B.

theorem finite_length_iff_finite_length_baseChange
    (A B : Type*) [CommRing A] [CommRing B] [Algebra A B] [IsLocalRing A] [IsLocalRing B]
    [IsLocalHom (algebraMap A B)] [Module.Flat A B]
    (hfin : Module.length B (B ⧸ extendedMaximalIdeal A B) < ⊤)
    (M : Type*) [AddCommGroup M] [Module A M] :
    Module.length A M < ⊤ ↔ Module.length B (B ⊗[A] M) < ⊤
Tag 02M2, a lemma

Tag 02M2 in the Stacks Project.

length_quotient_maximalIdeal_map_mul_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/FlatLocalHom.lean, line 143. References: EGA IV (2.5.5.1), “special case”; EGA IV (2.5.5.2), “special case”; EGA IV (2.5.5.3), “special case”.

For flat local homomorphisms of local rings f : A → B and g : B → C, the length of B / m_A B over B times the length of C / m_B C over C equals the length of C / m_A C over C, where m_A C is the extension of m_A along the composite A → C. The equality holds in ℕ∞.

theorem length_quotient_maximalIdeal_map_mul_eq
    (_hf_local : IsLocalHom f) (hg_local : IsLocalHom g)
    (_hf_flat : f.Flat) (hg_flat : g.Flat) :
    Module.length B (B ⧸ Ideal.map f (maximalIdeal A)) *
        Module.length C (C ⧸ Ideal.map g (maximalIdeal B))
      = Module.length C (C ⧸ Ideal.map (g.comp f) (maximalIdeal A))
Sources
LeanModule.length · Module.length_eq_height · Module.length_compositionSeries · Module.length_ne_top_iff · isFiniteLength_iff_isNoetherian_isArtinian · Module.IsNoetherian.finite · Module.length_eq_add_of_exact · exists_pow_maximalIdeal_smul_eq_bot_of_length_lt_top

Section10.53 Artinian rings#

Section 10.53 of the Stacks Project, Tag 00J4. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00J5, a definition

Tag 00J5 in the Stacks Project.

Declarations registered for the tag:

Tag 00J6, a lemma

Tag 00J6 in the Stacks Project.

finite_dimensional_algebra_is_artinian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Artinian/Basic.lean, line 158. References: EGA IV (2.5.8.8), “special case”.

A finite-dimensional algebra over a field is an Artinian ring.

theorem finite_dimensional_algebra_is_artinian
    (K : Type*) [Field K] (R : Type*) [Ring R] [Algebra K R]
    [FiniteDimensional K R] : IsArtinianRing R
Tag 00JA, a lemma

Tag 00JA in the Stacks Project.

MaximalSpectrum.algebraMap_pi_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Artinian/Basic.lean, line 102. The attribute's comment: “The product decomposition, for an arbitrary family of localizations. Discreteness of Spec R is the tag's own hypothesis, by PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical.”. References: SGA 3 VIIB (0.1.1), “partial”.

Stacks 00JA and 00JB (the product decomposition). A commutative semiring with discrete prime spectrum — in particular an Artinian ring — is the product of its localizations at its (finitely many) maximal ideals: for any family Rₘ of localizations of R at the maximal ideals of R, the canonical map R → ∀ 𝔪, Rₘ 𝔪 is bijective.

public theorem algebraMap_pi_bijective (R : Type*) [CommSemiring R]
    [DiscreteTopology (PrimeSpectrum R)]
    (Rₘ : MaximalSpectrum R → Type*) [∀ m, CommSemiring (Rₘ m)] [∀ m, Algebra R (Rₘ m)]
    [∀ m, IsLocalization.AtPrime (Rₘ m) m.asIdeal] :
    Function.Bijective (algebraMap R (∀ m, Rₘ m))

nonempty_ringEquiv_pi_localization_and_isMaximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Artinian/Basic.lean, line 122. References: EGA I (6.2.2), “affine, special case”.

A ring with finitely many maximal ideals whose Jacobson radical is contained in the nilradical is isomorphic to the product of its localizations at its maximal ideals, and every prime ideal of it is maximal.

theorem nonempty_ringEquiv_pi_localization_and_isMaximal (R : Type*) [CommRing R] [Finite
  (MaximalSpectrum R)]
    (h : Ring.jacobson R ≤ nilradical R) :
    Nonempty (R ≃+* (Π m : MaximalSpectrum R, Localization.AtPrime m.asIdeal)) ∧
    (∀ p : Ideal R, p.IsPrime → p.IsMaximal)
Tag 00JB, a lemma

Tag 00JB in the Stacks Project.

MaximalSpectrum.algebraMap_pi_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Artinian/Basic.lean, line 102. The attribute's comment: “The final assertion, under discreteness of Spec R in place of Artinian-ness”. References: SGA 3 VIIB (0.1.1), “partial”.

Stacks 00JA and 00JB (the product decomposition). A commutative semiring with discrete prime spectrum — in particular an Artinian ring — is the product of its localizations at its (finitely many) maximal ideals: for any family Rₘ of localizations of R at the maximal ideals of R, the canonical map R → ∀ 𝔪, Rₘ 𝔪 is bijective.

public theorem algebraMap_pi_bijective (R : Type*) [CommSemiring R]
    [DiscreteTopology (PrimeSpectrum R)]
    (Rₘ : MaximalSpectrum R → Type*) [∀ m, CommSemiring (Rₘ m)] [∀ m, Algebra R (Rₘ m)]
    [∀ m, IsLocalization.AtPrime (Rₘ m) m.asIdeal] :
    Function.Bijective (algebraMap R (∀ m, Rₘ m))

isArtinianRing_iff_isFiniteLength_and_isNoetherianRing_and_toPiLocalization_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Artinian/Basic.lean, line 291. The attribute's comment: “All four assertions: the finite-length criterion, Noetherianness, maximality of the primes, and the product decomposition, the last as bijectivity of the canonical map.”. References: EGA I (6.2.2), “affine, special case”; SGA 3 VIIB (0.1.1), “partial, special case”.

Artinian rings have finite length, and decompose. A commutative ring R is Artinian if and only if it has finite length as a module over itself; and any Artinian ring R is also Noetherian, has all of its prime ideals maximal, has only finitely many maximal ideals, and is the product of its localizations at them, in the sense that the canonical R-algebra map R → ∀ 𝔪 : MaximalSpectrum R, Localization.AtPrime 𝔪 is bijective.

public theorem
    isArtinianRing_iff_isFiniteLength_and_isNoetherianRing_and_toPiLocalization_bijective
    (R : Type*) [CommRing R] :
    (IsArtinianRing R ↔ IsFiniteLength R R) ∧
      (IsArtinianRing R → IsNoetherianRing R ∧ (∀ p : Ideal R, p.IsPrime → p.IsMaximal) ∧
        Finite (MaximalSpectrum R) ∧
        Function.Bijective (MaximalSpectrum.toPiLocalization R))
Sources
Leanmonotone_stabilizes_iff_artinian · finite_dimensional_algebra_is_artinian · MaximalSpectrum.algebraMap_pi_bijective · nonempty_ringEquiv_pi_localization_and_isMaximal · isArtinianRing_iff_isFiniteLength_and_isNoetherianRing_and_toPiLocalization_bijective

Section10.54 Homomorphisms essentially of finite type#

Section 10.54 of the Stacks Project, Tag 07DR. 5 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00QM, a definition

Tag 00QM in the Stacks Project.

IsEssentiallyOfFiniteType, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/EssentialFiniteness/Defs.lean, line 55. The attribute's comment: “(1)”. References: EGA IV (1.3.8).

A ring map f : R →+* S is essentially of finite type if S is, as an R-algebra (via f), the localization at some submonoid of an R-algebra T of finite type.

def IsEssentiallyOfFiniteType.{u} (R S : Type u) [CommRing R] [CommRing S]
    (f : R →+* S) : Prop

IsEssentiallyOfFinitePresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/EssentialFiniteness/Defs.lean, line 65. The attribute's comment: “(2)”.

A ring map f : R →+* S is essentially of finite presentation if S is, as an R-algebra (via f), the localization at some submonoid of an R-algebra T of finite presentation.

def IsEssentiallyOfFinitePresentation.{u} (R S : Type u) [CommRing R] [CommRing S]
    (f : R →+* S) : Prop
Tag 07DS, a lemma

Tag 07DS in the Stacks Project.

essFiniteType_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/EssentialFiniteness/Composition.lean, line 256. The attribute's comment: “(1)”. References: EGA IV (1.3.9).

Statement 1. The class of ring maps essentially of finite type is preserved under composition (Stacks Tag 07DS, first assertion).

theorem essFiniteType_comp {R : Type u} {S : Type v} {T : Type w}
    [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : S →+* T}
    (hf : f.EssFiniteType) (hg : g.EssFiniteType) : (g.comp f).EssFiniteType

essFinitePresentation_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/EssentialFiniteness/Composition.lean, line 282. The attribute's comment: “(2)”.

Statement 2. The class of ring maps essentially of finite presentation is preserved under composition (Stacks Tag 07DS, second assertion).

The proof combines Stacks tag 053N, transitivity of finite presentation, localization-of-localization, and a universe re-presentation:

  1. Unpack hf: f.p. R-algebra A, with S = M⁻¹A (IsLocalization M S). Unpack hg: f.p. S-algebra B, with T = N₂⁻¹B (IsLocalization N₂ T).
  2. A acts on B through S (IsScalarTower A S B).
  3. essFP_descent M B: descend B to a f.p. A-algebra B₀ with B = N⁻¹B₀ (IsLocalization N B).
  4. Algebra.FinitePresentation.trans R A B₀: since A is f.p./R and B₀ is f.p./A, B₀ is f.p./R.
  5. localization-of-localization: B = N⁻¹B₀ and T = N₂⁻¹B, so T = U⁻¹B₀ for U := localizationLocalizationSubmodule N N₂ (IsLocalization.localization_localization_isLocalization).
  6. essFP_reuniverse: re-present the f.p. R-algebra B₀ : Type (max u v w) (with its localization IsLocalization U T) by a f.p. R-algebra A' : Type (max u w) carrying IsLocalization U' T, matching the universe demanded by RingHom.EssentiallyOfFinitePresentation for g.comp f : R →+* T.
theorem essFinitePresentation_comp {R : Type u} {S : Type v} {T : Type w}
    [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : S →+* T}
    (hf : f.EssentiallyOfFinitePresentation) (hg : g.EssentiallyOfFinitePresentation) :
    (g.comp f).EssentiallyOfFinitePresentation
Tag 0AUF, a lemma

Tag 0AUF in the Stacks Project.

RingHom.EssentiallyOfFinitePresentation.baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/EssentialFiniteness/BaseChange.lean, line 84. The attribute's comment: “(2)”.

Essential finite presentation is preserved by base change. The target is written in the canonical tensor-product model of the pushout; invariance under isomorphism identifies this with any other model of the base change.

theorem baseChange {R : Type u} {S : Type v} {T : Type w}
    [CommRing R] [CommRing S] [CommRing T] [Algebra R S]
    (f : R →+* T) (h : f.EssentiallyOfFinitePresentation) :
    letI := f.toAlgebra
    ((Algebra.TensorProduct.includeLeft (R := R) (S := S) (A := S) (B := T)).toRingHom)
      |>.EssentiallyOfFinitePresentation

Declarations registered for the tag:

Tag 07DT, a lemma

Tag 07DT in the Stacks Project.

finite_iff_residue_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/EssentialFiniteness/ArtinianTarget.lean, line 296. The attribute's comment: “(1)”.

f : R → S is finite if and only if the composite π ∘ f : R → S/m is finite.

theorem finite_iff_residue_finite (f : R →+* S) :
    f.Finite ↔ ((IsLocalRing.residue S).comp f).Finite

finiteType_iff_residue_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/EssentialFiniteness/ArtinianTarget.lean, line 306. The attribute's comment: “(2)”. References: EGA I (6.4.11), “special case”.

f : R → S is of finite type if and only if the composite π ∘ f : R → S/m is of finite type.

theorem finiteType_iff_residue_finiteType (f : R →+* S) :
    f.FiniteType ↔ ((IsLocalRing.residue S).comp f).FiniteType

essFiniteType_iff_residue_essFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/EssentialFiniteness/ArtinianTarget.lean, line 316. The attribute's comment: “(3)”. References: EGA I (6.4.11), “special case”.

f : R → S is essentially of finite type if and only if the composite π ∘ f : R → S/m is essentially of finite type.

theorem essFiniteType_iff_residue_essFiniteType (f : R →+* S) :
    f.EssFiniteType ↔ ((IsLocalRing.residue S).comp f).EssFiniteType
Tag 0AUG, a lemma

Tag 0AUG in the Stacks Project.

exists_isLocalizationOfQuotientMap_mvPolynomial_atMaximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/ClosedPointOfSpecialFibre.lean, line 827.

Let R → S be a ring map of local rings, not necessarily local, that is essentially of finite type. Then there are n : ℕ and a maximal ideal 𝔪 ⊆ R[x_1, …, x_n] lying over the maximal ideal of R such that S is a localization of a quotient of the local ring R[x_1, …, x_n]_𝔪, compatibly with the R-algebra structures.

theorem exists_isLocalizationOfQuotientMap_mvPolynomial_atMaximal
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
    [Algebra R S] [Algebra.EssFiniteType R S] :
    ∃ (n : ℕ) (𝔪 : Ideal (MvPolynomial (Fin n) R)) (_ : 𝔪.IsMaximal),
      haveI : 𝔪.IsPrime := (‹𝔪.IsMaximal›).isPrime
      𝔪.comap (algebraMap R (MvPolynomial (Fin n) R)) = IsLocalRing.maximalIdeal R ∧
      ∃ (g : Localization.AtPrime 𝔪 →+* S),
        g.comp (algebraMap R (Localization.AtPrime 𝔪)) = algebraMap R S ∧
        IsLocalizationOfQuotientMap g
Sources
LeanIsEssentiallyOfFiniteType · IsEssentiallyOfFinitePresentation · essFiniteType_comp · essFinitePresentation_comp · RingHom.EssentiallyOfFinitePresentation.baseChange · RingHom.EssFiniteType.isStableUnderBaseChange · finite_iff_residue_finite · finiteType_iff_residue_finiteType

Section10.55 K-groups#

Section 10.55 of the Stacks Project, Tag 00JC. 8 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00JD, a lemma

Tag 00JD in the Stacks Project.

length_K0prime_hom_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/Defs.lean, line 185.

Stacks Tag 00JD. If R is an Artinian local ring then the length function defines an abelian group homomorphism K'_0(R) →+ ℤ sending the class of each presentation P to its integer length.

theorem length_K0prime_hom_exists (R : Type u) [CommRing R]
    [IsArtinianRing R] [IsLocalRing R] :
    ∃ φ : K0prime R →+ ℤ,
      ∀ P : FGPres R, φ (K0prime.mk P) = lengthOfPresℤ R P
Tag 00JE, an example

Tag 00JE in the Stacks Project.

finrank_additive_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/Field.lean, line 55. References: SGA 6 I (6.0), “(ii), special case”.

Over a field k, the (finite) dimension function is additive on short exact sequences of k-vector spaces in ModuleCat.{u} k: if 0 → X₁ → X₂ → X₃ → 0 is short exact and X₂ is finite-dimensional, then finrank k X₂ = finrank k X₁ + finrank k X₃.

This is the core computation underlying the informal Stacks remark that K₀(k) = K'₀(k) ≅ ℤ for a field k, with the isomorphism given by the dimension/length function. Indeed, this additivity is exactly the condition that makes finrank descend to a well-defined homomorphism from the Grothendieck group of finitely generated k-modules to ℤ.

theorem finrank_additive_of_shortExact {k : Type u} [Field k]
    (S : ShortComplex (ModuleCat.{u} k))
    (hfin : Module.Finite k S.X₂)
    (hS : S.ShortExact) :
    Module.finrank k S.X₂ = Module.finrank k S.X₁ + Module.finrank k S.X₃
Tag 00JF, an example

Tag 00JF in the Stacks Project.

K0_polynomial_isoZ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/PID.lean, line 977. The attribute's comment: “K0(k[x]) ≅ ℤ”. References: SGA 6 IX (1.7), “special case”.

K0(k[x]) ≅ ℤ, exhibited by an explicit isomorphism that sends the class [k[x]] of the rank-1 free module to 1. (The rank map.)

theorem K0_polynomial_isoZ (k : Type*) [Field k] :
    ∃ e : K0OfProjGen (Polynomial k) ≃+ ℤ,
      e (K0OfProjGen.mk (Polynomial k) (K0Gen.free1 (Polynomial k))) = 1

K0'_polynomial_isoZ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/PID.lean, line 989. The attribute's comment: “K0'(k[x]) ≅ ℤ”. References: SGA 6 IX (1.7), “Lemma 1.7, case A = k[T]”; SGA 6 IX (3.4), “Case S = Spec k”.

K0'(k[x]) ≅ ℤ, exhibited by an explicit isomorphism that sends the class [k[x]] to 1 (the rank of the free part). Every torsion finite module has class 0.

theorem K0'_polynomial_isoZ (k : Type*) [Field k] :
    ∃ e : K0PrimeOfFinPres (Polynomial k) ≃+ ℤ,
      e (K0PrimeOfFinPres.mk (Polynomial k) (K0'Gen.free1 (Polynomial k))) = 1

K0toK0'_polynomial_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/PID.lean, line 1005. The attribute's comment: “K0(k[x]) ≅ K0'(k[x])”.

The canonical homomorphism ι : K0(k[x]) → K0'(k[x]) is an isomorphism (it is bijective).

Argument: rankHom ∘ K0toK0' = rankHomK0 (definitionally, rankHomK0), and both rankHom (D6) and rankHomK0 (D9) are bijective. Therefore K0toK0' = rankHom.symm ∘ rankHomK0 (as maps), a composite of bijections, hence bijective. Formally: K0toK0' is injective because rankHom ∘ K0toK0' = rankHomK0 is injective; it is surjective because rankHom is bijective and rankHomK0 = rankHom ∘ K0toK0' is surjective.

theorem K0toK0'_polynomial_bijective (k : Type*) [Field k] :
    Function.Bijective (K0toK0' (Polynomial k))
Tag 00JG, an example

Tag 00JG in the Stacks Project.

nodeRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NodeRing.lean, line 59. References: EGA IV (6.5.5).

The "node" ring R = {f ∈ k[x] ∣ f(0) = f(1)}, the subring of polynomials agreeing at 0 and 1.

def nodeRing (k : Type*) [Field k] : Subring (Polynomial k)
Tag 00JH, a lemma

Tag 00JH in the Stacks Project.

K0_product, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/Product/K0.lean, line 405. The attribute's comment: “K_0”.

For a product ring R = R₁ × R₂, the natural homomorphism K₀(R) → K₀(R₁) × K₀(R₂), given on generators by [M] ↦ ([M ⊗_R R₁], [M ⊗_R R₂]) (base change along the two projections), is an isomorphism of abelian groups.

The product map is characterized by its values on the generating classes K0.mk M; since these generate K0 (R₁ × R₂), the additive isomorphism e below is unique with the stated property, so this faithfully expresses that the product map is an isomorphism.

theorem K0_product (R1 R2 : Type u) [CommRing R1] [CommRing R2] :
    ∃ e : K0 (R1 × R2) ≃+ (K0 R1 × K0 R2),
      ∀ M : FGProj (R1 × R2),
        e (K0.mk M) =
          ( K0.mk (M.baseChangeHom (RingHom.fst R1 R2)),
            K0.mk (M.baseChangeHom (RingHom.snd R1 R2)) )

K0prime_product, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/Product/K0Prime.lean, line 513. The attribute's comment: “K'_0”.

Assume in addition that R₁ and R₂ are Noetherian (equivalently that R = R₁ × R₂ is Noetherian). Then the natural homomorphism K'₀(R) → K'₀(R₁) × K'₀(R₂), given on generators by [M] ↦ ([M ⊗_R R₁], [M ⊗_R R₂]), is an isomorphism of abelian groups.

As for Statement 1, the classes K0prime.mk M generate K0prime (R₁ × R₂), so the additive isomorphism e is uniquely determined by the stated property.

theorem K0prime_product (R1 R2 : Type u) [CommRing R1] [CommRing R2]
    [IsNoetherianRing R1] [IsNoetherianRing R2] :
    ∃ e : K0prime (R1 × R2) ≃+ (K0prime R1 × K0prime R2),
      ∀ M : FGPres (R1 × R2),
        e (K0prime.mk M) =
          ( K0prime.baseChangeMk (RingHom.fst R1 R2) M.module,
            K0prime.baseChangeMk (RingHom.snd R1 R2) M.module )
Tag 00JI, a lemma

Tag 00JI in the Stacks Project.

exists_finite_module_length_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/Artinian.lean, line 92. The attribute's comment: “Surjectivity ingredient only: every n : ℕ is the length of a finite module. K'_0(R) and the isomorphism length_R : K'_0(R) ≃ ℤ are not formalized.”.

Stacks 00JI (length-surjectivity form).

For an Artinian local ring R, the length map on finitely generated R-modules hits every natural number: for each n : ℕ there is a finitely generated R-module M with Module.length R M = n.

This is the surjectivity ingredient of the Stacks statement that length_R : K'_0(R) → ℤ is an isomorphism. The full Stacks statement also needs the construction of K'_0(R) (Stacks 00JH) and the injectivity of length_R; those rely on the composition-series structure of Artinian local rings and are left to a follow-up file once Mathlib has K'_0(R). The witness here is the standard one: M = (ResidueField R)^n.

theorem exists_finite_module_length_eq.{u} {R : Type u} [CommRing R] [IsLocalRing R]
    [IsArtinianRing R] (n : ℕ) :
    ∃ (M : Type u) (_ : AddCommGroup M) (_ : Module R M) (_ : Module.Finite R M),
      Module.length R M = n
Tag 00JJ, a lemma

Tag 00JJ in the Stacks Project.

K0.rank_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/Defs.lean, line 508.

Over a local ring, the rank map K_0(R) → ℤ is an isomorphism. Combined with finite_projective_is_finite_free, this gives the full statement of Stacks 00JJ.

theorem K0.rank_isIso
    (R : Type u) [CommRing R] [IsLocalRing R] :
    ∃ e : K0 R ≃+ ℤ, ⇑e = K0.rank R
Tag 00JK, a lemma

Tag 00JK in the Stacks Project.

length_eq_finrank_mul_length_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/KTheory/Grothendieck/Artinian.lean, line 143. The attribute's comment: “Numerical identity length P = rank P * length R only; the commutative diagram K_0(R) → K'_0(R) → ℤ is not formalized.”.

Over a local Artinian ring R, the length of any finite projective R-module P equals the rank of P times the length of R. This is the mathematical content of the commutative diagram relating K₀(R) and K'₀(R) for a local Artinian ring R: the rank-of-R length factor is exactly the bottom map of the diagram, and both vertical maps (rank and length) are isomorphisms with ℤ.

Proof sketch. Since R is a local ring and P is finitely generated and projective (hence flat), P is free of finite rank by Module.free_of_flat_of_isLocalRing. Then Module.length_of_free_of_finite gives the desired identity.

theorem length_eq_finrank_mul_length_self
    (R : Type*) [CommRing R] [IsLocalRing R] [IsArtinianRing R]
    (P : Type*) [AddCommGroup P] [Module R P]
    [Module.Finite R P] [Module.Projective R P] :
    Module.length R P = Module.finrank R P * Module.length R R
Sources
Leanlength_K0prime_hom_exists · finrank_additive_of_shortExact · K0_polynomial_isoZ · K0'_polynomial_isoZ · K0toK0'_polynomial_bijective · nodeRing · K0_product · K0prime_product

Section10.56 Graded rings#

Section 10.56 of the Stacks Project, Tag 00JL. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0EKB, a lemma

Tag 0EKB in the Stacks Project.

Submodule.IsHomogeneous.le_of_le_smul_of_le_irrelevant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Nakayama.lean, line 242.

Stacks 0EKB (graded Nakayama). Let A = ⨁ᵢ 𝒜ᵢ be a graded ring and M = ⨁_d ℳ_d a graded A-module. Let N, N' ⊆ M be graded submodules with N' finitely generated, and let I ⊆ 𝒜₊ = ⨁_{i > 0} 𝒜ᵢ be an ideal. If N' ⊆ N + I N', then N' ⊆ N.

public theorem Submodule.IsHomogeneous.le_of_le_smul_of_le_irrelevant
    {ιA ιM σA σM A M : Type*} [CommSemiring A] [AddCommMonoid M] [Module A M]
    [DecidableEq ιA] [AddCommMonoid ιA] [PartialOrder ιA] [CanonicallyOrderedAdd ιA]
    [SetLike σA A] [AddSubmonoidClass σA A] {𝒜 : ιA → σA} [GradedRing 𝒜]
    [DecidableEq ιM] [PartialOrder ιM] [SetLike σM M] [AddSubmonoidClass σM M]
    {ℳ : ιM → σM} [DirectSum.Decomposition ℳ]
    [AddAction ιA ιM] [IsOrderedCancelVAdd ιA ιM] [SetLike.GradedSMul 𝒜 ℳ]
    {I : Ideal A} {N N' : Submodule A M}
    (hN : N.IsHomogeneous ℳ) (hN' : N'.IsHomogeneous ℳ) (hfg : N'.FG)
    (hI : I ≤ 𝒜₊.toIdeal) (hle : N' ≤ N ⊔ I • N') :
    N' ≤ N
Tag 0EGH, a lemma

Tag 0EGH in the Stacks Project.

Stacks.Veronese.veronese_generated_in_deg_one_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Veronese.lean, line 516. References: EGA II (3.1.10), “affine case”; EGA II (2.1.6).

Theorem (Stacks Tag 0EGH, Lemma 10.56.2). Let S be a graded ring that is finitely generated over S_0. Then for all sufficiently divisible d the algebra S^{(d)} is generated in degree 1 over S_0: there is a d₀ ≥ 1 such that for every positive multiple d of d₀ and every n ≥ 1, the S_0-module S_{nd} equals the S_0-span of the n-fold products of elements of S_d.

ASSEMBLY: 1. Get homogeneous positive-degree generators (Step A homogeneous_generators_of_finiteType). 2. Case split on r = 0 (degenerate, use veroneseGeneratedInDegOne_of_trivial, witness d₀ = 1; Set.range f = ∅ since Fin 0 is empty) vs r ≥ 1. 3. For r ≥ 1: set L := ∏ i, deg i (positive common multiple of each deg i: 1 ≤ L by Finset.prod_pos; deg i ∣ L by Finset.dvd_prod_of_mem), witness d₀ := r * L ≥ 1, and discharge each positive multiple via Step H (veroneseGeneratedInDegOne_of_multiple).

theorem veronese_generated_in_deg_one_of_finiteType
    (h : FinitelyGeneratedOverGradeZero 𝒜) :
    ForAllSufficientlyDivisible (fun d => VeroneseGeneratedInDegOne 𝒜 d)
Tag 077G, a lemma

Tag 077G in the Stacks Project.

integralClosure_carrier_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/IntegralClosure/Homogeneous.lean, line 633.

If the structure map respects the gradings, an element of S is integral over R exactly when all of its homogeneous components are.

theorem integralClosure_carrier_eq
    (hφ : RespectsGrading ℛ 𝒮) :
    (integralClosure R S : Set S)
      = {s : S | ∀ d : ℕ, GradedRing.proj 𝒮 d s ∈ integralClosure R S}
Sources
LeanSubmodule.IsHomogeneous.le_of_le_smul_of_le_irrelevant · Stacks.Veronese.veronese_generated_in_deg_one_of_finiteType · integralClosure_carrier_eq

Section10.57 Proj of a graded ring#

Section 10.57 of the Stacks Project, Tag 00JM. 10 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00JN, a definition

Tag 00JN in the Stacks Project.

Proj, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Proj/Defs.lean, line 51. References: EGA II (2.3.1), “set of graded primes”; EGA III (4.3.13).

The homogeneous spectrum Proj 𝒜 of a graded ring: the set of homogeneous prime ideals 𝔭 of A with 𝒜₊ ⊄ 𝔭, topologized by the subspace topology from Spec A.

abbrev Proj : Type _
Tag 00JO, a lemma

Tag 00JO in the Stacks Project.

gradedPrimesComparison_isHomeomorph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Proj/Defs.lean, line 467.

Let S be a ℤ-graded ring containing a homogeneous invertible element of positive degree. Then the comparison map Φ : G → Spec(S₀), q ↦ q ∩ S₀, from the space of ℤ-graded primes of S (with the subspace topology) to Spec(S₀), is a homeomorphism.

theorem gradedPrimesComparison_isHomeomorph
    (hf : HasHomogeneousUnitOfPosDegree 𝒜) :
    IsHomeomorph (gradedPrimesComparison 𝒜)
Tag 00JP, a lemma

Tag 00JP in the Stacks Project.

ProjectiveSpectrum.zeroLocus_empty_iff_irrelevant_le_radical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean, line 128. The attribute's comment: “Assertion (10); see the module docstring for the other nine.”. References: EGA II (2.3.16); EGA II (2.3.13), “more general”; EGA II (2.3.2), “V₊(S₊)=∅”; EGA II (8.3.4), “partial”.

The projective zero locus V₊(I) of a homogeneous ideal I of a graded ring A is empty if and only if the irrelevant ideal 𝒜₊ is contained in the radical of I.

theorem zeroLocus_empty_iff_irrelevant_le_radical (I : HomogeneousIdeal 𝒜) :
    zeroLocus 𝒜 (I : Set A) = ∅ ↔ HomogeneousIdeal.irrelevant 𝒜 ≤ I.radical
Tag 00JQ, an example

Tag 00JQ in the Stacks Project.

projToSpec_isHomeomorph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Proj/Defs.lean, line 623. References: EGA II (3.1.7), “partial”.

The natural map Proj(R[X]) → Spec(R) is a bijection and a homeomorphism.

theorem projToSpec_isHomeomorph : IsHomeomorph (projToSpec R)
Tag 00JR, a lemma

Tag 00JR in the Stacks Project.

HomogeneousLocalization.isLocalizedModule_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HomogeneousLocalization/DegreeZero/AtPrime.lean, line 521. The attribute's comment: “The module equality M_(𝔭) = (M_(f))_{𝔭'}; the ring equality S_(𝔭) = (S_(f))_{𝔭'} is AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime.”.

Let A be a graded ring, let M be a graded A-module, let 𝔭 be a homogeneous prime ideal of A, and let f ∈ A be homogeneous of positive degree with f ∉ 𝔭. Let 𝔭' be the prime of the degree-zero localization A⁰_f consisting of the fractions a/fⁿ with a ∈ 𝔭. Then the A⁰_f-module M_(𝔭) of degree-zero fractions y/g with g ∉ 𝔭 homogeneous is the localization of the A⁰_f-module M_(f) of degree-zero fractions y/fⁿ at 𝔭'.

public theorem isLocalizedModule_atPrime {σ τ A M : Type*} [CommRing A] [SetLike σ A]
    [AddSubgroupClass σ A] [AddCommGroup M] [Module A M] [SetLike τ M] [AddSubmonoidClass τ M]
    (𝒜 : ℕ → σ) [GradedRing 𝒜] (ℳ : ℤ → τ) [DirectSum.Decomposition ℳ]
    (hℳ : ∀ (i : ℕ) (j : ℤ) (a : A) (y : M), a ∈ 𝒜 i → y ∈ ℳ j → a • y ∈ ℳ (i + j)) (𝔭 : Ideal A)
    [𝔭.IsPrime] (h𝔭 : 𝔭.IsHomogeneous 𝒜) {f : A} {m : ℕ} (hf : f ∈ 𝒜 m) (hm : 0 < m) (hf𝔭 : f ∉ 𝔭)
    (𝔭' : Ideal (Away 𝒜 f)) [𝔭'.IsPrime]
    (h𝔭' : ∀ z : NumDenSameDeg 𝒜 (Submonoid.powers f), mk z ∈ 𝔭' ↔ (z.num : A) ∈ 𝔭) :
    letI : Module (Away 𝒜 f) (LocalizedModule (Submonoid.powers f) M) :=
      Module.compHom _ (algebraMap (Away 𝒜 f) (Localization (Submonoid.powers f)))
    letI : Module (Away 𝒜 f) (LocalizedModule 𝔭.primeCompl M) :=
      Module.compHom _
        ((algebraMap (AtPrime 𝒜 𝔭) (Localization 𝔭.primeCompl)).comp
          (mapId 𝒜 (Submonoid.powers_le.mpr hf𝔭)))
    ∃ φ :
      ↥(Submodule.span (Away 𝒜 f)
            {z : LocalizedModule (Submonoid.powers f) M |
              ∃ (i : ℕ) (y : M) (g : Submonoid.powers f),
                y ∈ ℳ (i : ℤ) ∧ (g : A) ∈ 𝒜 i ∧ z = .mk y g}) →ₗ[Away 𝒜 f]
        ↥(Submodule.span (Away 𝒜 f)
            {z : LocalizedModule 𝔭.primeCompl M |
              ∃ (i : ℕ) (y : M) (g : 𝔭.primeCompl), y ∈ ℳ (i : ℤ) ∧ (g : A) ∈ 𝒜 i ∧ z = .mk y g}),
      (∀ z,
          (φ z : LocalizedModule 𝔭.primeCompl M) =
            LocalizedModule.liftOfLE _ _ (Submonoid.powers_le.mpr hf𝔭) (z : _)) ∧
        IsLocalizedModule 𝔭'.primeCompl φ
Tag 00JS, a lemma

Tag 00JS in the Stacks Project.

graded_silly, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Proj/PrimeAvoidance.lean, line 255. References: SGA 3 V (7.2), “partial”.

Graded prime avoidance: if p₁, …, p_r are homogeneous prime ideals of a graded ring and I is a homogeneous ideal contained in the irrelevant ideal with ¬ I ≤ pᵢ for every i, then I contains a homogeneous element of positive degree lying outside every pᵢ.

theorem graded_silly
    {r : ℕ} (p : Fin r → HomogeneousIdeal 𝒜) (hp : ∀ i, (p i).toIdeal.IsPrime)
    (I : HomogeneousIdeal 𝒜) (hI : I ≤ HomogeneousIdeal.irrelevant 𝒜)
    (hIp : ∀ i, ¬ I ≤ p i) :
    ∃ x : S, x ∈ I.toIdeal ∧ (∃ d : ℕ, 1 ≤ d ∧ x ∈ 𝒜 d) ∧ ∀ i, x ∉ (p i).toIdeal
Tag 00JT, a lemma

Tag 00JT in the Stacks Project.

Declarations registered for the tag:

Tag 00JU, a lemma

Tag 00JU in the Stacks Project.

Ideal.IsHomogeneous.isHomogeneous_of_mem_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Proj/HomogeneousPrimes.lean, line 65. The attribute's comment: “part (2)”.

Part (2): Given a homogeneous ideal I, any minimal prime over I is homogeneous.

theorem Ideal.IsHomogeneous.isHomogeneous_of_mem_minimalPrimes
    {I p : Ideal A} (hI : I.IsHomogeneous 𝒜) (hp : p ∈ I.minimalPrimes) :
    p.IsHomogeneous 𝒜

GradedRing.isHomogeneous_of_mem_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Proj/HomogeneousPrimes.lean, line 78. The attribute's comment: “part (1)”.

Part (1): Any minimal prime of a graded ring is a homogeneous ideal. This is the special case of part (2) where I = ⊥.

theorem GradedRing.isHomogeneous_of_mem_minimalPrimes
    {p : Ideal A} (hp : p ∈ minimalPrimes A) :
    p.IsHomogeneous 𝒜
Tag 07Z2, a lemma

Tag 07Z2 in the Stacks Project.

homogeneousLocalization_away_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HomogeneousLocalization/DegreeZero/Finiteness.lean, line 43. The attribute's comment: “(1)”.

Tag 07Z2, part 1. Let S be a graded R-algebra of finite type over R, and let f ∈ S_d be homogeneous with d ≥ 1. Then the degree-0 localization S_(f) is of finite type over R (a finitely generated R-algebra).

theorem homogeneousLocalization_away_finiteType (hf : f ∈ 𝒜 d) [Algebra.FiniteType R S] :
    Algebra.FiniteType R (SLoc 𝒜 f)

moduleLocalization_away_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HomogeneousLocalization/DegreeZero/Finiteness.lean, line 716. The attribute's comment: “(2)”.

Tag 07Z2, part 2. Under the same hypotheses, if moreover M is a finite (finitely generated) graded S-module — with grading ℳ satisfying M = ⨁_n ℳ n (DirectSum.Decomposition ℳ) and the compatibility 𝒜 i · ℳ j ⊆ ℳ (i + j) (SetLike.GradedSMul 𝒜 ℳ) — then the degree-0 localization M_(f) is a finite S_(f)-module.

theorem moduleLocalization_away_finite (hf : f ∈ 𝒜 d) (hd : 1 ≤ d) [Algebra.FiniteType R S]
    [Module.Finite S M] : Module.Finite (SLoc 𝒜 f) (MLoc 𝒜 ℳ f d)
Tag 052N, a lemma

Tag 052N in the Stacks Project.

exists_gradedAlgebra_degZeroPart_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/ReesModel.lean, line 2290.

Stacks Tag 052N (Lemma 10.57.10). Let R be a ring, R' a finite type R-algebra, and M a finite R'-module. Then there exist a graded R-algebra S, a graded S-module N, and a degree-1 element f ∈ S₁ such that R' ≅ S_(f) as R-algebras, M ≅ N_(f) as modules (compatibly), S₀ = R, S is generated by finitely many degree-1 elements over R, and N is a finite S-module. Here S_(f) is HomogeneousLocalization.Away 𝒜 f and N_(f) is degZeroPart f N ℬ, the degree-0 part of the localization induced from the grading ℬ.

theorem exists_gradedAlgebra_degZeroPart_equiv
    (R : Type uR) [CommRing R]
    (R' : Type uB) [CommRing R'] [Algebra R R'] [Algebra.FiniteType R R']
    (M : Type uM) [AddCommGroup M] [Module R' M] [Module.Finite R' M] :
    ∃ (S : Type (max uR uB)) (_ : CommRing S) (_ : Algebra R S)
      -- `𝒜` is the family of homogeneous pieces; `GradedAlgebra 𝒜` makes `S` a
      -- graded `R`-algebra graded by `ℕ = ℤ_{≥0}`.
      (𝒜 : ℕ → Submodule R S) (_ : GradedAlgebra 𝒜)
      -- `N` is an `S`-module with `ℤ`-graded homogeneous pieces `ℬ`.
      (N : Type uM) (_ : AddCommGroup N) (_ : Module S N)
      (ℬ : ℤ → AddSubgroup N) (_ : SetLike.GradedSMul 𝒜 ℬ) (_ : DirectSum.Decomposition ℬ)
      -- `f` is homogeneous of degree `1`.
      (f : S) (_ : f ∈ 𝒜 1),
      -- (2) `S₀ = R`: the structure map `R → S` is injective with range `𝒜 0`;
      -- and `S` is generated over `R` by finitely many degree-`1` elements.
      (Function.Injective (algebraMap R S) ∧
        Set.range (algebraMap R S) = (𝒜 0 : Set S)) ∧
      (∃ (gs : Finset S), (∀ g ∈ gs, g ∈ 𝒜 1) ∧
        Algebra.adjoin R (gs : Set S) = ⊤) ∧
      -- (3) `N` is a finite `S`-module.
      Module.Finite S N ∧
      -- (1) `R' ≅ S_(f)` as `R`-algebras and `M ≅ N_(f)` as modules.
      --
      -- `eR` is a ring isomorphism `R' ≃+* S_(f)`; it is an `R`-algebra
      -- isomorphism because it is compatible with the structure maps: the image
      -- of `r : R` in `R'` is sent to the image of `r` in `S_f` (which lies in the
      -- degree-`0` part `S_(f)`).  Since `S₀ = R` by (2), this is exactly the
      -- `R`-algebra compatibility `eR ∘ (R → R') = (R → S_(f))`.
      --
      -- `eM` is an additive isomorphism `M ≃+ N_(f)` to the faithfully-defined
      -- degree-`0` part `N_(f) = degZeroPart f N ℬ`.  It is semilinear over `eR`:
      -- `eM (r • m) = (eR r).val • eM m` inside `N_f`, where `S_(f)` acts via the
      -- embedding `HomogeneousLocalization.val : S_(f) → S_f`.  Together with the
      -- `R`-compatibility of `eR`, this expresses `M ≅ N_(f)` as `R' ≅ S_(f)`-modules.
      (∃ (eR : R' ≃+* HomogeneousLocalization.Away 𝒜 f)
         (eM : M ≃+ (degZeroPart f N ℬ)),
         (∀ r : R, (eR (algebraMap R R' r)).val
            = algebraMap S (Localization (Submonoid.powers f)) (algebraMap R S r)) ∧
         (∀ (r : R') (m : M),
           (eM (r • m) : LocalizedModule (Submonoid.powers f) N)
             = (eR r).val • (eM m : LocalizedModule (Submonoid.powers f) N)))
Sources
LeanProj · gradedPrimesComparison_isHomeomorph · ProjectiveSpectrum.zeroLocus_empty_iff_irrelevant_le_radical · projToSpec_isHomeomorph · HomogeneousLocalization.isLocalizedModule_atPrime · graded_silly · Ideal.IsPrime.homogeneousCore · Ideal.homogeneousCore

Section10.58 Noetherian graded rings#

Section 10.58 of the Stacks Project, Tag 00JV. 8 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07Z4, a lemma

Tag 07Z4 in the Stacks Project.

generates_algebra_iff_generates_irrelevant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/FinitelyGenerated.lean, line 459. References: EGA II (2.1.3); EGA II (2.1.4), “partial”.

Stacks Tag 07Z4: for a family (f i) of homogeneous elements of strictly positive degree in a graded ring A with grading 𝒜 (the GradedRing 𝒜 hypothesis, together with the explicit DirectSum.Decomposition 𝒜, encodes the direct-sum decomposition A = ⨁_d 𝒜 d), the family generates A as an algebra over the degree-zero subring 𝒜 0 if and only if it generates the irrelevant ideal S₊ as an ideal of A.

theorem generates_algebra_iff_generates_irrelevant
    {I : Type*} (f : I → A) (d : I → ℕ)
    (hd : ∀ i, 0 < d i) (hf : ∀ i, f i ∈ 𝒜 (d i)) :
    Algebra.adjoin ↥(𝒜 0) (Set.range f) = ⊤ ↔
    Ideal.span (Set.range f) = (HomogeneousIdeal.irrelevant 𝒜).toIdeal
Tag 00JW, a lemma

Tag 00JW in the Stacks Project.

GradedRing.isNoetherianRing_iff_isNoetherianRing_gradeZero_and_irrelevant_fg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Noetherian.lean, line 284. References: EGA II (2.1.5), “necessity”.

A graded ring A = ⨁_d 𝒜 d is Noetherian if and only if its degree-zero subring 𝒜 0 is a Noetherian ring and its irrelevant ideal ⨁_{d > 0} 𝒜 d is finitely generated as an ideal of A.

public theorem isNoetherianRing_iff_isNoetherianRing_gradeZero_and_irrelevant_fg
    (𝒜 : ℕ → σ) [GradedRing 𝒜] :
    IsNoetherianRing A ↔
      IsNoetherianRing (𝒜 0) ∧ (HomogeneousIdeal.irrelevant 𝒜).toIdeal.FG
Tag 00JX, a definition

Tag 00JX in the Stacks Project.

IsNumericalPolynomial, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NumericalPolynomial.lean, line 68.

A function f : ℤ → A (with A an additive abelian group) is a numerical polynomial if there exist r : ℕ and elements a : Fin (r + 1) → A such that f n = ∑_{i = 0}^{r} (n choose i) • a i holds for all sufficiently large integers n.

def IsNumericalPolynomial (f : ℤ → A) : Prop
Tag 00JY, a lemma

Tag 00JY in the Stacks Project.

numerical_polynomial_functorial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NumericalPolynomial.lean, line 113.

Numerical polynomials are functorial: if φ : A →+ A' is a homomorphism of abelian groups and f : ℤ → A is a numerical polynomial, then n ↦ φ (f n) is a numerical polynomial valued in A'.

theorem numerical_polynomial_functorial
    {A A' : Type*} [AddCommGroup A] [AddCommGroup A']
    (φ : A →+ A') (f : ℤ → A) (hf : IsNumericalPolynomial f) :
    IsNumericalPolynomial (fun n => φ (f n))
Tag 00JZ, a lemma

Tag 00JZ in the Stacks Project.

main_00JZ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NumericalPolynomial.lean, line 221.

Let A be an abelian group and f : ℤ → A. If the backward difference n ↦ f n - f (n - 1) is a numerical polynomial, then so is f.

theorem main_00JZ {A : Type*} [AddCommGroup A] (f : ℤ → A)
    (hdiff : IsNumericalPolynomial (fun n => f n - f (n - 1))) :
    IsNumericalPolynomial f
Tag 00K0, a lemma

Tag 00K0 in the Stacks Project.

graded_module_pieces_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/FinitelyGenerated.lean, line 266. References: EGA II (2.1.6), “(i)”.

Stacks 00K0. Let S = ⨁_{n ≥ 0} 𝒜 n be a graded ring and M = ⨁_{n ∈ ℤ} ℳ n a graded S-module, with S_d · M_e ⊆ M_{d+e}. If M is finitely generated as an S-module and S is finitely generated as an 𝒜 0-algebra, then every graded piece ℳ n is a finite 𝒜 0-module.

theorem graded_module_pieces_finite (ℳ : ℤ → Submodule (𝒜 0) M) [DirectSum.Decomposition ℳ]
    (hsmul : ∀ (d : ℕ) (e : ℤ) (s : S), s ∈ 𝒜 d → ∀ m : M, m ∈ ℳ e → s • m ∈ ℳ ((d : ℤ) + e))
    (hM : Module.Finite S M)
    (hS : Algebra.FiniteType (𝒜 0) S) : ∀ n : ℤ, Module.Finite (𝒜 0) (ℳ n)
Tag 00K1, a proposition

Tag 00K1 in the Stacks Project.

hilbertFun_isNumericalPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertFunction/Polynomiality.lean, line 741.

Main statement (Stacks Tag 00K1, Proposition 10.58.7). Let S be a Noetherian graded ring with degree-zero ring S_0 = ↥(𝒮 0), graded nonnegatively (𝒮 d = 0 for d < 0), and let M be a finite graded S-module. Assume the irrelevant ideal S_+ is generated by elements of degree 1 (GeneratedInDegreeOne 𝒮). Then the Hilbert function n ↦ [M_n] ∈ K'_0(S_0) is a numerical polynomial.

theorem hilbertFun_isNumericalPolynomial (hneg : ∀ d : ℤ, d < 0 → 𝒮 d = ⊥)
    (hgen : GeneratedInDegreeOne 𝒮) : IsEventualNumericalPolynomial (hilbertFun 𝒮 ℳ hneg)
Tag 00K3, a lemma

Tag 00K3 in the Stacks Project.

Stacks.HilbertFunction.PolynomialQuotient.hilbertFunction_degree_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertFunction/DegreeBound.lean, line 605.

Main Theorem (Stacks Lemma 10.58.10, Tag 00K3). Let k be a field, d ≥ 1, and S = k[X_1, …, X_d] with the standard grading. Let I ⊆ S be a nonzero graded ideal and set M = S / I. Then the Hilbert function H_M(n) = dim_k(M_n) is, for large n, given by a rational polynomial P whose degree is strictly less than d - 1.

Concretely: there exist P ∈ ℚ[T] with deg P < d - 1 and an integer N such that dim_k(M_n) = P(n) for all n ≥ N. The degree bound deg P < d - 1 is expressed using Polynomial.degree : ℚ[X] → WithBot ℕ, which sends the zero polynomial to ⊥; thus deg P < d - 1 automatically allows P = 0 (the case -∞ < d - 1), and when d = 1 it forces P = 0.

theorem hilbertFunction_degree_lt (hd : 1 ≤ d) (I : Ideal (MvPolynomial (Fin d) k))
    (hI_hom : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin d) k) I)
    (hI_ne : I ≠ ⊥) :
    ∃ (P : Polynomial ℚ) (N : ℕ),
      P.degree < ((d - 1 : ℕ) : WithBot ℕ) ∧
        ∀ n : ℕ, N ≤ n → (hilbertFunction I n : ℚ) = P.eval (n : ℚ)
Sources
Leangenerates_algebra_iff_generates_irrelevant · GradedRing.isNoetherianRing_iff_isNoetherianRing_gradeZero_and_irrelevant_fg · IsNumericalPolynomial · numerical_polynomial_functorial · main_00JZ · graded_module_pieces_finite · hilbertFun_isNumericalPolynomial · Stacks.HilbertFunction.PolynomialQuotient.hilbertFunction_degree_lt

Section10.59 Noetherian local rings#

Section 10.59 of the Stacks Project, Tag 00K4. 10 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07DU, a definition

Tag 07DU in the Stacks Project.

IsIdealOfDefinition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertSamuel/Defs.lean, line 161. References: EGA 0 (16.2.1); EGA 0 (7.1.2), “special case”; EGA III (4.3.13); EGA IV (21.13.12.1); EGA IV (6.1.3); SGA 1 I (2.1).

An ideal I of a Noetherian local ring (R, m) is an ideal of definition if its radical is the maximal ideal, i.e. √I = m.

def IsIdealOfDefinition {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (I : Ideal R) : Prop
Tag 00K5, a lemma

Tag 00K5 in the Stacks Project.

chi_bounds_of_quotient_finiteLength, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertSamuel/Function.lean, line 182.

Let (R, m, k) be a Noetherian local ring, I ⊆ R an ideal of definition, and M' ⊆ M finite R-modules with M / M' of finite length. Then there are constants c₁, c₂ ∈ ℕ such that for all n ≥ c₂, c₁ + χ_{I,M'}(n - c₂) ≤ χ_{I,M}(n) ≤ c₁ + χ_{I,M'}(n).

theorem chi_bounds_of_quotient_finiteLength
    {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (I : Ideal R) (hI : IsIdealOfDefinition I)
    {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M]
    (M' : Submodule R M) (hlen : Module.length R (M ⧸ M') < ⊤) :
    ∃ c₁ c₂ : ℕ, ∀ n : ℕ, c₂ ≤ n →
      (c₁ : ℕ∞) + chi I M' (n - c₂) ≤ chi I M n ∧
      chi I M n ≤ (c₁ : ℕ∞) + chi I M' n
Tag 00K6, a lemma

Tag 00K6 in the Stacks Project.

additivity_of_characteristic_and_hilbert_functions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertSamuel/Function.lean, line 404.

Given a short exact sequence 0 → M' → M → M'' → 0 of finite R-modules over a Noetherian local ring (R, m) and an ideal I with √I = m, there are a submodule N ⊆ M' of finite colength l = length_R (M'/N) and an integer c ≥ 0 such that for all n ≥ c χ_{I,M}(n) = χ_{I,M''}(n) + χ_{I,N}(n - c) + l and φ_{I,M}(n) = φ_{I,M''}(n) + φ_{I,N}(n - c).

theorem additivity_of_characteristic_and_hilbert_functions
    (R : Type*) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (I : Ideal R) (hI : I.radical = IsLocalRing.maximalIdeal R)
    (M' M M'' : Type*)
    [AddCommGroup M'] [Module R M'] [Module.Finite R M']
    [AddCommGroup M] [Module R M] [Module.Finite R M]
    [AddCommGroup M''] [Module R M''] [Module.Finite R M'']
    (f : M' →ₗ[R] M) (g : M →ₗ[R] M'')
    (hf : Function.Injective f) (hg : Function.Surjective g)
    (hfg : Function.Exact f g) :
    ∃ (N : Submodule R M') (c : ℕ) (l : ℕ),
      Module.length R (M' ⧸ N) = (l : ℕ∞) ∧
      (∀ n ≥ c, charFn R I M n = charFn R I M'' n + charFn R I N (n - c) + (l : ℕ∞)) ∧
      (∀ n ≥ c, hilbertFn R I M n = hilbertFn R I M'' n + hilbertFn R I N (n - c))
Tag 00K7, a lemma

Tag 00K7 in the Stacks Project.

chi_change_ideal_of_definition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertSamuel/Defs.lean, line 124.

Let (R, m) be a Noetherian local ring, let I, I' be two ideals of definition of R, and let M be a finite R-module. Then there exists a positive integer a such that χ_{I,M}(n) ≤ χ_{I',M}(a·n) for all n ≥ 1.

theorem chi_change_ideal_of_definition
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (I I' : Ideal R) (hI : IsIdealOfDefinition' I) (hI' : IsIdealOfDefinition' I') :
    ∃ a : ℕ, 0 < a ∧ ∀ n : ℕ, 1 ≤ n → hilbertSamuel_chi I M n ≤ hilbertSamuel_chi I' M (a * n)
Tag 00K8, a proposition

Tag 00K8 in the Stacks Project.

Ideal.exists_eventually_length_quotient_smul_pow_eq_sum_choose_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertFunction/Numerical.lean, line 1207. References: EGA 0 (16.2.1), “local case”.

Stacks 00K8. Let R be a Noetherian local ring, let I ⊆ R be an ideal of definition (I.radical is the maximal ideal of R) and let M be a finite R-module. Then the Hilbert function n ↦ length_R (I ^ n • M / I ^ (n + 1) • M) and the function n ↦ length_R (M / I ^ (n + 1) • M) are numerical polynomials: each takes finite values which, for all n ≫ 0, are given by a ℤ-linear combination of the binomial coefficients n choose 0, …, n choose r.

public theorem Ideal.exists_eventually_length_quotient_smul_pow_eq_sum_choose_mul
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (I : Ideal R)
    (hI : I.radical = IsLocalRing.maximalIdeal R)
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    ∃ (r : ℕ) (a b : ℕ → ℤ), ∀ᶠ n : ℕ in Filter.atTop,
      (∃ p : ℕ, Module.length R (↥(I ^ n • (⊤ : Submodule R M)) ⧸
            (I ^ (n + 1) • (⊤ : Submodule R M)).submoduleOf (I ^ n • ⊤)) = p ∧
          (p : ℤ) = ∑ i ∈ Finset.range (r + 1), (n.choose i : ℤ) * a i) ∧
      (∃ q : ℕ, Module.length R (M ⧸ (I ^ (n + 1) • (⊤ : Submodule R M))) = q ∧
          (q : ℤ) = ∑ i ∈ Finset.range (r + 1), (n.choose i : ℤ) * b i)
Tag 09CA, a definition

Tag 09CA in the Stacks Project.

Ideal.hilbertPolynomial, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertFunction/Defs.lean, line 132. The attribute's comment: “Stated relative to an ideal I ⊆ R, as the rest of the section is (Tags 00K8, 00K9, 00KA); the Hilbert polynomial of Definition 09CA is the case I = IsLocalRing.maximalIdeal R, for R Noetherian local and M finite, where Proposition 00K8 makes the characterising property satisfiable. The property is what the definition consumes, and it determines the polynomial uniquely; the value is 0 where nothing has it.”.

Stacks 09CA. The Hilbert polynomial of an R-module M relative to an ideal I ⊆ R: the polynomial P ∈ ℚ[t] such that P(n) = φ_{I,M}(n) = length_R (I ^ n M / I ^ (n + 1) M) for all n ≫ 0. At most one polynomial has this property, so this is a definition of that element; the value is 0 in the case that none has it. For R Noetherian local, M finite and I an ideal of definition — in particular for I = m, the Hilbert polynomial of M over R — such a P exists by Proposition 00K8.

public noncomputable def Ideal.hilbertPolynomial {R : Type*} [CommRing R] (I : Ideal R)
    (M : Type*) [AddCommGroup M] [Module R M] : ℚ[X]
Tag 00K9, a lemma

Tag 00K9 in the Stacks Project.

Ideal.exists_degree_eq_of_eventually_eval_eq_length_quotient_smul_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertSamuel/DegreeInvariance.lean, line 289. The attribute's comment: “The degree of a numerical polynomial is spelled as the degree of any rational polynomial computing it at all large n, and independence of I as the two degrees being quantified outside the ideal of definition. Part (1) of the tag is the first conjunct, part (2) the second.”. References: EGA 0 (16.2.3), “special case”.

Stacks 00K9. Let R be a Noetherian local ring and let M be a finite R-module. Then there are d e : WithBot ℕ, depending on R and M only, such that for every ideal of definition I ⊆ R (that is, I.radical = m): every polynomial P ∈ ℚ[t] agreeing with the Hilbert function φ_{I,M}(n) = length_R (I ^ n M / I ^ (n + 1) M) for all n ≫ 0 has degree d, and every polynomial P ∈ ℚ[t] agreeing with χ_{I,M}(n) = length_R (M / I ^ (n + 1) M) for all n ≫ 0 has degree e. That is, the degrees of the numerical polynomials φ_{I,M} and χ_{I,M} are independent of the ideal of definition I.

public theorem Ideal.exists_degree_eq_of_eventually_eval_eq_length_quotient_smul_pow
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    ∃ d e : WithBot ℕ, ∀ I : Ideal R, I.radical = maximalIdeal R → ∀ P : ℚ[X],
      ((∀ᶠ n : ℕ in atTop, ∃ p : ℕ,
            Module.length R (↥(I ^ n • (⊤ : Submodule R M)) ⧸
              (I ^ (n + 1) • (⊤ : Submodule R M)).submoduleOf (I ^ n • ⊤)) = p ∧
            P.eval (n : ℚ) = (p : ℚ)) → P.degree = d) ∧
      ((∀ᶠ n : ℕ in atTop, ∃ q : ℕ,
            Module.length R (M ⧸ (I ^ (n + 1) • (⊤ : Submodule R M))) = q ∧
            P.eval (n : ℚ) = (q : ℚ)) → P.degree = e)
Tag 00KA, a definition

Tag 00KA in the Stacks Project.

Ideal.hilbertSamuelDegree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertSamuel/Defs.lean, line 79. The attribute's comment: “Definition 00KA is the case I = maximalIdeal R, spelled Module.hilbertSamuelDegree. The definition is stated for an arbitrary ideal because that is the generality of the surrounding section, and because Lemma 00K9(2) is the assertion that this value is the same for all ideals of definition.”. References: EGA 0 (16.2.3).

The degree, an element of {-∞, 0, 1, 2, …} = WithBot ℕ, of the numerical polynomial χ_{I,M}(n) = length_R (M / I ^ (n + 1) M): the degree of a polynomial P ∈ ℚ[t] with P(n) = χ_{I,M}(n) for all n ≫ 0, and -∞ if there is no such polynomial.

public noncomputable def Ideal.hilbertSamuelDegree {R : Type*} [CommRing R] (I : Ideal R)
    (M : Type*) [AddCommGroup M] [Module R M] : WithBot ℕ

Module.hilbertSamuelDegree, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertSamuel/Defs.lean, line 93. The attribute's comment: “The d(M) of the definition. Case (1) is not a separate branch: for M = 0 the polynomial computing χ_M is 0, whose degree is -∞ = ⊥, and conversely a computing polynomial of degree -∞ forces M = m ^ n M for n ≫ 0, hence M = 0 by Nakayama. See the module docstring.”. References: EGA 0 (16.2.3), “special case”.

The invariant d(M) ∈ {-∞, 0, 1, 2, …} = WithBot ℕ of a module M over a local ring (R, m): the degree of the numerical polynomial χ_M(n) = length_R (M / m ^ (n + 1) M), that is Ideal.hilbertSamuelDegree at the maximal ideal.

public noncomputable abbrev Module.hilbertSamuelDegree (R : Type*) [CommRing R] [IsLocalRing R]
    (M : Type*) [AddCommGroup M] [Module R M] : WithBot ℕ
Tag 00KB, a lemma

Tag 00KB in the Stacks Project.

HilbertSamuel.degree_sub_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertSamuel/Function.lean, line 787. References: EGA 0 (16.2.2.2), “special case”.

Let (R, m) be a Noetherian local ring, I ⊆ R an ideal of definition, and M a finite R-module which does not have finite length. Let M' ⊆ M be a submodule with finite colength, and let χ_{I,M}, χ_{I,M'} ∈ Q[t] be the Hilbert–Samuel polynomials of M and M'. Then the difference χ_{I,M} - χ_{I,M'} has degree strictly less than the degree of each of the two Hilbert–Samuel polynomials.

theorem degree_sub_lt
    [IsNoetherianRing R] [IsLocalRing R]
    (I : Ideal R) (hI : IsIdealOfDefinition I)
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (hM : ¬ HasFiniteLength R M)
    (M' : Submodule R M) (hM' : HasFiniteColength M')
    (χM χM' : ℚ[X])
    (hχM : IsHilbertSamuelPoly I M χM)
    (hχM' : IsHilbertSamuelPoly I (↥M') χM') :
    (χM - χM').degree < χM.degree ∧ (χM - χM').degree < χM'.degree
Tag 00KC, a lemma

Tag 00KC in the Stacks Project.

Ideal.max_degree_eq_degree_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertSamuel/ShortExact.lean, line 549. The attribute's comment: “The first conjunct is parts (1) and (2) of the tag, for polynomials computing the three Hilbert–Samuel functions as in Tags 00K8 and 00K9, so χ_{I,M} - χ_{I,M''} - χ_{I,M'} is P - P'' - P'; that this is again a numerical polynomial is inherited from the hypotheses on the three polynomials, and the degree bound is the content. The second conjunct is part (2) for the invariant of Definition 00KA, and part (3) of the tag is its case I = maximalIdeal R. See the module docstring.”. References: EGA 0 (16.2.2.2), “(1) deg bound, (2)”.

Stacks 00KC. Let R be a Noetherian local ring, let I ⊆ R be an ideal of definition (I.radical is the maximal ideal of R) and let 0 → M' → M → M'' → 0 be a short exact sequence of finite R-modules, given by f : M' →ₗ[R] M injective, g : M →ₗ[R] M'' surjective and Function.Exact f g. Then

  1. if M' does not have finite length, then χ_{I,M} - χ_{I,M''} - χ_{I,M'} is a numerical polynomial of degree < the degree of χ_{I,M'},
  2. max {deg χ_{I,M'}, deg χ_{I,M''}} = deg χ_{I,M}, and
  3. max {d(M'), d(M'')} = d(M), for the invariant d(-) of Definition 00KA — the case I = m of the last conjunct, since d(N) = (maximalIdeal R).hilbertSamuelDegree N.

Here P', P, P'' are the numerical polynomials χ_{I,M'}, χ_{I,M}, χ_{I,M''}, that is, the polynomials with P'(n) = length_R (M' / I ^ (n + 1) M') for all n ≫ 0 and likewise for M and M'', and Ideal.hilbertSamuelDegree I N is the degree of χ_{I,N}.

public theorem Ideal.max_degree_eq_degree_of_exact
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (I : Ideal R) (hI : I.radical = maximalIdeal R)
    {M' M M'' : Type*} [AddCommGroup M'] [Module R M'] [Module.Finite R M']
    [AddCommGroup M] [Module R M] [Module.Finite R M]
    [AddCommGroup M''] [Module R M''] [Module.Finite R M'']
    {f : M' →ₗ[R] M} {g : M →ₗ[R] M''} (hfg : Function.Exact f g)
    (hf : Function.Injective f) (hg : Function.Surjective g) :
    (∀ P' P P'' : ℚ[X],
      (∀ᶠ n : ℕ in atTop, ∃ p : ℕ,
          Module.length R (M' ⧸ (I ^ (n + 1) • (⊤ : Submodule R M'))) = p ∧
            P'.eval (n : ℚ) = (p : ℚ)) →
        (∀ᶠ n : ℕ in atTop, ∃ p : ℕ,
          Module.length R (M ⧸ (I ^ (n + 1) • (⊤ : Submodule R M))) = p ∧
            P.eval (n : ℚ) = (p : ℚ)) →
        (∀ᶠ n : ℕ in atTop, ∃ p : ℕ,
          Module.length R (M'' ⧸ (I ^ (n + 1) • (⊤ : Submodule R M''))) = p ∧
            P''.eval (n : ℚ) = (p : ℚ)) →
        (¬ IsFiniteLength R M' → (P - P'' - P').degree < P'.degree) ∧
          max P'.degree P''.degree = P.degree) ∧
      max (I.hilbertSamuelDegree M') (I.hilbertSamuelDegree M'') =
        I.hilbertSamuelDegree M
Sources
LeanIsIdealOfDefinition · chi_bounds_of_quotient_finiteLength · additivity_of_characteristic_and_hilbert_functions · chi_change_ideal_of_definition · Ideal.exists_eventually_length_quotient_smul_pow_eq_sum_choose_mul · Ideal.hilbertPolynomial · Ideal.exists_degree_eq_of_eventually_eval_eq_length_quotient_smul_pow · Ideal.hilbertSamuelDegree

Section10.60 Dimension#

Section 10.60 of the Stacks Project, Tag 00KD. 13 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 6 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GIE, a definition

Tag 0GIE in the Stacks Project.

Declarations registered for the tag:

Tag 00KE, a definition

Tag 00KE in the Stacks Project.

Declarations registered for the tag:

Tag 00KF, a definition

Tag 00KF in the Stacks Project.

Declarations registered for the tag:

Tag 00KG, a lemma

Tag 00KG in the Stacks Project.

ringKrullDim_eq_iSup_height, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/Defs.lean, line 28.

The Krull dimension of R equals the supremum of the heights of its prime ideals.

theorem ringKrullDim_eq_iSup_height (R : Type*) [CommRing R] :
    ringKrullDim R = ⨆ (I : PrimeSpectrum R), (I.asIdeal.height : WithBot ℕ∞)

ringKrullDim_eq_iSup_height_maximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/Defs.lean, line 35.

The Krull dimension of R equals the supremum of the heights of its maximal ideals.

theorem ringKrullDim_eq_iSup_height_maximal (R : Type*) [CommRing R] :
    ringKrullDim R =
      ⨆ (I : {I : PrimeSpectrum R // I.asIdeal.IsMaximal}),
        (I.val.asIdeal.height : WithBot ℕ∞)
Tag 00KI, a lemma

Tag 00KI in the Stacks Project.

IsLocalRing.ringKrullDim_eq_zero_iff_hilbertSamuelDegree_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/DimensionOneNoetherianLocal.lean, line 123. The attribute's comment: “The source reads this off from d(R) = 0 if and only if R has finite length; here it is read off from d(M) = dim Supp(M) (Lemma 00L8) for M = R.”.

A Noetherian local ring has dimension zero exactly when its Hilbert–Samuel degree d(R) is zero.

theorem ringKrullDim_eq_zero_iff_hilbertSamuelDegree_eq_zero :
    ringKrullDim R = 0 ↔ Module.hilbertSamuelDegree R R = 0

Declarations registered for the tag:

Tag 00KJ, a proposition

Tag 00KJ in the Stacks Project.

isArtinianRing_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Artinian/TFAE.lean, line 272. The attribute's comment: “Items (1)-(10); see the module docstring for the form of (2), (5), (6) and (7).”. References: EGA 0 (14.1.9), “affine case: X = Spec R”; EGA 0 (16.1.10), “case M = A”; EGA I (6.2.2), “affine case”; EGA IV (10.4.3), “partial”; SGA 3 VIIB (0.1.1), “partial”; SGA 3 VIIB (3.2), “U = C”.

Characterizations of Artinian rings. For a commutative ring R the following are equivalent: R is Artinian; R is Noetherian of Krull dimension zero; R has finite length as a module over itself; R is a finite product of Artinian local rings; R is Noetherian with discrete prime spectrum; R is a finite product of Noetherian local rings of dimension zero; R is a finite product of Noetherian local rings of finite length; R is a finite product of Noetherian local rings with nilpotent maximal ideal; R is Noetherian with finitely many maximal ideals and nilpotent Jacobson radical; and R is Noetherian with no strict inclusions among its primes.

public theorem isArtinianRing_tfae (R : Type u) [CommRing R] :
    List.TFAE
      [ IsArtinianRing R,
        IsNoetherianRing R ∧ Ring.KrullDimLE 0 R,
        IsFiniteLength R R,
        ∃ (ι : Type u) (_ : Finite ι) (S : ι → Type u) (_ : ∀ i, CommRing (S i))
          (_ : ∀ i, IsLocalRing (S i)), (∀ i, IsArtinianRing (S i)) ∧ Nonempty (R ≃+* ∀ i, S i),
        IsNoetherianRing R ∧ DiscreteTopology (PrimeSpectrum R),
        ∃ (ι : Type u) (_ : Finite ι) (S : ι → Type u) (_ : ∀ i, CommRing (S i))
          (_ : ∀ i, IsLocalRing (S i)), (∀ i, IsNoetherianRing (S i) ∧ Ring.KrullDimLE 0 (S i)) ∧
            Nonempty (R ≃+* ∀ i, S i),
        ∃ (ι : Type u) (_ : Finite ι) (S : ι → Type u) (_ : ∀ i, CommRing (S i))
          (_ : ∀ i, IsLocalRing (S i)), (∀ i, IsFiniteLength (S i) (S i)) ∧
            Nonempty (R ≃+* ∀ i, S i),
        ∃ (ι : Type u) (_ : Finite ι) (S : ι → Type u) (_ : ∀ i, CommRing (S i))
          (_ : ∀ i, IsLocalRing (S i)),
          (∀ i, IsNoetherianRing (S i) ∧ IsNilpotent (IsLocalRing.maximalIdeal (S i))) ∧
            Nonempty (R ≃+* ∀ i, S i),
        IsNoetherianRing R ∧ Finite (MaximalSpectrum R) ∧ IsNilpotent (Ring.jacobson R),
        IsNoetherianRing R ∧ ∀ p q : Ideal R, p.IsPrime → q.IsPrime → p ≤ q → p = q ]
Tag 00KK, a lemma

Tag 00KK in the Stacks Project.

IsLocalRing.ringKrullDim_eq_one_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/DimensionOneNoetherianLocal.lean, line 134. The attribute's comment: “Items (1)-(5), in the source's order. The ideal generated by zero elements is ⊥; an ideal of definition is an ideal with radical m.”. References: EGA IV (5.1.6), “special case”.

Noetherian local rings of dimension one. For a Noetherian local ring (R, m) the following are equivalent: dim(R) = 1; d(R) = 1; there is a non-nilpotent x ∈ m with V(x) = {m}; there is a non-nilpotent x ∈ m with m = √(x); some ideal of definition is generated by one element, and the ideal (0) generated by zero elements is not an ideal of definition.

theorem ringKrullDim_eq_one_tfae :
    List.TFAE
      [ringKrullDim R = 1,
        Module.hilbertSamuelDegree R R = 1,
        ∃ x ∈ maximalIdeal R, ¬ IsNilpotent x ∧ zeroLocus {x} = {closedPoint R},
        ∃ x ∈ maximalIdeal R, ¬ IsNilpotent x ∧ (Ideal.span {x}).radical = maximalIdeal R,
        (∃ x : R, (Ideal.span {x}).radical = maximalIdeal R) ∧
          (⊥ : Ideal R).radical ≠ maximalIdeal R]
Tag 00KQ, a proposition

Tag 00KQ in the Stacks Project.

IsLocalRing.ringKrullDim_eq_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertSamuel/DimensionTheorem.lean, line 1000. The attribute's comment: “Items (1)-(3); see the module docstring for the form of (2) and (3).”. References: EGA 0 (16.2.5), “local case”; EGA 0 (16.2.5), “local case”; EGA IV (5.1.6).

Dimension of a Noetherian local ring. For a Noetherian local ring (R, m) and a natural number d the following are equivalent: dim(R) = d; the Hilbert–Samuel function n ↦ length_R (R / m ^ (n + 1)) is eventually a ℤ-combination ∑_{i ≤ d} (n choose i) * a i of binomial coefficients with a d ≠ 0, i.e. d(R) = d; and d is the least number of generators of an ideal of definition of R, i.e. some ideal of definition is generated by d elements and none is generated by fewer.

public theorem IsLocalRing.ringKrullDim_eq_tfae {R : Type*} [CommRing R] [IsNoetherianRing R]
    [IsLocalRing R] (d : ℕ) :
    List.TFAE
      [ringKrullDim R = d,
        ∃ a : ℕ → ℤ,
          a d ≠ 0 ∧
            ∀ᶠ n : ℕ in Filter.atTop,
              ∃ p : ℕ,
                Module.length R (R ⧸ maximalIdeal R ^ (n + 1)) = p ∧
                  (p : ℤ) = ∑ i ∈ Finset.range (d + 1), (n.choose i : ℤ) * a i,
        IsLeast {n : ℕ | ∃ I : Ideal R, I.radical = maximalIdeal R ∧ I.spanFinrank = n} d]
Tag 00KU, a definition

Tag 00KU in the Stacks Project.

IsLocalRing.IsSystemOfParameters, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/SystemOfParameters/Defs.lean, line 116. The attribute's comment: “Item (1). Item (2)'s predicate on the ring is Mathlib's IsRegularLocalRing, tagged 00KU there; a regular system of parameters is Ideal.ofList rs = maximalIdeal R together with ringKrullDim R = rs.length, a composite for which no name is introduced. See the module docstring.”. References: EGA 0 (16.3.6), “case M = R, local”.

System of parameters of a local ring. A sequence rs of elements of a local ring (R, m) is a system of parameters of R if it generates an ideal of definition of R, that is an ideal with radical m, and has dim R entries. Over a Noetherian local ring this is the source's notion: dim R elements of m generating an ideal of definition, dim R being the least number of generators an ideal of definition can have. A regular system of parameters is one generating m itself; the rings admitting one are the regular local rings, IsRegularLocalRing.

public def IsLocalRing.IsSystemOfParameters {R : Type*} [CommRing R] [IsLocalRing R]
    (rs : List R) : Prop
Tag 00KV, a lemma

Tag 00KV in the Stacks Project.

Ideal.not_lt_of_lt_of_mem_minimalPrimes_sup_span_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/KrullsHeightTheorem.lean, line 321. The attribute's comment: “Item (2); item (1) is Mathlib's Krull principal ideal theorem.”.

Krull's principal ideal theorem, chain form. Let R be a Noetherian ring, x : R, and let p be a prime ideal. If a prime q is minimal over p + (x), then no prime r lies strictly between p and q.

public theorem Ideal.not_lt_of_lt_of_mem_minimalPrimes_sup_span_singleton {R : Type*}
    [CommRing R] [IsNoetherianRing R] {x : R} {p q r : Ideal R} [p.IsPrime] [r.IsPrime]
    (hq : q ∈ (p ⊔ Ideal.span {x}).minimalPrimes) (hpr : p < r) : ¬r < q
Tag 0BBZ, a lemma

Tag 0BBZ in the Stacks Project.

Ideal.map_height_le_spanRank_toENat_of_mem_minimalPrimes_sup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/KrullsHeightTheorem.lean, line 180. The attribute's comment: “Item (2), for an arbitrary ideal in place of the prime; item (1) is Mathlib's Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes.”. References: EGA 0 (16.3.1), “b ⇒ a”; EGA 0 (16.3.2), “more general”.

Stacks 0BBZ (2), Krull's height theorem in relative form. Let R be a Noetherian ring and let I, J be ideals of R. If a prime q is minimal over I + J, then the height of q / I in R / I is at most the minimal number of generators of J; equivalently, every chain of primes between I and q has length at most that number.

public theorem Ideal.map_height_le_spanRank_toENat_of_mem_minimalPrimes_sup {R : Type*}
    [CommRing R] [IsNoetherianRing R] {I J q : Ideal R} (hq : q ∈ (I ⊔ J).minimalPrimes) :
    (q.map (Ideal.Quotient.mk I)).height ≤ J.spanRank.toENat
Tag 00KW, a lemma

Tag 00KW in the Stacks Project.

Ideal.height_le_height_map_add_encard_of_span_eq_ker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/AffineIntersection.lean, line 86. The attribute's comment: “through a surjection”.

Krull's height theorem through a surjection. If δ is a surjective ring map whose kernel is generated by a set s, and M is a prime containing s, then the height of M is at most the height of its image plus the cardinality of s. This is the iterated form of Stacks Tag 00KW that the reduction to the diagonal consumes.

theorem Ideal.height_le_height_map_add_encard_of_span_eq_ker {T C : Type*} [CommRing T]
    [CommRing C] [IsNoetherianRing T] (δ : T →+* C) (hδ : Function.Surjective δ) (s : Set T)
    (hspan : Ideal.span s = RingHom.ker δ) (M : Ideal T) [M.IsPrime] (hsM : s ⊆ M) :
    M.height ≤ (M.map δ).height + s.encard
Tag 02IE, a lemma

Tag 02IE in the Stacks Project.

ringKrullDim_add_length_eq_ringKrullDim_of_radical_ofList_append_eq_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/SystemOfParameters.lean, line 247. References: EGA 0 (16.2.3.1), “(ii), special case”.

Dimension of a quotient by part of a system of parameters. Let (R, m) be a Noetherian local ring and let x₁, …, x_d ∈ m generate an ideal of definition of R, with d ≤ dim R — equivalently, x₁, …, x_d is a system of parameters. Then killing any part l of the sequence drops the dimension by exactly the number of elements killed: dim R/(l) + |l| = dim R. Taking l to be the prefix x₁, …, x_i gives dim R/(x₁, …, x_i) = d - i.

public theorem ringKrullDim_add_length_eq_ringKrullDim_of_radical_ofList_append_eq_maximalIdeal
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (l l' : List R)
    (hdef : (Ideal.ofList (l ++ l')).radical = IsLocalRing.maximalIdeal R)
    (hdim : ((l.length + l'.length : ℕ) : WithBot ℕ∞) ≤ ringKrullDim R) :
    ringKrullDim (R ⧸ Ideal.ofList l) + l.length =
      ringKrullDim R
Sources
LeanLTSeries.mk · RelSeries.length · ringKrullDim · IsLocalization.AtPrime.ringKrullDim_eq_height · ringKrullDim_eq_iSup_height · ringKrullDim_eq_iSup_height_maximal · IsLocalRing.ringKrullDim_eq_zero_iff_hilbertSamuelDegree_eq_zero · isArtinianRing_iff_krullDimLE_zero

Section10.61 Applications of dimension theory#

Section 10.61 of the Stacks Project, Tag 02IF. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02IG, a lemma

Tag 02IG in the Stacks Project.

PrimeSpectrum.infinite_of_two_le_ringKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/DimensionTwoOpens.lean, line 129. References: EGA IV (10.5.1), “e) ⇒ f) for local B”.

A nonempty open subset of the spectrum of a Noetherian local domain of dimension at least two is infinite.

public theorem infinite_of_two_le_ringKrullDim (R : Type*) [CommRing R] [IsNoetherianRing R]
    [IsLocalRing R] [IsDomain R] (hR : 2 ≤ ringKrullDim R) (U : Set (PrimeSpectrum R))
    (hU : IsOpen U) (hU' : U.Nonempty) : U.Infinite
Tag 0ALV, a lemma

Tag 0ALV in the Stacks Project.

Ring.krullDimLE_one_of_finite_primeSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/FinitePrimeSpectrum.lean, line 181.

A Noetherian ring with finitely many primes has dimension at most 1: every prime ideal is either minimal or maximal.

public theorem krullDimLE_one_of_finite_primeSpectrum (R : Type*) [CommRing R]
    [IsNoetherianRing R] [Finite (PrimeSpectrum R)] :
    KrullDimLE 1 R
Tag 0ALW, a lemma

Tag 0ALW in the Stacks Project.

Algebra.FiniteType.krullDimLE_zero_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Artinian/FiniteType.lean, line 580. The attribute's comment: “Items (1)-(8); (4) via 04MG's Hausdorff and totally disconnected conditions.”. References: EGA I (6.4.4), “affine case”.

Zero-dimensional finite type algebras. For an algebra S of finite type over an Artinian ring R the following are equivalent: S has Krull dimension at most 0; S has finitely many prime ideals; S has finitely many maximal ideals; Spec S is Hausdorff; S is finite as an R-module; S is Artinian; Spec S is discrete; and Spec S is totally disconnected. Over a field R = k the fifth condition says that S is finite dimensional as a k-vector space.

public theorem krullDimLE_zero_tfae (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    [IsArtinianRing R] [Algebra.FiniteType R S] :
    List.TFAE
      [ Ring.KrullDimLE 0 S,
        Finite (PrimeSpectrum S),
        Finite (MaximalSpectrum S),
        T2Space (PrimeSpectrum S),
        Module.Finite R S,
        IsArtinianRing S,
        DiscreteTopology (PrimeSpectrum S),
        TotallyDisconnectedSpace (PrimeSpectrum S) ]
Tag 00KX, a lemma

Tag 00KX in the Stacks Project.

isJacobsonRing_of_forall_isMaximal_or_infinite_setOf_isPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Jacobson/Criteria.lean, line 203. References: EGA IV (10.5.2), “sufficiency”; EGA IV (10.5.5), “(ii) sufficiency, affine”; EGA IV (10.4.3), “Artinian, PID clauses”.

A Noetherian ring in which every prime ideal is either maximal or contained in infinitely many prime ideals is a Jacobson ring.

public theorem isJacobsonRing_of_forall_isMaximal_or_infinite_setOf_isPrime (R : Type*)
    [CommRing R] [IsNoetherianRing R] (h : ∀ p : Ideal R, p.IsPrime →
      p.IsMaximal ∨ {q : Ideal R | p ≤ q ∧ q.IsPrime}.Infinite) :
    IsJacobsonRing R
Sources
LeanPrimeSpectrum.infinite_of_two_le_ringKrullDim · Ring.krullDimLE_one_of_finite_primeSpectrum · Algebra.FiniteType.krullDimLE_zero_tfae · isJacobsonRing_of_forall_isMaximal_or_infinite_setOf_isPrime

Section10.62 Support and dimension of modules#

Section 10.62 of the Stacks Project, Tag 00KY. 6 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00L4, a lemma

Tag 00L4 in the Stacks Project.

support_eq_iUnion_zeroLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Support/Finite.lean, line 140.

Stacks 00L4, main statement. With the filtration data of Stacks 00L0, the support of M is the union of the closed sets V(𝔭ᵢ).

theorem support_eq_iUnion_zeroLocus
    (A : Type*) [CommRing A] (M : Type*) [AddCommGroup M] [Module A M]
    [IsNoetherianRing A] [Module.Finite A M]
    (s : RelSeries {(N₁, N₂) : Submodule A M × Submodule A M |
          N₁.IsQuotientEquivQuotientPrime N₂})
    (hhead : s.head = ⊥) (hlast : s.last = ⊤)
    (p : Fin s.length → PrimeSpectrum A)
    (hp : ∀ i : Fin s.length,
      Nonempty (((s.toFun i.succ) ⧸ (s.toFun i.castSucc).submoduleOf (s.toFun i.succ))
        ≃ₗ[A] A ⧸ (p i).asIdeal)) :
    Module.support A M
      = ⋃ i : Fin s.length, PrimeSpectrum.zeroLocus ((p i).asIdeal : Set A)

mem_support_of_isQuotientEquivQuotientPrime_series, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Support/Finite.lean, line 161.

Stacks 00L4, "in particular". Each prime 𝔭ᵢ lies in the support of M.

theorem mem_support_of_isQuotientEquivQuotientPrime_series
    (A : Type*) [CommRing A] (M : Type*) [AddCommGroup M] [Module A M]
    [IsNoetherianRing A] [Module.Finite A M]
    (s : RelSeries {(N₁, N₂) : Submodule A M × Submodule A M |
          N₁.IsQuotientEquivQuotientPrime N₂})
    (hhead : s.head = ⊥) (hlast : s.last = ⊤)
    (p : Fin s.length → PrimeSpectrum A)
    (hp : ∀ i : Fin s.length,
      Nonempty (((s.toFun i.succ) ⧸ (s.toFun i.castSucc).submoduleOf (s.toFun i.succ))
        ≃ₗ[A] A ⧸ (p i).asIdeal)) :
    ∀ i : Fin s.length, p i ∈ Module.support A M
Tag 00L5, a lemma

Tag 00L5 in the Stacks Project.

support_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Support/Finite.lean, line 328. References: EGA 0 (16.1.10), “local ring case”; EGA IV (4.7.7), “special case”; SGA 6 X (1.1.2), “special case”.

Stacks 00L5. Over a Noetherian local ring R with maximal ideal m, a nonzero finite R-module M has support equal to the singleton {m} if and only if M has finite length over R.

theorem support_point {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] :
    Module.support R M = {IsLocalRing.closedPoint R} ↔ IsFiniteLength R M
Tag 00L6, a lemma

Tag 00L6 in the Stacks Project.

main_theorem_00l6, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Support/Finite.lean, line 354. References: EGA I (9.3.4), “affine case”.

For a finite module M over a Noetherian ring R and an ideal I ⊆ R, some power of I annihilates M if and only if the support of M is contained in the zero locus of I.

theorem main_theorem_00l6 {R : Type*} {M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    [IsNoetherianRing R] [Module.Finite R M] (I : Ideal R) :
    (∃ n : ℕ, (I ^ n) • (⊤ : Submodule R M) = ⊥) ↔
      Module.support R M ⊆ PrimeSpectrum.zeroLocus (I : Set R)
Tag 00L7, a lemma

Tag 00L7 in the Stacks Project.

Module.setOf_minimal_range_eq_setOf_minimal_support_and_ncard_eq_length, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/Additivity.lean, line 417.

Stacks 00L7. Let R be a ring, M an R-module, and let 0 = N₀ ⊆ N₁ ⊆ ⋯ ⊆ Nₙ = M be a filtration whose successive quotients are Nᵢ₊₁ ⧸ Nᵢ ≅ R ⧸ 𝔭ᵢ for primes 𝔭ᵢ = p i of R, as produced by Stacks 00L0. Then the minimal elements of the set {𝔭ᵢ} are exactly the minimal elements of Supp(M), and each minimal 𝔭 ∈ Supp(M) occurs among the 𝔭ᵢ exactly length_{R_𝔭} M_𝔭 times.

public theorem setOf_minimal_range_eq_setOf_minimal_support_and_ncard_eq_length {R M : Type*}
    [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (N : Fin (n + 1) → Submodule R M)
    (p : Fin n → PrimeSpectrum R) (hle : ∀ i : Fin n, N i.castSucc ≤ N i.succ)
    (hquot : ∀ i : Fin n,
      Nonempty ((↥(N i.succ) ⧸ (N i.castSucc).submoduleOf (N i.succ)) ≃ₗ[R] R ⧸ (p i).asIdeal))
    (hbot : N 0 = ⊥) (htop : N (Fin.last n) = ⊤) :
    {q | Minimal (· ∈ Set.range p) q} = {q | Minimal (· ∈ Module.support R M) q} ∧
      ∀ q : PrimeSpectrum R, Minimal (· ∈ Module.support R M) q →
        ({i | p i = q}.ncard : ℕ∞) =
          Module.length (Localization.AtPrime q.asIdeal)
            (LocalizedModule q.asIdeal.primeCompl M)
Tag 00L8, a lemma

Tag 00L8 in the Stacks Project.

Module.hilbertSamuelDegree_eq_supportDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HilbertSamuel/Dimension.lean, line 310. References: EGA 0 (16.2.3), “special case”.

Stacks 00L8. Let R be a Noetherian local ring and let M be a finite R-module. Then the Hilbert–Samuel degree d(M) of Definition 00KA equals the dimension of the support of M, that is, the Krull dimension of Supp(M) ⊆ Spec(R).

The equation is stated in WithBot ℕ∞, where dim Supp(M) lives, with d(M) : WithBot ℕ transported along the order embedding WithBot.map (Nat.cast : ℕ → ℕ∞); it therefore also asserts that dim Supp(M) is finite. Both sides are ⊥ = -∞ exactly when M = 0.

public theorem hilbertSamuelDegree_eq_supportDim (R : Type*) [CommRing R] [IsNoetherianRing R]
    [IsLocalRing R] (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    (hilbertSamuelDegree R M).map (Nat.cast : ℕ → ℕ∞) = supportDim R M
Tag 0B51, a lemma

Tag 0B51 in the Stacks Project.

Module.supportDim_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/Module.lean, line 222.

Stacks 0B51. Let R be a commutative ring and let 0 → M → N → P → 0 be a short exact sequence of R-modules, given by f : M →ₗ[R] N injective, g : N →ₗ[R] P surjective and Function.Exact f g. Then dim Supp(N) = max (dim Supp(M)) (dim Supp(P)).

The source assumes R Noetherian and the three modules finite; neither hypothesis is needed for this formulation of the dimension of the support.

public theorem supportDim_of_exact {R M N P : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P}
    (h : Function.Exact f g) (hf : Function.Injective f) (hg : Function.Surjective g) :
    supportDim R N = max (supportDim R M) (supportDim R P)
Sources
Leansupport_eq_iUnion_zeroLocus · mem_support_of_isQuotientEquivQuotientPrime_series · support_point · main_theorem_00l6 · Module.setOf_minimal_range_eq_setOf_minimal_support_and_ncard_eq_length · Module.hilbertSamuelDegree_eq_supportDim · Module.supportDim_of_exact

Section10.63 Associated primes#

Section 10.63 of the Stacks Project, Tag 00L9. 16 tags here are carried by 16 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00LA, a definition

Tag 00LA in the Stacks Project.

IsAssociatedPrimeStacks, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Defs.lean, line 50. References: SGA 2 III (1.1), “Ass M clause”.

Stacks 00LA. A prime ideal p of R is associated to the R-module M when it is the annihilator of a single element of M.

def IsAssociatedPrimeStacks (p : Ideal R) : Prop
Tag 0586, a lemma

Tag 0586 in the Stacks Project.

assPrimes_subset_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Defs.lean, line 137. References: SGA 2 III (1.2), “(ii) ⇒ (i)”.

Stacks Tag 0586. Every associated prime of M lies in the support of M: Ass(M) ⊆ Supp(M). Here Module.support R M is the set of primes p at which the localization M_p is nonzero.

theorem assPrimes_subset_support (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M] :
    assAssociatedPrimes R M ⊆ Module.support R M
Tag 00LB, a lemma

Tag 00LB in the Stacks Project.

ass_subset_of_filtration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Filtration.lean, line 205.

Stacks Tag 00LB. If M admits a finite filtration by R-submodules 0 = M_0 ⊆ M_1 ⊆ ... ⊆ M_n = M whose successive quotients M_i / M_{i-1} are isomorphic to R / p_i for prime ideals p_i, then every associated prime of M is among the p_i.

theorem ass_subset_of_filtration
    (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M]
    (n : ℕ) (Mfil : Fin (n + 1) → Submodule R M)
    (hbot : Mfil 0 = ⊥) (htop : Mfil (Fin.last n) = ⊤)
    (hmono : Monotone Mfil)
    (p : Fin n → Ideal R)
    (hp : ∀ i : Fin n, (p i).IsPrime)
    (hquot : ∀ i : Fin n,
      Nonempty (((Mfil i.succ) ⧸ (Submodule.comap (Mfil i.succ).subtype (Mfil i.castSucc)))
        ≃ₗ[R] (R ⧸ p i))) :
    assPrimes R M ⊆ Set.range p
Tag 02CE, a proposition

Tag 02CE in the Stacks Project.

Module.setOf_minimal_support_eq_setOf_minimal_associatedPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Support.lean, line 137. The attribute's comment: “Parts (1) and (2); the equality with part (3) is the first conclusion of Stacks 00L7, which the source's own proof cites for that step.”.

Let R be a Noetherian ring and M a finite R-module. The primes minimal in Supp(M) are exactly the primes minimal in Ass(M).

public theorem setOf_minimal_support_eq_setOf_minimal_associatedPrimes {R M : Type*} [CommRing R]
    [IsNoetherianRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] :
    {q : PrimeSpectrum R | Minimal (· ∈ Module.support R M) q} =
      {q : PrimeSpectrum R | Minimal (· ∈ PrimeSpectrum.asIdeal ⁻¹' associatedPrimes R M) q}
Tag 0587, a lemma

Tag 0587 in the Stacks Project.

Declarations registered for the tag:

Tag 05BV, a lemma

Tag 05BV in the Stacks Project.

Module.mem_associatedPrimes_of_minimal_mem_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Support.lean, line 244.

Let R be a Noetherian ring and let M be an R-module. Any prime 𝔭 which is minimal among the elements of the support of M is an associated prime of M.

public theorem Module.mem_associatedPrimes_of_minimal_mem_support {R : Type*} [CommRing R]
    [IsNoetherianRing R] {M : Type*} [AddCommGroup M] [Module R M] {p : PrimeSpectrum R}
    (hp : Minimal (· ∈ Module.support R M) p) :
    p.asIdeal ∈ associatedPrimes R M
Tag 00LD, a lemma

Tag 00LD in the Stacks Project.

Declarations registered for the tag:

Tag 05BW, a lemma

Tag 05BW in the Stacks Project.

spec_image_ass_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Functoriality.lean, line 335. References: EGA IV (3.1.10.1), “Contraction inclusion”.

Stacks Tag 05BW (Lemma 10.63.11): for a ring map φ : R → S and an S-module M viewed as an R-module via restriction of scalars along φ (encoded by hcompat : ∀ r m, r • m = φ r • m), the image of Ass_S(M) under the contraction map Spec(φ) = Ideal.comap φ is contained in Ass_R(M).

theorem spec_image_ass_subset
    {R S M : Type*} [CommSemiring R] [CommSemiring S]
    [AddCommMonoid M] [Module R M] [Module S M] (φ : R →+* S)
    (hcompat : ∀ (r : R) (m : M), r • m = φ r • m) :
    (Ideal.comap φ) '' (assOf S (M := M)) ⊆ assOf R (M := M)
Tag 05BX, a remark

Tag 05BX in the Stacks Project.

assExact_not_functorial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Functoriality.lean, line 545.

Together, the two statements above witness the failure of functoriality of associated primes along algebraMap k (S k): Ass_k(S) ≠ ∅ while Ass_S(S) = ∅.

theorem assExact_not_functorial (k : Type*) [Field k] :
    (assExact k (S k)).Nonempty ∧ assExact (S k) (S k) = ∅
Tag 05DZ, a lemma

Tag 05DZ in the Stacks Project.

Module.associatedPrimes.image_comap_associatedPrimes_eq_associatedPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Functoriality.lean, line 263.

Stacks 05DZ. Let S be an R-algebra and let M be an S-module, viewed as an R-module through algebraMap R S. If S is Noetherian, then contracting ideals along algebraMap R S — the map Spec(φ) on spectra — carries the associated primes of M over S onto the associated primes of M over R: Spec(φ)(Ass_S(M)) = Ass_R(M).

The inclusion ⊆ needs no Noetherian hypothesis (Stacks 05BW), and by Stacks 05BX the reverse inclusion genuinely does.

public theorem Module.associatedPrimes.image_comap_associatedPrimes_eq_associatedPrimes
    {R S : Type*} [CommSemiring R] [CommSemiring S] [Algebra R S] [IsNoetherianRing S]
    {M : Type*} [AddCommMonoid M] [Module S M] [Module R M] [IsScalarTower R S M] :
    Ideal.comap (algebraMap R S) '' associatedPrimes S M = associatedPrimes R M
Tag 05BY, a lemma

Tag 05BY in the Stacks Project.

Stacks.AssociatedPrimes.main_theorem_05by, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Defs.lean, line 223.

Stacks Tag 05BY. Contraction along π : R → R ⧸ I carries the associated primes of M over R ⧸ I onto the associated primes of M over R.

theorem main_theorem_05by :
    (fun p : Ideal (R ⧸ I) => p.comap (Ideal.Quotient.mk I)) '' assPrimes (R ⧸ I) M =
      assPrimes R M
Tag 05BZ, a lemma

Tag 05BZ in the Stacks Project.

Stacks.AssociatedPrimes.assPrimes_eq_image_comap_assPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/LocalizationSpectrum.lean, line 92. The attribute's comment: “(1)”.

Stacks 05BZ (1). For R' a localization S⁻¹R and any R'-module M' (in particular M' = S⁻¹M), the associated primes of M' over R are the contractions along Spec(S⁻¹R) → Spec(R) of its associated primes over R': Ass_R(M') = Ass_{S⁻¹R}(M').

theorem assPrimes_eq_image_comap_assPrimes :
    assPrimes R M' = Ideal.comap (algebraMap R R') '' assPrimes R' M'

Stacks.AssociatedPrimes.assPrimes_inter_image_comap_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/LocalizationSpectrum.lean, line 133. The attribute's comment: “(2)”.

Stacks 05BZ (2). Via the canonical injection Spec(S⁻¹R) → Spec(R), whose image is Ideal.comap (algebraMap R R') '' {J | J.IsPrime}, we have Ass_R(M) ∩ Spec(S⁻¹R) ⊆ Ass_R(S⁻¹M).

theorem assPrimes_inter_image_comap_subset :
    assPrimes R M ∩ Ideal.comap (algebraMap R R') '' {J | J.IsPrime} ⊆ assPrimes R M'

Stacks.AssociatedPrimes.assPrimes_inter_image_comap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/LocalizationSpectrum.lean, line 146. The attribute's comment: “(3)”.

Stacks 05BZ (3). If R is Noetherian, the inclusion of Stacks 05BZ (2) is an equality: Ass_R(M) ∩ Spec(S⁻¹R) = Ass_R(S⁻¹M).

theorem assPrimes_inter_image_comap_eq [IsNoetherianRing R] :
    assPrimes R M ∩ Ideal.comap (algebraMap R R') '' {J | J.IsPrime} = assPrimes R M'
Tag 05C0, a lemma

Tag 05C0 in the Stacks Project.

AssLocalization.assPrimes_localizedModule_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Localization.lean, line 130.

Stacks Tag 05C0 / Lemma 10.63.17. If every element of the multiplicative subset S is a nonzerodivisor on the R-module M, then the (exact-annihilator) associated primes of M and of its localization S⁻¹M = LocalizedModule S M (both as R-modules) coincide.

theorem assPrimes_localizedModule_eq (S : Submonoid R) (hS : AllNonZeroDivisorsOn S M) :
    Stacks.AssociatedPrimes.assPrimes R M
      = Stacks.AssociatedPrimes.assPrimes R (LocalizedModule S M)
Tag 00LL, a lemma

Tag 00LL in the Stacks Project.

Ideal.exists_mem_isSMulRegular_iff_forall_associatedPrimes_not_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Basic.lean, line 115. References: SGA 2 III (2.1), “(ii) <=> (iv)”.

Let R be a Noetherian ring, M an R-module with finitely many associated primes and I ⊆ R an ideal. Then I contains an element that is a nonzerodivisor on M if and only if I is contained in no associated prime of M.

public theorem Ideal.exists_mem_isSMulRegular_iff_forall_associatedPrimes_not_le {R : Type*}
    [CommRing R] [IsNoetherianRing R] (I : Ideal R) (M : Type*) [AddCommGroup M] [Module R M]
    (hM : (associatedPrimes R M).Finite) :
    (∃ x ∈ I, IsSMulRegular M x) ↔
      ∀ 𝔮 ∈ associatedPrimes R M, ¬ I ≤ 𝔮
Tag 0311, a lemma

Tag 0311 in the Stacks Project.

zero_at_ass_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Support.lean, line 162.

Over a Noetherian ring, the canonical map from \(M\) into the product of its localizations at associated primes is injective.

theorem zero_at_ass_zero (R : Type*) [CommRing R] [IsNoetherianRing R]
    (M : Type*) [AddCommGroup M] [Module R M] :
    Function.Injective (assMap R M)
Tag 0GEC, a lemma

Tag 0GEC in the Stacks Project.

exists_mem_nonZeroDivisors_not_isUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Basic.lean, line 159. References: SGA 3 VIA (1.1.2), “special case”.

For a finite type algebra S over a field k with 0 < dim S, some element of S is simultaneously a nonzerodivisor and a nonunit.

theorem exists_mem_nonZeroDivisors_not_isUnit {k : Type*} [Field k] {S : Type*} [CommRing S]
    [Algebra k S] [Algebra.FiniteType k S] (h : 0 < ringKrullDim S) :
    ∃ f : S, f ∈ nonZeroDivisors S ∧ ¬ IsUnit f
Sources
LeanIsAssociatedPrimeStacks · assPrimes_subset_support · ass_subset_of_filtration · Module.setOf_minimal_support_eq_setOf_minimal_associatedPrimes · associatedPrimes.eq_empty_of_subsingleton · associatedPrimes.nonempty · Module.mem_associatedPrimes_of_minimal_mem_support · biUnion_associatedPrimes_eq_zero_divisors

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.