10.105 Catenary rings to 10.124 Applications of…

Section10.105 Catenary rings#

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

Tag 00NI, a definition

Tag 00NI in the Stacks Project.

Ring.IsCatenary, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Basic.lean, line 1261. References: EGA 0 (16.1.4), “catenary ring def”.

A commutative ring R is catenary if for every pair of prime ideals p ⊆ q there is an integer bounding the lengths of the finite chains of primes from p to q, and all non-refinable such chains have the same length. Chains are LTSeries in PrimeSpectrum R, and non-refinability of a chain with fixed endpoints is the condition that each of its steps be a covering pair ⋖.

public def Ring.IsCatenary (R : Type*) [CommRing R] : Prop

Tag 02IH, a lemma

Tag 02IH in the Stacks Project.

Catenary.isCatenaryRing_iff_isCatenarySpace_primeSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Defs.lean, line 145. References: EGA 0 (16.1.4); EGA IV (5.1.1).

A commutative ring R is catenary if and only if the poset of irreducible closed subsets of PrimeSpectrum R is a catenary order.

theorem isCatenaryRing_iff_isCatenarySpace_primeSpectrum (R : Type*) [CommRing R] :
    IsCatenaryRing R ↔ IsCatenaryOrder (IrreducibleCloseds (PrimeSpectrum R))

Tag 00NL, a definition

Tag 00NL in the Stacks Project.

Ring.IsUniversallyCatenary, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Basic.lean, line 1270. References: EGA IV (5.6.2).

A commutative ring R is universally catenary if every R-algebra of finite type is catenary.

public def Ring.IsUniversallyCatenary (R : Type u) [CommRing R] : Prop

IsUniversallyCatenary, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Defs.lean, line 35. References: EGA IV (5.6.2).

A commutative ring R is universally catenary if every finite-type R-algebra C has catenary prime spectrum.

def IsUniversallyCatenary (R : Type u) [CommRing R] : Prop

Tag 00NJ, a lemma

Tag 00NJ in the Stacks Project.

localization_isUniversallyCatenary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Basic.lean, line 704. References: EGA IV (10.7.2), “more general”; EGA IV (5.6.3); EGA IV (7.8.2), “partial”.

A localization of a Noetherian universally catenary ring is universally catenary.

theorem localization_isUniversallyCatenary
    (R : Type u) [CommRing R] [IsNoetherianRing R] (S : Submonoid R)
    (A : Type u) [CommRing A] [Algebra R A] [IsLocalization S A]
    (h : IsUniversallyCatenary R) :
    IsUniversallyCatenary A

Tag 0ECE, a lemma

Tag 0ECE in the Stacks Project.

universally_catenary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Basic.lean, line 1164. References: EGA IV (10.6.1), “(i)”; EGA IV (10.7.2), “more general”; EGA IV (10.7.3), “partial”; EGA IV (5.6.3); EGA IV (7.8.2), “partial”.

Let A be a Noetherian ring such that every finite-type A-algebra has catenary spectrum. Then every A-algebra S essentially of finite type is Noetherian, and every finite-type S-algebra has catenary spectrum.

theorem universally_catenary
    (A : Type*) [CommRing A] [IsNoetherianRing A]
    (hA : ∀ (B : Type u) [CommRing B] [Algebra A B] [Algebra.FiniteType A B],
            IrreducibleClosedsCodim.IsCatenarySpace (PrimeSpectrum B))
    (S : Type*) [CommRing S] [Algebra A S] [Algebra.EssFiniteType A S] :
    IsNoetherianRing S ∧
    (∀ (C : Type u) [CommRing C] [Algebra S C] [Algebra.FiniteType S C],
       IrreducibleClosedsCodim.IsCatenarySpace (PrimeSpectrum C))

Tag 0AUN, a lemma

Tag 0AUN in the Stacks Project.

catenary_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Basic.lean, line 1109. The attribute's comment: “catenary”. References: EGA 0 (16.1.4); EGA IV (5.1.5), “special case”; EGA IV (5.6.3), “(i), special case”.

For a commutative ring R the following are equivalent: 1. R is catenary; 2. the localization R_p is catenary for every prime ideal p; 3. the localization R_m is catenary for every maximal ideal m.

theorem catenary_tfae (R : Type u) [CommRing R] :
    [ IrreducibleClosedsCodim.IsCatenarySpace (PrimeSpectrum R),
      ∀ (p : Ideal R) [p.IsPrime],
        IrreducibleClosedsCodim.IsCatenarySpace (PrimeSpectrum (Localization.AtPrime p)),
      ∀ (m : Ideal R) [m.IsMaximal],
        IrreducibleClosedsCodim.IsCatenarySpace
          (PrimeSpectrum (Localization.AtPrime m)) ].TFAE

universallyCatenary_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Basic.lean, line 1136. The attribute's comment: “universally catenary”. References: EGA IV (10.7.2), “more general”; EGA IV (5.6.3); EGA IV (7.8.2); EGA IV (7.8.3), “(i)”.

For a Noetherian commutative ring R the following are equivalent: 1. R is universally catenary; 2. the localization R_p is universally catenary for every prime ideal p; 3. the localization R_m is universally catenary for every maximal ideal m.

theorem universallyCatenary_tfae (R : Type u) [CommRing R] [IsNoetherianRing R] :
    [ IsUniversallyCatenary R,
      ∀ (p : Ideal R) [p.IsPrime], IsUniversallyCatenary (Localization.AtPrime p),
      ∀ (m : Ideal R) [m.IsMaximal], IsUniversallyCatenary (Localization.AtPrime m) ].TFAE

Tag 00NK, a lemma

Tag 00NK in the Stacks Project.

Ring.isCatenary_and_isUniversallyCatenary_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Basic.lean, line 1296. References: EGA 0 (16.1.4); EGA IV (5.6.3), “partial”.

If f : A →+* B is surjective, then B is catenary if A is, and B is universally catenary if A is.

public theorem Ring.isCatenary_and_isUniversallyCatenary_of_surjective {A B : Type u} [CommRing A]
    [CommRing B] {f : A →+* B} (hf : Function.Surjective f) :
    (Ring.IsCatenary A → Ring.IsCatenary B) ∧
      (Ring.IsUniversallyCatenary A → Ring.IsUniversallyCatenary B)

Ring.IsCatenary.of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Basic.lean, line 1314.

If f : A →+* B is surjective and A is catenary, then so is B.

public theorem Ring.IsCatenary.of_surjective {A B : Type u} [CommRing A] [CommRing B]
    {f : A →+* B} (hf : Function.Surjective f) (hA : Ring.IsCatenary A) : Ring.IsCatenary B

Ring.IsUniversallyCatenary.of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Basic.lean, line 1320.

If f : A →+* B is surjective and A is universally catenary, then so is B.

public theorem Ring.IsUniversallyCatenary.of_surjective {A B : Type u} [CommRing A] [CommRing B]
    {f : A →+* B} (hf : Function.Surjective f) (hA : Ring.IsUniversallyCatenary A) :
    Ring.IsUniversallyCatenary B

Tag 0AUP, a lemma

Tag 0AUP in the Stacks Project.

isCatenaryRing_iff_quotient_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Basic.lean, line 233. The attribute's comment: “(1)”. References: EGA 0 (16.1.4), “special case”.

A Noetherian ring R is catenary if and only if R ⧸ p is catenary for every minimal prime p of R.

theorem isCatenaryRing_iff_quotient_minimalPrimes
    (R : Type u) [CommRing R] [IsNoetherianRing R] :
    IsCatenaryRing R ↔
      ∀ p : Ideal R, (hp : p ∈ minimalPrimes R) →
        haveI : p.IsPrime := hp.1.1
        IsCatenaryRing (R ⧸ p)

isUniversallyCatenaryRing_iff_quotient_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Basic.lean, line 266. The attribute's comment: “(2)”. References: EGA IV (5.6.3).

A Noetherian ring R is universally catenary if and only if R ⧸ p is universally catenary for every minimal prime p of R.

theorem isUniversallyCatenaryRing_iff_quotient_minimalPrimes
    (R : Type u) [CommRing R] [IsNoetherianRing R] :
    IsUniversallyCatenaryRing R ↔
      ∀ p : Ideal R, (hp : p ∈ minimalPrimes R) →
        haveI : p.IsPrime := hp.1.1
        haveI : IsNoetherianRing (R ⧸ p) := inferInstance
        IsUniversallyCatenaryRing (R ⧸ p)

Tag 00NM, a lemma

Tag 00NM in the Stacks Project.

Ring.IsUniversallyCatenary.of_isCohenMacaulay_of_support_eq_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Catenary.lean, line 376. The attribute's comment: “The source's M Cohen-Macaulay with Supp(M) = Spec(R) is Module.IsCohenMacaulay R M (Definition 0AAH) together with Module.support R M = Set.univ, the spelling of the companion Tag 0AAE; the Noetherian and finiteness hypotheses, which the source keeps inside Definitions 00N3 and 0AAH, are assumed explicitly; and the first sentence of the tag is the case M = R, where the support condition holds for every ring. See the module docstring.”. References: EGA 0 (16.5.12), “local CM ring case”; EGA IV (6.3.7), “CM ring itself”; EGA IV (7.2.7), “universally catenary”; SGA 6 X (1.5), “Affine ambient case”.

A Noetherian ring with a Cohen–Macaulay module of full support is universally catenary. If R is Noetherian and M is a finite Cohen–Macaulay R-module (Definition 0AAH) with Supp(M) = Spec(R), then every R-algebra of finite type is catenary. Taking M = R, where the support condition is automatic, this says that a Noetherian Cohen–Macaulay ring is universally catenary. The universes of R and M are independent: the localisations the hypothesis speaks of are named inside Definition 0AAH, which puts M_𝔭 in Type (max u v).

public theorem Ring.IsUniversallyCatenary.of_isCohenMacaulay_of_support_eq_univ {R : Type u}
    [CommRing R] [IsNoetherianRing R] {M : Type v} [AddCommGroup M] [Module R M]
    [Module.Finite R M] (hM : Module.IsCohenMacaulay R M)
    (hsupp : Module.support R M = Set.univ) :
    Ring.IsUniversallyCatenary R

Tag 0ECF, a lemma

Tag 0ECF in the Stacks Project.

catenary_iff_isDimensionFunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Basic.lean, line 974.

A Noetherian local ring A is catenary if and only if p ↦ dim(A ⧸ p) is a dimension function on PrimeSpectrum A.

theorem catenary_iff_isDimensionFunction
    (A : Type*) [CommRing A] [IsNoetherianRing A] [IsLocalRing A] :
    IsCatenaryRingSaturated A ↔ IsDimensionFunctionProp (X := PrimeSpectrum A) deltaDim

Sources

• Section 10.105, Tag 00NH
• AxiomMath/Stacks at 5ed82d14

LeanRing.IsCatenary · Catenary.isCatenaryRing_iff_isCatenarySpace_primeSpectrum · Ring.IsUniversallyCatenary · IsUniversallyCatenary · localization_isUniversallyCatenary · universally_catenary · catenary_tfae · universallyCatenary_tfae

Section10.106 Regular local rings#

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

Tag 00NO, a lemma

Tag 00NO in the Stacks Project.

IsRegularLocalRing.gradedRing_maximalIdeal_isPolynomialAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/AssociatedGradedPolynomial.lean, line 432. The attribute's comment: “The graded-RING form: the canonical ring map κ[X_1, …, X_d] → ⨁_{n ≥ 0} 𝔪^n/𝔪^(n+1), X_i ↦ x_i mod 𝔪^2, of a minimal generating sequence of the maximal ideal is bijective, and carries the degree-n homogeneous polynomials exactly onto 𝔪^n/𝔪^(n+1); that is the source's isomorphism of the graded ring with the graded polynomial algebra, with the isomorphism pinned to the source's own map rather than merely asserted. See also IsRegularLocalRing.isQuasiRegular for the graded-module form (Tag 061N/061P).”.

Stacks 00NO, in the form of a graded-ring isomorphism. Let (R, 𝔪, κ) be a regular local ring of dimension d and let xs = x_1, …, x_d be a minimal set of generators of 𝔪, that is, a list generating 𝔪 whose length is the minimal number of generators of 𝔪 (which equals dim R). Then the canonical map of graded rings κ[X_1, …, X_d] → ⨁_{n ≥ 0} 𝔪^n/𝔪^(n+1), X_i ↦ x_i mod 𝔪^2, is bijective (first clause) and carries the homogeneous polynomials of degree n onto the degree-n part 𝔪^n/𝔪^(n+1) (second clause). Together: the graded ring ⨁_{n ≥ 0} 𝔪^n/𝔪^(n+1) is the graded polynomial algebra κ[X_1, …, X_d] over the residue field, as graded rings.

public theorem gradedRing_maximalIdeal_isPolynomialAlgebra
    (hxs : Ideal.ofList xs = maximalIdeal R)
    (hmin : xs.length = (maximalIdeal R).spanFinrank)
    (hx : ∀ i : Fin xs.length, xs[i] ∈ maximalIdeal R) :
    Function.Bijective
        (AssociatedGraded.polyGradedHom (maximalIdeal R) (fun i : Fin xs.length => xs[i]) hx) ∧
      ∀ (n : ℕ) (y : AssociatedGraded.gradedRing (maximalIdeal R)),
        y ∈ AssociatedGraded.grading (maximalIdeal R) n ↔
          ∃ p : MvPolynomial (Fin xs.length) (R ⧸ maximalIdeal R), p.IsHomogeneous n ∧
            AssociatedGraded.polyGradedHom (maximalIdeal R)
              (fun i : Fin xs.length => xs[i]) hx p = y

IsRegularLocalRing.isQuasiRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/Basic.lean, line 478. The attribute's comment: “Stated as quasi-regularity (Tag 061P) of a minimal generating sequence of the maximal ideal, which is exactly the assertion that the source's graded surjection κ[X_1, …, X_d] → ⨁ m^n/m^(n+1), X_i ↦ x_i mod m^2, is an isomorphism. See the module docstring.”.

Stacks 00NO. Let (R, m, κ) be a regular local ring of dimension d and let xs = x_1, …, x_d be a minimal set of generators of m, that is, a list generating m whose length is the minimal number of generators of m (which equals dim R). Then xs is a quasi-regular sequence: the canonical map of graded κ[X_1, …, X_d]-modules κ[X_1, …, X_d] ⊗_κ (R/m) → ⨁_{n ≥ 0} m^n/m^(n + 1), X^e ⊗ 1 ↦ x^e mod m^(|e| + 1), is bijective. Equivalently, the graded ring ⨁_{n ≥ 0} m^n/m^(n + 1) is the graded polynomial algebra κ[X_1, …, X_d] over the residue field.

public theorem IsRegularLocalRing.isQuasiRegular {R : Type*} [CommRing R] [IsRegularLocalRing R]
    (xs : List R) (hxs : Ideal.ofList xs = maximalIdeal R)
    (hmin : xs.length = (maximalIdeal R).spanFinrank) :
    RingTheory.Sequence.IsQuasiRegular R xs

Tag 00NP, a lemma

Tag 00NP in the Stacks Project.

IsRegularLocalRing.isDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/Basic.lean, line 779.

A regular local ring is a domain. If the maximal ideal of a Noetherian local ring R can be generated by dim R elements, then R has no zero divisors.

public theorem IsRegularLocalRing.isDomain (R : Type*) [CommRing R] [IsRegularLocalRing R] :
    IsDomain R

Tag 00NQ, a lemma

Tag 00NQ in the Stacks Project.

Stacks.Blowup.isWeaklyRegular_of_span_range_eq_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ProjectiveLineExceptional.lean, line 307. The attribute's comment: “for a two-dimensional regular local ring and a two-element generating family of the maximal ideal”.

Two generators of the maximal ideal of a regular local ring of dimension two form a regular sequence. A family of two elements spanning 𝔪 has the minimal length (𝔪).spanFinrank = dim A = 2, so Tag 00NQ applies to it.

theorem isWeaklyRegular_of_span_range_eq_maximalIdeal (A : Type u) [CommRing A]
    [IsRegularLocalRing A] (hdim : ringKrullDim A = 2) (x : Fin 2 → A)
    (hspan : IsLocalRing.maximalIdeal A = Ideal.span (Set.range x)) :
    RingTheory.Sequence.IsWeaklyRegular A [x 0, x 1]

IsRegularLocalRing.isRegular_and_isRegularLocalRing_quotient_and_isMaximalCohenMacaulay, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/Basic.lean, line 1038. The attribute's comment: “Cohen-Macaulayness is the named predicate Module.IsMaximalCohenMacaulay R R (Definition 00NF), the equality depth_𝔪(R) = dim R; the minimal generating sequence is bound inside the clause that uses it, so the in particular is a statement about R alone. See the module docstring.”. References: EGA 0 (17.1.3), “CM clause”; SGA 4½ Cycle (2.2.1), “special case”.

A minimal set of generators of the maximal ideal of a regular local ring is a regular sequence. Let (R, 𝔪) be a regular local ring. Then every list xs = x₁, …, x_d generating 𝔪 of the minimal length d = (𝔪).spanFinrank is a regular sequence on R, and each initial quotient R/(x₁, …, x_c) is a regular local ring of dimension d - c; in particular R is Cohen-Macaulay, that is, maximal Cohen-Macaulay over itself.

public theorem isRegular_and_isRegularLocalRing_quotient_and_isMaximalCohenMacaulay
    (R : Type*) [CommRing R] [IsRegularLocalRing R] :
    (∀ xs : List R, Ideal.ofList xs = maximalIdeal R →
        xs.length = (maximalIdeal R).spanFinrank →
        RingTheory.Sequence.IsRegular R xs ∧
          ∀ c ≤ xs.length, IsRegularLocalRing (R ⧸ Ideal.ofList (xs.take c)) ∧
            ringKrullDim (R ⧸ Ideal.ofList (xs.take c)) + c = ringKrullDim R) ∧
      Module.IsMaximalCohenMacaulay R R

Tag 00NR, a lemma

Tag 00NR in the Stacks Project.

IsRegularLocalRing.exists_ofList_eq_maximalIdeal_length_eq_spanFinrank_and_ofList_take_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/Basic.lean, line 1403. The attribute's comment: “A minimal set of generators of 𝔪 is a list generating it whose length is (𝔪).spanFinrank, and (x₁, …, x_c) is the ideal generated by the length-c prefix of that list, as in Tag 00NQ. The source's existentially bound c is pinned by the dimension equation dim (R ⧸ I) + c = dim R proved along with it. See the module docstring.”.

An ideal of a regular local ring with regular quotient is generated by part of a minimal set of generators of the maximal ideal. Let (R, 𝔪) be a regular local ring and let I be an ideal of R such that R ⧸ I is a regular local ring as well. Then there is a list xs = x₁, …, x_d generating 𝔪 of the minimal length d = (𝔪).spanFinrank and a c ≤ d with I = (x₁, …, x_c); moreover dim (R ⧸ I) + c = dim R, i.e. c = dim R - dim (R ⧸ I).

public theorem exists_ofList_eq_maximalIdeal_length_eq_spanFinrank_and_ofList_take_eq
    {R : Type*} [CommRing R] [IsRegularLocalRing R] (I : Ideal R)
    (hI : IsRegularLocalRing (R ⧸ I)) :
    ∃ xs : List R, Ideal.ofList xs = maximalIdeal R ∧
      xs.length = (maximalIdeal R).spanFinrank ∧
      ∃ c ≤ xs.length, Ideal.ofList (xs.take c) = I ∧
        ringKrullDim (R ⧸ I) + c = ringKrullDim R

Tag 00NS, a lemma

Tag 00NS in the Stacks Project.

free_mod_x, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/MaximalCohenMacaulay.lean, line 67. References: EGA 0 (10.1.2), “special case”; EGA 0 (10.2.2), “(x), special case”; SGA 1 IV (4.1), “(b), special case”.

Stacks Tag 00NS. Let R be a Noetherian local ring with maximal ideal m, and let x ∈ m. Let M be a finite R-module on which x is a nonzerodivisor and such that M / xM is free over R / xR. Then M is free over R.

theorem free_mod_x
    (R : Type*) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (x : R) (hx : x ∈ maximalIdeal R)
    (hnzd : IsSMulRegular M x)
    (hfree : Module.Free (R ⧸ Ideal.span {x})
      (M ⧸ (Ideal.span {x} • (⊤ : Submodule R M)))) :
    Module.Free R M

Tag 00NT, a lemma

Tag 00NT in the Stacks Project.

regular_mcm_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/MaximalCohenMacaulay.lean, line 2010. References: EGA 0 (17.3.5), “(i), sufficiency”; EGA IV (6.1.5), “special case”.

Stacks Tag 00NT (Lemma 10.106.6): over a regular local ring, any nonzero finitely generated maximal Cohen-Macaulay module is free.

theorem regular_mcm_free
    (R : Type*) [CommRing R] [IsRegularLocalRing R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M]
    (hM : IsMaxCM R M) : Module.Free R M

Tag 00NU, a lemma

Tag 00NU in the Stacks Project.

isRegularLocalRing_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/Criteria.lean, line 145. The attribute's comment: “regular sequence”. References: EGA IV (19.1.2), “sufficiency direction”; EGA 0 (17.1.1), “more general”; EGA 0 (17.1.7), “b⇒regularity of A”; EGA IV (16.9.12), “sufficiency”; EGA IV (7.9.7), “partial”; SGA 6 X (7.7), “special case”.

Stacks 00NU, regular sequence case. Let R be a Noetherian local ring, and rs a regular sequence such that R / (rs) is a regular local ring. Then R is a regular local ring.

theorem isRegularLocalRing_of_isRegular (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherian R R]
    (rs : List R) (hrs : RingTheory.Sequence.IsRegular R rs)
    (hreg : IsRegularLocalRing (R ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing R

isRegularLocalRing_of_nonZeroDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/Criteria.lean, line 199. The attribute's comment: “single element”. References: EGA IV (19.1.2), “principal J, sufficiency”; EGA 0 (17.1.1), “(d) ⇒ (c)”; EGA 0 (17.1.7), “r=1: b⇒regularity of A”; EGA 0 (17.1.8), “a ⇒ b”; EGA IV (16.9.12), “special case”; EGA IV (7.9.7), “partial”; SGA 6 X (7.7), “special case”.

Stacks 00NU, single nonzerodivisor case. Let R be a Noetherian local ring, and x a nonzerodivisor such that R / xR is a regular local ring. Then R is a regular local ring.

This is the special case rs = [x] of isRegularLocalRing_of_isRegular.

theorem isRegularLocalRing_of_nonZeroDivisor (R : Type*) [CommRing R] [IsLocalRing R]
    [IsNoetherian R R]
    (x : R) (hx : x ∈ nonZeroDivisors R)
    (hreg : IsRegularLocalRing (R ⧸ Ideal.span {x})) :
    IsRegularLocalRing R

Tag 07DX, a lemma

Tag 07DX in the Stacks Project.

CommRingCat.isRegularLocalRing_pt_of_forall_isRegularLocalRing_of_forall_isLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/Colimit.lean, line 439. The attribute's comment: “The directed system is a functor on a nonempty u-small directed preorder together with an arbitrary colimit cocone, as in 0AS7; locality of a transition map is IsLocalHom of the underlying ring homomorphism; IsRegularLocalRing of the colimit includes the assertion that it is local. See the module docstring.”.

Let F : J ⥤ CommRingCat be a directed system (R i, φ i i') of commutative rings over a nonempty, u-small directed preorder J, and let c be a colimit cocone on F, so that c.pt is colim_i R i. If every R i is a regular local ring, every transition map is a local ring map, and the colimit is Noetherian, then the colimit is a regular local ring — in particular it is local, its maximal ideal being the colimit of the maximal ideals of the R i.

public theorem isRegularLocalRing_pt_of_forall_isRegularLocalRing_of_forall_isLocalHom
    {J : Type w} [Preorder J] [IsDirectedOrder J] [Nonempty J] [Small.{u} J]
    {F : J ⥤ CommRingCat.{u}}
    (hreg : ∀ j : J, IsRegularLocalRing (F.obj j))
    (hloc : ∀ ⦃i j : J⦄ (u : i ⟶ j), IsLocalHom (F.map u).hom)
    {c : Cocone F} (hc : IsColimit c) [IsNoetherianRing c.pt] :
    IsRegularLocalRing c.pt

Sources

• Section 10.106, Tag 00NN
• AxiomMath/Stacks at 5ed82d14

LeanIsRegularLocalRing.gradedRing_maximalIdeal_isPolynomialAlgebra · IsRegularLocalRing.isQuasiRegular · IsRegularLocalRing.isDomain · Stacks.Blowup.isWeaklyRegular_of_span_range_eq_maximalIdeal · IsRegularLocalRing.isRegular_and_isRegularLocalRing_quotient_and_isMaximalCohenMacaulay · IsRegularLocalRing.exists_ofList_eq_maximalIdeal_length_eq_spanFinrank_and_ofList_take_eq · free_mod_x · regular_mcm_free

Section10.107 Epimorphisms of rings#

Section 10.107 of the Stacks Project, Tag 04VM. 13 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 04VN, a lemma

Tag 04VN in the Stacks Project.

CommRingCat.epi_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/Basic.lean, line 190. The attribute's comment: “Item (1) is CategoryTheory.Epi in CommRingCat, the source's categorical notion, rather than the class Algebra.IsEpi, which is by definition injectivity of the multiplication map and would make item (5) restate item (1); CommRingCat.epi_iff_epi transfers between them. The source's either of the ring maps is the two items (3) and (4) below, one per map, and is an isomorphism is Function.Bijective. See the module docstring.”.

The tensor square detects a ring epimorphism (Stacks 04VN). Let R → S be a ring map. The following are equivalent: (1) R → S is an epimorphism of commutative rings; (2) the two ring maps S → S ⊗_R S, namely s ↦ s ⊗ 1 and s ↦ 1 ⊗ s, are equal; (3) s ↦ s ⊗ 1 is an isomorphism; (4) s ↦ 1 ⊗ s is an isomorphism; (5) the multiplication map S ⊗_R S → S is an isomorphism.

theorem CommRingCat.epi_tfae {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] :
    List.TFAE
      [CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R S)),
       (Algebra.TensorProduct.includeLeft : S →ₐ[R] S ⊗[R] S) = Algebra.TensorProduct.includeRight,
       Function.Bijective (Algebra.TensorProduct.includeLeft : S →ₐ[R] S ⊗[R] S),
       Function.Bijective (Algebra.TensorProduct.includeRight : S →ₐ[R] S ⊗[R] S),
       Function.Bijective (Algebra.TensorProduct.lmul' (S := S) R)]

Tag 04VP, a lemma

Tag 04VP in the Stacks Project.

Declarations registered for the tag:

• CategoryTheory.epi_comp registered with add_to_stacks in StacksFrontier/Algebra/Category/Ring/Epi/Basic.lean, line 377 (StacksFrontier): “The case C = CommRingCat of the general categorical fact.”. References: SGA 3 IV (1.4).

Tag 04VQ, a lemma

Tag 04VQ in the Stacks Project.

epi_includeLeftRingHom_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/Basic.lean, line 432.

Base change of an epimorphism is an epimorphism. If R → S is an epimorphism in CommRingCat and R → R' is any ring map, then the canonical ring map R' → R' ⊗_R S is an epimorphism.

theorem epi_includeLeftRingHom_of_epi
    (R R' S : Type) [CommRing R] [CommRing R'] [CommRing S]
    [Algebra R R'] [Algebra R S]
    (h : Epi (CommRingCat.ofHom (algebraMap R S))) :
    Epi (CommRingCat.ofHom
      (Algebra.TensorProduct.includeLeftRingHom :
        R' →+* TensorProduct R R' S))

Tag 04VR, a lemma

Tag 04VR in the Stacks Project.

Algebra.IsEpi.tower_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/Basic.lean, line 217. The attribute's comment: “Epimorphy is Mathlib's Algebra.IsEpi (equivalently CategoryTheory.Epi in CommRingCat, by CommRingCat.epi_iff_epi), and the source's hypothesis that A → C is the composite A → B → C is IsScalarTower A B C. Named after its sibling Algebra.IsIntegral.tower_top. See the module docstring.”.

An epimorphism of rings stays one over a larger base (Stacks 04VR). If A → B → C are ring maps, A → C being the composite, and A → C is an epimorphism, then B → C is an epimorphism.

The proof transports the identity 1 ⊗ c = c ⊗ 1 along the base-enlargement comparison map TensorProduct.mapOfCompatibleSMul B A B C C : C ⊗[A] C →ₗ[B] C ⊗[B] C, whose TensorProduct.CompatibleSMul B A C C instance is where IsScalarTower A B C enters.

theorem tower_top {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
    [Algebra A B] [Algebra A C] [Algebra B C] [IsScalarTower A B C] [Algebra.IsEpi A C] :
    Algebra.IsEpi B C

Tag 04VS, a lemma

Tag 04VS in the Stacks Project.

CommRingCat.epi_ofHom_iff_forall_prime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/Basic.lean, line 671.

Stacks Tag 04VS. Being an epimorphism is a local property of a ring map: a ring map f : R →+* S is an epimorphism of rings if and only if for every prime ideal p of R, the induced map R_p →+* S_p is an epimorphism of rings.

theorem CommRingCat.epi_ofHom_iff_forall_prime {R S : Type u} [CommRing R] [CommRing S]
    (f : R →+* S) :
    Epi (CommRingCat.ofHom f) ↔
      ∀ (p : Ideal R) [p.IsPrime], Epi (CommRingCat.ofHom (inducedLocalizationMap f p))

Tag 04VT, a lemma

Tag 04VT in the Stacks Project.

Declarations registered for the tag:

• RingHom.surjective_iff_epi_and_finite registered with add_to_stacks in StacksFrontier/Algebra/Category/Ring/Epi/Basic.lean, line 700 (StacksFrontier): “a ring map is surjective iff it is a finite epimorphism”.

Tag 04VU, a lemma

Tag 04VU in the Stacks Project.

faithfullyFlat_epimorphism_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/Basic.lean, line 739. References: SGA 3 VIB (12.1), “affine case”; SGA 3 XI (3.9), “Affine case”.

If algebraMap R S is an epimorphism of commutative rings and S is faithfully flat as an R-module, then algebraMap R S is bijective, i.e. an isomorphism of rings.

theorem faithfullyFlat_epimorphism_isIso
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.IsEpi R S] [Module.FaithfullyFlat R S] :
    Function.Bijective (algebraMap R S)

Tag 04VV, a lemma

Tag 04VV in the Stacks Project.

Algebra.IsEpi.surjective_algebraMap_of_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/Basic.lean, line 233. The attribute's comment: “The source's S = k or S = 0 is stated as surjectivity of algebraMap k S, which over a field is equivalent to it; the target need not be commutative. See the module docstring.”.

An epimorphism of rings k → S out of a field k is surjective; equivalently, S = k or S = 0.

Over a field the line k · 1 ⊆ S is split off by a linear functional φ : S →ₗ[k] k with φ 1 = 1; applying φ to the left factor of the identity 1 ⊗ s = s ⊗ 1 in S ⊗[k] S turns it into s = algebraMap k S (φ s).

theorem surjective_algebraMap_of_field {k S : Type*} [Field k] [Ring S] [Algebra k S]
    [Algebra.IsEpi k S] : Function.Surjective (algebraMap k S)

Tag 04VW, a lemma

Tag 04VW in the Stacks Project.

PrimeSpectrum.comap_injective_and_residueFieldMap_bijective_of_isEpi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/Basic.lean, line 353. The attribute's comment: “The equality κ(𝔭) = κ(𝔮) of part (2) is bijectivity of the canonical map Ideal.ResidueField.map; it is not surjectivity of R_𝔭 → S_𝔮, which is false for epimorphisms. See the module docstring.”.

Let R → S be an epimorphism of rings. Then Spec S → Spec R is injective, and for every prime 𝔮 ⊆ S lying over a prime 𝔭 ⊆ R the canonical residue field extension κ(𝔭) → κ(𝔮) is bijective, that is, κ(𝔭) = κ(𝔮).

theorem comap_injective_and_residueFieldMap_bijective_of_isEpi
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsEpi R S] :
    Function.Injective (comap (algebraMap R S)) ∧
      ∀ (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] (h : p = q.comap (algebraMap R S)),
        Function.Bijective (Ideal.ResidueField.map p q (algebraMap R S) h)

Tag 04VX, a lemma

Tag 04VX in the Stacks Project.

TensorProduct.sum_tmul_eq_zero_iff_exists_finsupp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/TensorProduct/SumTmulEqZero.lean, line 69.

Vanishing of a sum of pure tensors. Let x : I → M generate M and y : J → N generate N, and let m : J →₀ M be a finitely supported family. Then ∑_j m_j ⊗ y_j = 0 in M ⊗_R N if and only if there are scalars a_{ij}, only finitely many nonzero, such that m_j = ∑_i a_{ij} x_i for every j and ∑_j a_{ij} y_j = 0 for every i.

The proof tensors the exact sequence 0 → K → (J →₀ R) → N → 0 given by the y_j with M, and writes an element of M ⊗_R K as ∑_i x_i ⊗ k_i using the generators x_i.

theorem sum_tmul_eq_zero_iff_exists_finsupp {x : I → M}
    (hx : Submodule.span R (Set.range x) = ⊤) {y : J → N}
    (hy : Submodule.span R (Set.range y) = ⊤) (m : J →₀ M) :
    (m.sum fun j mj ↦ mj ⊗ₜ[R] y j) = 0 ↔
      ∃ a : I →₀ J →₀ R, (∀ j, m j = a.sum fun i aᵢ ↦ aᵢ j • x i) ∧
        ∀ i, ((a i).sum fun j r ↦ r • y j) = 0

Tag 04VY, a lemma

Tag 04VY in the Stacks Project.

tmul_one_eq_one_tmul_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/Cardinality.lean, line 1125.

For g : S, the identity g ⊗ 1 = 1 ⊗ g in S ⊗[R] S holds if and only if g = ∑ i, ∑ j, φ (xᵢⱼ) * yᵢ * zⱼ for some yᵢ, zⱼ : S and xᵢⱼ : R whose column sums ∑ i, φ (xᵢⱼ) * yᵢ and row sums ∑ j, φ (xᵢⱼ) * zⱼ all lie in the image of φ.

theorem tmul_one_eq_one_tmul_iff (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] (g : S) :
    (g ⊗ₜ[R] (1 : S) = (1 : S) ⊗ₜ[R] g) ↔
    (∃ (n : ℕ) (y z : Fin n → S) (x : Fin n → Fin n → R),
      g = ∑ i, ∑ j, (algebraMap R S (x i j)) * y i * z j ∧
      (∀ j, ∃ r : R, ∑ i, (algebraMap R S (x i j)) * y i = algebraMap R S r) ∧
      (∀ i, ∃ r : R, ∑ j, (algebraMap R S (x i j)) * z j = algebraMap R S r))

Tag 04W0, a lemma

Tag 04W0 in the Stacks Project.

epi_card_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/Cardinality.lean, line 828.

If f : R → S is an epimorphism of commutative rings, then |S| ≤ |R|.

theorem epi_card_le (R S : Type u) [CommRing R] [CommRing S] (f : R →+* S)
    (hf : Epi (CommRingCat.ofHom f)) :
    Cardinal.mk S ≤ Cardinal.mk R

Tag 08YS, a lemma

Tag 08YS in the Stacks Project.

CommRingCat.epi_tfae_restrictScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/RestrictionOfScalars.lean, line 129.

For a homomorphism R → S of commutative rings, the following are equivalent:

1. R → S is an epimorphism of (commutative) rings;
2. for all S-modules N₁, N₂, every R-linear map is S-linear, i.e. Hom_S(N₁,N₂) = Hom_R(N₁,N₂);
3. the restriction-of-scalars functor Mod_S → Mod_R is fully faithful.

theorem epi_tfae_restrictScalars :
    [ Epi (CommRingCat.ofHom (algebraMap R S)),
      ∀ (N₁ N₂ : Type (max u v)) [AddCommGroup N₁] [AddCommGroup N₂] [Module R N₁]
        [Module R N₂] [Module S N₁] [Module S N₂] [IsScalarTower R S N₁]
        [IsScalarTower R S N₂],
        Function.Surjective (LinearMap.restrictScalars R : (N₁ →ₗ[S] N₂) → N₁ →ₗ[R] N₂),
      Nonempty (ModuleCat.restrictScalars.{max u v} (algebraMap R S)).FullyFaithful
    ].TFAE

Sources

• Section 10.107, Tag 04VM
• AxiomMath/Stacks at 5ed82d14

LeanCommRingCat.epi_tfae · CategoryTheory.epi_comp · epi_includeLeftRingHom_of_epi · Algebra.IsEpi.tower_top · CommRingCat.epi_ofHom_iff_forall_prime · RingHom.surjective_iff_epi_and_finite · faithfullyFlat_epimorphism_isIso · Algebra.IsEpi.surjective_algebraMap_of_field

Section10.108 Pure ideals#

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

Tag 04PS, a lemma

Tag 04PS in the Stacks Project.

Ideal.pure_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/Pure.lean, line 427.

Characterizations of pure ideals. For an ideal I of a commutative ring R the following are equivalent: (1) I is pure, i.e. R ⧸ I is flat over R; (2) I ⊓ J = I * J for every ideal J; (3) the same for every finitely generated J; (4) the same for every principal J; (5) every x ∈ I satisfies x = x * y for some y ∈ I; (6) finitely many elements of I admit a common such y; (7) I localizes to ⊥ or to ⊤ at every prime; (8) the support of I is the complement of V(I); (9) I is the kernel of R → (1 + I)⁻¹R; (10) R ⧸ I is R-algebra isomorphic to a localization of R; (11) R ⧸ I is R-algebra isomorphic to (1 + I)⁻¹R.

public theorem Ideal.pure_tfae {R : Type*} [CommRing R] (I : Ideal R) :
    List.TFAE
      [I.Pure,
       ∀ J : Ideal R, I ⊓ J = I * J,
       ∀ J : Ideal R, J.FG → I ⊓ J = I * J,
       ∀ x : R, I ⊓ Ideal.span {x} = I * Ideal.span {x},
       ∀ x ∈ I, ∃ y ∈ I, x = x * y,
       ∀ s : Finset R, (s : Set R) ⊆ I → ∃ y ∈ I, ∀ x ∈ s, x = x * y,
       ∀ p : PrimeSpectrum R,
         I.map (algebraMap R (Localization.AtPrime p.asIdeal)) = ⊥ ∨
           I.map (algebraMap R (Localization.AtPrime p.asIdeal)) = ⊤,
       Module.support R I = (PrimeSpectrum.zeroLocus (I : Set R))ᶜ,
       RingHom.ker (algebraMap R
         (Localization (Submonoid.comap (Ideal.Quotient.mk I).toMonoidHom ⊥))) = I,
       ∃ S : Submonoid R, Nonempty ((R ⧸ I) ≃ₐ[R] Localization S),
       Nonempty ((R ⧸ I) ≃ₐ[R]
         Localization (Submonoid.comap (Ideal.Quotient.mk I).toMonoidHom ⊥))]

Tag 04PU, a lemma

Tag 04PU in the Stacks Project.

bijOn_zeroLocus_isPure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/Pure.lean, line 868.

(Stacks 04PU) The map I ↦ V(I) is a bijection between the set of pure ideals of R and the set of closed subsets of Spec(R) that are closed under generalizations. This packages the three claims above as a single Set.BijOn statement.

theorem bijOn_zeroLocus_isPure {R : Type*} [CommRing R] :
    Set.BijOn (fun I : Ideal R => zeroLocus (I : Set R))
      {I : Ideal R | I.IsPure}
      {Z : Set (PrimeSpectrum R) | IsClosed Z ∧ StableUnderGeneralization Z}

Tag 05KK, a lemma

Tag 05KK in the Stacks Project.

pure_fg_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/Pure.lean, line 938.

For an ideal I of a commutative ring R, the following are equivalent: I is pure and finitely generated; I is generated by an idempotent; I is pure with open vanishing locus; R ⧸ I is a projective R-module.

theorem pure_fg_tfae (R : Type*) [CommRing R] (I : Ideal R) :
    [ -- (1) `I` is pure and finitely generated
      I.IsPure ∧ I.FG,
      -- (2) `I` is generated by an idempotent
      ∃ e : R, e ^ 2 = e ∧ I = Ideal.span {e},
      -- (3) `I` is pure and `V(I)` is open in `Spec(R)`
      I.IsPure ∧ IsOpen (PrimeSpectrum.zeroLocus (I : Set R)),
      -- (4) `R/I` is a projective `R`-module
      Module.Projective R (R ⧸ I) ].TFAE

Tag 052U, a lemma

Tag 052U in the Stacks Project.

PrimeSpectrum.forall_isOpen_of_isClosed_of_stableUnderGeneralization_iff_forall_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/LocallyFree/FiniteFlat.lean, line 458. The attribute's comment: “Finite local freeness is spelled Module.Projective; see the module docstring.”.

Let R be a commutative ring. Every closed subset of Spec(R) that is stable under generalization is open if and only if every finite flat R-module is finite locally free, the latter being spelled "finite projective" (Stacks 00NX (2) ⇔ (7)).

public theorem forall_isOpen_of_isClosed_of_stableUnderGeneralization_iff_forall_projective
    (R : Type u) [CommRing R] :
    (∀ Z : Set (PrimeSpectrum R), IsClosed Z → StableUnderGeneralization Z → IsOpen Z) ↔
      ∀ (M : Type u) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Flat R M],
        Module.Projective R M

Sources

• Section 10.108, Tag 04PQ
• AxiomMath/Stacks at 5ed82d14

LeanIdeal.pure_tfae · bijOn_zeroLocus_isPure · pure_fg_tfae · PrimeSpectrum.forall_isOpen_of_isClosed_of_stableUnderGeneralization_iff_forall_projective

Section10.109 Rings of finite global dimension#

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

Tag 00O3, a lemma

Tag 00O3 in the Stacks Project.

schanuel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ProjectiveDimension.lean, line 923.

Schanuel's Lemma (Stacks Tag 00O3). Given two short exact sequences 0 → K → P₁ → M → 0 and 0 → L → P₂ → M → 0 with P₁, P₂ projective, there are R-linear isomorphisms φ : K × P₂ ≃ P₁ × L and ψ : P₁ × P₂ ≃ P₁ × P₂ fitting into a commutative diagram of short exact sequences whose right-hand vertical map is the identity on M.

theorem schanuel
    {R : Type*} [Ring R]
    {K L P₁ P₂ M : Type*}
    [AddCommGroup K] [AddCommGroup L] [AddCommGroup P₁] [AddCommGroup P₂] [AddCommGroup M]
    [Module R K] [Module R L] [Module R P₁] [Module R P₂] [Module R M]
    (c₁ : K →ₗ[R] P₁) (p₁ : P₁ →ₗ[R] M) (c₂ : L →ₗ[R] P₂) (p₂ : P₂ →ₗ[R] M)
    (hP₁ : Module.Projective R P₁) (hP₂ : Module.Projective R P₂)
    -- first short exact sequence `0 → K → P₁ → M → 0`
    (hc₁ : Function.Injective c₁) (hp₁ : Function.Surjective p₁)
    (hex₁ : Function.Exact c₁ p₁)
    -- second short exact sequence `0 → L → P₂ → M → 0`
    (hc₂ : Function.Injective c₂) (hp₂ : Function.Surjective p₂)
    (hex₂ : Function.Exact c₂ p₂) :
    ∃ (φ : (K × P₂) ≃ₗ[R] (P₁ × L)) (ψ : (P₁ × P₂) ≃ₗ[R] (P₁ × P₂)),
      let topLeft : (K × P₂) →ₗ[R] (P₁ × P₂) := c₁.prodMap LinearMap.id
      let topRight : (P₁ × P₂) →ₗ[R] M := LinearMap.coprod p₁ 0
      let botLeft : (P₁ × L) →ₗ[R] (P₁ × P₂) := LinearMap.id.prodMap c₂
      let botRight : (P₁ × P₂) →ₗ[R] M := LinearMap.coprod 0 p₂
      -- (1) both rows are short exact sequences
      (Function.Injective topLeft ∧ Function.Surjective topRight ∧
        Function.Exact topLeft topRight) ∧
      (Function.Injective botLeft ∧ Function.Surjective botRight ∧
        Function.Exact botLeft botRight) ∧
      -- (3a) left square commutes: `(id, c₂) ∘ φ = ψ ∘ (c₁, id)`
      (botLeft.comp φ.toLinearMap = ψ.toLinearMap.comp topLeft) ∧
      -- (3b) right square commutes: `(0, p₂) ∘ ψ = (p₁, 0)`
      (botRight.comp ψ.toLinearMap = topRight)

Tag 00O4, a definition

Tag 00O4 in the Stacks Project.

Module.projectiveDimension, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ProjectiveDimension/Defs.lean, line 136. References: EGA 0 (17.2.1), “dim.proj definition”.

The projective dimension of an R-module M: the least d with Ext^i(M, -) = 0 for all i > d. For R small in M's universe this is the source's invariant, the least d for which there is an exact sequence 0 → P_d → ⋯ → P_0 → M → 0 with all P_i projective (00O5, 0CXC), and M then has finite projective dimension in the sense of the source exactly when this is ≠ ⊤ (CategoryTheory.projectiveDimension_ne_top_iff). It is ⊥ for the zero module.

public noncomputable abbrev Module.projectiveDimension (R : Type u) [Ring R] (M : Type v)
    [AddCommGroup M] [Module R M] : WithBot ℕ∞

Tag 00O5, a lemma

Tag 00O5 in the Stacks Project.

pd_syzygy_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ProjectiveDimension.lean, line 1490. References: EGA 0 (17.2.1), “Necessity”.

Stacks Tag 00O5 / Lemma 10.109.3. Let M have projective dimension d and let F_e → ⋯ → F_0 → M → 0 be exact with every F_i projective and d ≤ e + 1. Then the leftmost syzygy Ker(F_e → F_{e-1}), or Ker(F_0 → M) when e = 0, is projective.

theorem pd_syzygy_projective (d e : ℕ)
    -- the truncated sequence `F_e → ⋯ → F_0 → M → 0`
    (S : ComposableArrows (ModuleCat R) (e + 2))
    -- `M`, the object at position `e + 1`, has projective dimension `d`
    (hpd : projectiveDimension (S.obj ⟨e + 1, by omega⟩) = (d : WithBot ℕ∞))
    -- the hypothesis `e ≥ d - 1`, equivalently `d ≤ e + 1`
    (hde : d ≤ e + 1)
    -- exactness at every internal object (in particular `F_0 → M` is surjective);
    -- note exactness is NOT imposed at the leftmost object `F_e`
    (hexact : S.Exact)
    -- the rightmost object (position `e + 2`) is the zero module
    (hzero : Limits.IsZero (S.obj (Fin.last (e + 2))))
    -- each `F_i` (positions `0, …, e`) is projective
    (hproj : ∀ i : Fin (e + 1), Projective (S.obj i.castSucc.castSucc)) :
    -- the leftmost syzygy `Ker(F_e → F_{e-1})` (or `Ker(F_0 → M)` when `e = 0`)
    -- is projective
    Projective (Limits.kernel (S.map' 0 1))

Tag 0CXC, a lemma

Tag 0CXC in the Stacks Project.

CategoryTheory.hasProjectiveDimensionLE_tfae_leftResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ProjectiveDimension.lean, line 659. The attribute's comment: “A resolution ⋯ → P₁ → P₀ → M → 0 is an ObjectProperty.LeftResolution by the class of projective objects (00LQ), the notion 00O7 uses; the source's M, Ker(P₀ → M) and Ker(P_{d-1} → P_{d-2}) are the single syzygy (F.complex.toSingle₀AsComplex X F.π).cycles d, the d-th cycles of the augmentation F.π read as a complex; see the module docstring.”. References: EGA 0 (17.2.1), “dim.proj resolution char”.

Stacks 0CXC. Let X be an object of an abelian category which admits a projective resolution, and let d : ℕ. The following are equivalent: (1) X has projective dimension at most d; (2) there is a resolution 0 → P_d → ⋯ → P₀ → X → 0 by projectives, that is, a left resolution F of X by projective objects with F.complex.X i = 0 for i > d; (3) for some resolution ⋯ → P₁ → P₀ → X → 0 by projectives the d-th syzygy of X, the d-th cycles object of the augmented complex, is projective; (4) for every such resolution the d-th syzygy is projective.

public theorem CategoryTheory.hasProjectiveDimensionLE_tfae_leftResolution {C : Type u}
    [Category.{v} C] [Abelian C] (X : C) [HasProjectiveResolution X] (d : ℕ) :
    List.TFAE
      [HasProjectiveDimensionLE X d,
        ∃ F : ObjectProperty.LeftResolution (isProjective C) X,
          ∀ i, d < i → Limits.IsZero (F.complex.X i),
        ∃ F : ObjectProperty.LeftResolution (isProjective C) X,
          Projective ((F.complex.toSingle₀AsComplex X F.π).cycles d),
        ∀ F : ObjectProperty.LeftResolution (isProjective C) X,
          Projective ((F.complex.toSingle₀AsComplex X F.π).cycles d)]

Tag 0CXD, a lemma

Tag 0CXD in the Stacks Project.

ModuleCat.hasProjectiveDimensionLE_iff_exists_leftResolution_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalRing/ProjectiveDimension.lean, line 177. The attribute's comment: “Condition (5) is added to Lemma 0CXC by stating its equivalence with item 1 of that lemma's TFAE. A resolution 0 → P_d → ⋯ → P₀ → M → 0 by frees is an ObjectProperty.LeftResolution for the class of free modules (00LQ), the notion 0CXC and 00O7 use, vanishing in degrees > d; see the module docstring.”.

Stacks 0CXD. Let R be a commutative local ring, let M be an R-module and let d : ℕ. Then M has projective dimension at most d — equivalently, by Stacks 0CXC, M has a resolution of length d by projectives — if and only if M has a resolution 0 → P_d → ⋯ → P₀ → M → 0 by free modules, that is, a left resolution F of M by free modules with F.complex.X i = 0 for i > d.

public theorem ModuleCat.hasProjectiveDimensionLE_iff_exists_leftResolution_free {R : Type u}
    [CommRing R] [IsLocalRing R] [Small.{v} R] (M : ModuleCat.{v} R) (d : ℕ) :
    HasProjectiveDimensionLE M d ↔
      ∃ F : ObjectProperty.LeftResolution (fun N : ModuleCat.{v} R => Module.Free R N) M,
        ∀ i, d < i → IsZero (F.complex.X i)

Tag 0CXE, a lemma

Tag 0CXE in the Stacks Project.

ModuleCat.hasProjectiveDimensionLE_iff_exists_leftResolution_projective_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ProjectiveDimension/FiniteResolution.lean, line 332. The attribute's comment: “Condition (6) is added to Lemma 0CXC by stating its equivalence with item 1 of that lemma's TFAE. A resolution 0 → P_d → ⋯ → P₀ → M → 0 by finite projectives is an ObjectProperty.LeftResolution for the class of finite projective modules (00LQ), the notion 0CXC, 0CXD and 00O7 use, vanishing in degrees > d; stated for a not necessarily commutative ring. See the module docstring.”. References: EGA 0 (17.2.2).

Stacks 0CXE. Let R be a Noetherian ring, let M be a finite R-module and let d : ℕ. Then M has projective dimension at most d — equivalently, by Stacks 0CXC, M has a resolution of length d by projectives — if and only if M has a resolution 0 → P_d → ⋯ → P₀ → M → 0 by finite projective modules, that is, a left resolution F of M by projective modules that are finite over R, with F.complex.X i = 0 for i > d.

public theorem ModuleCat.hasProjectiveDimensionLE_iff_exists_leftResolution_projective_finite
    {R : Type u} [Ring R] [IsNoetherianRing R] [Small.{v} R] (M : ModuleCat.{v} R)
    [Module.Finite R M] (d : ℕ) :
    HasProjectiveDimensionLE M d ↔
      ∃ F : ObjectProperty.LeftResolution
          (fun N : ModuleCat.{v} R => Projective N ∧ Module.Finite R N) M,
        ∀ i, d < i → IsZero (F.complex.X i)

Tag 0CXF, a lemma

Tag 0CXF in the Stacks Project.

ModuleCat.hasProjectiveDimensionLE_iff_exists_leftResolution_free_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalRing/ProjectiveDimension.lean, line 379. The attribute's comment: “Condition (7) is added to Lemmas 0CXC, 0CXD and 0CXE by stating its equivalence with item 1 of 0CXC's TFAE. A resolution 0 → F_d → ⋯ → F₀ → M → 0 by finite frees is an ObjectProperty.LeftResolution for the class of finite free modules (00LQ), the notion 00O7 uses, vanishing in degrees > d; see the module docstring.”. References: EGA 0 (17.2.2).

Stacks 0CXF. Let R be a local Noetherian ring, let M be a finite R-module and let d : ℕ. Then M has projective dimension at most d — equivalently, by Stacks 0CXC, 0CXD and 0CXE, M has a resolution of length d by projectives, by frees, or by finite projectives — if and only if M has a resolution 0 → F_d → ⋯ → F₀ → M → 0 by finite free modules, that is, a left resolution F of M by free modules that are finite over R, with F.complex.X i = 0 for i > d.

public theorem ModuleCat.hasProjectiveDimensionLE_iff_exists_leftResolution_free_finite
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v} R]
    (M : ModuleCat.{v} R) [Module.Finite R M] (d : ℕ) :
    HasProjectiveDimensionLE M d ↔
      ∃ F : ObjectProperty.LeftResolution
          (fun N : ModuleCat.{v} R => Module.Free R N ∧ Module.Finite R N) M,
        ∀ i, d < i → IsZero (F.complex.X i)

Tag 065R, a lemma

Tag 065R in the Stacks Project.

CategoryTheory.hasProjectiveDimensionLT_of_enoughProjectives, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/Projective/Dimension.lean, line 103. The attribute's comment: “The implication (3) ⇒ (1), proved the source's way: in an abelian category with enough projectives, indexed by HasProjectiveDimensionLT X n, so that the source's R-modules of projective dimension ≤ n are the case C = ModuleCat.{v} R at n + 1. The converse (1) ⇒ (2) and, at a single degree, (2) ⇒ (3) are hasProjectiveDimensionLT_iff; the sibling under enough injectives is hasProjectiveDimensionLT_of_enoughInjectives. Projective dimension is Ext-measured here rather than defined by a finite projective resolution (Definition 00O4, Lemma 0CXC); see the module docstring.”.

Let X be an object of an abelian category with enough projectives and let n : ℕ. If the single group Extⁿ(X, Y) vanishes for every object Y, then X has projective dimension < n.

public theorem CategoryTheory.hasProjectiveDimensionLT_of_enoughProjectives {C : Type u}
    [Category.{v} C] [Abelian C] [HasExt.{w} C] [EnoughProjectives C] (X : C) (n : ℕ)
    (hX : ∀ Y : C, Subsingleton (Ext.{w} X Y n)) : HasProjectiveDimensionLT X n

Tag 065S, a lemma

Tag 065S in the Stacks Project.

Declarations registered for the tag:

• CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₁ registered with add_to_stacks in StacksFrontier/Algebra/Homology/ProjectiveDimension.lean, line 1785 (StacksFrontier): “(1)”.
• CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₂ registered with add_to_stacks in StacksFrontier/Algebra/Homology/ProjectiveDimension.lean, line 1786 (StacksFrontier): “(2)”.
• CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃ registered with add_to_stacks in StacksFrontier/Algebra/Homology/ProjectiveDimension.lean, line 1787 (StacksFrontier): “(3)”.

Tag 00O6, a definition

Tag 00O6 in the Stacks Project.

ringGlobalDimension, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GlobalDimension/Defs.lean, line 128. The attribute's comment: “The global dimension is the supremum ⨆ M, projectiveDimension M over the R-modules in R's own universe; R has finite global dimension iff this is ≠ ⊤. See the module docstring.”.

The global dimension of a ring R: the supremum of the projective dimensions of all R-modules, an element of WithBot ℕ∞. It is ≤ n exactly when every R-module admits a resolution of length ≤ n by projective modules (00O5, 0CXC), so it is the source's minimal such n, and R has finite global dimension exactly when ringGlobalDimension R ≠ ⊤. It is ⊥ for the zero ring.

public noncomputable abbrev ringGlobalDimension (R : Type u) [Ring R] : WithBot ℕ∞

Tag 0D1U, a lemma

Tag 0D1U in the Stacks Project.

ModuleCat.hasProjectiveDimensionLT_of_monotone_of_iSup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ProjectiveDimension/Filtration.lean, line 637. The attribute's comment: “Indexed by HasProjectiveDimensionLT _ n, so that the source's ≤ n is the case n + 1; the source's well-ordered family of submodules is a Monotone family over a type with [LinearOrder E] [WellFoundedLT E], its union is ⨆ e, N e = ⊤, and the graded piece at e is ↥(N e) ⧸ (⨆ e' < e, N e').submoduleOf (N e). See the module docstring.”.

Stacks 0D1U. Let R be a ring and let M be an R-module which is the union ⨆ e, N e = ⊤ of a monotone family of submodules N indexed by a well-ordered type E. If each graded piece N e ⧸ ⨆ e' < e, N e' has projective dimension < n, then so does M.

public theorem ModuleCat.hasProjectiveDimensionLT_of_monotone_of_iSup_eq_top {R : Type u} [Ring R]
    [Small.{v} R] {M : ModuleCat.{v} R} {E : Type w} [LinearOrder E] [WellFoundedLT E]
    (N : E → Submodule R M) (hN : Monotone N) (hNtop : ⨆ e, N e = ⊤) (n : ℕ)
    (hquot : ∀ e, HasProjectiveDimensionLT
      (ModuleCat.of R (↥(N e) ⧸ (⨆ e' < e, N e').submoduleOf (N e))) n) :
    HasProjectiveDimensionLT M n

Tag 065T, a lemma

Tag 065T in the Stacks Project.

ringGlobalDimension_lt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GlobalDimension/Cyclic.lean, line 273. The attribute's comment: “Indexed by HasProjectiveDimensionLT _ n, so that the source's ≤ n is the case n + 1; item (1) is the global dimension ⨆ M, projectiveDimension M of Tag 00O6, and the modules of items (2) and (3) range over an arbitrary universe v with Small.{v} R, of which the source is the case v = u. See the module docstring.”. References: EGA 0 (17.2.8), “a) <=> a')”.

Stacks 065T. Let R be a ring and n : ℕ. The following are equivalent: the global dimension of R is < n; every R-module has projective dimension < n; every finite R-module has projective dimension < n; every cyclic R-module R ⧸ I has projective dimension < n. The source's bound ≤ n is the case n + 1.

public theorem ringGlobalDimension_lt_tfae (R : Type u) [Ring R] [Small.{v} R] (n : ℕ) :
    List.TFAE
      [(⨆ M : ModuleCat.{u} R, projectiveDimension M) < n,
       ∀ M : ModuleCat.{v} R, HasProjectiveDimensionLT M n,
       ∀ M : ModuleCat.{v} R, Module.Finite R M → HasProjectiveDimensionLT M n,
       ∀ I : Ideal R, HasProjectiveDimensionLT (ModuleCat.of R (R ⧸ I)) n]

Tag 00O8, a lemma

Tag 00O8 in the Stacks Project.

projectiveDimension_localization_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ProjectiveDimension.lean, line 1728. The attribute's comment: “(1)”. References: EGA 0 (17.2.5), “partial”; EGA IV (6.2.1), “(i), special case”.

Statement 1. If M has projective dimension ≤ n as an R-module, then the localization S⁻¹M has projective dimension ≤ n as an S⁻¹R-module.

Proof by induction on n: base case proved inline (projective localizes to projective); inductive step is projectiveDimension_localization_le_step. The induction generalizes M so the hypothesis applies to the syzygy K at the next level.

theorem projectiveDimension_localization_le
    (R : Type u) [CommRing R] (S : Submonoid R)
    (M : Type u) [AddCommGroup M] [Module R M] (n : ℕ)
    (hM : ModuleProjectiveDimensionLE R M n) :
    ModuleProjectiveDimensionLE (Localization S) (LocalizedModule S M) n

globalDimension_localization_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ProjectiveDimension.lean, line 1759. The attribute's comment: “(2)”. References: EGA 0 (17.2.10), “partial”.

Statement 2. If R has global dimension ≤ n, then S⁻¹R has global dimension ≤ n.

This reduces to Statement 1. Let X : ModuleCat (S⁻¹R) be arbitrary, with underlying type M'. View M' as an R-module by restriction of scalars along algebraMap R (S⁻¹R) (Module.compHom, giving IsScalarTower R (S⁻¹R) M'). Every S⁻¹R-module is its own localization: isLocalizedModule_id S M' (Localization S) gives IsLocalizedModule S (LinearMap.id : M' →ₗ[R] M'), whence IsLocalizedModule.iso S LinearMap.id : LocalizedModule S M' ≃ₗ[R] M', upgraded to a Localization S-linear equivalence by LinearEquiv.extendScalarsOfIsLocalization S (Localization S). This linear equivalence yields an isomorphism e : ModuleCat.of (S⁻¹R) (LocalizedModule S M') ≅ X in ModuleCat (S⁻¹R) (LinearEquiv.toModuleIso). By hR (applied to ModuleCat.of R M'), M' has pd_R M' ≤ n, i.e. ModuleProjectiveDimensionLE R M' n. Statement 1 gives ModuleProjectiveDimensionLE (S⁻¹R) (LocalizedModule S M') n, i.e. HasProjectiveDimensionLT (ModuleCat.of (S⁻¹R) (LocalizedModule S M')) (n+1). Transport across e with hasProjectiveDimensionLT_of_iso to obtain HasProjectiveDimensionLT X (n+1).

theorem globalDimension_localization_le
    (R : Type u) [CommRing R] (S : Submonoid R) (n : ℕ)
    (hR : RingGlobalDimensionLE R n) :
    RingGlobalDimensionLE (Localization S) n

Sources

• Section 10.109, Tag 00O2
• AxiomMath/Stacks at 5ed82d14

Leanschanuel · Module.projectiveDimension · pd_syzygy_projective · CategoryTheory.hasProjectiveDimensionLE_tfae_leftResolution · ModuleCat.hasProjectiveDimensionLE_iff_exists_leftResolution_free · ModuleCat.hasProjectiveDimensionLE_iff_exists_leftResolution_projective_finite · ModuleCat.hasProjectiveDimensionLE_iff_exists_leftResolution_free_finite · CategoryTheory.hasProjectiveDimensionLT_of_enoughProjectives

Section10.110 Regular rings and global dimension#

Section 10.110 of the Stacks Project, Tag 065U. 9 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00O7, a proposition

Tag 00O7 in the Stacks Project.

Stacks.RegularLocalRing.ShortFreeResolution.solution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/GlobalDimension.lean, line 219. The attribute's comment: “Stated with ringKrullDim R ≤ d and e ≤ depth_𝔪(M); see the module docstring of the statement file.”. References: EGA 0 (17.3.4), “dim.proj ≤ n - prof”; SGA 2 IV (5.3), “partial”; SGA 6 IX (1.5), “partial”.

Stacks 00O7. Let R be a regular local ring of dimension at most d. Every finite R-module M whose 𝔪-depth is at least e has a resolution 0 → F_{d-e} → ⋯ → F_0 → M → 0 by finite free R-modules, and every R-module has projective dimension at most d.

public theorem solution {R : Type u} [CommRing R] [IsRegularLocalRing R] {d : ℕ}
    (hd : ringKrullDim R ≤ (d : WithBot ℕ∞)) :
    (∀ (M : ModuleCat.{u} R) [Module.Finite R M] (e : ℕ),
        (e : ℕ∞) ≤ Module.depth R (maximalIdeal R) M →
        ∃ F : ObjectProperty.LeftResolution
            (fun N : ModuleCat.{u} R => Module.Free R N ∧ Module.Finite R N) M,
          ∀ i, d - e < i → IsZero (F.complex.X i)) ∧
      ∀ M : ModuleCat.{u} R, HasProjectiveDimensionLE M d

IsRegularLocalRing.exists_leftResolution_free_finite_and_hasProjectiveDimensionLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/GlobalDimension.lean, line 366. The attribute's comment: “Stated with ringKrullDim R ≤ d and e ≤ depth_𝔪(M); the length d - e of the resolution is the vanishing of its terms in degrees > d - e, and R having global dimension ≤ d is ∀ M, HasProjectiveDimensionLE M d. See the module docstring.”. References: EGA 0 (17.3.4), “dim.proj ≤ n - prof”; EGA 0 (17.3.1), “Sufficiency, partial”; SGA 2 IV (5.3), “partial”; SGA 6 IX (1.5), “partial”.

Stacks 00O7. Let R be a regular local ring of dimension at most d. Every finite R-module M whose 𝔪-depth is at least e has a resolution 0 → F_{d-e} → ⋯ → F_0 → M → 0 by finite free R-modules, and every R-module has projective dimension at most d; that is, R has global dimension at most d.

public theorem IsRegularLocalRing.exists_leftResolution_free_finite_and_hasProjectiveDimensionLE
    {R : Type u} [CommRing R] [IsRegularLocalRing R] {d : ℕ}
    (hd : ringKrullDim R ≤ (d : WithBot ℕ∞)) :
    (∀ (M : ModuleCat.{u} R) [Module.Finite R M] (e : ℕ),
        (e : ℕ∞) ≤ Module.depth R (maximalIdeal R) M →
        ∃ F : ObjectProperty.LeftResolution
            (fun N : ModuleCat.{u} R => Module.Free R N ∧ Module.Finite R N) M,
          ∀ i, d - e < i → IsZero (F.complex.X i)) ∧
      ∀ M : ModuleCat.{u} R, HasProjectiveDimensionLE M d

Tag 00O9, a lemma

Tag 00O9 in the Stacks Project.

Ring.forall_hasProjectiveDimensionLE_iff_forall_isLocalization_maximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GlobalDimension/Localization.lean, line 289.

Global dimension of a Noetherian ring is detected at the maximal ideals. For a Noetherian ring R and n : ℕ, every R-module has projective dimension ≤ n if and only if, for every maximal ideal 𝔪 of R, every module over the localization R_𝔪 has projective dimension ≤ n. Taking ∃ n on both sides gives the source's statement that R has finite global dimension iff the global dimensions of the R_𝔪 are bounded.

public theorem Ring.forall_hasProjectiveDimensionLE_iff_forall_isLocalization_maximal
    {R : Type u} [CommRing R] [IsNoetherianRing R] (n : ℕ)
    (Rₘ : (𝔪 : Ideal R) → [𝔪.IsMaximal] → Type v)
    [∀ (𝔪 : Ideal R) [𝔪.IsMaximal], CommRing (Rₘ 𝔪)]
    [∀ (𝔪 : Ideal R) [𝔪.IsMaximal], Algebra R (Rₘ 𝔪)]
    [∀ (𝔪 : Ideal R) [𝔪.IsMaximal], IsLocalization.AtPrime (Rₘ 𝔪) 𝔪] :
    (∀ M : ModuleCat.{u} R, HasProjectiveDimensionLE M n) ↔
      ∀ (𝔪 : Ideal R) [𝔪.IsMaximal] (M : ModuleCat.{v} (Rₘ 𝔪)),
        HasProjectiveDimensionLE M n

Tag 00OA, a lemma

Tag 00OA in the Stacks Project.

IsLocalRing.finrank_cotangentSpace_le_projectiveDimension_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalRing/EmbeddingDimension.lean, line 765. The attribute's comment: “dim_κ 𝔪/𝔪² is the finrank of IsLocalRing.CotangentSpace R over IsLocalRing.ResidueField R, and pd_R κ is CategoryTheory.projectiveDimension of κ in ModuleCat R, valued in WithBot ℕ∞. See the module docstring.”.

The projective dimension of the residue field bounds the embedding dimension. For a Noetherian local ring (R, 𝔪, κ), the projective dimension of κ as an R-module is at least dim_κ 𝔪/𝔪², the dimension of the cotangent space of R.

public theorem finrank_cotangentSpace_le_projectiveDimension_residueField
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] :
    (Module.finrank (ResidueField R) (CotangentSpace R) : WithBot ℕ∞) ≤
      projectiveDimension (ModuleCat.of R (ResidueField R))

Tag 00OB, a lemma

Tag 00OB in the Stacks Project.

Module.projectiveDimension_le_ringKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ProjectiveDimension/KrullDimension.lean, line 187. The attribute's comment: “Stated for an arbitrary finite module M rather than only for κ, the source's proof using nothing else; pd_R M is Module.projectiveDimension (Tag 00O4) and finiteness of it is ≠ ⊤. See the module docstring.”.

Finite projective dimension is bounded by the dimension. Let (R, 𝔪) be a Noetherian local ring and let M be a finite R-module of finite projective dimension. Then pd_R M ≤ dim R. The source states the case M = κ, for which the inequality is an equality (Proposition 00OC).

public theorem projectiveDimension_le_ringKrullDim {R : Type u} [CommRing R] [IsNoetherianRing R]
    [IsLocalRing R] [Small.{v} R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (hM : projectiveDimension R M ≠ ⊤) :
    projectiveDimension R M ≤ ringKrullDim R

Tag 00OC, a proposition

Tag 00OC in the Stacks Project.

isRegularLocalRing_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/GlobalDimension.lean, line 595. The attribute's comment: “Global dimension is the supremum of the projective dimensions of all R-modules (Mathlib has no name for it) and "finite" is ≠ ⊤; dim_κ 𝔪/𝔪² is the finrank of IsLocalRing.CotangentSpace R over IsLocalRing.ResidueField R. The source's two "moreover" equalities are items (4) and (5) of the list, each of which implies the other three. See the module docstring.”. References: EGA 0 (17.3.1).

Serre's characterisation of regular local rings (Stacks 00OC). For a Noetherian local ring (R, 𝔪, κ) the following are equivalent: (1) κ has finite projective dimension over R; (2) R has finite global dimension; (3) R is a regular local ring; (4) the global dimension of R is dim R; (5) the global dimension of R is dim_κ 𝔪/𝔪². Items (4) and (5) are the source's final sentence, and together they give gl dim R = dim R = dim_κ 𝔪/𝔪².

public theorem isRegularLocalRing_tfae {R : Type u} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] :
    List.TFAE
      [projectiveDimension (ModuleCat.of R (ResidueField R)) ≠ ⊤,
       (⨆ M : ModuleCat.{u} R, projectiveDimension M) ≠ ⊤,
       IsRegularLocalRing R,
       (⨆ M : ModuleCat.{u} R, projectiveDimension M) = ringKrullDim R,
       (⨆ M : ModuleCat.{u} R, projectiveDimension M) =
         (Module.finrank (ResidueField R) (CotangentSpace R) : WithBot ℕ∞)]

Tag 0AFS, a lemma

Tag 0AFS in the Stacks Project.

IsLocalRing.isRegularRing_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularRing/GlobalDimension.lean, line 625. The attribute's comment: “Both sentences of the source as one List.TFAE: (1) ↔ (2) is the equivalence of regularity with finiteness of the global dimension, and (1) → (3) is "R_𝔭 is a regular local ring for all primes 𝔭", spelled with Mathlib's IsRegularRing (Definition 00OD). Global dimension is the supremum of the projective dimensions of all R-modules, Mathlib having no name for it, and "finite" is ≠ ⊤. See the module docstring.”. References: EGA 0 (17.3.1), “fin. coh. dim ⇔ regular”; EGA 0 (17.3.1), “fin. coh. dim ⇔ regular”.

A regular local ring is a regular ring (Stacks 0AFS). For a Noetherian local ring R the following are equivalent: (1) R is a regular local ring; (2) R has finite global dimension; (3) R is a regular ring, that is, R_𝔭 is a regular local ring for every prime 𝔭 of R.

public theorem IsLocalRing.isRegularRing_tfae {R : Type u} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] :
    List.TFAE
      [IsRegularLocalRing R,
       (⨆ M : ModuleCat.{u} R, projectiveDimension M) ≠ ⊤,
       IsRegularRing R]

Tag 00OD, a definition

Tag 00OD in the Stacks Project.

IsRegularRing.isRegularLocalRing_of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularRing/Defs.lean, line 114. The attribute's comment: “Definition 00OD is Mathlib's class IsRegularRing, which is the source's sentence verbatim (IsNoetherianRing R plus IsRegularLocalRing (Localization.AtPrime p) for every prime p), so no predicate is redefined here. Its defining field pins the concrete model Localization.AtPrime p, while the source says "the localizations R_𝔭"; this is the definition in that model-independent form, universe-polymorphic in the localization. See the module docstring.”.

A localization of a regular ring at a prime is a regular local ring (Stacks 00OD). A Noetherian ring R is regular when all of its localizations R_𝔭 at primes are regular local rings; read for an arbitrary model S of R_𝔭, that is the statement below.

public theorem IsRegularRing.isRegularLocalRing_of_isLocalization {R : Type u} [CommRing R]
    [IsRegularRing R] (p : Ideal R) [p.IsPrime] (S : Type v) [CommRing S] [Algebra R S]
    [IsLocalization.AtPrime S p] : IsRegularLocalRing S

Tag 00OE, a lemma

Tag 00OE in the Stacks Project.

isRegularRing_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularRing/GlobalDimension.lean, line 440. The attribute's comment: “Stated for a fixed n : ℕ: the source re-quantifies n existentially in items (3) and (4), but "with equality for at least one 𝔪" pins it, and exists_congr on n recovers the source's reading. Global dimension is the supremum of the projective dimensions of all R-modules, Mathlib having no name for it; "regular" is IsRegularRing (Definition 00OD) and dimensions are ringKrullDim. See the module docstring.”.

A Noetherian ring has global dimension n if and only if it is regular of dimension n (Stacks 00OE). For a Noetherian ring R and n : ℕ the following are equivalent: (1) the global dimension of R is n; (2) R is a regular ring and dim R = n; (3) every localization R_𝔪 at a maximal ideal is a regular local ring of dimension ≤ n, with dim R_𝔪 = n for at least one 𝔪; (4) the same for the localizations at all primes.

public theorem isRegularRing_tfae {R : Type u} [CommRing R] [IsNoetherianRing R] (n : ℕ) :
    List.TFAE
      [(⨆ M : ModuleCat.{u} R, projectiveDimension M) = (n : WithBot ℕ∞),
       IsRegularRing R ∧ ringKrullDim R = (n : WithBot ℕ∞),
       (∀ 𝔪 : Ideal R, ∀ _ : 𝔪.IsMaximal, IsRegularLocalRing (Localization.AtPrime 𝔪) ∧
            ringKrullDim (Localization.AtPrime 𝔪) ≤ (n : WithBot ℕ∞)) ∧
         ∃ 𝔪 : Ideal R, ∃ _ : 𝔪.IsMaximal,
           ringKrullDim (Localization.AtPrime 𝔪) = (n : WithBot ℕ∞),
       (∀ 𝔭 : Ideal R, ∀ _ : 𝔭.IsPrime, IsRegularLocalRing (Localization.AtPrime 𝔭) ∧
            ringKrullDim (Localization.AtPrime 𝔭) ≤ (n : WithBot ℕ∞)) ∧
         ∃ 𝔭 : Ideal R, ∃ _ : 𝔭.IsPrime,
           ringKrullDim (Localization.AtPrime 𝔭) = (n : WithBot ℕ∞)]

Tag 00OF, a lemma

Tag 00OF in the Stacks Project.

IsRegularLocalRing.of_flat_of_isLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/FlatLocalHom.lean, line 518. The attribute's comment: “The source's "local Noetherian and regular" for S is the single class IsRegularLocalRing S (Definition 00KU), which extends IsLocalRing and IsNoetherianRing; the homomorphism is algebraMap R S, flat as Module.Flat R S and local as IsLocalHom (algebraMap R S), the hypothesis pair of Module.FaithfullyFlat.of_flat_of_isLocalHom. See the module docstring.”. References: SGA 1 I (9.1), “B regular ⇒ A regular”.

Regularity descends along a flat local homomorphism (Stacks 00OF). Let R → S be a local homomorphism of local Noetherian rings. If it is flat and S is regular, then R is regular.

public theorem IsRegularLocalRing.of_flat_of_isLocalHom {R : Type u} (S : Type v) [CommRing R]
    [CommRing S] [IsLocalRing R] [IsNoetherianRing R] [Algebra R S] [Module.Flat R S]
    [IsLocalHom (algebraMap R S)] [IsRegularLocalRing S] : IsRegularLocalRing R

Sources

• Section 10.110, Tag 065U
• AxiomMath/Stacks at 5ed82d14

LeanStacks.RegularLocalRing.ShortFreeResolution.solution · IsRegularLocalRing.exists_leftResolution_free_finite_and_hasProjectiveDimensionLE · Ring.forall_hasProjectiveDimensionLE_iff_forall_isLocalization_maximal · IsLocalRing.finrank_cotangentSpace_le_projectiveDimension_residueField · Module.projectiveDimension_le_ringKrullDim · isRegularLocalRing_tfae · IsLocalRing.isRegularRing_tfae · IsRegularRing.isRegularLocalRing_of_isLocalization

Section10.111 Auslander-Buchsbaum#

Section 10.111 of the Stacks Project, Tag 090U. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 090V, a proposition

Tag 090V in the Stacks Project.

Module.projectiveDimension_add_depth_eq_depth_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ProjectiveDimension/AuslanderBuchsbaum.lean, line 755. The attribute's comment: “Stated with the sum on the left, in WithBot ℕ∞, for Module.projectiveDimension (Tag 00O4) and Module.depth along the maximal ideal (Tag 00LI). See the module docstring.”. References: EGA 0 (17.3.4), “more general”.

The Auslander-Buchsbaum formula. Let (R, 𝔪) be a Noetherian local ring and let M be a nonzero finite R-module of finite projective dimension. Then pd_R(M) + depth_𝔪(M) = depth_𝔪(R). The equality is read in WithBot ℕ∞; the hypotheses make all three quantities finite.

public theorem projectiveDimension_add_depth_eq_depth_self {R : Type u} [CommRing R]
    [IsNoetherianRing R] [IsLocalRing R] [Small.{v} R] (M : Type v) [AddCommGroup M] [Module R M]
    [Module.Finite R M] [Nontrivial M] (hM : projectiveDimension R M ≠ ⊤) :
    projectiveDimension R M + (depth R (IsLocalRing.maximalIdeal R) M : WithBot ℕ∞) =
      (depth R (IsLocalRing.maximalIdeal R) R : WithBot ℕ∞)

Sources

• Section 10.111, Tag 090U
• AxiomMath/Stacks at 5ed82d14

LeanModule.projectiveDimension_add_depth_eq_depth_self

Section10.112 Homomorphisms and dimension#

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

Tag 00OH, a lemma

Tag 00OH in the Stacks Project.

ringKrullDim_le_of_goingUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/GoingUpGoingDown.lean, line 158. References: EGA IV (5.4.1), “(ii), special case”.

Going-up version. If φ : R → S satisfies going up and the induced map Spec(S) → Spec(R) is surjective, then dim(R) ≤ dim(S).

This follows from chain_lift_goingUp through krullDim_le_of_chain_lift, since ringKrullDim R is krullDim (PrimeSpectrum R) by definition.

theorem ringKrullDim_le_of_goingUp (φ : R →+* S) (hup : GoingUp_00oh φ)
    (hsurj : Function.Surjective (PrimeSpectrum.comap φ)) :
    ringKrullDim R ≤ ringKrullDim S

ringKrullDim_le_of_goingDown, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/GoingUpGoingDown.lean, line 169. References: EGA IV (5.4.1), “(ii), special case”.

Going-down version. If φ : R → S satisfies going down and the induced map Spec(S) → Spec(R) is surjective, then dim(R) ≤ dim(S).

This follows from chain_lift_goingDown through krullDim_le_of_chain_lift.

theorem ringKrullDim_le_of_goingDown (φ : R →+* S) (hdown : GoingDown_00oh φ)
    (hsurj : Function.Surjective (PrimeSpectrum.comap φ)) :
    ringKrullDim R ≤ ringKrullDim S

Tag 00OI, a lemma

Tag 00OI in the Stacks Project.

comap_isMaximal_of_goingUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/GoingUpGoingDown.lean, line 208.

Stacks Tag 00OI. If φ : R → S satisfies going up and q ⊆ S is a maximal ideal, then its contraction φ⁻¹(q) is a maximal ideal of R.

theorem comap_isMaximal_of_goingUp (φ : R →+* S) (hφ : GoingUp φ)
    (q : Ideal S) (hq : q.IsMaximal) :
    (Ideal.comap φ q).IsMaximal

Tag 00OJ, a lemma

Tag 00OJ in the Stacks Project.

integral_dim_up, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/GoingUpGoingDown.lean, line 259. References: EGA 0 (16.1.5), “dim(B) ≤ dim(A)”; EGA IV (4.1.2), “(ii), special case”; EGA IV (5.4.2), “Affine case”; EGA IV (5.4.3), “dim(B) ≤ dim(A)”; EGA IV (5.5.1), “special case”; EGA IV (5.5.2), “special case”; EGA IV (5.6.6), “special case”.

Stacks Tag 00OJ. If f : R → S is a ring map making S integral over R, then ringKrullDim S ≤ ringKrullDim R and every closed point of Spec(S) contracts to a closed point of Spec(R).

theorem integral_dim_up
    {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S)
    (hf : f.IsIntegral) :
    ringKrullDim S ≤ ringKrullDim R ∧
    ∀ q : PrimeSpectrum S, IsClosed ({q} : Set (PrimeSpectrum S)) →
      IsClosed ({PrimeSpectrum.comap f q} : Set (PrimeSpectrum R))

Tag 00OK, a lemma

Tag 00OK in the Stacks Project.

Algebra.IsIntegral.ringKrullDim_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/IntegralExtension.lean, line 215. The attribute's comment: “The source's ring inclusion R ⊆ S is stated as an R-algebra S with algebraMap R S injective, spelled FaithfulSMul R S; see the module docstring.”. References: EGA 0 (16.1.5), “ρ injective case”; EGA 0 (16.1.5), “ρ injective case”; EGA IV (5.4.3), “more general”.

Stacks 00OK. If S is an integral R-algebra whose structure map R → S is injective (for instance an integral ring extension R ⊆ S), then R and S have the same Krull dimension.

public theorem Algebra.IsIntegral.ringKrullDim_eq (R S : Type*) [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsIntegral R S] [FaithfulSMul R S] :
    ringKrullDim R = ringKrullDim S

Tag 00OL, a definition

Tag 00OL in the Stacks Project.

Declarations registered for the tag:

• Ideal.Fiber registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch10.lean, line 237 (StacksFrontier): “the fibre ring S ⊗_R κ(p) (written κ(p) ⊗_R S)”. References: EGA III (4.6.2), “special case”; EGA IV (7.3.13), “more general”; EGA IV (12.1.1.4), “special case”; EGA IV (15.1.1), “affine, special case”; EGA IV (15.4.1), “special case”; EGA IV (1.8.6), “affine case”; EGA IV (2.2.1), “special case”; EGA IV (2.5.5), “affine fiber module”; EGA IV (3.3.1), “special case”; SGA 1 II (4.8), “more general”; SGA 1 III (1.7); SGA 7 VI (5.1).
• PrimeSpectrum.primesOverOrderIsoFiber registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch10.lean, line 238 (StacksFrontier): “primes q of S lying over p = primes of the fibre ring (inverse: comap along S -> κ(p) ⊗_R S)”.
• Ideal.Fiber.localizationAlgEquivQuotient registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch10.lean, line 240 (StacksFrontier): “(S ⊗_R κ(p))_q = S_q / p S_q, with q the prime of S under the fibre prime”.
• Localization.AtPrime.isLocalRing registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch10.lean, line 242 (StacksFrontier): “the localization at a prime is a local ring”. References: EGA 0 (10.3.1.1), “B is a local ring”; EGA 0 (1.2.3), “A_p is a local ring”; EGA 0 (1.2.7), “A_p is local”; EGA 0 (7.6.17), “special case”; EGA I (1.1.1), “A_x is a local ring”; SGA 3 VIIB (0.1.1), “partial”.

Tag 031E, a lemma

Tag 031E in the Stacks Project.

isRegularLocalRing_of_flat_of_closedFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/FlatLocalHom.lean, line 268. References: EGA IV (6.5.2), “(ii), local case”; EGA IV (7.5.1.1), “special case”; SGA 1 I (9.1), “A regular ⇒ B regular”.

Let φ : R → S be a local homomorphism of local Noetherian rings such that: 1. R is regular, 2. the closed fibre S / m_R S is regular, and 3. φ : R → S is flat. Then S is regular.

theorem isRegularLocalRing_of_flat_of_closedFibre (R S : Type*) [CommRing R] [CommRing S]
    [IsLocalRing R] [IsNoetherianRing R] [IsLocalRing S] [IsNoetherianRing S]
    [Algebra R S] [IsLocalHom (algebraMap R S)]
    (hR : IsRegularLocalRing R)
    (hfibre : IsRegularLocalRing (ClosedFibre R S))
    (hflat : Module.Flat R S) :
    IsRegularLocalRing S

Tag 00R5, a lemma

Tag 00R5 in the Stacks Project.

Module.isMaximalCohenMacaulay_self_and_ringKrullDim_eq_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/FlatLocalHom.lean, line 206. The attribute's comment: “Cohen-Macaulayness of a Noetherian local ring A (Definition 00N8) is Module.IsMaximalCohenMacaulay A A, i.e. depth_{𝔪_A}(A) = dim A; the source's two alternatives are the disjunctive hypothesis h over the flatness common to both. See the module docstring.”. References: EGA 0 (17.3.5), “(ii) necessity”.

Stacks 00R5. Let R → S be a local homomorphism of Noetherian local rings with R Cohen–Macaulay, i.e. depth_{𝔪_R}(R) = dim(R). If S is flat over R and is either finite over R or of dimension at most dim(R), then S is Cohen–Macaulay and dim(R) = dim(S).

public theorem Module.isMaximalCohenMacaulay_self_and_ringKrullDim_eq_of_flat
    {R S : Type*} [CommRing R] [CommRing S] [IsNoetherianRing R] [IsNoetherianRing S]
    [IsLocalRing R] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)]
    [Module.Flat R S] (hR : Module.IsMaximalCohenMacaulay R R)
    (h : Module.Finite R S ∨ ringKrullDim S ≤ ringKrullDim R) :
    Module.IsMaximalCohenMacaulay S S ∧ ringKrullDim R = ringKrullDim S

Sources

• Section 10.112, Tag 00OG
• AxiomMath/Stacks at 5ed82d14

LeanringKrullDim_le_of_goingUp · ringKrullDim_le_of_goingDown · comap_isMaximal_of_goingUp · integral_dim_up · Algebra.IsIntegral.ringKrullDim_eq · Ideal.Fiber · PrimeSpectrum.primesOverOrderIsoFiber · Ideal.Fiber.localizationAlgEquivQuotient

Section10.113 The dimension formula#

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

Tag 02IJ, a lemma

Tag 02IJ in the Stacks Project.

height_add_trdeg_residue_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DimensionFormula/GeneratorInduction.lean, line 790. References: EGA IV (13.3.4), “partial”; EGA IV (5.5.6), “partial”; EGA IV (5.5.7), “more general”; EGA IV (5.5.8), “more general”; EGA IV (5.6.5), “special case”.

Stacks 02IJ. For R Noetherian, S a finite-type domain extension of the domain R, and q a prime of S lying over p, q.height + trdeg_{κ(p)} κ(q) ≤ p.height + trdeg_R S.

theorem height_add_trdeg_residue_le
    [IsNoetherianRing R] [Algebra.FiniteType R S] [IsDomain R] [IsDomain S]
    (hinj : Function.Injective (algebraMap R S))
    (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p] :
    letI := Ideal.ResidueField.algebraOfLiesOver p q
    q.height + (Cardinal.toNat (Algebra.trdeg p.ResidueField q.ResidueField) : ℕ∞)
      ≤ p.height + (Cardinal.toNat (Algebra.trdeg R S) : ℕ∞)

height_add_trdeg_residue_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DimensionFormula/GeneratorInduction.lean, line 810. References: EGA IV (13.3.4), “special case”; EGA IV (5.5.6), “special case”; EGA IV (5.5.7), “special case”; EGA IV (5.6.5), “partial”.

Stacks 02IJ. If in addition R is universally catenary, the dimension formula is an equality: q.height + trdeg_{κ(p)} κ(q) = p.height + trdeg_R S.

theorem height_add_trdeg_residue_eq
    [IsNoetherianRing R] [Algebra.FiniteType R S] [IsDomain R] [IsDomain S]
    (hinj : Function.Injective (algebraMap R S)) (hcat : IsUniversallyCatenary R)
    (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p] :
    letI := Ideal.ResidueField.algebraOfLiesOver p q
    q.height + (Cardinal.toNat (Algebra.trdeg p.ResidueField q.ResidueField) : ℕ∞)
      = p.height + (Cardinal.toNat (Algebra.trdeg R S) : ℕ∞)

Tag 02MA, a lemma

Tag 02MA in the Stacks Project.

Ideal.primesOver_finite_and_forall_height_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/Over/HeightOne.lean, line 325. The attribute's comment: “Finiteness of the induced extension of fraction fields is stated as Algebra.IsAlgebraic A B, to which it is equivalent for B of finite type over A; see the module docstring.”.

Generically finite maps are quasi-finite in codimension one. Let A ⊆ B be an extension of domains with A Noetherian, B algebraic and of finite type over A, and let p be a prime of A of height one. Then only finitely many primes of B lie over p, and each of them has height one. Algebraicity of B over A is, under the finite type hypothesis, finiteness of the induced extension of fraction fields.

public theorem Ideal.primesOver_finite_and_forall_height_eq_one {A : Type*} [CommRing A]
    [IsNoetherianRing A] (p : Ideal A) [p.IsPrime] (B : Type*) [CommRing B] [IsDomain B]
    [Algebra A B] [FaithfulSMul A B] [Algebra.IsAlgebraic A B] [Algebra.FiniteType A B]
    (hp : p.height = 1) :
    (p.primesOver B).Finite ∧ ∀ q ∈ p.primesOver B, q.height = 1

Sources

• Section 10.113, Tag 02II
• AxiomMath/Stacks at 5ed82d14

Leanheight_add_trdeg_residue_le · height_add_trdeg_residue_eq · Ideal.primesOver_finite_and_forall_height_eq_one

Section10.114 Dimension of finite type algebras over fields#

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

Tag 00OP, a lemma

Tag 00OP in the Stacks Project.

maximal_ideal_generated_by_n, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MvPolynomial/MaximalIdeal.lean, line 245.

A maximal ideal m of k[x_1, …, x_n] is generated by at most n elements.

theorem maximal_ideal_generated_by_n
    {k : Type*} [Field k] (n : ℕ) (m : Ideal (MvPolynomial (Fin n) k))
    (hm : m.IsMaximal) :
    GeneratedByAtMost n m

ringKrullDim_localization_atPrime_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MvPolynomial/MaximalIdeal.lean, line 255. References: EGA IV (5.5.3), “special case”; EGA IV (5.6.1), “special case”.

Part 2 of tag 00OP: the localization of k[x_1, …, x_n] at a maximal ideal has Krull dimension n.

theorem ringKrullDim_localization_atPrime_eq
    {k : Type*} [Field k] (n : ℕ) (m : Ideal (MvPolynomial (Fin n) k))
    (hm : m.IsMaximal) :
    haveI : m.IsPrime := hm.isPrime
    ringKrullDim (Localization.AtPrime m) = (n : WithBot ℕ∞)

isRegularLocalRing_localization_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MvPolynomial/MaximalIdeal.lean, line 267.

The localization of k[x_1, …, x_n] at a maximal ideal is a regular local ring.

theorem isRegularLocalRing_localization_atPrime
    {k : Type*} [Field k] (n : ℕ) (m : Ideal (MvPolynomial (Fin n) k))
    (hm : m.IsMaximal) :
    haveI : m.IsPrime := hm.isPrime
    IsRegularLocalRing (Localization.AtPrime m)

Tag 00OQ, a proposition

Tag 00OQ in the Stacks Project.

MvPolynomial.isRegularRing_and_iSup_projectiveDimension_eq_and_isRegularLocalRing_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MvPolynomial/RegularRing.lean, line 210. The attribute's comment: “The number of variables is Nat.card ι for an arbitrary finite index type ι, the global dimension is the supremum of the projective dimensions of all modules (Mathlib has no name for it), and the localization at a maximal ideal is an abstract IsLocalization.AtPrime. See the module docstring.”. References: SGA 6 VI (1.5.2), “more general”.

Stacks 00OQ. A polynomial algebra k[ι] in finitely many variables over a field is a regular ring; its global dimension, the supremum of the projective dimensions of its modules, is the number Nat.card ι of variables; and every localization of k[ι] at a maximal ideal is a regular local ring of dimension Nat.card ι.

public theorem isRegularRing_and_iSup_projectiveDimension_eq_and_isRegularLocalRing_localization
    (k : Type u) [Field k] (ι : Type v) [Finite ι] :
    IsRegularRing (MvPolynomial ι k) ∧
      (⨆ M : ModuleCat.{max u v} (MvPolynomial ι k), projectiveDimension M) =
        (Nat.card ι : WithBot ℕ∞) ∧
      ∀ (𝔪 : Ideal (MvPolynomial ι k)) [𝔪.IsMaximal] (A : Type w) [CommRing A]
          [Algebra (MvPolynomial ι k) A] [IsLocalization.AtPrime A 𝔪],
        IsRegularLocalRing A ∧ ringKrullDim A = (Nat.card ι : WithBot ℕ∞)

Tag 00OR, a lemma

Tag 00OR in the Stacks Project.

IsRegularRing.height_last_eq_length_add_height_head, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularRing/Dimension.lean, line 257. The attribute's comment: “Stated for an arbitrary regular ring, of which a polynomial algebra in finitely many variables over a field is an instance (the source's ring, via Proposition 00OQ); a maximal chain between 𝔭 and 𝔮 is a RelSeries for the covering relation ⋖ on PrimeSpectrum R with the given head and last, and the formula is stated additively. See the module docstring.”.

Stacks 00OR. In a regular ring, every maximal chain of primes between 𝔭 and 𝔮 — a chain from 𝔭 to 𝔮 no two consecutive members of which admit a prime strictly between them — has length height 𝔮 - height 𝔭, stated as height 𝔮 = length + height 𝔭.

public theorem IsRegularRing.height_last_eq_length_add_height_head {R : Type*} [CommRing R]
    [IsRegularRing R] (s : RelSeries {(p, q) : PrimeSpectrum R × PrimeSpectrum R | p ⋖ q}) :
    s.last.asIdeal.height = s.length + s.head.asIdeal.height

Tag 00OS, a lemma

Tag 00OS in the Stacks Project.

Algebra.FiniteType.ringKrullDim_eq_height_of_isMaximal_and_length_eq_ringKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/FiniteTypeOverField.lean, line 533. The attribute's comment: “dim(S_𝔪) is written 𝔪.height, the Krull dimension of any model of the local ring at 𝔪; the source's "in words" clause is kept as a second conjunct, a maximal chain of primes being a RelSeries for the covering relation ⋖ on PrimeSpectrum S whose head is minimal and whose last is maximal. See the module docstring.”.

Stacks 00OS. Let k be a field and let S be a finite type k-algebra which is a domain. Then dim S = dim S_𝔪 = height 𝔪 for every maximal ideal 𝔪 of S, and every maximal chain of primes of S — one starting at a minimal prime, ending at a maximal ideal, and with all steps covering pairs — has length dim S.

public theorem ringKrullDim_eq_height_of_isMaximal_and_length_eq_ringKrullDim (k : Type*)
    [Field k] (S : Type*) [CommRing S] [IsDomain S] [Algebra k S] [Algebra.FiniteType k S] :
    (∀ (𝔪 : Ideal S) [𝔪.IsMaximal], ringKrullDim S = (𝔪.height : WithBot ℕ∞)) ∧
      ∀ s : RelSeries {(p, q) : PrimeSpectrum S × PrimeSpectrum S | p ⋖ q},
        IsMin s.head → IsMax s.last → (s.length : WithBot ℕ∞) = ringKrullDim S

Tag 00OT, a lemma

Tag 00OT in the Stacks Project.

PrimeSpectrum.localKrullDim_eq_iSup_irreducibleComponents_and_eq_iInf_height, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/LocalDimension.lean, line 381. The attribute's comment: “dim_x X is TopologicalSpace.localKrullDim, Topology Definition 0055 (4); dim(S_𝔪) is 𝔪.height; the components are irreducibleComponents and their dimension is topologicalKrullDim, and the source's max/min are iSup/iInf in WithBot ℕ∞. See the module docstring.”.

Stacks 00OT. Let k be a field, let S be a finite type k-algebra, let X = Spec S, and let x ∈ X be a point, with prime ideal 𝔭 = x.asIdeal. Then the dimension of X at x is both the largest dimension of an irreducible component of X through x and the smallest of the dimensions dim S_𝔪 = height 𝔪 over the maximal ideals 𝔪 ⊇ 𝔭.

public theorem localKrullDim_eq_iSup_irreducibleComponents_and_eq_iInf_height
    (k : Type u) [Field k] {S : Type v} [CommRing S] [Algebra k S] [Algebra.FiniteType k S]
    (x : PrimeSpectrum S) :
    (TopologicalSpace.localKrullDim (PrimeSpectrum S) x =
        ⨆ Z ∈ {Z ∈ irreducibleComponents (PrimeSpectrum S) | x ∈ Z}, topologicalKrullDim Z) ∧
      (TopologicalSpace.localKrullDim (PrimeSpectrum S) x =
        ⨅ 𝔪 ∈ {𝔪 : Ideal S | 𝔪.IsMaximal ∧ x.asIdeal ≤ 𝔪}, (𝔪.height : WithBot ℕ∞))

Tag 00OU, a lemma

Tag 00OU in the Stacks Project.

Scheme.localKrullDim, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Dimension/LocalKrullDim.lean, line 186. References: EGA IV (17.15.8); EGA IV (21.10.1), “partial”; SGA 1 II (5.9).

The local dimension of a scheme X at a point x: the Krull dimension of the local ring of X at x.

noncomputable def Scheme.localKrullDim (X : Scheme) (x : X) : WithBot ℕ∞

Tag 00OV, a lemma

Tag 00OV in the Stacks Project.

PrimeSpectrum.isLocallyConstant_localKrullDim_and_equidimensional_fiber_and_finite_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Equidimensional.lean, line 806. The attribute's comment: “The source's family T_d is pinned as the fibers of TopologicalSpace.localKrullDim (Topology Definition 0055 (4)), so that disjointness and covering are definitional, T_d open and closed is IsLocallyConstant.isClopen_fiber, and finiteness of the union is finiteness of the range; the index runs over WithBot ℕ∞. Cohen-Macaulayness of the Noetherian ring S (Definition 00NC) is spelled out over its localizations at primes, as in tags 00ND and 00R9. The equivalent decomposition of S as a product of rings is the image of this one under Lemma 00EM and is not restated. See the module docstring.”.

Stacks 00OV. Let k be a field and let S be a Cohen-Macaulay finite type k-algebra. Then Spec S is the disjoint union of the level sets T_d of its local dimension; these are open and closed, there are finitely many nonempty ones, and T_d is equidimensional of dimension d.

public theorem
    isLocallyConstant_localKrullDim_and_equidimensional_fiber_and_finite_range
    {k S : Type*} [Field k] [CommRing S] [Algebra k S] [Algebra.FiniteType k S]
    (hS : ∀ (p : Ideal S) [p.IsPrime],
      Module.IsMaximalCohenMacaulay (Localization.AtPrime p) (Localization.AtPrime p)) :
    IsLocallyConstant (localKrullDim (PrimeSpectrum S)) ∧
      (∀ d : WithBot ℕ∞,
        Equidimensional ↥(localKrullDim (PrimeSpectrum S) ⁻¹' {d}) ∧
          ((localKrullDim (PrimeSpectrum S) ⁻¹' {d}).Nonempty →
            topologicalKrullDim ↥(localKrullDim (PrimeSpectrum S) ⁻¹' {d}) = d)) ∧
        (Set.range (localKrullDim (PrimeSpectrum S))).Finite

Sources

• Section 10.114, Tag 00OO
• AxiomMath/Stacks at 5ed82d14

Leanmaximal_ideal_generated_by_n · ringKrullDim_localization_atPrime_eq · isRegularLocalRing_localization_atPrime · MvPolynomial.isRegularRing_and_iSup_projectiveDimension_eq_and_isRegularLocalRing_localization · IsRegularRing.height_last_eq_length_add_height_head · Algebra.FiniteType.ringKrullDim_eq_height_of_isMaximal_and_length_eq_ringKrullDim · PrimeSpectrum.localKrullDim_eq_iSup_irreducibleComponents_and_eq_iInf_height · Scheme.localKrullDim

Section10.115 Noether normalization#

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

Tag 051M, a lemma

Tag 051M in the Stacks Project.

exists_separating_exponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NoetherNormalization/Basic.lean, line 232.

For a finite set N ⊆ ℕ^n, there is an exponent tuple e ∈ ℕ^n such that e · ν = e · ν' ↔ ν = ν' for all ν, ν' ∈ N.

theorem exists_separating_exponents {n : ℕ} (N : Finset (Fin n → ℕ)) :
    ∃ e : Fin n → ℕ, ∀ ν ∈ N, ∀ ν' ∈ N, (e ⬝ᵥ ν = e ⬝ᵥ ν' ↔ ν = ν')

Tag 051N, a lemma

Tag 051N in the Stacks Project.

exists_substitution_with_constant_leadingCoeff_of_nonconstant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NoetherNormalization/Basic.lean, line 454.

Let g be a nonconstant polynomial in MvPolynomial (Fin (n+1)) R, that is one not in the image of the constant inclusion MvPolynomial.C : R → …. Then there exist exponents e with e 0 = 1, encoding e_n = 1, a positive integer d, and an element a ∈ R such that:

1. a is one of the nonzero coefficients of g: there is a multi-index ν in the support of g with a = g.coeff ν, so in particular a ≠ 0.

2. Viewing f = subst n e g as a polynomial in the distinguished variable X 0 via finSuccEquiv R n, its degree in that variable is d and its leading coefficient is the constant MvPolynomial.C a, the image of a ∈ R inside S = MvPolynomial (Fin n) R.

theorem exists_substitution_with_constant_leadingCoeff_of_nonconstant
    (n : ℕ) (g : MvPolynomial (Fin (n + 1)) R)
    (hg : ¬ ∃ r : R, g = MvPolynomial.C r) :
    ∃ (e : Fin (n + 1) → ℕ) (d : ℕ) (a : R),
      e 0 = 1 ∧
      (∃ ν ∈ g.support, a = g.coeff ν) ∧
      0 < d ∧
      (finSuccEquiv R n (subst n e g)).natDegree = d ∧
      (finSuccEquiv R n (subst n e g)).leadingCoeff = MvPolynomial.C a

Tag 00OX, a lemma

Tag 00OX in the Stacks Project.

Stacks.RingTheory.NagataNormalization.exists_isIntegral_aeval, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NoetherNormalization.lean, line 152.

Stacks 00OX, in the form the induction uses. If the generators x 0, …, x n of a k-algebra S satisfy a nonzero polynomial relation f, then S is integral over the subalgebra generated by the n elements y i = x (i + 1) - x 0 ^ D ^ (i + 1), where D = f.totalDegree + 2; these lie in the ℤ-subalgebra generated by the x i.

lemma exists_isIntegral_aeval {k : Type*} [Field k] {n : ℕ} {S : Type*} [CommRing S]
    [Algebra k S] (x : Fin (n + 1) → S) (hx : Algebra.adjoin k (Set.range x) = ⊤)
    {f : MvPolynomial (Fin (n + 1)) k} (hf : f ≠ 0) (hfx : MvPolynomial.aeval x f = 0) :
    ∃ y : Fin n → S, (∀ i, y i ∈ Algebra.adjoin ℤ (Set.range x)) ∧
      (MvPolynomial.aeval y : MvPolynomial (Fin n) k →ₐ[k] S).toRingHom.IsIntegral

Tag 00OY, a lemma

Tag 00OY in the Stacks Project.

exists_finite_inj_aeval_ringKrullDim_eq_of_adjoin_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NoetherNormalization.lean, line 436. The attribute's comment: “Stated for a nonzero k-algebra with a finite generating set s rather than for a presentation k[x_1, …, x_n]/I, the source's ℤ-subalgebra being Algebra.adjoin ℤ s; the map k[y_1, …, y_r] → S is pinned as MvPolynomial.aeval y. See the module docstring.”.

Stacks 00OY (Noether normalization). Let k be a field and let S be a nonzero commutative k-algebra generated by a finite set s. Then there are r : ℕ and y : Fin r → S with every y i in the ℤ-subalgebra of S generated by s, such that the k-algebra map MvPolynomial (Fin r) k →ₐ[k] S sending X i to y i is injective and finite; the number r is the Krull dimension of S.

public theorem exists_finite_inj_aeval_ringKrullDim_eq_of_adjoin_eq_top (k : Type*) {S : Type*}
    [Field k] [CommRing S] [Nontrivial S] [Algebra k S] {s : Set S} (hs : s.Finite)
    (hgen : Algebra.adjoin k s = ⊤) :
    ∃ (r : ℕ) (y : Fin r → S), (∀ i, y i ∈ Algebra.adjoin ℤ s) ∧
      Function.Injective (MvPolynomial.aeval y : MvPolynomial (Fin r) k →ₐ[k] S) ∧
      (MvPolynomial.aeval y : MvPolynomial (Fin r) k →ₐ[k] S).Finite ∧
      ringKrullDim S = r

Tag 00OZ, a lemma

Tag 00OZ in the Stacks Project.

noether_normalization_at_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NoetherNormalization/Basic.lean, line 178.

Noether normalization at a point: for a field k, a finite type k-algebra S, and a prime ideal q of S corresponding to a point x of X = Spec(S), there exist an element g ∉ q, a natural number d, and a k-algebra homomorphism ψ : k[y_1, …, y_d] → S_g, where k[y_1, …, y_d] = MvPolynomial (Fin d) k, such that d = dim(S_g) = dim_x(X) and ψ is injective and finite.

theorem noether_normalization_at_point
    {k S : Type*} [Field k] [CommRing S] [Algebra k S] [Algebra.FiniteType k S]
    (q : Ideal S) [q.IsPrime] :
    ∃ (g : S) (_ : g ∉ q) (d : ℕ)
      (ψ : MvPolynomial (Fin d) k →ₐ[k] Localization.Away g),
      (d : WithBot ℕ∞) = ringKrullDim (Localization.Away g) ∧
      (d : WithBot ℕ∞) = localDimAtPrime k q ∧
      Function.Injective ψ ∧
      ψ.toRingHom.Finite

Tag 051P, a lemma

Tag 051P in the Stacks Project.

MvPolynomial.exists_finite_comap_eq_span_X_image_of_trdeg_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MvPolynomial/PrimeStandardForm.lean, line 669. The attribute's comment: “The two polynomial rings are the one type MvPolynomial (Fin n) k, with (y_{r + 1}, …, y_n) spelled Ideal.span (X '' {i | r ≤ (i : ℕ)}); φ is a k-algebra map, as the source's construction gives, and κ(q) is the canonical Ideal.ResidueField. See the module docstring.”.

Let k be a field, let q ⊆ k[x_1, …, x_n] be a prime ideal, and let r be the transcendence degree of the residue field κ(q) over k. Then there is a finite k-algebra map φ : k[y_1, …, y_n] → k[x_1, …, x_n] whose preimage of q is the ideal (y_{r + 1}, …, y_n) generated by the last n - r variables.

public theorem exists_finite_comap_eq_span_X_image_of_trdeg_eq {k : Type u} [Field k]
    {n : ℕ} (q : Ideal (MvPolynomial (Fin n) k)) [q.IsPrime] {r : ℕ}
    (hr : Algebra.trdeg k q.ResidueField = r) :
    ∃ φ : MvPolynomial (Fin n) k →ₐ[k] MvPolynomial (Fin n) k,
      φ.toRingHom.Finite ∧ q.comap φ = Ideal.span (X '' {i : Fin n | r ≤ (i : ℕ)})

Tag 07NA, a lemma

Tag 07NA in the Stacks Project.

exists_subalgebra_finite_inj_aeval_pow_smul_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NoetherNormalization.lean, line 886. The attribute's comment: “The chain R → R[y_1, …, y_d] → S' → S is realized with S' a Subalgebra R S and the middle map MvPolynomial.aeval y; S'_f ≅ S_f is stated in the elementary form ∀ x : S, ∃ n, f ^ n • x ∈ S'. See the module docstring.”.

Stacks 07NA (Noether normalization over a domain). Let R be a domain and let S be an R-algebra of finite type with R → S injective. Then there are an integer d, an R-subalgebra S' of S, elements y_1, …, y_d ∈ S' and a nonzero f ∈ R such that the R-algebra map R[Y_1, …, Y_d] → S', Y_i ↦ y_i, is injective and makes S' a finite module over R[Y_1, …, Y_d], and such that every element of S lies in S' after multiplication by a power of f; the last condition says precisely that S'_f ≅ S_f.

public theorem exists_subalgebra_finite_inj_aeval_pow_smul_mem (R S : Type*) [CommRing R]
    [IsDomain R] [CommRing S] [Algebra R S] [FaithfulSMul R S] [Algebra.FiniteType R S] :
    ∃ (d : ℕ) (S' : Subalgebra R S) (y : Fin d → S') (f : R), f ≠ 0 ∧
      Function.Injective (MvPolynomial.aeval y : MvPolynomial (Fin d) R →ₐ[R] S') ∧
      (MvPolynomial.aeval y : MvPolynomial (Fin d) R →ₐ[R] S').Finite ∧
      ∀ x : S, ∃ n : ℕ, f ^ n • x ∈ S'

Sources

• Section 10.115, Tag 00OW
• AxiomMath/Stacks at 5ed82d14

Leanexists_separating_exponents · exists_substitution_with_constant_leadingCoeff_of_nonconstant · Stacks.RingTheory.NagataNormalization.exists_isIntegral_aeval · exists_finite_inj_aeval_ringKrullDim_eq_of_adjoin_eq_top · noether_normalization_at_point · MvPolynomial.exists_finite_comap_eq_span_X_image_of_trdeg_eq · exists_subalgebra_finite_inj_aeval_pow_smul_mem

Section10.116 Dimension of finite type algebras over fields, reprise#

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

Tag 00P0, a lemma

Tag 00P0 in the Stacks Project.

ringKrullDim_eq_trdeg_and_ringKrullDim_localization_eq_trdeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/FiniteTypeOverField.lean, line 255. The attribute's comment: “The transcendence degree is compared through Cardinal.toENat, the field of fractions is an abstract IsFractionRing and the local ring an abstract IsLocalization.AtPrime. See the module docstring.”. References: EGA IV (5.5.8), “special case”.

Stacks 00P0. Let k be a field, let S be a finite type k-algebra which is a domain, and let K be its field of fractions. Then the Krull dimension of S is the transcendence degree of K over k, and the local ring of S at every maximal ideal has that same dimension.

public theorem ringKrullDim_eq_trdeg_and_ringKrullDim_localization_eq_trdeg
    (k : Type u) [Field k] (S : Type v) [CommRing S] [IsDomain S] [Algebra k S]
    [Algebra.FiniteType k S] (K : Type w) [Field K] [Algebra S K] [IsFractionRing S K]
    [Algebra k K] [IsScalarTower k S K] :
    ringKrullDim S = (Cardinal.toENat (Algebra.trdeg k K) : WithBot ℕ∞) ∧
      ∀ (𝔪 : Ideal S) [𝔪.IsMaximal] (A : Type x) [CommRing A] [Algebra S A]
          [IsLocalization.AtPrime A 𝔪],
        ringKrullDim A = (Cardinal.toENat (Algebra.trdeg k K) : WithBot ℕ∞)

Tag 06RP, a lemma

Tag 06RP in the Stacks Project.

Ideal.trdeg_residueField_lt_trdeg_residueField_of_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TranscendenceDegree/ResidueField.lean, line 193. The attribute's comment: “The residue field κ(𝔮) is Mathlib's Ideal.ResidueField, the fraction field of S ⧸ 𝔮, and the comparison is a strict inequality of Cardinal, both degrees being finite. See the module docstring.”.

Stacks 06RP. Let k be a field, let S be a finite type k-algebra, and let 𝔮 ⊊ 𝔮' be prime ideals of S. Then the transcendence degree over k of the residue field κ(𝔮') is strictly smaller than that of κ(𝔮).

public theorem Ideal.trdeg_residueField_lt_trdeg_residueField_of_lt
    (k : Type u) [Field k] {S : Type v} [CommRing S] [Algebra k S] [Algebra.FiniteType k S]
    {q q' : Ideal S} [q.IsPrime] [q'.IsPrime] (h : q < q') :
    Algebra.trdeg k q'.ResidueField < Algebra.trdeg k q.ResidueField

Tag 00P1, a lemma

Tag 00P1 in the Stacks Project.

PrimeSpectrum.localKrullDim_eq_height_add_trdeg_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/LocalDimension.lean, line 783. The attribute's comment: “dim_x X is TopologicalSpace.localKrullDim, Definition 0055 (4); dim(S_𝔭) is 𝔭.height, κ(𝔭) is Ideal.ResidueField, and the transcendence degree is compared through Cardinal.toENat. See the module docstring.”. References: EGA IV (17.15.8), “special case”.

Stacks 00P1. Let k be a field, let S be a finite type k-algebra, let X = Spec S, and let x ∈ X be a point, with prime ideal 𝔭 = x.asIdeal. Then the dimension of X at x — the least dimension of an open neighbourhood of x — is the height of 𝔭 plus the transcendence degree over k of the residue field κ(𝔭).

public theorem localKrullDim_eq_height_add_trdeg_residueField
    (k : Type u) [Field k] {S : Type v} [CommRing S] [Algebra k S] [Algebra.FiniteType k S]
    (x : PrimeSpectrum S) :
    TopologicalSpace.localKrullDim (PrimeSpectrum S) x =
      ((x.asIdeal.height + Cardinal.toENat (Algebra.trdeg k x.asIdeal.ResidueField) : ℕ∞) :
        WithBot ℕ∞)

Tag 00P2, a lemma

Tag 00P2 in the Stacks Project.

PrimeSpectrum.localKrullDim_comap_add_height_eq_localKrullDim_add_height_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/Codimension.lean, line 164. The attribute's comment: “dim_x X is TopologicalSpace.localKrullDim, Definition 0055 (4), and height 𝔭 is Ideal.height, as in the sibling 00P1; the source's difference of differences is stated as the equivalent equality of sums, subtraction in WithBot ℕ∞ being truncated. See the module docstring.”.

Stacks 00P2. Let k be a field, let f : S' → S be a surjection of finite type k-algebras, let x ∈ Spec S be a point and let x' = comap f x be the corresponding point of Spec S'. Then the dimension of Spec S' at x' exceeds the dimension of Spec S at x by exactly the amount by which the height of x' exceeds the height of x.

public theorem localKrullDim_comap_add_height_eq_localKrullDim_add_height_comap
    (k : Type u) [Field k] {S' : Type v} {S : Type w} [CommRing S'] [CommRing S]
    [Algebra k S'] [Algebra k S] [Algebra.FiniteType k S'] (f : S' →ₐ[k] S)
    (hf : Function.Surjective f) (x : PrimeSpectrum S) :
    TopologicalSpace.localKrullDim (PrimeSpectrum S') (comap f.toRingHom x) +
        (x.asIdeal.height : WithBot ℕ∞) =
      TopologicalSpace.localKrullDim (PrimeSpectrum S) x +
        ((comap f.toRingHom x).asIdeal.height : WithBot ℕ∞)

Tag 00P3, a lemma

Tag 00P3 in the Stacks Project.

Algebra.IsPushout.ringKrullDim_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/BaseChange.lean, line 246. The attribute's comment: “The base change K ⊗_k S is an arbitrary pushout square of k-algebras Algebra.IsPushout k K S T; the source's literal form is inferInstance once Algebra.TensorProduct.rightAlgebra is a local instance. See the module docstring.”.

Stacks 00P3. Let k be a field, let S be a k-algebra of finite type and let K/k be a field extension. Then S and its base change T = K ⊗_k S have the same Krull dimension.

public theorem Algebra.IsPushout.ringKrullDim_eq (k K S T : Type*) [Field k] [Field K]
    [CommRing S] [CommRing T] [Algebra k K] [Algebra k S] [Algebra k T] [Algebra K T]
    [Algebra S T] [IsScalarTower k K T] [IsScalarTower k S T] [Algebra.IsPushout k K S T]
    [Algebra.FiniteType k S] :
    ringKrullDim S = ringKrullDim T

Tag 00P4, a lemma

Tag 00P4 in the Stacks Project.

Algebra.IsPushout.localKrullDim_comap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/BaseChange.lean, line 570. The attribute's comment: “dim_x X is TopologicalSpace.localKrullDim, Definition 0055 (4), as in the siblings 00P1 and 00P2; the base change K ⊗_k S is an arbitrary pushout square of k-algebras Algebra.IsPushout k K S T, as in the sibling 00P3; and q_K lying over q is expressed by taking x = PrimeSpectrum.comap (algebraMap S T) xK. See the module docstring.”.

Stacks 00P4. Let k be a field, let S be a finite type k-algebra, let K/k be a field extension and let T = K ⊗_k S be the base change, presented as a pushout square. Let xK ∈ Spec T be a point, with prime q_K, and let x = comap (algebraMap S T) xK ∈ Spec S be the point of the prime q = q_K ∩ S that it lies over. Then Spec S has the same dimension at x as Spec T has at xK.

public theorem localKrullDim_comap_eq (k K S T : Type*) [Field k] [Field K]
    [CommRing S] [CommRing T] [Algebra k K] [Algebra k S] [Algebra k T] [Algebra K T]
    [Algebra S T] [IsScalarTower k K T] [IsScalarTower k S T] [Algebra.IsPushout k K S T]
    [Algebra.FiniteType k S] (xK : PrimeSpectrum T) :
    TopologicalSpace.localKrullDim (PrimeSpectrum S)
        (PrimeSpectrum.comap (algebraMap S T) xK) =
      TopologicalSpace.localKrullDim (PrimeSpectrum T) xK

Tag 0CWE, a lemma

Tag 0CWE in the Stacks Project.

Algebra.IsPushout.height_fiber_add_height_eq_and_add_trdeg_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullDimension/BaseChange.lean, line 873. The attribute's comment: “The dimension of the fibre (S_K ⊗_S κ(𝔮))_{𝔮_K} is the height of the image of 𝔮_K in S_K ⧸ 𝔮 S_K, Mathlib's spelling in the going-down height formula (Lemma 00ON); the two equalities are stated additively rather than with a truncated subtraction in ℕ∞; the base change K ⊗_k S is an arbitrary pushout square of k-algebras, as in the siblings 00P3 and 00P4; and transcendence degrees are compared through Cardinal.toENat, as in 00P1. See the module docstring.”.

Stacks 0CWE. Let k be a field, let S be a finite type k-algebra, let K/k be a field extension and let T = K ⊗_k S be the base change, presented as a pushout square. Then for every prime q of S and every prime Q of T lying over q, the dimension of the fibre ring (T ⊗_S κ(q))_Q — the height of the image of Q in T ⧸ q T — added to dim S_q gives dim T_Q, and added to trdeg_K κ(Q) gives trdeg_k κ(q). Moreover, given q there is a prime Q over q for which this dimension is zero.

public theorem height_fiber_add_height_eq_and_add_trdeg_eq (k K S T : Type*) [Field k] [Field K]
    [CommRing S] [CommRing T] [Algebra k K] [Algebra k S] [Algebra k T] [Algebra K T]
    [Algebra S T] [IsScalarTower k K T] [IsScalarTower k S T] [Algebra.IsPushout k K S T]
    [Algebra.FiniteType k S] :
    (∀ (q : Ideal S) [q.IsPrime] (Q : Ideal T) [Q.IsPrime] [Q.LiesOver q],
        (Q.map (Ideal.Quotient.mk (q.map (algebraMap S T)))).height + q.height = Q.height ∧
        (Q.map (Ideal.Quotient.mk (q.map (algebraMap S T)))).height
            + Cardinal.toENat (Algebra.trdeg K Q.ResidueField)
          = Cardinal.toENat (Algebra.trdeg k q.ResidueField)) ∧
      ∀ (q : Ideal S) [q.IsPrime], ∃ (Q : Ideal T) (_ : Q.IsPrime) (_ : Q.LiesOver q),
        (Q.map (Ideal.Quotient.mk (q.map (algebraMap S T)))).height = 0

Sources

• Section 10.116, Tag 07NB
• AxiomMath/Stacks at 5ed82d14

LeanringKrullDim_eq_trdeg_and_ringKrullDim_localization_eq_trdeg · Ideal.trdeg_residueField_lt_trdeg_residueField_of_lt · PrimeSpectrum.localKrullDim_eq_height_add_trdeg_residueField · PrimeSpectrum.localKrullDim_comap_add_height_eq_localKrullDim_add_height_comap · Algebra.IsPushout.ringKrullDim_eq · Algebra.IsPushout.localKrullDim_comap_eq · Algebra.IsPushout.height_fiber_add_height_eq_and_add_trdeg_eq

Section10.117 Dimension of graded algebras over a field#

Section 10.117 of the Stacks Project, Tag 00P5. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00P6, a lemma

Tag 00P6 in the Stacks Project.

GradedAlgebra.irrelevant_isMaximal_and_ringKrullDim_eq_natDegree_add_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/KrullDimension.lean, line 943. The attribute's comment: “Items (1)-(4). dim_x Spec(S) is the height of the irrelevant ideal, and the convention deg 0 = -1 is unfolded into the cases P = 0, P ≠ 0. See the module docstring.”. References: EGA IV (6.10.5), “special case”.

Stacks 00P6. Let k be a field and let S be a graded k-algebra with S_0 = k that is generated over k by finitely many elements of degree 1. Let P ∈ ℚ[T] be the polynomial with dim_k S_d = P(d) for all d ≫ 0. Then: (1) the irrelevant ideal m = S_+ is maximal; (2) every minimal prime of S is homogeneous and contained in S_+; (3) dim(S) = deg(P) + 1, with deg(0) = -1, and this equals the dimension dim_x Spec(S) = dim(S_m) = height(m) of Spec(S) at the closed point x given by m; (4) the Hilbert function d ↦ length_{S_m} (m^d S_m / m^{d + 1} S_m) of the local ring S_m is the Hilbert function d ↦ dim_k S_d of S.

public theorem GradedAlgebra.irrelevant_isMaximal_and_ringKrullDim_eq_natDegree_add_one
    {k S : Type*} [Field k] [CommRing S] [Nontrivial S] [Algebra k S]
    (𝒜 : ℕ → Submodule k S) [GradedAlgebra 𝒜] (h0 : 𝒜 0 = 1)
    [Module.Finite k ↥(𝒜 1)] (hgen : Algebra.adjoin k (𝒜 1 : Set S) = ⊤)
    (P : ℚ[X]) (hP : ∀ᶠ d : ℕ in Filter.atTop, P.eval (d : ℚ) = Module.finrank k ↥(𝒜 d)) :
    ∃ hm : 𝒜₊.toIdeal.IsMaximal,
      letI := hm.isPrime
      (∀ p ∈ minimalPrimes S, Ideal.IsHomogeneous 𝒜 p ∧ p ≤ 𝒜₊.toIdeal) ∧
      (P = 0 → ringKrullDim S = 0) ∧
      (P ≠ 0 → ringKrullDim S = (P.natDegree + 1 : ℕ)) ∧
      ringKrullDim S = 𝒜₊.toIdeal.height ∧
      ∀ d : ℕ, Module.length (Localization.AtPrime (𝒜₊).toIdeal)
          (↥(IsLocalRing.maximalIdeal (Localization.AtPrime (𝒜₊).toIdeal) ^ d) ⧸
            (IsLocalRing.maximalIdeal (Localization.AtPrime (𝒜₊).toIdeal) ^ (d + 1)).submoduleOf
              (IsLocalRing.maximalIdeal (Localization.AtPrime (𝒜₊).toIdeal) ^ d))
        = Module.finrank k ↥(𝒜 d)

Sources

• Section 10.117, Tag 00P5
• AxiomMath/Stacks at 5ed82d14

LeanGradedAlgebra.irrelevant_isMaximal_and_ringKrullDim_eq_natDegree_add_one

Section10.118 Generic flatness#

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

Tag 051R, a lemma

Tag 051R in the Stacks Project.

Module.exists_ne_zero_free_localizedModule_away, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/GenericFlatness/Noetherian.lean, line 510. The attribute's comment: “The localizations are abstract: the conclusion asserts freeness over every model Rf of R_f and Mf of M_f, pinned by IsLocalization.Away and IsLocalizedModule. The R-module structure on M is the one induced by R → S. See the module docstring.”. References: EGA IV (6.9.2); EGA IV (8.9.4), “affine Noetherian case”; SGA 1 IV (6.7).

Stacks 051R (generic freeness). Let R be a Noetherian domain, let S be an R-algebra of finite type and let M be a finite S-module. Then there is a nonzero f ∈ R such that the localization M_f is a free R_f-module.

The proof is not the source's induction on dim (K ⊗_R S): it reduces to M = A ⧸ I over a polynomial ring A = R[y_1, …, y_d] and settles that case by division with remainder, so IsNoetherianRing R is not used. See the module docstring.

public theorem exists_ne_zero_free_localizedModule_away
    {R S M : Type*} [CommRing R] [IsNoetherianRing R] [IsDomain R] [CommRing S] [Algebra R S]
    [Algebra.FiniteType R S] [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.Finite S M] :
    ∃ f : R, f ≠ 0 ∧ ∀ (Rf : Type*) [CommRing Rf] [Algebra R Rf] [IsLocalization.Away f Rf]
      (Mf : Type*) [AddCommGroup Mf] [Module R Mf] [Module Rf Mf] [IsScalarTower R Rf Mf]
      (g : M →ₗ[R] Mf) [IsLocalizedModule (Submonoid.powers f) g],
      Module.Free Rf Mf

Tag 051S, a lemma

Tag 051S in the Stacks Project.

Module.FinitePresentation.exists_ne_zero_free_localizedModule_away, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/GenericFlatness/FinitePresentation.lean, line 248. The attribute's comment: “The localizations are abstract: the conclusion asserts freeness over every model Rf of R_f and Mf of M_f, pinned by IsLocalization.Away and IsLocalizedModule. The R-module structure on M is the one induced by R → S. See the module docstring.”. References: EGA IV (8.9.4), “affine, free case”; EGA IV (8.9.4.1); EGA IV (8.9.4), “affine, free case”; EGA IV (11.4.6), “special case”; EGA IV (6.9.2), “more general”; SGA 1 IV (6.7), “more general”.

Stacks 051S (generic freeness). Let R be a domain, let S be an R-algebra of finite presentation and let M be an S-module of finite presentation. Then there is a nonzero f ∈ R such that the localization M_f is a free R_f-module.

Write S = P/I with P = R[x_1, …, x_n], so that M ≅ P^t/K with K finitely generated, and let R₀ ⊆ R be the ℤ-subalgebra generated by the coefficients of generators of K. Then R₀ is a domain of finite type over ℤ, hence Noetherian, and M is the base change along R₀ → R of the finite R₀[x]-module M₀ defined by the descended generators, so 051R applies over R₀.

public theorem exists_ne_zero_free_localizedModule_away
    {R S M : Type*} [CommRing R] [IsDomain R] [CommRing S] [Algebra R S]
    [Algebra.FinitePresentation R S] [AddCommGroup M] [Module R M] [Module S M]
    [IsScalarTower R S M] [Module.FinitePresentation S M] :
    ∃ f : R, f ≠ 0 ∧ ∀ (Rf : Type*) [CommRing Rf] [Algebra R Rf] [IsLocalization.Away f Rf]
      (Mf : Type*) [AddCommGroup Mf] [Module R Mf] [Module Rf Mf] [IsScalarTower R Rf Mf]
      (g : M →ₗ[R] Mf) [IsLocalizedModule (Submonoid.powers f) g],
      Module.Free Rf Mf

Tag 051T, a lemma

Tag 051T in the Stacks Project.

Algebra.exists_ne_zero_isFinitePresentationFreeAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/GenericFlatness/GenericFinitePresentation.lean, line 398. The attribute's comment: “The four conclusions are the condition of Equation 051U, so they are cited as Algebra.IsFinitePresentationFreeAway rather than written out; that definition fixes the models of R_f, S_f and M_f, and Algebra.isFinitePresentationFreeAway_iff moves the conclusion to any other models. See the module docstring.”. References: EGA IV (6.9.2), “more general”; EGA IV (8.9.4.1); EGA IV (11.4.6), “special case”; EGA IV (6.11.9), “more general”; SGA 1 IV (6.7), “more general”; SGA 1 IV (6.7), “more general”.

Stacks 051T (generic freeness and generic finite presentation). Let R be a domain, let S be an R-algebra of finite type and let M be a finite S-module. Then some nonzero f ∈ R satisfies the condition Algebra.IsFinitePresentationFreeAway R S M f of Equation 051U: the localizations S_f and M_f are free R_f-modules, S_f is a finitely presented R_f-algebra and M_f is a finitely presented S_f-module.

public theorem exists_ne_zero_isFinitePresentationFreeAway
    {R S M : Type*} [CommRing R] [IsDomain R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
    [AddCommGroup M] [Module S M] [Module.Finite S M] :
    ∃ f : R, f ≠ 0 ∧ Algebra.IsFinitePresentationFreeAway R S M f

Tag 051U, an equation

Tag 051U in the Stacks Project.

Algebra.IsFinitePresentationFreeAway, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/FreeAway.lean, line 385. The attribute's comment: “The condition of the source's display, as a predicate on f, with the canonical models of the localizations; M_f is the base change S_f ⊗[S] M. See the module docstring.”.

Stacks 051U. Let R → S be a ring map, let M be an S-module and let f : R. The condition Algebra.IsFinitePresentationFreeAway R S M f says that, after inverting f, the ring S_f is of finite presentation as an R_f-algebra, the module M_f is of finite presentation as an S_f-module, and S_f and M_f are free as R_f-modules. The localizations are the canonical ones: R_f = Localization.Away f, S_f is the localization of S at the image of the powers of f, and M_f = S_f ⊗[S] M; by Algebra.isFinitePresentationFreeAway_iff the four properties may be tested on any other models.

public def IsFinitePresentationFreeAway (R S M : Type*) [CommRing R] [CommRing S] [Algebra R S]
    [AddCommGroup M] [Module S M] (f : R) : Prop

Tag 051W, a lemma

Tag 051W in the Stacks Project.

Algebra.iUnion_basicOpen_isFinitePresentationFreeAway_inter_subset_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/GenericFlatness/Locus.lean, line 244. The attribute's comment: “The locus U(R → S, M) of Equation 051V, which has no separate definition here, is written out as the union of the standard opens D(f) over the f satisfying Equation 051U, i.e. over Algebra.IsFinitePresentationFreeAway R S M f. See the module docstring.”.

Stacks 051W. Let R → S be a ring map and let 0 → M₁ → M₂ → M₃ → 0 be a short exact sequence of S-modules. Writing U(R → S, M) = ⋃ \{D(f) | Algebra.IsFinitePresentationFreeAway R S M f} for the locus of Equation 051V, one has U(R → S, M₁) ∩ U(R → S, M₃) ⊆ U(R → S, M₂): an extension of free modules is free and an extension of finitely presented modules is finitely presented, so if f₁ and f₃ satisfy Equation 051U for M₁ and M₃ then f₁f₃ satisfies it for M₂.

public theorem iUnion_basicOpen_isFinitePresentationFreeAway_inter_subset_of_shortExact
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    {M₁ M₂ M₃ : Type*} [AddCommGroup M₁] [Module S M₁] [AddCommGroup M₂] [Module S M₂]
    [AddCommGroup M₃] [Module S M₃] (i : M₁ →ₗ[S] M₂) (q : M₂ →ₗ[S] M₃)
    (hi : Function.Injective i) (hq : Function.Surjective q) (hiq : Function.Exact i q) :
    (⋃ f ∈ {f : R | IsFinitePresentationFreeAway R S M₁ f},
          (basicOpen f : Set (PrimeSpectrum R))) ∩
        (⋃ f ∈ {f : R | IsFinitePresentationFreeAway R S M₃ f},
          (basicOpen f : Set (PrimeSpectrum R))) ⊆
      ⋃ f ∈ {f : R | IsFinitePresentationFreeAway R S M₂ f},
        (basicOpen f : Set (PrimeSpectrum R))

Tag 051X, a lemma

Tag 051X in the Stacks Project.

Algebra.image_comap_iUnion_basicOpen_isFinitePresentationFreeAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/GenericFlatness/Locus.lean, line 274. The attribute's comment: “The locus U(R → S, M) of Equation 051V is written out as the union of the standard opens D(g) over the g satisfying 051U, cited as Algebra.IsFinitePresentationFreeAway; the identification Spec(R_f) = D(f) is the open embedding PrimeSpectrum.comap (algebraMap R R_f), along which the left-hand side is pushed forward. See the module docstring.”.

Stacks 051X. Let R → S be a ring map, let M be an S-module and let f : R. Call g good for a module when it satisfies the condition Algebra.IsFinitePresentationFreeAway of Equation 051U, and let U(R → S, M) ⊆ Spec R be the union of the standard opens D(g) over the good g (Equation 051V). Then, under the identification of Spec(R_f) with D(f) given by PrimeSpectrum.comap (algebraMap R R_f), one has U(R_f → S_f, M_f) = D(f) ∩ U(R → S, M). Here R_f, S_f and M_f are arbitrary models of the localizations at the powers of f.

public theorem image_comap_iUnion_basicOpen_isFinitePresentationFreeAway
    {R S M : Type*} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module S M] (f : R)
    (Rf : Type*) [CommRing Rf] [Algebra R Rf] [IsLocalization.Away f Rf]
    (Sf : Type*) [CommRing Sf] [Algebra R Sf] [Algebra S Sf] [Algebra Rf Sf]
      [IsScalarTower R S Sf] [IsScalarTower R Rf Sf]
      [IsLocalization.Away (algebraMap R S f) Sf]
    (Mf : Type*) [AddCommGroup Mf] [Module S Mf] [Module Sf Mf] [IsScalarTower S Sf Mf]
    (l : M →ₗ[S] Mf) [IsLocalizedModule.Away (algebraMap R S f) l] :
    comap (algebraMap R Rf) ''
        (⋃ g ∈ {g : Rf | Algebra.IsFinitePresentationFreeAway Rf Sf Mf g},
          (basicOpen g : Set (PrimeSpectrum Rf))) =
      (basicOpen f : Set (PrimeSpectrum R)) ∩
        ⋃ g ∈ {g : R | Algebra.IsFinitePresentationFreeAway R S M g},
          (basicOpen g : Set (PrimeSpectrum R))

Tag 051Y, a lemma

Tag 051Y in the Stacks Project.

Algebra.dense_iUnion_basicOpen_isFinitePresentationFreeAway_of_localizationAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/GenericFlatness/Locus.lean, line 344. The attribute's comment: “The dense open U of the source is the union of the D(f), f ∈ s, so it is not a separate variable; the locus of Equation 051V is written out as the union of the D(f) over the f satisfying 051U, and density in D(f) is stated in Spec(R_f). See the module docstring.”.

Stacks 051Y. Let R → S be a ring map and let M be an S-module. Call f ∈ R good when S_f is of finite presentation over R_f, M_f is of finite presentation over S_f and S_f, M_f are free over R_f (Equation 051U), and let U(R → S, M) ⊆ Spec R be the union of the standard opens D(f) over the good f (Equation 051V). If the opens D(f), f ∈ s, have dense union in Spec R — that is, they cover a dense open — and if for each f ∈ s the locus U(R_f → S_f, M_f) is dense in Spec(R_f) = D(f), then U(R → S, M) is dense in Spec R.

public theorem dense_iUnion_basicOpen_isFinitePresentationFreeAway_of_localizationAway
    {R S M : Type*} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module S M]
    (s : Set R) (hs : Dense (⋃ f ∈ s, (basicOpen f : Set (PrimeSpectrum R))))
    (H : ∀ f ∈ s, Dense (⋃ g ∈ {g : Localization.Away f |
          IsFinitePresentationFreeAway (Localization.Away f)
            (Localization (algebraMapSubmonoid S (.powers f)))
            (Localization (algebraMapSubmonoid S (.powers f)) ⊗[S] M) g},
        (basicOpen g : Set (PrimeSpectrum (Localization.Away f))))) :
    Dense (⋃ f ∈ {f : R | IsFinitePresentationFreeAway R S M f},
      (basicOpen f : Set (PrimeSpectrum R)))

Tag 051Z, a lemma

Tag 051Z in the Stacks Project.

Algebra.exists_isOpen_dense_isFinitePresentationFreeAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/GenericFlatness.lean, line 867. The attribute's comment: “The four conditions on f are the condition of Equation 051U, cited as Algebra.IsFinitePresentationFreeAway; that definition fixes the models of R_f, S_f and M_f, and Algebra.isFinitePresentationFreeAway_iff moves the conclusion to any other models.”.

Stacks 051Z (generic flatness over a reduced base). Let R → S be a ring map of finite type with R reduced, and let M be a finite S-module. Then there is an open dense subset U ⊆ Spec R such that every u ∈ U lies in a standard open D(f) ⊆ U for which M_f and S_f are free over R_f, S_f is a finitely presented R_f-algebra and M_f is a finitely presented S_f-module.

public theorem exists_isOpen_dense_isFinitePresentationFreeAway {R S M : Type*} [CommRing R]
    [IsReduced R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S] [AddCommGroup M]
    [Module S M] [Module.Finite S M] :
    ∃ U : Set (PrimeSpectrum R), IsOpen U ∧ Dense U ∧
      ∀ u ∈ U, ∃ f : R, u ∈ basicOpen f ∧ (basicOpen f : Set (PrimeSpectrum R)) ⊆ U ∧
        IsFinitePresentationFreeAway R S M f

Sources

• Section 10.118, Tag 051Q
• AxiomMath/Stacks at 5ed82d14

LeanModule.exists_ne_zero_free_localizedModule_away · Module.FinitePresentation.exists_ne_zero_free_localizedModule_away · Algebra.exists_ne_zero_isFinitePresentationFreeAway · Algebra.IsFinitePresentationFreeAway · Algebra.iUnion_basicOpen_isFinitePresentationFreeAway_inter_subset_of_shortExact · Algebra.image_comap_iUnion_basicOpen_isFinitePresentationFreeAway · Algebra.dense_iUnion_basicOpen_isFinitePresentationFreeAway_of_localizationAway · Algebra.exists_isOpen_dense_isFinitePresentationFreeAway

Section10.119 Around Krull-Akizuki#

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

Tag 00P8, a lemma

Tag 00P8 in the Stacks Project.

exists_localSubring_isNoetherian_ringKrullDim_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullAkizuki/DominatingDimOne.lean, line 330.

Stacks Tag 00P8 (Lemma 10.119.1). Let R be a local Noetherian domain with fraction field K that is not a field. Then there exists a local subring R' of K (so R' ⊆ K) such that:

1. R' dominates R (LocalSubring.range (algebraMap R K) ≤ R'); this encodes both R ⊆ R' and the fact that the inclusion R → R' is a local ring map;
2. R' is Noetherian;
3. R' has Krull dimension 1;
4. the inclusion R → R' is essentially of finite type.

theorem exists_localSubring_isNoetherian_ringKrullDim_eq_one
    (R : Type*) [CommRing R] [IsDomain R] [IsLocalRing R] [IsNoetherianRing R]
    (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]
    (hR : ¬ IsField R) :
    ∃ (R' : LocalSubring K) (hle : LocalSubring.range (algebraMap R K) ≤ R'),
      IsNoetherianRing R'.toSubring ∧
      ringKrullDim R'.toSubring = 1 ∧
      letI : Algebra R R'.toSubring :=
        algebraOfRange R'.toSubring (LocalSubring.le_def.mp hle).choose
      Algebra.EssFiniteType R R'.toSubring

Tag 0BHZ, a lemma

Tag 0BHZ in the Stacks Project.

IsLocalRing.existsUnique_isArtinianRing_or_isRegularLocalRing_or_two_le_depth_or_exists_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalRing/FiniteModification.lean, line 773. The attribute's comment: “The four alternatives are indexed by Fin 4 in the order of the tag, so that ∃! states both that they cover and that they are pairwise exclusive. See the module docstring for the spelling of each one, in particular for case (4).”.

Kollár's four cases. For a Noetherian local ring (R, 𝔪) exactly one of the following holds: (0) R is Artinian; (1) R is regular of dimension 1; (2) depth_𝔪(R) ≥ 2; (3) there is a finite ring map R → R' to a nonzero ring, not an isomorphism, whose kernel and cokernel are annihilated by a power of 𝔪 and for which 𝔪 is not an associated prime of R'.

public theorem
    IsLocalRing.existsUnique_isArtinianRing_or_isRegularLocalRing_or_two_le_depth_or_exists_finite
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] :
    ∃! i : Fin 4,
      ![IsArtinianRing R,
        IsRegularLocalRing R ∧ ringKrullDim R = 1,
        2 ≤ Module.depth R (maximalIdeal R) R,
        ∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R'), Nontrivial R' ∧
          Module.Finite R R' ∧ ¬ Function.Bijective (algebraMap R R') ∧
          maximalIdeal R ∉ associatedPrimes R R' ∧
          ∃ n : ℕ, maximalIdeal R ^ n * RingHom.ker (algebraMap R R') = ⊥ ∧
            maximalIdeal R ^ n • (⊤ : Submodule R R') ≤
              LinearMap.range (Algebra.linearMap R R')] i

Tag 00P9, a lemma

Tag 00P9 in the Stacks Project.

IsLocalRing.exists_finite_of_ringKrullDim_eq_one_of_one_lt_finrank_cotangentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalRing/FiniteModification.lean, line 958. The attribute's comment: “The conclusion is case (4) of Lemma 0BHZ, spelled the same way there; see the module docstring for the reading of each of the four conditions. The hypothesis dim(𝔪/𝔪²) > 1 is 1 < finrank (ResidueField R) (CotangentSpace R).”.

A one-dimensional local ring with non-principal maximal ideal admits a finite modification. Let (R, 𝔪) be a Noetherian local ring of dimension 1 with dim_κ(𝔪/𝔪²) > 1, i.e. with 𝔪 not principal. Then there is a ring map R → R' which is finite, is not an isomorphism, whose kernel and cokernel are annihilated by a power of 𝔪, and for which 𝔪 is not an associated prime of R'.

public theorem
    IsLocalRing.exists_finite_of_ringKrullDim_eq_one_of_one_lt_finrank_cotangentSpace
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (hdim : ringKrullDim R = 1)
    (hcotangent : 1 < Module.finrank (ResidueField R) (CotangentSpace R)) :
    ∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R'), Nontrivial R' ∧
      Module.Finite R R' ∧ ¬ Function.Bijective (algebraMap R R') ∧
      maximalIdeal R ∉ associatedPrimes R R' ∧
      ∃ n : ℕ, maximalIdeal R ^ n * RingHom.ker (algebraMap R R') = ⊥ ∧
        maximalIdeal R ^ n • (⊤ : Submodule R R') ≤
          LinearMap.range (Algebra.linearMap R R')

Tag 00PB, an example

Tag 00PB in the Stacks Project.

exists_noetherianLocalDomain_adicCompletion_not_reduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Counterexample.lean, line 389. The attribute's comment: “The existential form of the tag, which is what Stacks 07NZ consumes: the source's k is any countable field of characteristic two, here ULift (ZMod 2), so that the witness lands in an arbitrary universe. StacksFrontier.RingTheory.AnalyticallyUnramified.Examples carries the source's other construction, over a field with [k : k^p] = ∞.”.

Stacks 00PB. There is a one-dimensional Noetherian local domain of positive prime characteristic whose completion at its maximal ideal is nonreduced, i.e. which is not analytically unramified.

public theorem exists_noetherianLocalDomain_adicCompletion_not_reduced :
    ∃ (p : ℕ), p.Prime ∧
      ∃ (R : Type u) (_ : CommRing R) (_ : CharP R p) (_ : IsLocalRing R)
        (_ : IsNoetherianRing R) (_ : IsDomain R),
        ringKrullDim R = 1 ∧ ¬ IsAnalyticallyUnramified R

PowerSeries.isDiscreteValuationRing_finiteCoeffSubring, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Examples.lean, line 240. The attribute's comment: “The ring A is a discrete valuation ring.”.

Stacks 00PB: A is a discrete valuation ring, with uniformizer x.

theorem isDiscreteValuationRing_finiteCoeffSubring :
    IsDiscreteValuationRing (finiteCoeffSubring k p)

PowerSeries.nonempty_algEquiv_adicCompletion_finiteCoeffSubring, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Examples.lean, line 292. The attribute's comment: “The completion of A is k[[x]]: an isomorphism of A-algebras A^ ≃ k[[x]].”.

Stacks 00PB: the completion of A is k[[x]]. The inclusion A ⊆ k[[x]] induces an isomorphism of A-algebras from the completion of A to k[[x]].

theorem nonempty_algEquiv_adicCompletion_finiteCoeffSubring :
    Nonempty (AdicCompletion (IsLocalRing.maximalIdeal (finiteCoeffSubring k p))
      (finiteCoeffSubring k p) ≃ₐ[finiteCoeffSubring k p] k⟦X⟧)

PowerSeries.isLocalRing_adjoinSubalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Examples.lean, line 453. The attribute's comment: “For f ∉ A the ring R = A[f] ⊆ k[[x]] is local.”.

Stacks 00PB: R = A[f] is local.

theorem isLocalRing_adjoinSubalgebra {f : k⟦X⟧} (hf : f ∉ finiteCoeffSubring k p) :
    IsLocalRing (adjoinSubalgebra (p := p) f)

PowerSeries.isNoetherianRing_adjoinSubalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Examples.lean, line 462. The attribute's comment: “The ring R = A[f] ⊆ k[[x]] is Noetherian.”.

Stacks 00PB: R = A[f] is Noetherian. It is of finite type over the Noetherian ring A.

theorem isNoetherianRing_adjoinSubalgebra (f : k⟦X⟧) :
    IsNoetherianRing (adjoinSubalgebra (p := p) f)

PowerSeries.ringKrullDim_adjoinSubalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Examples.lean, line 471. The attribute's comment: “For f ∉ A the ring R = A[f] ⊆ k[[x]] has Krull dimension one.”.

Stacks 00PB: R = A[f] has dimension one. It is integral over A, with the same Krull dimension.

theorem ringKrullDim_adjoinSubalgebra {f : k⟦X⟧} (hf : f ∉ finiteCoeffSubring k p) :
    ringKrullDim (adjoinSubalgebra (p := p) f) = 1

PowerSeries.not_isAnalyticallyUnramified_adjoinSubalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Examples.lean, line 489. The attribute's comment: “For f ∉ A the completion of R = A[f] is not reduced, i.e. R is not analytically unramified (Definition 032X).”.

Stacks 00PB: the completion of R = A[f] is not reduced. The series f is a p-th root of f ^ p ∈ A in the completion k[[x]] of A, while R = A[T] ⧸ (T ^ p - f ^ p); so the completion of R contains the nonzero nilpotent T - f (AdjoinRoot.not_isReduced_adicCompletion_of_pow_eq).

theorem not_isAnalyticallyUnramified_adjoinSubalgebra {f : k⟦X⟧}
    (hf : f ∉ finiteCoeffSubring k p) :
    letI := isLocalRing_adjoinSubalgebra hf
    ¬ IsAnalyticallyUnramified (adjoinSubalgebra (p := p) f)

PowerSeries.isPurelyInseparable_laurentSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Examples.lean, line 544. The attribute's comment: “The extension k((x)) of the fraction field of A is purely inseparable; that it has infinite degree is PowerSeries.not_finiteDimensional_laurentSeries.”.

Stacks 00PB: k((x)) is purely inseparable over the fraction field of A. The p-th power of x ^ m g, g ∈ k[[x]], is x ^ (p m) g ^ p with g ^ p ∈ A.

theorem isPurelyInseparable_laurentSeries :
    letI := (fractionRingToLaurentSeries (k := k) (p := p)).toAlgebra
    IsPurelyInseparable (FractionRing (finiteCoeffSubring k p)) (LaurentSeries k)

PowerSeries.not_finiteDimensional_laurentSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Examples.lean, line 920. The attribute's comment: “The extension k((x)) of the fraction field of A has infinite degree when [k : k^p] = ∞.”.

Stacks 00PB: k((x)) has infinite degree over the fraction field of A, when [k : k^p] = ∞. The series f_j = ∑ₙ t_{⟨j, n⟩} xⁿ built from a p-independent sequence (tᵢ) in k satisfy f_m ∉ Frac(A)(f_0, …, f_{m-1}).

theorem not_finiteDimensional_laurentSeries
    (hk : ¬ FiniteDimensional (pthPowerSubfield k p) k) :
    letI := (fractionRingToLaurentSeries (k := k) (p := p)).toAlgebra
    ¬ FiniteDimensional (FractionRing (finiteCoeffSubring k p)) (LaurentSeries k)

Tag 00PD, a lemma

Tag 00PD in the Stacks Project.

isDiscreteValuationRing_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/TFAE.lean, line 300. The attribute's comment: “Item (6) is the source's closing sentence, stated as an item because it is equivalent to the others: it is item (4) with IsNoetherianRing traded for the factorization property. 0 is excluded there, being of no such form in a domain. See the module docstring for the spelling of dimension 1, of generated by a single nonzero element and of normal.”. References: EGA 0 (17.1.4), “(ii)”; EGA II (7.1.6), “more general”; EGA 0 (17.1.4), “(ii)”; EGA IV (14.5.7), “more general”.

Characterizations of a discrete valuation ring. For a commutative ring A the following are equivalent: (1) A is a discrete valuation ring; (2) A is a Noetherian valuation ring and not a field; (3) A is a regular local ring of dimension 1; (4) A is a Noetherian local domain whose maximal ideal is generated by a single nonzero element; (5) A is a Noetherian local normal domain of dimension 1; (6) A is a local domain whose maximal ideal is generated by a single nonzero element, and for every generator π of the maximal ideal every nonzero x ∈ A is u * π ^ n for a unique pair (n, u).

public theorem isDiscreteValuationRing_tfae (A : Type u) [CommRing A] :
    List.TFAE
      [ ∃ _ : IsDomain A, IsDiscreteValuationRing A,
        ∃ _ : IsDomain A, ValuationRing A ∧ IsNoetherianRing A ∧ ¬ IsField A,
        IsRegularLocalRing A ∧ ringKrullDim A = 1,
        ∃ _ : IsLocalRing A, IsNoetherianRing A ∧ IsDomain A ∧
          (maximalIdeal A).IsPrincipal ∧ maximalIdeal A ≠ ⊥,
        IsNoetherianRing A ∧ IsLocalRing A ∧ IsDomain A ∧ IsIntegrallyClosed A ∧
          ringKrullDim A = 1,
        ∃ _ : IsLocalRing A, IsDomain A ∧ (maximalIdeal A).IsPrincipal ∧ maximalIdeal A ≠ ⊥ ∧
          ∀ π : A, maximalIdeal A = Ideal.span {π} →
            ∀ x : A, x ≠ 0 → ∃! p : ℕ × Aˣ, x = p.2 * π ^ p.1 ]

Tag 09DZ, a definition

Tag 09DZ in the Stacks Project.

Declarations registered for the tag:

• IsDiscreteValuationRing.irreducible_iff_uniformizer registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch10.lean, line 259 (StacksFrontier).

Tag 00PE, a lemma

Tag 00PE in the Stacks Project.

length_quotient_span_singleton_lt_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullAkizuki/LengthBound.lean, line 63. The attribute's comment: “(1)”.

Statement 1 (Finiteness). If R is a local Noetherian integral domain of Krull dimension 1 and x ≠ 0, then R / xR has finite length as an R-module.

theorem length_quotient_span_singleton_lt_top (hdim : ringKrullDim R = 1) (x : R) (hx : x ≠ 0) :
    Module.length R (R ⧸ Ideal.span {x}) < ⊤

length_quot_smul_le_mul_length_quot_span, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullAkizuki/LengthBound.lean, line 474. The attribute's comment: “(2)”.

Statement 2 (Bound). Let R be a local Noetherian integral domain of Krull dimension 1 with fraction field K = FractionRing R. For a non-negative integer r, any R-submodule M of K^r = (Fin r → K), and any nonzero x ∈ R, the length of M / xM is bounded by r * length (R / xR). Here xM = x • M and M / xM is the quotient of M by the submodule Submodule.comap M.subtype (x • M).

theorem length_quot_smul_le_mul_length_quot_span
    (r : ℕ) (M : Submodule R (Fin r → FractionRing R)) (x : R) (hx : x ≠ 0) :
    Module.length R (M ⧸ Submodule.comap M.subtype (x • M))
      ≤ r * Module.length R (R ⧸ Ideal.span {x})

Tag 031F, a lemma

Tag 031F in the Stacks Project.

Ideal.isMaximal_and_finite_primesOver_and_module_finite_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/Over/HeightOne.lean, line 654. The attribute's comment: “The three assertions of the tag, for an arbitrary maximal ideal m of a Noetherian domain with Ring.KrullDimLE 1 rather than for the maximal ideal of a local ring of dimension one, together with the finite-dimensionality of S/mS over κ(m) from which the author's proof deduces them. See the module docstring.”.

Let R be a Noetherian domain of Krull dimension at most one with fraction field K, let L/K be a finite field extension, and let S be a domain with fraction field L which is an R-algebra compatibly with K ⊆ L. Then, for every maximal ideal m of R, every prime n of S lying over m is maximal, only finitely many primes of S lie over m, each residue field extension κ(n)/κ(m) is finite, and moreover S/mS is a finite-dimensional κ(m)-vector space.

public theorem isMaximal_and_finite_primesOver_and_module_finite_quotient
    (R S K L : Type*) [CommRing R] [IsDomain R] [IsNoetherianRing R] [Ring.KrullDimLE 1 R]
    [CommRing S] [IsDomain S] [Algebra R S]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra S L] [IsFractionRing S L]
    [Algebra K L] [FiniteDimensional K L] [Algebra R L] [IsScalarTower R K L]
    [IsScalarTower R S L] (m : Ideal R) [m.IsMaximal] :
    (∀ (n : Ideal S) [n.IsPrime] [n.LiesOver m], n.IsMaximal) ∧
      (m.primesOver S).Finite ∧
      (∀ (n : Ideal S) [n.IsPrime] [n.LiesOver m], Module.Finite (R ⧸ m) (S ⧸ n)) ∧
      Module.Finite (R ⧸ m) (S ⧸ m.map (algebraMap R S))

Tag 00PF, a lemma

Tag 00PF in the Stacks Project.

isFiniteLength_quotSMulTop_of_finiteDimensional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Length/QuotSMulTop.lean, line 380. The attribute's comment: “For an arbitrary finite-dimensional vector space V over the fraction field in place of K^{⊕ r}, and with dim R = 1 weakened to Ring.KrullDimLE 1 R. See the module docstring.”.

Let R be a Noetherian domain of Krull dimension at most one with fraction field K, let V be a finite-dimensional K-vector space and let M be an R-submodule of V. Then for every nonzero x ∈ R the R-module M / xM has finite length. Note that M is not assumed to be a finitely generated R-module.

public theorem isFiniteLength_quotSMulTop_of_finiteDimensional
    {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] [Ring.KrullDimLE 1 R]
    (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]
    {V : Type*} [AddCommGroup V] [Module K V] [FiniteDimensional K V]
    [Module R V] [IsScalarTower R K V]
    (M : Submodule R V) {x : R} (hx : x ≠ 0) :
    IsFiniteLength R (QuotSMulTop x M)

Tag 00PG, a lemma

Tag 00PG in the Stacks Project.

krull_akizuki, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/KrullAkizuki/IntermediateRingNoetherian.lean, line 728. References: EGA IV (18.9.7.8), “more general”; EGA IV (21.9.10), “Domain case”.

Krull-Akizuki (Stacks Tag 00PG). Let R be a Noetherian integral domain of Krull dimension one, with fraction field K, and let L be a finite field extension of K. Then every intermediate ring A with R ⊆ A ⊆ L is Noetherian.

theorem krull_akizuki
    (R : Type*) [CommRing R] [IsDomain R]
    (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]
    (L : Type*) [Field L] [Algebra K L] [Module.Finite K L]
    [Algebra R L] [IsScalarTower R K L]
    [IsNoetherianRing R] (hdim : ringKrullDim R = 1)
    (A : Subring L) (hA : (algebraMap R L).range ≤ A) :
    IsNoetherianRing A

Tag 00PH, a lemma

Tag 00PH in the Stacks Project.

exists_isDiscreteValuationRing_isFractionRing_of_not_isField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/Existence.lean, line 460. The attribute's comment: “A is produced as a Subalgebra R L, so that both inclusions are algebraMaps and domination is IsLocalHom (algebraMap R ↥A). L/K finitely generated as a field extension is Algebra.EssFiniteType K L, by IntermediateField.fg_top_iff. See the module docstring.”. References: EGA II (7.1.7); EGA IV (15.1.1.6), “DVR dom. A, frac field K”; EGA II (7.1.7); EGA II (7.1.2), “special case”.

Stacks 00PH. Let R be a Noetherian local domain with fraction field K which is not a field, and let L/K be a finitely generated field extension. Then there is an R-subalgebra A of L which is a discrete valuation ring with fraction field L and which dominates R, the last condition being IsLocalHom (algebraMap R ↥A), that is 𝔪_A ∩ R = 𝔪_R.

public theorem exists_isDiscreteValuationRing_isFractionRing_of_not_isField
    {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsLocalRing R]
    (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]
    {L : Type*} [Field L] [Algebra K L] [Algebra.EssFiniteType K L]
    [Algebra R L] [IsScalarTower R K L] (hR : ¬ IsField R) :
    ∃ A : Subalgebra R L, IsDiscreteValuationRing A ∧ IsFractionRing A L ∧
      IsLocalHom (algebraMap R A)

Sources

• Section 10.119, Tag 00P7
• AxiomMath/Stacks at 5ed82d14

Leanexists_localSubring_isNoetherian_ringKrullDim_eq_one · IsLocalRing.existsUnique_isArtinianRing_or_isRegularLocalRing_or_two_le_depth_or_exists_finite · IsLocalRing.exists_finite_of_ringKrullDim_eq_one_of_one_lt_finrank_cotangentSpace · exists_noetherianLocalDomain_adicCompletion_not_reduced · PowerSeries.isDiscreteValuationRing_finiteCoeffSubring · PowerSeries.nonempty_algEquiv_adicCompletion_finiteCoeffSubring · PowerSeries.isLocalRing_adjoinSubalgebra · PowerSeries.isNoetherianRing_adjoinSubalgebra

Section10.120 Factorization#

Section 10.120 of the Stacks Project, Tag 034O. 17 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 17 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 034P, a definition

Tag 034P in the Stacks Project.

Declarations registered for the tag:

• Associated registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch10.lean, line 126 (StacksFrontier): “(1) associates”.
• Ideal.span_singleton_prime registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch10.lean, line 130 (StacksFrontier): “(3) prime element, for nonzero elements”.

Tag 034Q, a lemma

Tag 034Q in the Stacks Project.

Declarations registered for the tag:

• Ideal.span_singleton_eq_span_singleton registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 63 (StacksFrontier): “associates generate the same principal ideal”.

Tag 034R, a lemma

Tag 034R in the Stacks Project.

Declarations registered for the tag:

• WfDvdMonoid.of_setOfPred_isPrincipal_wellFoundedOn_gt registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 68 (StacksFrontier): “ACC on principal ideals implies WfDvdMonoid”.
• WfDvdMonoid.not_isUnit_iff_exists_factors_eq registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 70 (StacksFrontier): “a nonzero nonunit factors into irreducibles”.

Tag 034S, a definition

Tag 034S in the Stacks Project.

Declarations registered for the tag:

• UniqueFactorizationMonoid registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 75 (StacksFrontier): “unique factorization domains”. References: EGA IV (21.7.7); SGA 2 XI (3.10).
• UniqueFactorizationMonoid.of_existsUnique_irreducible_factors registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 78 (StacksFrontier): “existence and uniqueness of irreducible factorizations characterize a UFD”.
• UniqueFactorizationMonoid.factors_unique registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 80 (StacksFrontier): “uniqueness of irreducible factorizations, up to associates and permutation”.

Tag 034T, a lemma

Tag 034T in the Stacks Project.

Declarations registered for the tag:

• UniqueFactorizationMonoid.irreducible_iff_prime registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 84 (StacksFrontier): “in a UFD every irreducible element is prime”.
• UniqueFactorizationMonoid.of_exists_prime_factors registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 86 (StacksFrontier): “factorization into primes gives a UFD”.

Tag 0AFU, a lemma

Tag 0AFU in the Stacks Project.

localized_irreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniqueFactorizationDomain/Nagata.lean, line 184. The attribute's comment: “(1)”.

(Localized irreducibility.) If x is irreducible in A, then its image in the localization S⁻¹A is irreducible or a unit.

theorem localized_irreducible (S : Submonoid A) (hS : GenByPrimes S)
    (x : A) (hx : Irreducible x) :
    Irreducible (algebraMap A (Localization S) x) ∨
      IsUnit (algebraMap A (Localization S) x)

prime_iff_localized_prime_or_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniqueFactorizationDomain/Nagata.lean, line 421. The attribute's comment: “(2)”.

(Primality criterion.) If x is irreducible in A, then x is prime in A if and only if its image in S⁻¹A is prime or a unit.

PROOF (assembled; sub-lemmas above carry the content): (→) Given Prime x. Decide IsUnit (φ x): if so, right disjunct; else by sub-lemma (2b) Prime (φ x), left disjunct. (←) Given Prime (φ x) ∨ IsUnit (φ x): the prime case is sub-lemma (2c), the unit case is sub-lemma (2a).

theorem prime_iff_localized_prime_or_unit (S : Submonoid A) (hS : GenByPrimes S)
    (x : A) (hx : Irreducible x) :
    Prime x ↔
      (Prime (algebraMap A (Localization S) x) ∨
        IsUnit (algebraMap A (Localization S) x))

nagata_criterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniqueFactorizationDomain/Nagata.lean, line 582. The attribute's comment: “Moreover”.

(Nagata's criterion for factoriality.) A is a UFD if and only if every nonzero nonunit of A factors into irreducibles and S⁻¹A is a UFD.

PROOF (assembled; the content is in the sub-lemmas above and theorems (1),(2)): (→) UFD A ⇒ irreducible factorizations exist (3b) and S⁻¹A is a UFD (3c). (←) Given irreducible factorizations and UFD (S⁻¹A): build UFD A via UniqueFactorizationMonoid.of_exists_prime_factors (Stacks 034T). For a ≠ 0: units factor as the empty product; for a nonunit, take its irreducible factorization and observe each irreducible factor is prime by (3a) (which itself uses theorems (1),(2) and UFD (S⁻¹A)); the product equals a exactly, hence is Associated to a.

theorem nagata_criterion (S : Submonoid A) (hS : GenByPrimes S) :
    UniqueFactorizationMonoid A ↔
      (HasIrreducibleFactorizations A ∧
        UniqueFactorizationMonoid (Localization S))

Tag 0BUD, a lemma

Tag 0BUD in the Stacks Project.

Declarations registered for the tag:

• Ideal.setOfPred_isPrincipal_wellFoundedOn_gt registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 108 (StacksFrontier): “a UFD satisfies ACC on principal ideals”.

Tag 0BUE, a lemma

Tag 0BUE in the Stacks Project.

polynomial_wfDvdMonoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 136.

Headline: if R is a commutative domain satisfying ACCP (WfDvdMonoid R), then R[X] also satisfies ACCP.

theorem polynomial_wfDvdMonoid {R : Type*} [CommRing R] [IsDomain R] [WfDvdMonoid R] :
    WfDvdMonoid (Polynomial R)

Tag 0BC1, a lemma

Tag 0BC1 in the Stacks Project.

Declarations registered for the tag:

• Polynomial.uniqueFactorizationMonoid registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 102 (StacksFrontier): “a polynomial ring over a UFD is a UFD”.
• MvPolynomial.uniqueFactorizationMonoid registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 103 (StacksFrontier): “a multivariate polynomial ring over a UFD is a UFD”.

Tag 0AFV, a lemma

Tag 0AFV in the Stacks Project.

Declarations registered for the tag:

• UniqueFactorizationMonoid.instIsIntegrallyClosed registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 94 (StacksFrontier): “a UFD is integrally closed”.

Tag 034U, a definition

Tag 034U in the Stacks Project.

Declarations registered for the tag:

• IsPrincipalIdealRing registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch10.lean, line 287 (StacksFrontier): “a principal ideal domain is a domain (IsDomain) that is a principal ideal ring”.

Tag 034V, a lemma

Tag 034V in the Stacks Project.

Declarations registered for the tag:

• PrincipalIdealRing.to_uniqueFactorizationMonoid registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 90 (StacksFrontier): “a principal ideal domain is a UFD”.

Tag 034W, a definition

Tag 034W in the Stacks Project.

HasUniquePrimeIdealFactorization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DedekindDomain/PrimeFactorization.lean, line 41.

The property that every nonzero ideal of R can be written as a product of nonzero prime ideals, uniquely up to permutation.

def HasUniquePrimeIdealFactorization (R : Type*) [CommRing R] : Prop

Tag 0AUQ, a lemma

Tag 0AUQ in the Stacks Project.

Declarations registered for the tag:

• IsPrincipalIdealRing.isDedekindDomain registered with add_to_stacks in StacksFrontier/RingTheory/UniqueFactorizationDomain/Basic.lean, line 97 (StacksFrontier): “a principal ideal domain is a Dedekind domain”. References: EGA III (7.4.3), “special case”.

Tag 09ME, a lemma

Tag 09ME in the Stacks Project.

Ideal.invertible_of_mul_eq_span_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/Invertible.lean, line 215. The attribute's comment: “Stated as Module.Invertible A ↥I for one factor: the hypotheses are symmetric in I and J, and finite generation and local freeness of rank 1 follow from invertibility. The source's I ≠ 0 and J ≠ 0 are consequences of the hypothesis on f and are omitted. See the module docstring.”.

A factor of a principal ideal generated by a nonzerodivisor is invertible. Let A be a commutative ring and let I and J be ideals of A with I * J = (f) for a nonzerodivisor f ∈ A. Then I is an invertible A-module, that is, finite locally free of rank 1; in particular I is a finitely generated ideal. Applying this to J * I = (f) gives the same conclusions for J.

public theorem invertible_of_mul_eq_span_singleton {A : Type*} [CommRing A] {I J : Ideal A}
    {f : A} (hf : f ∈ nonZeroDivisors A) (hIJ : I * J = Ideal.span {f}) :
    Module.Invertible A I

Tag 034X, a lemma

Tag 034X in the Stacks Project.

Stacks.hasUniquePrimeIdealFactorization_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DedekindDomain/TFAE.lean, line 236.

Stacks 034X. For a ring R the following are equivalent: 1. R is a Dedekind domain in the sense of tag 034W: a domain in which every nonzero ideal is a product of nonzero prime ideals, uniquely up to permutation; 2. R is a Noetherian domain and R_𝔪 is a discrete valuation ring for every nonzero maximal ideal 𝔪; 3. R is a Noetherian normal domain of Krull dimension at most one.

In (2) the domain hypothesis is an existential binder, so that it is available as an instance when stating that the localizations are discrete valuation rings.

theorem hasUniquePrimeIdealFactorization_tfae (R : Type*) [CommRing R] :
    [IsDomain R ∧ HasUniquePrimeIdealFactorization R,
      ∃ _ : IsDomain R, IsNoetherianRing R ∧
        ∀ (m : Ideal R) [m.IsMaximal], m ≠ ⊥ → IsDiscreteValuationRing (Localization.AtPrime m),
      IsDomain R ∧ IsNoetherianRing R ∧ IsIntegrallyClosed R ∧ ringKrullDim R ≤ 1].TFAE

Tag 09IG, a lemma

Tag 09IG in the Stacks Project.

IsIntegralClosure.isDedekindDomain_and_comap_surjective_and_quasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/DedekindDomain.lean, line 339. The attribute's comment: “Finite fibres and finiteness of the induced residue field extensions are packaged as Algebra.QuasiFinite A C, from which they follow by name; dim A = 1 is weakened to Ring.DimensionLEOne A. See the module docstring.”. References: EGA 0 (23.2.6), “residue extensions”; EGA 0 (23.2.8), “(ii), dim ≤ 1”; EGA 0 (23.2.7), “partial”; EGA IV (18.9.7.8), “more general”; EGA IV (9.5.7), “B is a Dedekind ring”.

Variant of Krull–Akizuki. Let A be a Noetherian domain of Krull dimension at most one with fraction field K, let L/K be a finite field extension and let C be the integral closure of A in L. Then C is a Dedekind domain, the map Spec(C) → Spec(A) is surjective, and C is quasi-finite over A; the latter says that every fibre κ(𝔭) ⊗[A] C is a finite-dimensional κ(𝔭)-vector space, whence Spec(C) → Spec(A) has finite fibres and induces finite residue field extensions. Neither A integrally closed nor L/K separable is assumed, so C need not be a finite A-algebra.

public theorem isDedekindDomain_and_comap_surjective_and_quasiFinite
    (A K L C : Type*) [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.DimensionLEOne A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L]
    [CommRing C] [Algebra A C] [Algebra C L] [IsScalarTower A C L] [IsIntegralClosure C A L] :
    IsDedekindDomain C ∧ Function.Surjective (PrimeSpectrum.comap (algebraMap A C)) ∧
      Algebra.QuasiFinite A C

Sources

• Section 10.120, Tag 034O
• AxiomMath/Stacks at 5ed82d14

LeanAssociated · Ideal.span_singleton_prime · Ideal.span_singleton_eq_span_singleton · WfDvdMonoid.of_setOfPred_isPrincipal_wellFoundedOn_gt · WfDvdMonoid.not_isUnit_iff_exists_factors_eq · UniqueFactorizationMonoid · UniqueFactorizationMonoid.of_existsUnique_irreducible_factors · UniqueFactorizationMonoid.factors_unique

Section10.121 Orders of vanishing#

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

Tag 02MC, a lemma

Tag 02MC in the Stacks Project.

Module.length_quotSMulTop_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Lattice/Distance.lean, line 146. The attribute's comment: “Stated for an arbitrary module M in place of R, of which the source's identity length_R(R ⧸ (ab)) = length_R(R ⧸ (a)) + length_R(R ⧸ (b)) is the case M = R, and with b a nonzerodivisor weakened to b acting injectively on M. The equation uses no hypothesis on R; the source's finiteness assertion is isFiniteLength_quotient_span_singleton. See the module docstring.”.

Let R be a commutative ring, M an R-module and a, b ∈ R with b acting injectively on M. Then length_R(M ⧸ abM) = length_R(M ⧸ aM) + length_R(M ⧸ bM), an identity in ℕ∞.

theorem Module.length_quotSMulTop_mul {R M : Type*} [CommRing R] [AddCommGroup M]
    [Module R M] {a b : R} (hb : IsSMulRegular M b) :
    Module.length R (QuotSMulTop (a * b) M) =
      Module.length R (QuotSMulTop a M) + Module.length R (QuotSMulTop b M)

Tag 02ME, a definition

Tag 02ME in the Stacks Project.

span_eq_top_of_isBaseChange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Lattice/Distance.lean, line 71. The attribute's comment: “The definition itself is Mathlib's Submodule.IsLattice K M, finite generation over R together with span_K M = ⊤; this is the implication from the source's phrasing V = K ⊗_R M, the remark following the definition. Locality of R, dimension one and finite dimensionality of V are used by neither.”.

If the canonical base-change map K ⊗[R] M → V induced by the inclusion M ↪ V is an isomorphism, then the K-span of M inside V is all of V.

lemma span_eq_top_of_isBaseChange (R : Type*) [CommRing R] (K : Type*) [CommRing K] [Algebra R K]
    (V : Type*) [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V]
    (M : Submodule R V) (h : IsBaseChange K M.subtype) :
    Submodule.span K (M : Set V) = ⊤

Tag 02MF, a lemma

Tag 02MF in the Stacks Project.

Module.length_quotient_submoduleOf_eq_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Lattice/Distance.lean, line 115. The attribute's comment: “(4). Stated for arbitrary submodules N ≤ S ≤ A of a module over a ring, and as an identity in ℕ∞, so that no finiteness and none of the source's hypotheses — locality, dimension one, lattices, finite dimensionality of V — are needed. Parts (1)-(3) are Submodule.isLattice_tfae_of_le_and_iff_of_ge_and_inf_sup and part (5) is Submodule.lengthDist_eq_sub.”.

For N ≤ S ≤ A submodules of V, length_R(A/N) = length_R(S/N) + length_R(A/S), an identity in ℕ∞.

theorem Module.length_quotient_submoduleOf_eq_add {N S A : Submodule R V} (hNS : N ≤ S)
    (hSA : S ≤ A) :
    Module.length R (↥A ⧸ N.submoduleOf A) =
      Module.length R (↥S ⧸ N.submoduleOf S) + Module.length R (↥A ⧸ S.submoduleOf A)

Submodule.isLattice_tfae_of_le_and_iff_of_ge_and_inf_sup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Lattice/Distance.lean, line 337. The attribute's comment: “Parts (1)-(3). Locality is dropped, being used by no part, and finite dimensionality of V follows from the existence of a lattice. Dimension one is an antecedent of parts (1) and (2), over which it is sharp — it is not weakened to Ring.KrullDimLE 1 R, which breaks (2) — and part (3) holds over any Noetherian domain, strengthening Mathlib's Submodule.IsLattice.inf. Parts (4) and (5) hold for arbitrary submodules of a module over a ring, with none of these hypotheses; they are Module.length_quotient_submoduleOf_eq_add and Submodule.lengthDist_eq_sub.”.

Let R be a Noetherian domain with fraction field K and let V be a K-vector space. If R has Krull dimension 1 then: (1) for M a lattice and M ≤ M', the conditions "M' is a lattice", "length_R(M'/M) < ∞" and "M' is finitely generated" are equivalent; (2) for M a lattice and M' ≤ M, M' is a lattice if and only if length_R(M/M') < ∞. Without any hypothesis on the dimension: (3) if M and M' are lattices then so are M ⊓ M' and M ⊔ M'.

theorem Submodule.isLattice_tfae_of_le_and_iff_of_ge_and_inf_sup {R : Type*} [CommRing R]
    [IsDomain R] [IsNoetherianRing R] {K : Type*} [Field K] [Algebra R K] [IsFractionRing R K]
    {V : Type*} [AddCommGroup V] [Module K V] [Module R V] [IsScalarTower R K V] :
    (ringKrullDim R = 1 →
      (∀ M M' : Submodule R V, Submodule.IsLattice K M → M ≤ M' →
          [Submodule.IsLattice K M', Module.length R (↥M' ⧸ M.submoduleOf M') ≠ ⊤,
            M'.FG].TFAE) ∧
      (∀ M M' : Submodule R V, Submodule.IsLattice K M → M' ≤ M →
          (Submodule.IsLattice K M' ↔ Module.length R (↥M ⧸ M'.submoduleOf M) ≠ ⊤))) ∧
    (∀ M M' : Submodule R V, Submodule.IsLattice K M → Submodule.IsLattice K M' →
        Submodule.IsLattice K (M ⊓ M') ∧ Submodule.IsLattice K (M ⊔ M'))

Submodule.lengthDist_eq_sub, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Lattice/Distance.lean, line 442. The attribute's comment: “(5), in the form length_R(M/M ∩ M') - length_R(M'/M ∩ M') = length_R(M/N) - length_R(M'/N); of the source's three expressions for d(M, M') this is the one formalised, the two through M + M' and through a lattice N' ⊇ M + M' being open. Locality is dropped and dimension one is spelled as the pair Ring.KrullDimLE 1 R and ¬ IsField R, which over a Noetherian domain is ringKrullDim R = 1.”.

For lattices M, M' and a lattice N below both, d(M, M') = length_R(M/N) - length_R(M'/N).

theorem Submodule.lengthDist_eq_sub (hR : ¬ IsField R) {M M' N : Submodule R V}
    [Submodule.IsLattice K M] [Submodule.IsLattice K M'] [Submodule.IsLattice K N] (hNM : N ≤ M)
    (hNM' : N ≤ M') :
    M.lengthDist M' = ((Module.length R (↥M ⧸ N.submoduleOf M)).toNat : ℤ)
      - ((Module.length R (↥M' ⧸ N.submoduleOf M')).toNat : ℤ)

Tag 02MG, a definition

Tag 02MG in the Stacks Project.

Submodule.lengthDist, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Lattice/Distance.lean, line 394. The attribute's comment: “Stated for arbitrary submodules of a module over a ring, since the formula uses none of the source's standing hypotheses: those make the two lengths finite, and are carried by 02MF and 02MH rather than left inert here. The difference is taken after ENat.toNat, which is faithful on pairs of lattices by 02MF (1)-(3). See the module docstring.”.

The distance between two submodules M, M' of a module V over a ring R: the integer d(M, M') = length_R(M/(M ∩ M')) - length_R(M'/(M ∩ M')), with both lengths truncated from ℕ∞ by ENat.toNat.

noncomputable def Submodule.lengthDist {R : Type*} [Ring R] {V : Type*} [AddCommGroup V]
    [Module R V] (M M' : Submodule R V) : ℤ

Submodule.lengthDist_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Lattice/Distance.lean, line 402. The attribute's comment: “The remark following the definition. Stated for arbitrary submodules of a module over a ring; on a pair of lattices the length is finite by 02MF (2).”.

For M' ≤ M, d(M, M') = length_R(M/M').

theorem Submodule.lengthDist_of_le {M M' : Submodule R V} (h : M' ≤ M) :
    M.lengthDist M' = (Module.length R (↥M ⧸ M'.submoduleOf M)).toNat

Tag 02MH, a lemma

Tag 02MH in the Stacks Project.

Submodule.lengthDist_antisymm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Lattice/Distance.lean, line 410. The attribute's comment: “(2). Stated for arbitrary submodules of a module over a ring: with both quotients normalised by M ⊓ M' the identity is the antisymmetry of a difference.”.

The distance between two submodules is antisymmetric: d(M, M') = -d(M', M).

theorem Submodule.lengthDist_antisymm (M M' : Submodule R V) :
    M.lengthDist M' = - M'.lengthDist M

Submodule.lengthDist_additive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Lattice/Distance.lean, line 457. The attribute's comment: “(1). Locality is dropped and dimension one is spelled as the pair Ring.KrullDimLE 1 R and ¬ IsField R, which over a Noetherian domain is ringKrullDim R = 1; finite dimensionality of V follows from the existence of a lattice.”.

For lattices M, M', M'' in V, d(M, M'') = d(M, M') + d(M', M'').

theorem Submodule.lengthDist_additive (hR : ¬ IsField R) (M M' M'' : Submodule R V)
    [Submodule.IsLattice K M] [Submodule.IsLattice K M'] [Submodule.IsLattice K M''] :
    M.lengthDist M'' = M.lengthDist M' + M'.lengthDist M''

Tag 02MI, a lemma

Tag 02MI in the Stacks Project.

Stacks.OrderOfVanishing.dist_map_eq_ord_det, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/OrderOfVanishing/Defs.lean, line 1338.

Stacks 02MI. Let R be a Noetherian local domain of dimension 1 with fraction field K, let V be a finite dimensional K-vector space, and let φ : V → V be a K-linear isomorphism. Then for any lattice M ⊆ V, d(M, φ(M)) = ord_R(det φ).

alias dist_map_eq_ord_det

Tag 02MJ, a lemma

Tag 02MJ in the Stacks Project.

ord_norm_eq_sum_inertiaDeg_mul_ord, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/OrderOfVanishing/Norm.lean, line 2765.

Stacks 02MJ. The order of vanishing of the norm of b is the sum, over the maximal ideals v of B, of the inertia degree of v times the order of vanishing of b in B_v.

The localization data for each maximal ideal of B is supplied as instance hypotheses: for each v : MaximalSpectrum B the localization Localization.AtPrime v.asIdeal is a Noetherian ring of Krull dimension at most 1, carries an algebra structure to L compatible with B → L, the IsScalarTower hypothesis pinning it down as the canonical localization map, and is a fraction ring of L. These say exactly that each B_{mᵢ} is a one-dimensional Noetherian local domain with fraction field L.

theorem ord_norm_eq_sum_inertiaDeg_mul_ord
    (A B : Type*) [CommRing A] [CommRing B] [IsDomain A] [IsDomain B]
    [Algebra A B] [Module.Finite A B]
    [IsNoetherianRing A] [IsLocalRing A] [Ring.KrullDimLE 1 A]
    (K L : Type*) [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L]
    [Fintype (MaximalSpectrum B)]
    [∀ v : MaximalSpectrum B, IsNoetherianRing (Localization.AtPrime v.asIdeal)]
    [∀ v : MaximalSpectrum B, Ring.KrullDimLE 1 (Localization.AtPrime v.asIdeal)]
    [∀ v : MaximalSpectrum B, Algebra (Localization.AtPrime v.asIdeal) L]
    [∀ v : MaximalSpectrum B, IsScalarTower B (Localization.AtPrime v.asIdeal) L]
    [∀ v : MaximalSpectrum B, IsFractionRing (Localization.AtPrime v.asIdeal) L]
    (hAB : Function.Injective (algebraMap A B))
    (y : L) (hy : y ≠ 0)
    (x : K) (hx : x = Algebra.norm K y)
    (hx0 : x ≠ 0) :
    ordInt A x hx0 =
      ∑ v : MaximalSpectrum B,
        (Ideal.inertiaDeg' (IsLocalRing.maximalIdeal A) v.asIdeal : ℤ) *
          ordInt (Localization.AtPrime v.asIdeal) y hy

Sources

• Section 10.121, Tag 02MB
• AxiomMath/Stacks at 5ed82d14

LeanModule.length_quotSMulTop_mul · span_eq_top_of_isBaseChange · Module.length_quotient_submoduleOf_eq_add · Submodule.isLattice_tfae_of_le_and_iff_of_ge_and_inf_sup · Submodule.lengthDist_eq_sub · Submodule.lengthDist · Submodule.lengthDist_of_le · Submodule.lengthDist_antisymm

Section10.122 Quasi-finite maps#

Section 10.122 of the Stacks Project, Tag 02MK. 9 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 00PJ, a lemma

Tag 00PJ in the Stacks Project.

PrimeSpectrum.isOpen_singleton_tfae_and_exists_algEquiv_prod_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Artinian/FiniteType.lean, line 371. The attribute's comment: “The source's field k is weakened to an artinian ring; S_𝔮 is an abstract localization Sq, dim_𝔮 Spec S is topologicalKrullDimAt and dim S_𝔮 is 𝔮.height. The closing assertion S_𝔮 = S_g is Mathlib's more general PrimeSpectrum.isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton, with which this tag is realized jointly. See the module docstring.”. References: EGA 0 (14.1.10), “(1)⇔(4), Spec f.t. alg”; EGA II (6.2.2), “affine, base a field”.

Stacks 00PJ. Let k be an artinian ring (a field, in the source), S a k-algebra of finite type, 𝔮 a prime of S and Sq a model of the local ring S_𝔮. The following are equivalent: 𝔮 is an isolated point of Spec S; S_𝔮 is finite over k; D(g) = {𝔮} for some g ∉ 𝔮; Spec S has dimension 0 at 𝔮; 𝔮 is a closed point and dim S_𝔮 = 0; the residue field κ(𝔮) is finite over k and dim S_𝔮 = 0. In that case S = S_𝔮 × S' for a finite type k-algebra S', compatibly with the localization map.

public theorem isOpen_singleton_tfae_and_exists_algEquiv_prod_of_finiteType (k : Type u)
    {S : Type v} [CommRing k] [IsArtinianRing k] [CommRing S] [Algebra k S]
    [Algebra.FiniteType k S] (𝔮 : Ideal S) [𝔮.IsPrime] (Sq : Type w) [CommRing Sq]
    [Algebra S Sq] [IsLocalization.AtPrime Sq 𝔮] [Algebra k Sq] [IsScalarTower k S Sq] :
    List.TFAE
        [IsOpen {(⟨𝔮, ‹_›⟩ : PrimeSpectrum S)},
          Module.Finite k Sq,
          ∃ g ∉ 𝔮, (basicOpen g : Set (PrimeSpectrum S)) = {⟨𝔮, ‹_›⟩},
          topologicalKrullDimAt (PrimeSpectrum S) ⟨𝔮, ‹_›⟩ = 0,
          IsClosed {(⟨𝔮, ‹_›⟩ : PrimeSpectrum S)} ∧ 𝔮.height = 0,
          Module.Finite k 𝔮.ResidueField ∧ 𝔮.height = 0] ∧
      (IsOpen {(⟨𝔮, ‹_›⟩ : PrimeSpectrum S)} →
        ∃ (S' : Type v) (_ : CommRing S') (_ : Algebra k S'), Algebra.FiniteType k S' ∧
          ∃ e : S ≃ₐ[k] Sq × S', ∀ x, (e x).1 = algebraMap S Sq x)

Tag 00PK, a lemma

Tag 00PK in the Stacks Project.

Algebra.isOpen_singleton_fiber_tfae_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/Basic.lean, line 492. The attribute's comment: “The fibre is the subspace comap (algebraMap R S) ⁻¹' {𝔭} of Spec S and q̄ is 𝔮 itself; S_𝔮/𝔭S_𝔮 is κ(𝔭) ⊗_R S_𝔮, i.e. 𝔭.Fiber (Localization.AtPrime 𝔮); dim_q̄ F is topologicalKrullDimAt. See the module docstring.”. References: EGA 0 (14.1.10), “(1)⇔(4) for fibres”; EGA II (6.2.1), “affine case”; EGA II (6.2.2), “affine case, one prime”.

Stacks 00PK. Let R → S be of finite type, let 𝔮 be a prime of S lying over a prime 𝔭 of R, let F = Spec (S ⊗_R κ(𝔭)) be the fibre of Spec S → Spec R over 𝔭 and let q̄ be the point of F corresponding to 𝔮. The following are equivalent: q̄ is an isolated point of F; S_𝔮/𝔭S_𝔮 is finite over κ(𝔭); some g ∉ 𝔮 has 𝔮 as the only prime of D(g) lying over 𝔭; dim_q̄ F = 0; q̄ is a closed point of F and dim S_𝔮/𝔭S_𝔮 = 0; κ(𝔮)/κ(𝔭) is finite and dim S_𝔮/𝔭S_𝔮 = 0.

public theorem isOpen_singleton_fiber_tfae_of_finiteType {R S : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.FiniteType R S] (𝔭 : Ideal R) [𝔭.IsPrime] (𝔮 : Ideal S) [𝔮.IsPrime]
    [𝔮.LiesOver 𝔭] [Algebra (Localization.AtPrime 𝔭) (Localization.AtPrime 𝔮)]
    [Localization.AtPrime.IsLiesOverAlgebra 𝔭 𝔮] :
    List.TFAE
      [IsOpen (X := PrimeSpectrum.comap (algebraMap R S) ⁻¹' {(⟨𝔭, ‹_›⟩ : PrimeSpectrum R)})
          {⟨⟨𝔮, ‹_›⟩, PrimeSpectrum.ext (𝔮.over_def 𝔭).symm⟩},
        Module.Finite 𝔭.ResidueField (𝔭.Fiber (Localization.AtPrime 𝔮)),
        ∃ g ∉ 𝔮, {q ∈ 𝔭.primesOver S | g ∉ q} = {𝔮},
        topologicalKrullDimAt
            ↥(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {(⟨𝔭, ‹_›⟩ : PrimeSpectrum R)})
            ⟨⟨𝔮, ‹_›⟩, PrimeSpectrum.ext (𝔮.over_def 𝔭).symm⟩ = 0,
        IsClosed (X := PrimeSpectrum.comap (algebraMap R S) ⁻¹' {(⟨𝔭, ‹_›⟩ : PrimeSpectrum R)})
            {⟨⟨𝔮, ‹_›⟩, PrimeSpectrum.ext (𝔮.over_def 𝔭).symm⟩} ∧
          ringKrullDim (𝔭.Fiber (Localization.AtPrime 𝔮)) = 0,
        Module.Finite 𝔭.ResidueField 𝔮.ResidueField ∧
          ringKrullDim (𝔭.Fiber (Localization.AtPrime 𝔮)) = 0]

Tag 0H8X, a lemma

Tag 0H8X in the Stacks Project.

quasiFiniteAt_forall_iff_finite_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/Basic.lean, line 1020. References: EGA II (6.2.2), “affine case, b)⇔c)”.

Stacks tag 0H8X, the equivalence of conditions (1) and (2): a finite type ring map R → S is quasi-finite at every prime of S lying over a prime p of R if and only if the fibre S ⊗_R κ(p) is a finite κ(p)-module.

theorem quasiFiniteAt_forall_iff_finite_fiber
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FiniteType R S] (p : Ideal R) [p.IsPrime] :
    -- (1) quasi-finite at every prime of S lying over p
    (∀ (q : Ideal S) [q.IsPrime], q.comap (algebraMap R S) = p →
        Algebra.QuasiFiniteAt R q)
    -- (2) the fibre S ⊗_R κ(p) is a finite κ(p)-module
    ↔ Module.Finite p.ResidueField (p.Fiber S)

moduleFinite_fiber_iff_finite_primeSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/Basic.lean, line 1060. References: EGA II (6.2.2), “affine, one fibre a)⇔b)”.

Stacks tag 0H8X, the equivalence of conditions (2) and (3): for a finite type ring map R → S and a prime p of R, the fibre S ⊗_R κ(p) is a finite κ(p)-module if and only if its prime spectrum Spec(S ⊗_R κ(p)) is finite.

theorem moduleFinite_fiber_iff_finite_primeSpectrum
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FiniteType R S] (p : Ideal R) [p.IsPrime] :
    -- (2) the fibre S ⊗_R κ(p) is a finite κ(p)-module
    Module.Finite p.ResidueField (p.Fiber S)
    -- (3) Spec(S ⊗_R κ(p)) is a finite set
    ↔ Finite (PrimeSpectrum (p.Fiber S))

Tag 077H, a lemma

Tag 077H in the Stacks Project.

quasiFiniteAt_localization_away_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/Basic.lean, line 666.

Stacks tag 077H (Lemma 10.122.6). For a finite type ring map R → S, a prime 𝔮 ⊂ S lying over 𝔭 ⊂ R, an element f ∈ R with f ∉ 𝔭 and an element g ∈ S with g ∉ 𝔮, with R_f = Localization.Away f and S_{fg} = Localization.Away ((algebraMap R S f) * g) and the induced R_f-algebra structure on S_{fg}, the map R → S is quasi-finite at 𝔮 iff R_f → S_{fg} is quasi-finite at Q = 𝔮 S_{fg}.

theorem quasiFiniteAt_localization_away_iff
    {R S Rf Sfg : Type*}
    [CommRing R] [CommRing S] [CommRing Rf] [CommRing Sfg]
    [Algebra R S] [Algebra R Rf] [Algebra R Sfg] [Algebra S Sfg] [Algebra Rf Sfg]
    [IsScalarTower R S Sfg] [IsScalarTower R Rf Sfg]
    (f : R) (g : S)
    [IsLocalization.Away f Rf]
    [IsLocalization.Away (algebraMap R S f * g) Sfg]
    [Algebra.FiniteType R S]
    (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p]
    (hf : f ∉ p) (hg : g ∉ q)
    (Q : Ideal Sfg) (hQ : Q = Ideal.map (algebraMap S Sfg) q) [Q.IsPrime] :
    Algebra.QuasiFiniteAt R q ↔ Algebra.QuasiFiniteAt Rf Q

Tag 00PN, a lemma

Tag 00PN in the Stacks Project.

four_rings_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/Basic.lean, line 543.

Four rings lemma. Given a commutative square of rings R → S, R → R', R' → S', S → S' (encoded by Algebra instances and the appropriate IsScalarTower data) such that R → S is of finite type and the canonical map S ⊗_R R' → S' is surjective, if R → S is quasi-finite at the prime q := q'.under S of S, then R' → S' is quasi-finite at q'.

Proof sketch: base change R → S quasi-finite at q'.under S along R → R', using Algebra.QuasiFiniteAt.baseChange with the tensor product R' ⊗[R] S, to obtain quasi-finiteness of R' → R' ⊗[R] S at a suitable prime P lying over q'.under S and below q'. Then push along the surjective R'-algebra map R' ⊗[R] S →ₐ[R'] S' using Algebra.QuasiFiniteAt.of_surjectiveOnStalks.

theorem four_rings_quasiFiniteAt
    (R S R' S' : Type*)
    [CommRing R] [CommRing S] [CommRing R'] [CommRing S']
    [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S']
    [IsScalarTower R R' S']
    [IsScalarTower R S S']
    [Algebra.FiniteType R S]
    (hsurj : Function.Surjective
      (Algebra.TensorProduct.productMap
        (IsScalarTower.toAlgHom R S S')
        (IsScalarTower.toAlgHom R R' S')))
    (q' : Ideal S') [q'.IsPrime]
    [Algebra.QuasiFiniteAt R (q'.under S)] :
    Algebra.QuasiFiniteAt R' q'

Tag 00PO, a lemma

Tag 00PO in the Stacks Project.

Declarations registered for the tag:

• RingHom.QuasiFinite.comp registered with add_to_stacks in StacksFrontier/RingTheory/QuasiFinite/Basic.lean, line 618 (StacksFrontier).

Tag 00PP, a lemma

Tag 00PP in the Stacks Project.

Algebra.quasiFiniteAt_baseChange_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/BaseChange.lean, line 145. The attribute's comment: “(1). The canonical map Spec(S') → Spec(S) is PrimeSpectrum.comap Algebra.TensorProduct.includeRight.toRingHom, so the source's equality of subsets of Spec(S') is this equivalence quantified over 𝔮'. Quasi-finiteness at a prime (Definition 00PL) is Algebra.QuasiFiniteAt, the source's notion under the finite type hypothesis. The ← direction is Algebra.QuasiFiniteAt.baseChange; → is the new content. Part (3) is Algebra.QuasiFinite.baseChange, tagged 00PP upstream; see the module docstring for part (2).”.

Let R → S be a ring map of finite type, let R → R' be any ring map and set S' = R' ⊗[R] S. Let 𝔮' be a prime of S' and let 𝔮 be its image under the canonical map Spec(S') → Spec(S). Then R' → S' is quasi-finite at 𝔮' if and only if R → S is quasi-finite at 𝔮; equivalently, the quasi-finite locus of Spec(S') is the inverse image of the quasi-finite locus of Spec(S).

public theorem Algebra.quasiFiniteAt_baseChange_iff {R S : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.FiniteType R S] (R' : Type*) [CommRing R'] [Algebra R R']
    (𝔮 : Ideal S) [𝔮.IsPrime] (𝔮' : Ideal (R' ⊗[R] S)) [𝔮'.IsPrime]
    (h : 𝔮 = 𝔮'.comap Algebra.TensorProduct.includeRight.toRingHom) :
    Algebra.QuasiFiniteAt R' 𝔮' ↔ Algebra.QuasiFiniteAt R 𝔮

Tag 0C6H, a lemma

Tag 0C6H in the Stacks Project.

quasiFiniteAt_of_comp_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/Basic.lean, line 822.

Permanence of quasi-finiteness (Stacks tag 0C6H): if the composite of f : A →+* B and g : B →+* C is quasi-finite at a prime r of C, then g itself is quasi-finite at r.

theorem quasiFiniteAt_of_comp_quasiFiniteAt
    {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
    (f : A →+* B) (g : B →+* C)
    (r : Ideal C) [r.IsPrime]
    (h : (g.comp f).QuasiFiniteAt r) :
    g.QuasiFiniteAt r

Tag 02ML, a lemma

Tag 02ML in the Stacks Project.

Algebra.exists_localization_away_map_finite_of_mem_minimalPrimes_of_finite_primesOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/GenericFiniteness.lean, line 393. The attribute's comment: “The hypothesis is (𝔭.primesOver S).Finite; the localizations are arbitrary models (IsLocalization.Away), and R_g → S_g is the canonical IsLocalization.Away.map, whose finiteness is RingHom.Finite. See the module docstring.”.

Generic finiteness of a finite-type map with finite fibre over a minimal prime. Let R → S be a ring map of finite type, let 𝔭 be a minimal prime of R, and assume that only finitely many primes of S lie over 𝔭. Then there is a g ∈ R, g ∉ 𝔭, such that the induced map R_g → S_g on localizations away from g and from its image is finite.

public theorem Algebra.exists_localization_away_map_finite_of_mem_minimalPrimes_of_finite_primesOver
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S] {𝔭 : Ideal R}
    (h𝔭 : 𝔭 ∈ minimalPrimes R) (hfin : (𝔭.primesOver S).Finite) :
    ∃ g ∉ 𝔭, ∀ (Rg Sg : Type*) [CommRing Rg] [CommRing Sg] [Algebra R Rg] [Algebra S Sg]
      [IsLocalization.Away g Rg] [IsLocalization.Away (algebraMap R S g) Sg],
      (IsLocalization.Away.map Rg Sg (algebraMap R S) g).Finite

Sources

• Section 10.122, Tag 02MK
• AxiomMath/Stacks at 5ed82d14

LeanPrimeSpectrum.isOpen_singleton_tfae_and_exists_algEquiv_prod_of_finiteType · Algebra.isOpen_singleton_fiber_tfae_of_finiteType · quasiFiniteAt_forall_iff_finite_fiber · moduleFinite_fiber_iff_finite_primeSpectrum · quasiFiniteAt_localization_away_iff · four_rings_quasiFiniteAt · RingHom.QuasiFinite.comp · Algebra.quasiFiniteAt_baseChange_iff

Section10.123 Zariski's Main Theorem#

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

Tag 00PQ, a lemma

Tag 00PQ in the Stacks Project.

Declarations registered for the tag:

• RingHom.isIntegralElem_leadingCoeff_mul registered with add_to_stacks in StacksFrontier/RingTheory/IntegralClosure/Basic.lean, line 353 (StacksFrontier): “scaling by the leading coefficient makes an element integral”.
• RingHom.isIntegralElem_zero registered with add_to_stacks in StacksFrontier/RingTheory/IntegralClosure/Basic.lean, line 355 (StacksFrontier): “the degenerate case, where the top coefficient vanishes”.

Tag 00PZ, a definition

Tag 00PZ in the Stacks Project.

StronglyTranscendental, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/StronglyTranscendental.lean, line 221.

An element x : S is strongly transcendental over R if for every u : S and every polynomial p : R[X], the equation u * p(x) = 0 in S forces u * (algebraMap R S) (p.coeff i) = 0 for every coefficient index i. This is the algebraic version of the Stacks definition.

def StronglyTranscendental (R S : Type*) [CommRing R] [CommRing S]
    [Algebra R S] (x : S) : Prop

Tag 00Q2, a lemma

Tag 00Q2 in the Stacks Project.

Algebra.not_quasiFiniteAt_of_isStronglyTranscendental, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/StronglyTranscendental.lean, line 199. The attribute's comment: “R ⊂ S is [FaithfulSMul R S] with both rings [IsReduced]; S finite over R[x] is (Polynomial.aeval x).toRingHom.Finite; and "not quasi-finite at any prime" is ¬ Algebra.QuasiFiniteAt R q for an arbitrary prime q of S. The contrapositive is Mathlib's Algebra.not_isStronglyTranscendental_of_quasiFiniteAt, which drops [IsReduced R] and [FaithfulSMul R S]. See the module docstring.”.

Stacks 00Q2. Let R ⊂ S be an inclusion of reduced rings, let x ∈ S be strongly transcendental over R, and assume S is finite over R[x]. Then R → S is not quasi-finite at any prime q of S.

public theorem not_quasiFiniteAt_of_isStronglyTranscendental {R S : Type*} [CommRing R]
    [CommRing S] [IsReduced R] [IsReduced S] [Algebra R S] [FaithfulSMul R S] {x : S}
    (hx : IsStronglyTranscendental R x) (hx' : (Polynomial.aeval (R := R) x).toRingHom.Finite)
    (q : Ideal S) [q.IsPrime] : ¬ QuasiFiniteAt R q

Tag 00Q8, a lemma

Tag 00Q8 in the Stacks Project.

main_theorem_00q8, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ZariskisMainTheorem/Monogenic.lean, line 634.

Stacks tag 00Q8 (Lemma 10.123.11). For S = R[X]/I monogenic over R and a prime q ⊂ S at which R → S is quasi-finite, there is an element g of the integral closure S' of R in S with g ∉ q such that the induced map S'_g → S_g is an isomorphism.

theorem main_theorem_00q8 (R : Type*) [CommRing R] (I : Ideal (R[X]))
    (q : Ideal (R[X] ⧸ I)) [q.IsPrime]
    (hqf : QuasiFiniteAt (R := R) q) :
    ∃ g : integralClosure R (R[X] ⧸ I), (g : R[X] ⧸ I) ∉ q ∧
      Function.Bijective (QF.locMap (R := R) g)

Tag 00QA, a lemma

Tag 00QA in the Stacks Project.

isOpen_quasiFiniteLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/Locus.lean, line 102. References: EGA III (4.4.10), “affine case”; EGA IV (13.1.4), “affine case”; EGA III (4.4.3), “affine case, X' open”; SGA 3 V (7.3), “special case”.

For a finite-type ring map R → S, the locus in Spec(S) where S/R is quasi-finite is open.

theorem isOpen_quasiFiniteLocus
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S] :
    IsOpen (quasiFiniteLocus R S)

Tag 00QB, a lemma

Tag 00QB in the Stacks Project.

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

The map on spectra Spec(S) → Spec(S') induced by the inclusion S' ↪ S is an open topological embedding: a homeomorphism of Spec(S) onto an open subset of Spec(S').

theorem quasiFinite_comap_integralClosure_isOpenEmbedding
    [Algebra.FiniteType R S] [Algebra.QuasiFinite R S] :
    IsOpenEmbedding (PrimeSpectrum.comap (integralClosure R S).val.toRingHom)

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

For every g ∈ S' such that the basic open D(g) ⊆ Spec(S') is contained in the image of Spec(S) → Spec(S'), the natural ring homomorphism S'_g → S_g induced by S' ↪ S is bijective.

theorem quasiFinite_awayMap_integralClosure_bijective
    [Algebra.FiniteType R S] [Algebra.QuasiFinite R S]
    (g : integralClosure R S)
    (hg : (PrimeSpectrum.basicOpen g : Set (PrimeSpectrum (integralClosure R S)))
      ⊆ Set.range (PrimeSpectrum.comap (integralClosure R S).val.toRingHom)) :
    Function.Bijective (Localization.awayMap (integralClosure R S).val.toRingHom g)

quasiFinite_exists_finite_subalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ZariskisMainTheorem.lean, line 680. The attribute's comment: “(3)”. References: EGA III (4.4.3), “affine case, X=X'”; EGA IV (8.12.6), “affine case”; EGA IV (18.12.13), “affine case”; EGA III (4.4.6), “special case”; EGA IV (8.12.9), “Affine case”; SGA 1 VIII (6.4), “affine case”.

There is an R-subalgebra S'' of S, contained in the integral closure S' and finite as an R-module, such that Spec(S) → Spec(S'') is an open topological embedding and S''_g → S_g is bijective for every g ∈ S'' whose basic open D(g) lies in the image of that map.

theorem quasiFinite_exists_finite_subalgebra
    [Algebra.FiniteType R S] [Algebra.QuasiFinite R S] :
    ∃ S'' : Subalgebra R S, S'' ≤ integralClosure R S ∧ Module.Finite R S'' ∧
      IsOpenEmbedding (PrimeSpectrum.comap S''.val.toRingHom) ∧
      ∀ g : S'', (PrimeSpectrum.basicOpen g : Set (PrimeSpectrum S'')) ⊆
          Set.range (PrimeSpectrum.comap S''.val.toRingHom) →
        Function.Bijective (Localization.awayMap S''.val.toRingHom g)

Sources

• Section 10.123, Tag 00PI
• AxiomMath/Stacks at 5ed82d14

LeanRingHom.isIntegralElem_leadingCoeff_mul · RingHom.isIntegralElem_zero · StronglyTranscendental · Algebra.not_quasiFiniteAt_of_isStronglyTranscendental · main_theorem_00q8 · isOpen_quasiFiniteLocus · quasiFinite_comap_integralClosure_isOpenEmbedding · quasiFinite_awayMap_integralClosure_bijective

Section10.124 Applications of Zariski's Main Theorem#

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

Tag 02MM, a lemma

Tag 02MM in the Stacks Project.

Ring.finite_maximalSpectrum_and_sum_inertiaDeg_mul_ord_le_and_eq_iff_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/OrderOfVanishing/Degree.lean, line 927. The attribute's comment: “ord is Ring.ord, valued in ℕ∞, applied to the image of x : A; the residue degrees are Ideal.inertiaDeg; semi-locality is Finite (MaximalSpectrum B); the sum is a finsum. See the module docstring.”.

The degree inequality for orders of vanishing. Let A ⊆ B be an extension of domains with A local Noetherian of dimension at most 1, B of finite type over A, and the induced extension L/K of fraction fields finite. Then B is semi-local, and for every nonzero x in the maximal ideal of A the sum over the maximal ideals 𝔪 of B of [κ(𝔪) : κ(𝔪_A)] · ord_{B_𝔪}(x) is at most [L : K] · ord_A(x), with equality if and only if A → B is finite.

public theorem Ring.finite_maximalSpectrum_and_sum_inertiaDeg_mul_ord_le_and_eq_iff_finite
    {A B : Type*} [CommRing A] [IsDomain A] [IsLocalRing A] [IsNoetherianRing A]
    [Ring.KrullDimLE 1 A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B]
    [Algebra.FiniteType A B] {K L : Type*} [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
    [Algebra B L] [IsFractionRing B L] [Algebra A L] [Algebra K L] [IsScalarTower A B L]
    [IsScalarTower A K L] [Module.Finite K L] :
    Finite (MaximalSpectrum B) ∧
      ∀ x ∈ IsLocalRing.maximalIdeal A, x ≠ 0 →
        (∑ᶠ m : MaximalSpectrum B, (m.asIdeal.inertiaDeg A : ℕ∞) *
              Ring.ord (Localization.AtPrime m.asIdeal)
                (algebraMap B (Localization.AtPrime m.asIdeal) (algebraMap A B x))
            ≤ (Module.finrank K L : ℕ∞) * Ring.ord A x) ∧
          ((∑ᶠ m : MaximalSpectrum B, (m.asIdeal.inertiaDeg A : ℕ∞) *
                Ring.ord (Localization.AtPrime m.asIdeal)
                  (algebraMap B (Localization.AtPrime m.asIdeal) (algebraMap A B x))
              = (Module.finrank K L : ℕ∞) * Ring.ord A x) ↔ Module.Finite A B)

Tag 052V, a lemma

Tag 052V in the Stacks Project.

Stacks.LocalizationOfFiniteAlgebra.essFiniteType_localization_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/EssentialFiniteness/ZariskiApplication.lean, line 305.

Let f : (R, m_R) → (S, m_S) be a local homomorphism of local rings. Assume f is essentially of finite type, the residue field extension κ(m_R) ⊆ κ(m_S) is finite, and the closed fiber S / m_R S has Krull dimension 0. Then S is a localization of a finite R-algebra: there exist a ring S'', a finite ring map g : R →+* S'', a submonoid T ≤ S'', and a ring map h : S'' →+* S exhibiting S as the localization of S'' at T, with h ∘ g = f as R-algebra maps.

theorem essFiniteType_localization_finite {R S : Type u} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (f : R →+* S) [IsLocalHom f]
    (hft : f.EssFiniteType)
    (hres : @Module.Finite (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
      _ _ (residueAlgebra f).toModule)
    (hdim : ringKrullDim (closedFiber f) = 0) :
    ∃ (S'' : Type u) (_ : CommRing S'') (g : R →+* S'') (h : S'' →+* S)
      (T : Submonoid S''),
      g.Finite ∧ h.comp g = f ∧ @IsLocalization S'' _ T S _ h.toAlgebra

Tag 07NC, a lemma

Tag 07NC in the Stacks Project.

AdicCompletion.exists_isIdempotentElem_nonempty_algEquiv_prod_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/QuasiFinite.lean, line 450. The attribute's comment: “The source's B is named here as the explicit factor (S ⊗[R] Rₚ^∧) ⧸ (e) of an idempotent e, which is what makes it an Rₚ^∧-algebra. See the module docstring.”.

Let R be a Noetherian ring, let S be an R-algebra of finite type, and let q be a prime of S lying over p ⊂ R at which R → S is quasi-finite. Let Rₚ and S_q be the local rings of R at p and of S at q. Then the base change of S along the completion Rₚ^∧ of Rₚ at its maximal ideal is, as an S-algebra, the product of the completion S_q^∧ of S_q at its maximal ideal with a complementary factor cut out by an idempotent: Rₚ^∧ ⊗[R] S = S_q^∧ × B for some Rₚ^∧-algebra B.

public theorem AdicCompletion.exists_isIdempotentElem_nonempty_algEquiv_prod_quotient
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [IsNoetherianRing R]
    [Algebra.FiniteType R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime]
    [q.LiesOver p] [Algebra.QuasiFiniteAt R q]
    (Rp : Type*) [CommRing Rp] [Algebra R Rp] [IsLocalization.AtPrime Rp p] [IsLocalRing Rp]
    (Sq : Type*) [CommRing Sq] [Algebra S Sq] [IsLocalization.AtPrime Sq q] [IsLocalRing Sq] :
    ∃ e : S ⊗[R] AdicCompletion (maximalIdeal Rp) Rp, IsIdempotentElem e ∧
      Nonempty (S ⊗[R] AdicCompletion (maximalIdeal Rp) Rp ≃ₐ[S]
        AdicCompletion (maximalIdeal Sq) Sq ×
          ((S ⊗[R] AdicCompletion (maximalIdeal Rp) Rp) ⧸ Ideal.span {e}))

Sources

• Section 10.124, Tag 03GB
• AxiomMath/Stacks at 5ed82d14

LeanRing.finite_maximalSpectrum_and_sum_inertiaDeg_mul_ord_le_and_eq_iff_finite · Stacks.LocalizationOfFiniteAlgebra.essFiniteType_localization_finite · AdicCompletion.exists_isIdempotentElem_nonempty_algEquiv_prod_quotient

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.