15.22 Torsion free modules to 15.42 Regular ring maps

Section15.22 Torsion free modules#

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

Tag 0536, a definition

Tag 0536 in the Stacks Project.

Declarations registered for the tag:

Tag 0537, a lemma

Tag 0537 in the Stacks Project.

Declarations registered for the tag:

Tag 0AUR, a lemma

Tag 0AUR in the Stacks Project.

Declarations registered for the tag:

Tag 0AXM, a lemma

Tag 0AXM in the Stacks Project.

isTorsionFree_baseChange_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/TorsionFree.lean, line 84. References: EGA IV (9.4.9), “partial”.

If R is a domain, R' is a flat R-algebra and M is a torsion-free R-module, then the base change R' ⊗[R] M is a torsion-free R'-module.

theorem isTorsionFree_baseChange_of_flat
    {R R' : Type*} [CommRing R] [CommRing R'] [Algebra R R']
    [IsDomain R] [Module.Flat R R']
    {M : Type*} [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] :
    Module.IsTorsionFree R' (TensorProduct R R' M)
Tag 0AUS, a lemma

Tag 0AUS in the Stacks Project.

isTorsionFree_of_injective_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/TorsionFree.lean, line 104.

For an injective exact pair of module maps, if the source and target modules are torsion-free, then the middle module is torsion-free.

theorem isTorsionFree_of_injective_of_exact
    {R : Type u} [Semiring R]
    {M : Type v} {M' : Type w} {M'' : Type x}
    [AddCommGroup M] [Module R M]
    [AddCommGroup M'] [Module R M']
    [AddCommGroup M''] [Module R M'']
    (f : M →ₗ[R] M') (g : M' →ₗ[R] M'')
    (hf : Function.Injective f) (hfg : Function.Exact f g)
    [Module.IsTorsionFree R M] [Module.IsTorsionFree R M''] :
    Module.IsTorsionFree R M'
Tag 0AUT, a lemma

Tag 0AUT in the Stacks Project.

isTorsionFree_iff_isLocalized_maximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/TorsionFree.lean, line 130.

A module over a domain is torsion-free if and only if its localization at every maximal ideal is torsion-free over the corresponding localized ring.

theorem isTorsionFree_iff_isLocalized_maximal
    {R : Type u} [CommRing R] [IsDomain R]
    {M : Type v} [AddCommMonoid M] [Module R M]
    (Rₚ : ∀ (P : Ideal R) [P.IsMaximal], Type w)
    [∀ (P : Ideal R) [P.IsMaximal], CommRing (Rₚ P)]
    [∀ (P : Ideal R) [P.IsMaximal], Algebra R (Rₚ P)]
    [∀ (P : Ideal R) [P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P]
    (Mₚ : ∀ (P : Ideal R) [P.IsMaximal], Type x)
    [∀ (P : Ideal R) [P.IsMaximal], AddCommMonoid (Mₚ P)]
    [∀ (P : Ideal R) [P.IsMaximal], Module R (Mₚ P)]
    [∀ (P : Ideal R) [P.IsMaximal], Module (Rₚ P) (Mₚ P)]
    [∀ (P : Ideal R) [P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)]
    (f : ∀ (P : Ideal R) [P.IsMaximal], M →ₗ[R] Mₚ P)
    [∀ (P : Ideal R) [P.IsMaximal], IsLocalizedModule.AtPrime P (f P)] :
    Module.IsTorsionFree R M ↔
      ∀ (P : Ideal R) [P.IsMaximal], Module.IsTorsionFree (Rₚ P) (Mₚ P)
Tag 0AUU, a lemma

Tag 0AUU in the Stacks Project.

isTorsionFree_iff_exists_injective_to_finite_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/TorsionFree.lean, line 210.

A finite module over a domain is torsion-free if and only if it embeds into a finite free module.

theorem isTorsionFree_iff_exists_injective_to_finite_free
    {R : Type u} [CommRing R] [IsDomain R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] :
    Module.IsTorsionFree R M ↔
      ∃ N : ModuleCat.{max u v} R,
        Module.Finite R N ∧ Module.Free R N ∧
          ∃ f : M →ₗ[R] N, Function.Injective f
Tag 0AUV, a lemma

Tag 0AUV in the Stacks Project.

isTorsionFree_iff_finiteFreeEmbedding_iff_associatedPrimes_iff_propertyS1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/TorsionFree.lean, line 293.

For a nonzero finite module over a Noetherian domain, the following are equivalent: it is torsion-free; it embeds into a finite free module; its only associated prime is zero; zero lies in its support and it satisfies (S₁); and zero lies in its support and it has no embedded associated prime.

theorem isTorsionFree_iff_finiteFreeEmbedding_iff_associatedPrimes_iff_propertyS1
    {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] :
    (Module.IsTorsionFree R M ↔
      ∃ N : ModuleCat.{max u v} R,
        Module.Finite R N ∧ Module.Free R N ∧
          ∃ f : M →ₗ[R] N, Function.Injective f) ∧
    ((∃ N : ModuleCat.{max u v} R,
        Module.Finite R N ∧ Module.Free R N ∧
          ∃ f : M →ₗ[R] N, Function.Injective f) ↔
      associatedPrimes R M = {⊥}) ∧
    (associatedPrimes R M = {⊥} ↔
      (⊥ : PrimeSpectrum R) ∈ Module.support R M ∧
        ∀ p : PrimeSpectrum R,
          min 1 (Module.supportDim (Localization.AtPrime p.asIdeal)
              (LocalizedModule p.asIdeal.primeCompl M)) ≤
            (Module.depth (Localization.AtPrime p.asIdeal)
              (IsLocalRing.maximalIdeal (Localization.AtPrime p.asIdeal))
              (LocalizedModule p.asIdeal.primeCompl M) : WithBot ℕ∞)) ∧
    (((⊥ : PrimeSpectrum R) ∈ Module.support R M ∧
        ∀ p : PrimeSpectrum R,
          min 1 (Module.supportDim (Localization.AtPrime p.asIdeal)
              (LocalizedModule p.asIdeal.primeCompl M)) ≤
            (Module.depth (Localization.AtPrime p.asIdeal)
              (IsLocalRing.maximalIdeal (Localization.AtPrime p.asIdeal))
              (LocalizedModule p.asIdeal.primeCompl M) : WithBot ℕ∞)) ↔
      (⊥ : PrimeSpectrum R) ∈ Module.support R M ∧
        ∀ p ∈ associatedPrimes R M, Minimal (· ∈ associatedPrimes R M) p)
Tag 0538, a lemma

Tag 0538 in the Stacks Project.

Declarations registered for the tag:

Tag 0539, a lemma

Tag 0539 in the Stacks Project.

Declarations registered for the tag:

Tag 0AUW, a lemma

Tag 0AUW in the Stacks Project.

projective_of_finite_isTorsionFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/TorsionFree.lean, line 344. The attribute's comment: “(2)”. References: EGA 0 (6.3.4), “finite, Dedekind domain”.

A finite torsion-free module over a Dedekind domain is projective, hence finite locally free.

theorem projective_of_finite_isTorsionFree
    (R : Type u) [CommRing R] [IsDedekindDomain R]
    (M : Type v) [AddCommGroup M] [Module R M]
    [Module.Finite R M] [Module.IsTorsionFree R M] :
    Module.Projective R M

Declarations registered for the tag:

Tag 0AUX, a lemma

Tag 0AUX in the Stacks Project.

Declarations registered for the tag:

Sources
LeanSubmodule.torsion · Module.IsTorsionFree · Module.IsTorsion · Submodule.mem_torsion_iff · Submodule.QuotientTorsion.instIsTorsionFree · IsLocalizedModule.isTorsionFree · isTorsionFree_baseChange_of_flat · isTorsionFree_of_injective_of_exact

Section15.24 Reflexive modules#

Section 15.24 of the Stacks Project, Tag 0AUY. 20 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 0AUZ, a definition

Tag 0AUZ in the Stacks Project.

Declarations registered for the tag:

Tag 0AV0, a lemma

Tag 0AV0 in the Stacks Project.

isTorsionFree_of_isReflexive_and_dualEval_isTorsion_and_injective_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 425.

Stacks Tag 0AV0. A reflexive module over a domain is torsion-free. For a finite module, the kernel and cokernel of the canonical evaluation map into the double dual are torsion, and that map is injective if and only if the module is torsion-free.

theorem isTorsionFree_of_isReflexive_and_dualEval_isTorsion_and_injective_iff
    {R : Type u} [CommRing R] [IsDomain R]
    {M : Type v} [AddCommGroup M] [Module R M] :
    (Module.IsReflexive R M → Module.IsTorsionFree R M) ∧
      (Module.Finite R M →
        Module.IsTorsion R (LinearMap.ker (Module.Dual.eval R M)) ∧
          Module.IsTorsion R
            (Module.Dual R (Module.Dual R M) ⧸ LinearMap.range (Module.Dual.eval R M))) ∧
      (Module.Finite R M →
        (Function.Injective (Module.Dual.eval R M) ↔ Module.IsTorsionFree R M))
Tag 0B36, a lemma

Tag 0B36 in the Stacks Project.

surjective_dualEval_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 679.

Stacks Tag 0B36. The canonical evaluation map from a finite module over a Dedekind domain to its double dual is surjective.

theorem surjective_dualEval_of_finite
    (R : Type u) [CommRing R] [IsDedekindDomain R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    Function.Surjective (Module.Dual.eval R M)
Tag 0AV1, a lemma

Tag 0AV1 in the Stacks Project.

reflexive_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive/Localization.lean, line 186.

Stacks 0AV1. Let R be a Noetherian ring and M a finite R-module. The following are equivalent: M is reflexive; M_p is a reflexive R_p-module for every prime p; M_m is a reflexive R_m-module for every maximal ideal m.

theorem reflexive_tfae
    (R : Type*) [CommRing R] [IsNoetherianRing R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    [ Module.IsReflexive R M,
      ∀ (p : Ideal R) [p.IsPrime],
        Module.IsReflexive (Localization.AtPrime p) (LocalizedModule p.primeCompl M),
      ∀ (m : Ideal R) [m.IsMaximal],
        Module.IsReflexive (Localization.AtPrime m) (LocalizedModule m.primeCompl M)
    ].TFAE
Tag 0EB8, a lemma

Tag 0EB8 in the Stacks Project.

isReflexive_of_exact_of_isReflexive_of_isTorsionFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 446.

Stacks Tag 0EB8. Let R be a Noetherian domain and let 0 → M → M' → M'' be an exact sequence of finite R-modules. If M' is reflexive and M'' is torsion-free, then M is reflexive.

theorem isReflexive_of_exact_of_isReflexive_of_isTorsionFree
    {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R]
    {M : Type v} {M' : Type w} {M'' : Type x}
    [AddCommGroup M] [Module R M] [Module.Finite R M]
    [AddCommGroup M'] [Module R M'] [Module.Finite R M']
    [AddCommGroup M''] [Module R M''] [Module.Finite R M'']
    (f : M →ₗ[R] M') (g : M' →ₗ[R] M'')
    (hf : Function.Injective f) (hfg : Function.Exact f g)
    (hM' : Module.IsReflexive R M') (hM'' : Module.IsTorsionFree R M'') :
    Module.IsReflexive R M
Tag 0AV2, a lemma

Tag 0AV2 in the Stacks Project.

isReflexive_iff_exists_finFree_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 526.

Stacks Tag 0AV2. A finite module over a Noetherian domain is reflexive if and only if it fits into a short exact sequence 0 → M → F → N → 0 with F finite free and N torsion-free.

theorem isReflexive_iff_exists_finFree_shortExact
    {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] :
    Module.IsReflexive R M ↔
      ∃ (n : ℕ) (N : Type u) (_ : AddCommGroup N) (_ : Module R N),
        Module.IsTorsionFree R N ∧
          ∃ (f : M →ₗ[R] (Fin n → R)) (g : (Fin n → R) →ₗ[R] N),
            Function.Injective f ∧ Function.Exact f g ∧ Function.Surjective g
Tag 0EB9, a lemma

Tag 0EB9 in the Stacks Project.

isReflexive_baseChange_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 636.

Stacks Tag 0EB9. A finite reflexive module over a Noetherian domain remains reflexive after flat base change to a Noetherian domain. The base-changed module is automatically finite.

theorem isReflexive_baseChange_of_flat
    {R : Type u} {R' : Type v} [CommRing R] [CommRing R'] [Algebra R R']
    [IsDomain R] [IsDomain R'] [IsNoetherianRing R] [IsNoetherianRing R']
    [Module.Flat R R'] {M : Type w} [AddCommGroup M] [Module R M]
    [Module.Finite R M] [Module.IsReflexive R M] :
    Module.IsReflexive R' (TensorProduct R R' M)
Tag 0AV3, a lemma

Tag 0AV3 in the Stacks Project.

isReflexive_linearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 612.

Stacks Tag 0AV3. Over a Noetherian domain, the module of linear maps from a finite module into a finite reflexive module is reflexive.

theorem isReflexive_linearMap
    {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M]
    {N : Type w} [AddCommGroup N] [Module R N] [Module.Finite R N]
    (hN : Module.IsReflexive R N) :
    Module.IsReflexive R (M →ₗ[R] N)
Tag 0AV4, a definition

Tag 0AV4 in the Stacks Project.

Module.reflexiveHull, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 116.

Stacks Tag 0AV4. The reflexive hull of an R-module M is its double dual Hom_R(Hom_R(M, R), R).

abbrev Module.reflexiveHull (R : Type u) [CommSemiring R]
    (M : Type v) [AddCommMonoid M] [Module R M]
Tag 0AV5, a lemma

Tag 0AV5 in the Stacks Project.

one_le_depth_and_two_le_depth_linearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 730.

Stacks Tag 0AV5. If M and N are finite modules over a Noetherian local ring, then Hom(M, N) has depth at least one (respectively, at least two) whenever N does.

theorem one_le_depth_and_two_le_depth_linearMap
    {R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M]
    {N : Type w} [AddCommGroup N] [Module R N] [Module.Finite R N] :
    ((1 : ℕ∞) ≤ Module.depth R (IsLocalRing.maximalIdeal R) N →
      (1 : ℕ∞) ≤ Module.depth R (IsLocalRing.maximalIdeal R) (M →ₗ[R] N)) ∧
    ((2 : ℕ∞) ≤ Module.depth R (IsLocalRing.maximalIdeal R) N →
      (2 : ℕ∞) ≤ Module.depth R (IsLocalRing.maximalIdeal R) (M →ₗ[R] N))
Tag 0AV6, a lemma

Tag 0AV6 in the Stacks Project.

propertySk_linearMap_one_two_and_isTorsionFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 843.

Stacks Tag 0AV6. For finite modules M and N over a Noetherian ring, the module Hom_R(M, N) inherits (S₁) and (S₂) from N; if the ring is a domain, it also inherits the conjunction of torsion-freeness and (S₂).

theorem propertySk_linearMap_one_two_and_isTorsionFree
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M]
    {N : Type w} [AddCommGroup N] [Module R N] [Module.Finite R N] :
    (PropertySkModule R N 1 → PropertySkModule R (M →ₗ[R] N) 1) ∧
      (PropertySkModule R N 2 → PropertySkModule R (M →ₗ[R] N) 2) ∧
      (IsDomain R → Module.IsTorsionFree R N → PropertySkModule R N 2 →
        Module.IsTorsionFree R (M →ₗ[R] N) ∧ PropertySkModule R (M →ₗ[R] N) 2)
Tag 0AV7, a lemma

Tag 0AV7 in the Stacks Project.

injective_of_injective_localized_at_associatedPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AssociatedPrime/Injective.lean, line 42.

Stacks Tag 0AV7. If for every prime ideal p of the Noetherian ring R either the localized map φ_p : M_p → N_p is injective or p is not an associated prime of M, then φ : M → N is injective.

theorem injective_of_injective_localized_at_associatedPrimes (φ : M →ₗ[R] N)
    (h : ∀ p : Ideal R, [p.IsPrime] →
      Function.Injective (LocalizedModule.map p.primeCompl φ) ∨ p ∉ associatedPrimes R M) :
    Function.Injective φ
Tag 0AV8, a lemma

Tag 0AV8 in the Stacks Project.

bijective_of_bijective_localized_or_depth_two_and_notMem_associatedPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 1009.

Stacks Tag 0AV8. A map from a finite module over a Noetherian ring is bijective if, at every prime, it is bijective after localization or the localized source has depth at least two and the prime is not associated to the target.

theorem bijective_of_bijective_localized_or_depth_two_and_notMem_associatedPrimes
    {R M N : Type*} [CommRing R] [IsNoetherianRing R]
    [AddCommGroup M] [Module R M] [Module.Finite R M]
    [AddCommGroup N] [Module R N] (φ : M →ₗ[R] N)
    (h : ∀ (p : Ideal R) (_ : p.IsPrime),
      Function.Bijective (LocalizedModule.map p.primeCompl φ) ∨
        2 ≤ Module.depth (Localization.AtPrime p)
          (IsLocalRing.maximalIdeal (Localization.AtPrime p))
          (LocalizedModule p.primeCompl M) ∧ p ∉ associatedPrimes R N) :
    Function.Bijective φ
Tag 0AV9, a lemma

Tag 0AV9 in the Stacks Project.

bijective_of_bijective_localized_or_depth_two_of_isTorsionFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 1120.

Stacks Tag 0AV9. A map from a finite nonzero module to a torsion-free module over a Noetherian domain is bijective if, at every prime, either its localization is bijective or the localized source has depth at least two.

theorem bijective_of_bijective_localized_or_depth_two_of_isTorsionFree
    {R M N : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R]
    [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M]
    [AddCommGroup N] [Module R N] [Module.IsTorsionFree R N]
    (φ : M →ₗ[R] N)
    (h : ∀ (p : Ideal R) (_ : p.IsPrime),
      Function.Bijective (LocalizedModule.map p.primeCompl φ) ∨
        2 ≤ Module.depth (Localization.AtPrime p)
          (IsLocalRing.maximalIdeal (Localization.AtPrime p))
          (LocalizedModule p.primeCompl M)) :
    Function.Bijective φ
Tag 0AVA, a lemma

Tag 0AVA in the Stacks Project.

isReflexive_iff_localized_isReflexive_or_depth_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 1177.

Stacks Tag 0AVA. A finite module over a Noetherian domain is reflexive if and only if, at every prime, its localization is reflexive or has depth at least two.

theorem isReflexive_iff_localized_isReflexive_or_depth_two
    {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] :
    Module.IsReflexive R M ↔
      ∀ (p : Ideal R) [p.IsPrime],
        Module.IsReflexive (Localization.AtPrime p) (LocalizedModule p.primeCompl M) ∨
          2 ≤ Module.depth (Localization.AtPrime p)
            (IsLocalRing.maximalIdeal (Localization.AtPrime p))
            (LocalizedModule p.primeCompl M)
Tag 0EBA, a lemma

Tag 0EBA in the Stacks Project.

depth_localized_ge_two_and_propertyS2_of_isReflexive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 868.

Stacks Tag 0EBA. A finite reflexive module over a Noetherian commutative ring has depth at least two at a prime whenever the localized ring does, and inherits Serre's condition (S₂) from the ring.

theorem depth_localized_ge_two_and_propertyS2_of_isReflexive
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M]
    [Module.IsReflexive R M] (p : Ideal R) [p.IsPrime] :
    ((2 : ℕ∞) ≤
        Module.depth (Localization.AtPrime p)
          (IsLocalRing.maximalIdeal (Localization.AtPrime p)) (Localization.AtPrime p) →
      (2 : ℕ∞) ≤
        Module.depth (Localization.AtPrime p)
          (IsLocalRing.maximalIdeal (Localization.AtPrime p)) (LocalizedModule.AtPrime p M)) ∧
      (PropertySkRing R 2 → PropertySkModule R M 2)
Tag 0EBB, an example

Tag 0EBB in the Stacks Project.

mvPolynomial_adjoin_reflexive_propertyS2_module_not_propertyS2, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 2811.

Stacks Tag 0EBB. The subalgebra R = k[1, y, x², xy, x³] of k[x, y] is a Noetherian domain which is not (S₂). Both R and k[x, y] are reflexive as R-modules, while k[x, y] is (S₂). Moreover, if m = (y, x², xy, x³), then the two successive R-duals of k[x, y] are m and k[x, y], respectively.

theorem mvPolynomial_adjoin_reflexive_propertyS2_module_not_propertyS2
    (k : Type u) [Field k] :
    let P := MvPolynomial (Fin 2) k
    let x : P := MvPolynomial.X 0
    let y : P := MvPolynomial.X 1
    let R : Subalgebra k P := Algebra.adjoin k {1, y, x ^ 2, x * y, x ^ 3}
    let m : Ideal R := Ideal.span {r | (r : P) ∈ ({y, x ^ 2, x * y, x ^ 3} : Set P)}
    ∃ (_ : IsNoetherianRing R) (_ : IsDomain R) (_ : Module.Finite R P),
      ∃ (dualPToM : Module.Dual R P ≃ₗ[R] m) (dualMToP : Module.Dual R m ≃ₗ[R] P),
        ¬ PropertySkRing R 2 ∧
          Module.IsReflexive R R ∧
          ¬ PropertySkModule R R 2 ∧
          (∀ (f : Module.Dual R P) (q : P),
            (↑(↑(dualPToM f) : R) : P) * q = (↑(f q) : P)) ∧
          (∀ (g : Module.Dual R m) (a : m),
            (↑(g a) : P) = dualMToP g * (↑(↑a : R) : P)) ∧
          Module.IsReflexive R P ∧
          PropertySkModule R P 2
Tag 0AVB, a lemma

Tag 0AVB in the Stacks Project.

isReflexive_isTorsionFree_propertyS2_intersection_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 1418. References: EGA 0 (23.2.9), “special case”; EGA IV (7.8.3), “(viii), special case”.

Stacks Tag 0AVB. Let R be a Noetherian normal domain and M a finite R-module. The following are equivalent: M is reflexive; M is torsion-free and satisfies (S₂); and M is torsion-free and equals the intersection of its localizations at the height-one primes inside its generic fibre.

theorem isReflexive_isTorsionFree_propertyS2_intersection_tfae
    {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] :
    List.TFAE [
      Module.IsReflexive R M,
      Module.IsTorsionFree R M ∧ PropertySkModule R M 2,
      Module.IsTorsionFree R M ∧
        ∀ x : LocalizedModule (nonZeroDivisors R) M,
          x ∈ LinearMap.range (LocalizedModule.mkLinearMap (nonZeroDivisors R) M) ↔
            ∀ (p : Ideal R) (_ : p.IsPrime), p.height = 1 →
              ∃ (m : M) (s : R), s ∉ p ∧
                s • x = LocalizedModule.mkLinearMap (nonZeroDivisors R) M m]
Tag 0AVC, a lemma

Tag 0AVC in the Stacks Project.

reflexiveHull_eq_iInf_localization_mod_torsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 1597. References: EGA 0 (23.2.9), “special case”.

Stacks Tag 0AVC. Let R be a Noetherian normal domain and M a finite R-module. Inside the generic fibre, the reflexive hull M⁎⁎ is the intersection over height-one primes p of M_p / (M_p)_tors, and this is also the intersection of (M / M_tors)_p.

Membership in the three submodules is written elementwise, with the first condition using the canonical localization of the evaluation map M → M⁎⁎.

theorem reflexiveHull_eq_iInf_localization_mod_torsion
    {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] :
    ∀ x : LocalizedModule (nonZeroDivisors R) M,
      (((IsLocalizedModule.map (nonZeroDivisors R)
          (LocalizedModule.mkLinearMap (nonZeroDivisors R) M)
          (LocalizedModule.mkLinearMap (nonZeroDivisors R)
            (Module.Dual R (Module.Dual R M)))
          (Module.Dual.eval R M)) x ∈
            LinearMap.range (LocalizedModule.mkLinearMap (nonZeroDivisors R)
              (Module.Dual R (Module.Dual R M)))) ↔
        ∀ (p : Ideal R) (_ : p.IsPrime), p.height = 1 →
          ∃ (m : M) (s : R), s ∉ p ∧
            s • x = LocalizedModule.mkLinearMap (nonZeroDivisors R) M m) ∧
      ((∀ (p : Ideal R) (_ : p.IsPrime), p.height = 1 →
          ∃ (m : M) (s : R), s ∉ p ∧
            s • x = LocalizedModule.mkLinearMap (nonZeroDivisors R) M m) ↔
        ∀ (p : Ideal R) (_ : p.IsPrime), p.height = 1 →
          ∃ (q : M ⧸ Submodule.torsion R M) (s : R), s ∉ p ∧
            s • x = Module.torsionQuotientToGenericFiber R M q)
Tag 0BM4, a lemma

Tag 0BM4 in the Stacks Project.

integralClosure_isReflexive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Reflexive.lean, line 1657.

Stacks Tag 0BM4. If A is a Noetherian normal domain, K is its fraction field, and L is a finite extension of K, then a module-finite integral closure of A in L is reflexive as an A-module.

theorem integralClosure_isReflexive
    (A : Type u) [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsIntegrallyClosed A]
    (K : Type v) [Field K] [Algebra A K] [IsFractionRing A K]
    (L : Type w) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
    [FiniteDimensional K L] (hB : Module.Finite A (integralClosure A L)) :
    Module.IsReflexive A (integralClosure A L)
Sources
LeanModule.IsReflexive · isTorsionFree_of_isReflexive_and_dualEval_isTorsion_and_injective_iff · surjective_dualEval_of_finite · reflexive_tfae · isReflexive_of_exact_of_isReflexive_of_isTorsionFree · isReflexive_iff_exists_finFree_shortExact · isReflexive_baseChange_of_flat · isReflexive_linearMap

Section15.25 Content ideals#

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

Tag 0ASA, a definition

Tag 0ASA in the Stacks Project.

IsContentIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/ContentIdeal.lean, line 58. References: SGA 3 XXII (5.1.1), “more general”.

I₀ is a content ideal of x: it is the least element of S_x under inclusion, i.e. x ∈ I₀ M and any ideal I with x ∈ I M contains I₀. Here the submodule I M of M is spelled I • (⊤ : Submodule A M).

Flatness of M is not needed to state this, so the predicate is given for an arbitrary module; for a flat module it is exactly the source's definition.

def IsContentIdeal (x : M) (I₀ : Ideal A) : Prop
Tag 0ASB, a lemma

Tag 0ASB in the Stacks Project.

contentIdeal_fg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/ContentIdeal.lean, line 95.

Stacks Tag 0ASB. If a content ideal I₀ of x exists, then I₀ is finitely generated.

The source states this for a flat module M, but flatness is never used: the content ideal is by definition the least ideal I with x ∈ I M, and x ∈ I₀ M already exhibits x inside J M for some finitely generated J ≤ I₀, whence J = I₀ by minimality. The hypothesis is therefore dropped, which only strengthens the statement.

theorem contentIdeal_fg {A : Type*} [CommRing A] {M : Type*} [AddCommGroup M] [Module A M]
    (x : M) (I₀ : Ideal A) (h : IsContentIdeal x I₀) :
    I₀.FG
Tag 0ASC, a lemma

Tag 0ASC in the Stacks Project.

isContentIdeal_map_of_injective_mapQ_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/ContentIdeal.lean, line 279.

Stacks Tag 0ASC. A map between flat modules over a local ring which is injective modulo the maximal ideal preserves content ideals of elements.

theorem isContentIdeal_map_of_injective_mapQ_maximalIdeal
    {A : Type*} [CommRing A] [IsLocalRing A]
    {M N : Type*} [AddCommGroup M] [Module A M] [Module.Flat A M]
    [AddCommGroup N] [Module A N] [Module.Flat A N]
    (u : M →ₗ[A] N)
    (hu : Function.Injective
      (Submodule.mapQ (maximalIdeal A • (⊤ : Submodule A M))
        (maximalIdeal A • (⊤ : Submodule A N)) u
        (Submodule.smul_top_le_comap_smul_top (maximalIdeal A) u)))
    {x : M} {I : Ideal A} (hx : IsContentIdeal x I) :
    IsContentIdeal (u x) I
Tag 0ASD, a lemma

Tag 0ASD in the Stacks Project.

exists_isContentIdeal_of_flat_isMittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/ContentIdeal.lean, line 445.

Stacks Tag 0ASD. Every element of a flat Mittag-Leffler module has a content ideal.

theorem exists_isContentIdeal_of_flat_isMittagLeffler
    {A : Type u} [CommRing A]
    {M : Type v} [AddCommGroup M] [Module A M]
    [Module.Flat A M]
    (hM : IsMittagLeffler.{u, max u v, v, max u v, max u v} A M) (x : M) :
    ∃ I : Ideal A, IsContentIdeal x I
Sources
LeanIsContentIdeal · contentIdeal_fg · isContentIdeal_map_of_injective_mapQ_maximalIdeal · exists_isContentIdeal_of_flat_isMittagLeffler

Section15.26 Flatness and finiteness conditions#

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

Tag 053A, a lemma

Tag 053A in the Stacks Project.

Module.finitePresentation_of_flat_of_localized, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Finiteness.lean, line 299.

Stacks Tag 053A. Let S = R[x₁, …, x_n] and let M be a finite S-module which is flat over R. If finitely many prime localizations jointly detect elements of R and M is finitely presented over S after localizing at every prime of R, then M is finitely presented over S.

theorem Module.finitePresentation_of_flat_of_localized
    {R : Type u} [CommRing R] {n : ℕ} {M : Type v} [AddCommGroup M]
    [Module (MvPolynomial (Fin n) R) M] [Module R M]
    [IsScalarTower R (MvPolynomial (Fin n) R) M]
    (hprimes : HasFiniteDetectingPrimes R)
    [Module.Finite (MvPolynomial (Fin n) R) M] [Module.Flat R M]
    (hlocal : ∀ p : PrimeSpectrum R,
      Module.FinitePresentation
        (Localization (Algebra.algebraMapSubmonoid (MvPolynomial (Fin n) R)
          p.asIdeal.primeCompl))
        (LocalizedModule (Algebra.algebraMapSubmonoid (MvPolynomial (Fin n) R)
          p.asIdeal.primeCompl) M)) :
    Module.FinitePresentation (MvPolynomial (Fin n) R) M
Tag 053B, a lemma

Tag 053B in the Stacks Project.

Algebra.FinitePresentation.of_flat_of_localized, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Finiteness.lean, line 358.

Stacks Tag 053B. Let R → S be a flat ring map of finite type. Suppose finitely many prime localizations jointly detect elements of R, and that for every prime p of R the localization of S at p is finitely presented over R localized at p. Then S is finitely presented over R.

theorem Algebra.FinitePresentation.of_flat_of_localized
    {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]
    (hprimes : HasFiniteDetectingPrimes R)
    [Algebra.FiniteType R S] [Module.Flat R S]
    (hlocal : ∀ p : PrimeSpectrum R,
      Algebra.FinitePresentation (Localization.AtPrime p.asIdeal)
        (Localization (Algebra.algebraMapSubmonoid S p.asIdeal.primeCompl))) :
    Algebra.FinitePresentation R S
Tag 053C, a lemma

Tag 053C in the Stacks Project.

finitePresentation_of_finite_flat_of_isLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/GradedFinitePresentation.lean, line 1056. References: EGA IV (11.2.9.4), “special case”; SGA 6 VI (1.6), “partial”.

Stacks Tag 053C. Let R be a local ring and let S = MvPolynomial (Fin n) R = R[x_1, ..., x_n] be the graded polynomial algebra with positive weights w_i = deg(x_i) > 0, graded by weightedHomogeneousSubmodule R w. Let M be a graded S-module, encoded by a family of R-submodules 𝓜 : ℤ → Submodule R M together with a compatible graded scalar multiplication and a direct-sum decomposition. If M is finite as an S-module and flat as an R-module, then M is finitely presented as an S-module.

theorem finitePresentation_of_finite_flat_of_isLocalRing
    (R : Type*) [CommRing R] [IsLocalRing R]
    (n : ℕ) (w : Fin n → ℤ) (hw : ∀ i, 0 < w i)
    (M : Type*) [AddCommGroup M] [Module (MvPolynomial (Fin n) R) M]
    -- `R` acts on `M` through the structure map `R → S` compatibly
    [Module R M] [IsScalarTower R (MvPolynomial (Fin n) R) M]
    -- the grading on `M` over `ℤ`, as a family of `R`-submodules
    (𝓜 : ℤ → Submodule R M)
    [SetLike.GradedSMul (weightedHomogeneousSubmodule R w) 𝓜]
    [DirectSum.Decomposition 𝓜]
    -- `M` is finite as an `S`-module
    [Module.Finite (MvPolynomial (Fin n) R) M]
    -- `M` is flat as an `R`-module
    [Module.Flat R M] :
    Module.FinitePresentation (MvPolynomial (Fin n) R) M
Tag 053D, a lemma

Tag 053D in the Stacks Project.

finitePresentation_of_flat_of_finiteType_of_finite_degreeZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Finiteness.lean, line 797. References: EGA IV (11.2.9.4), “Module clause”.

Stacks Tag 053D. Let S = ⨁_d 𝒜 d be a nonnegatively graded R-algebra of finite type whose degree-zero part is finite over R, and suppose a finite family of prime localizations jointly detects elements of R. Then an R-flat S is finitely presented as an R-algebra, and every finite graded S-module which is flat over R is finitely presented as an S-module.

theorem finitePresentation_of_flat_of_finiteType_of_finite_degreeZero
    {R : Type u} {S : Type v} {M : Type w} [CommRing R] [CommRing S]
    [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M]
    (𝒜 : ℕ → Submodule R S) [GradedAlgebra 𝒜]
    (ℳ : ℤ → Submodule R M) [SetLike.GradedSMul 𝒜 ℳ] [DirectSum.Decomposition ℳ]
    [Algebra.FiniteType R S] [Module.Finite R (𝒜 0)]
    (hprimes : HasFiniteDetectingPrimes R) :
    (Module.Flat R S → Algebra.FinitePresentation R S) ∧
      (Module.Flat R M → Module.Finite S M → Module.FinitePresentation S M)
Tag 05GS, a remark

Tag 05GS in the Stacks Project.

hasFiniteDetectingPrimes_of_standard_conditions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Finiteness.lean, line 1297.

Stacks Tag 05GS. Let R be a commutative ring. If R is local, Noetherian, a domain, reduced with finitely many minimal primes, or has finitely many weakly associated primes, then finitely many prime localizations jointly detect elements of R, so that Tags 053A, 053B and 053D apply to R.

theorem hasFiniteDetectingPrimes_of_standard_conditions
    {R : Type u} [CommRing R]
    (h : IsLocalRing R ∨ IsNoetherianRing R ∨ IsDomain R ∨
      (IsReduced R ∧ (minimalPrimes R).Finite) ∨
      {p : Ideal R | ∃ x : R, p ∈ (R ∙ x).annihilator.minimalPrimes}.Finite) :
    HasFiniteDetectingPrimes R
Tag 053E, a lemma

Tag 053E in the Stacks Project.

finitePresentation_of_flat_of_finiteType_of_valuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Finiteness.lean, line 1174.

Stacks Tag 053E (Nagata). Let A be a valuation ring, B an A-algebra of finite type, and M a B-module. If B is flat over A, then B is finitely presented as an A-algebra. If M is finite over B and flat over A, then M is finitely presented as a B-module.

theorem finitePresentation_of_flat_of_finiteType_of_valuationRing
    {A : Type u} {B : Type v} {M : Type w} [CommRing A] [IsDomain A] [ValuationRing A]
    [CommRing B] [Algebra A B] [Algebra.FiniteType A B] [AddCommGroup M] [Module B M]
    [Module A M] [IsScalarTower A B M] :
    (Module.Flat A B → Algebra.FinitePresentation A B) ∧
      (Module.Flat A M → Module.Finite B M → Module.FinitePresentation B M)
Tag 0GSE, a lemma

Tag 0GSE in the Stacks Project.

essentiallyOfFinitePresentation_and_finitePresentation_of_flat_of_valuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Finiteness.lean, line 1229.

Stacks Tag 0GSE. Let A be a valuation ring, B an essentially-of-finite-type A-algebra, and M a B-module. If B is flat over A, then A → B is essentially of finite presentation. If M is finite over B and flat over A, then M is finitely presented over B.

theorem essentiallyOfFinitePresentation_and_finitePresentation_of_flat_of_valuationRing
    {A : Type u} {B : Type v} {M : Type w} [CommRing A] [IsDomain A] [ValuationRing A]
    [CommRing B] [Algebra A B] [Algebra.EssFiniteType A B] [AddCommGroup M] [Module B M]
    [Module A M] [IsScalarTower A B M] :
    (Module.Flat A B → (algebraMap A B).EssentiallyOfFinitePresentation) ∧
      (Module.Flat A M → Module.Finite B M → Module.FinitePresentation B M)
Sources
LeanModule.finitePresentation_of_flat_of_localized · Algebra.FinitePresentation.of_flat_of_localized · finitePresentation_of_finite_flat_of_isLocalRing · finitePresentation_of_flat_of_finiteType_of_finite_degreeZero · hasFiniteDetectingPrimes_of_standard_conditions · finitePresentation_of_flat_of_finiteType_of_valuationRing · essentiallyOfFinitePresentation_and_finitePresentation_of_flat_of_valuationRing

Section15.27 Blowing up and flatness#

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

Tag 053H, a definition

Tag 053H in the Stacks Project.

strictTransform, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/StrictTransform.lean, line 45.

The strict transform of an R-module M along the affine blowup algebra R → R[I/a]: the scalar extension R[I/a] ⊗[R] M, modulo the elements annihilated by some power of the image of a.

noncomputable def strictTransform (I : Ideal R) (a : R) [Fact (a ∈ I)]
    (M : Type v) [AddCommGroup M] [Module R M]
Tag 053I, a lemma

Tag 053I in the Stacks Project.

Stacks.Flatness.BlowupFlattening.stacks053I, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/BlowupFlattenAssembly.lean, line 1046.

Stacks Tag 053I: flattening by blowing up. Let (R, 𝔪) be a local domain with fraction field K and 𝔪 ≠ 0, let S be a finite type R-algebra, let M be a finite S-module and let A ⊆ K be a valuation ring dominating R. Then there is an admissible affine blowup chart R[I/a] — so I ⊆ 𝔪 is finitely generated, the fibre ring of R → R[I/a] at 𝔪 is nonzero and A has center on R[I/a] — on which the strict transform of S is flat and of finite presentation over R[I/a] and the strict transform of M is flat over R[I/a] and finitely presented over the strict transform of S.

The polynomial case is Stacks.Flatness.BlowupFlattening.exists_admissiblePair_mvPolynomial. The reduction to it is the source's first step: write S as a quotient of P = R[x_1, …, x_n] and apply the polynomial case to the P-module N = S ⊕ M. The strict transform of N is the product of the strict transforms of S and of M (Stacks.Flatness.BlowupFlattening.prodLinearEquiv, the version of strictTransform.prodEquiv that is linear over the strict transform of P), so flatness and finite presentation of each summand follow from Module.Flat.prod_iff and Module.FinitePresentation.prod_iff. Finite presentation of the strict transform of S as an R[I/a]-algebra is then Algebra.FinitePresentation.of_surjective_of_module_finitePresentation, and finite presentation of the strict transform of M over the strict transform of S is Stacks Tag 0561, Module.FinitePresentation.of_restrictScalars_of_finiteType.

The statement deviates from the source in two ways: the hypothesis 𝔪 ≠ 0, without which the conclusion is unsatisfiable, and clause (4) being read over R[I/a] rather than over R.

theorem stacks053I (hdom : Dominates R A) (hm : IsLocalRing.maximalIdeal R ≠ ⊥) (S : Type w)
    [CommRing S] [Algebra R S] [Algebra.FiniteType R S] (M : Type uM) [AddCommGroup M]
    [Module S M] [Module R M] [IsScalarTower R S M] [Module.Finite S M] :
    Stacks053IConclusion R A S M
Tag 0CZM, a lemma

Tag 0CZM in the Stacks Project.

fittingIdeal_strictTransform_affineBlowup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Blowup.lean, line 182.

Stacks Tag 0CZM. Let M be a finite module over a commutative ring R, and let I be its kth Fitting ideal. On the affine blowup chart R[I/a] associated to any a ∈ I, the kth Fitting ideal of the strict transform of M — the quotient of R[I/a] ⊗[R] M by its a-power torsion — is the unit ideal.

theorem fittingIdeal_strictTransform_affineBlowup_eq_top
    {R : Type u} [CommRing R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M]
    (k : ℕ) (a : R) (ha : a ∈ fittingIdeal (R := R) (M := M) (k : ℤ))
    (S : Type w) [CommRing S] [Algebra R S] [IsLocalization.Away a S] :
    let I := fittingIdeal (R := R) (M := M) (k : ℤ)
    let R' := affineBlowupAlgebra I a S
    let M' := (R' ⊗[R] M) ⧸
      Ideal.primaryComponent (R' ⊗[R] M)
        (Ideal.span {algebraMap R R' a})
    fittingIdeal (R := R') (M := M') (k : ℤ) = ⊤
Tag 0CZN, a lemma

Tag 0CZN in the Stacks Project.

isFiniteLocallyFreeOfRank_strictTransform_affineBlowup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Blowup.lean, line 306.

Stacks Tag 0CZN. Let M be a finite module over a commutative ring R, and let I be its kth Fitting ideal. Suppose that the localization of M at every prime outside V(I) is free of rank k. Then the strict transform of M on the affine blowup chart R[I/a], for any a ∈ I, is finite locally free of rank k.

theorem isFiniteLocallyFreeOfRank_strictTransform_affineBlowup
    {R : Type u} [CommRing R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M]
    (k : ℕ)
    (hfree : ∀ (p : Ideal R) [p.IsPrime],
      ¬ fittingIdeal (R := R) (M := M) (k : ℤ) ≤ p →
        Nonempty ((Fin k → Localization.AtPrime p) ≃ₗ[Localization.AtPrime p]
          LocalizedModule.AtPrime p M))
    (a : R) (ha : a ∈ fittingIdeal (R := R) (M := M) (k : ℤ))
    (S : Type w) [CommRing S] [Algebra R S] [IsLocalization.Away a S] :
    let I := fittingIdeal (R := R) (M := M) (k : ℤ)
    let R' := affineBlowupAlgebra I a S
    let M' := (R' ⊗[R] M) ⧸
      Ideal.primaryComponent (R' ⊗[R] M)
        (Ideal.span {algebraMap R R' a})
    Module.IsFiniteLocallyFreeOfRank R' M' k
Tag 0BBJ, a lemma

Tag 0BBJ in the Stacks Project.

exists_fg_ideal_strictTransform_isFiniteLocallyFreeOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Blowup.lean, line 616.

Stacks Tag 0BBJ. Let M be a finite module over a commutative ring R. If the localization of M away from f is finite locally free of rank r, then there is a finitely generated ideal I with the same vanishing locus as f such that, on every affine blowup chart R[I/a] with a ∈ I, the strict transform of M is finite locally free of rank r.

theorem exists_fg_ideal_strictTransform_isFiniteLocallyFreeOfRank
    {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M]
    (f : R) (r : ℕ)
    (hf : Module.IsFiniteLocallyFreeOfRank (Localization.Away f)
      (LocalizedModule.Away f M) r) :
    ∃ I : Ideal R, I.FG ∧
      PrimeSpectrum.zeroLocus ({f} : Set R) = PrimeSpectrum.zeroLocus (I : Set R) ∧
      ∀ a : I,
        let _ : Fact ((a : R) ∈ I) := ⟨a.property⟩
        Module.IsFiniteLocallyFreeOfRank (Blowup I a) (strictTransform I a M) r
Sources
LeanstrictTransform · Stacks.Flatness.BlowupFlattening.stacks053I · fittingIdeal_strictTransform_affineBlowup_eq_top · isFiniteLocallyFreeOfRank_strictTransform_affineBlowup · exists_fg_ideal_strictTransform_isFiniteLocallyFreeOfRank

Section15.28 Completion and flatness#

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

Tag 05BC, a lemma

Tag 05BC in the Stacks Project.

AdicCompletion.universallyInjective_directSumToPi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Flat/DirectSumToPi.lean, line 415.

Let R be a Noetherian ring that is I-adically complete. Then the canonical map (⊕_{α ∈ A} R)^∧ → ∏_{α ∈ A} R from the I-adic completion of a direct sum of copies of R into the product of copies of R is universally injective.

theorem AdicCompletion.universallyInjective_directSumToPi
    (R : Type u) [CommRing R] (I : Ideal R) (A : Type v)
    [IsNoetherianRing R] [IsAdicComplete I R] :
    UniversallyInjective (AdicCompletion.directSumToPi R I A)
Tag 06LE, a lemma

Tag 06LE in the Stacks Project.

AdicCompletion.flat_directSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Flat/FlatCompletion.lean, line 202. References: EGA 0 (7.3.3), “more general”; SGA 1 IV (3.1), “more general”.

For a Noetherian ring R and an ideal I, the I-adic completion (⊕_{α ∈ A} R)^∧ of an arbitrary direct sum of copies of R is a flat R-module.

theorem AdicCompletion.flat_directSum
    (R : Type u) [CommRing R] (I : Ideal R) (A : Type v) [IsNoetherianRing R] :
    Module.Flat R (AdicCompletion I (DirectSum A (fun _ : A => R)))
Tag 0911, a lemma

Tag 0911 in the Stacks Project.

tor_pro_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/ProZero.lean, line 204.

Let A be a Noetherian ring, I ⊆ A an ideal, and M a finite A-module. Then for every p > 0 there exists c > 0 such that, for all n ≥ c, the map Tor_p^A(M, A/I^n) → Tor_p^A(M, A/I^{n-c}) induced by the canonical surjection A/I^n ↠ A/I^{n-c} is the zero map.

theorem tor_pro_zero
    [IsNoetherianRing A]
    (M : ModuleCat A) [Module.Finite A M]
    {p : ℕ} (hp : 0 < p) :
    ∃ c : ℕ, 0 < c ∧ ∀ n : ℕ, c ≤ n →
      ((Tor (ModuleCat A) p).obj M).map
        (torProZeroTransition I (Nat.sub_le n c)) = 0
Tag 0912, a lemma

Tag 0912 in the Stacks Project.

flat_limit_and_tensor_limit_of_flat_quotients, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Flat/TensorLimit.lean, line 367.

Let A be a Noetherian ring and I ⊆ A an ideal. Let (M_n) be an inverse system of A-modules such that each M_n is flat over A ⧸ Iⁿ (compatibly with its A-module structure) and each transition map M_{n+1} → M_n is surjective. Then M = lim M_n is flat over A, and for every finite A-module Q the canonical comparison map Q ⊗_A lim M_n → lim (Q ⊗_A M_n) is an isomorphism.

theorem flat_limit_and_tensor_limit_of_flat_quotients
    {A : Type u} [CommRing A] [IsNoetherianRing A] (I : Ideal A)
    (M : ℕᵒᵖ ⥤ ModuleCat.{u} A)
    (quotientModule : ∀ n : ℕ, Module (A ⧸ I ^ n) (M.obj (.op n)))
    (hscalar : ∀ n : ℕ, letI := quotientModule n
      IsScalarTower A (A ⧸ I ^ n) (M.obj (.op n)))
    (hflat : ∀ n : ℕ, letI := quotientModule n
      Module.Flat (A ⧸ I ^ n) (M.obj (.op n)))
    (hsurjective : ∀ n : ℕ, Function.Surjective
      (M.map (homOfLE (Nat.le_succ n)).op)) :
    Module.Flat A (limit M : ModuleCat.{u} A) ∧
      ∀ (Q : ModuleCat.{u} A), Module.Finite A Q →
        IsIso (limit.post M
          ((MonoidalCategory.tensoringLeft (ModuleCat.{u} A)).obj Q))
Tag 0AGW, a lemma

Tag 0AGW in the Stacks Project.

AdicCompletion.isNoetherianRing_and_flat_of_flat_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Flat/FlatCompletion.lean, line 489. References: EGA 0 (10.2.3), “forward implication”.

Let R be a commutative ring, I ⊆ R a finitely generated ideal and M an R-module. If R/I is Noetherian, M/IM is flat over R/I and Tor₁ᴿ(M, R/I) = 0, then the I-adic completion R^∧ is a Noetherian ring and the I-adic completion M^∧ is flat over R^∧.

theorem AdicCompletion.isNoetherianRing_and_flat_of_flat_quotient
    {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M]
    (I : Ideal R) (hI : I.FG) (hRI : IsNoetherianRing (R ⧸ I))
    (hflat : Module.Flat (R ⧸ I) (M ⧸ (I • (⊤ : Submodule R M))))
    (htor : IsZero
      (((Tor (ModuleCat.{max u v} (ULift.{v} R)) 1).obj
        (ModuleCat.of (ULift.{v} R) (ULift.{u} M))).obj
        (ModuleCat.of (ULift.{v} R) (ULift.{v} (R ⧸ I))))) :
    IsNoetherianRing (AdicCompletion I R) ∧
      Module.Flat (AdicCompletion I R) (AdicCompletion I M)
Sources
LeanAdicCompletion.universallyInjective_directSumToPi · AdicCompletion.flat_directSum · tor_pro_zero · flat_limit_and_tensor_limit_of_flat_quotients · AdicCompletion.isNoetherianRing_and_flat_of_flat_quotient

Section15.29 The Koszul complex#

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

Tag 0622, a definition

Tag 0622 in the Stacks Project.

Koszul.differentialGradedAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/DifferentialGradedAlgebra.lean, line 138. References: EGA III (1.1.1); SGA 3 III (4.6.1), “definition”; SGA 6 VII (1.1), “more general”.

The Koszul differential graded algebra K•(φ): its underlying graded algebra is the exterior algebra ⋀[R] E, and its differential is contraction by φ.

The chain complex obtained from its homogeneous pieces is Koszul.complex φ.

noncomputable def differentialGradedAlgebra (φ : E →ₗ[R] R) :
    HomologicalDifferentialGradedExteriorAlgebra φ
Tag 0623, a definition

Tag 0623 in the Stacks Project.

Koszul.seqDual, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Defs.lean, line 158.

The functional Rʳ →ₗ[R] R attached to a sequence f₁, …, f_r of elements of R, namely v ↦ ∑ i, vᵢ * fᵢ; it sends the i-th standard basis vector to fᵢ.

noncomputable def seqDual (f : Fin r → R) : Module.Dual R (Fin r → R)

Koszul.seqComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Defs.lean, line 185. References: EGA III (1.1.1).

The Koszul complex K_•(f₁, …, f_r) of a sequence of elements of R: the Koszul complex of the functional Koszul.seqDual f on Rʳ.

noncomputable def seqComplex (f : Fin r → R) : ChainComplex (ModuleCat.{u} R) ℕ
Tag 0624, a lemma

Tag 0624 in the Stacks Project.

koszul_map_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Functoriality.lean, line 65. References: EGA III (1.1.5).

Functoriality of the Koszul complex.

Let φ : E → R and φ' : E' → R be R-module maps and let ψ : E → E' be an R-module map with φ' ∘ ψ = φ. Then the induced graded-algebra homomorphism ∧(ψ) commutes with the Koszul differentials, i.e. ∧(ψ) ∘ d = d' ∘ ∧(ψ), where d = Koszul.contraction φ and d' = Koszul.contraction φ'. Together with the fact that ∧(ψ) = ExteriorAlgebra.map ψ is automatically a unital graded R-algebra homomorphism, this exhibits ∧(ψ) as a homomorphism of differential graded R-algebras K_•(φ) → K_•(φ').

theorem koszul_map_comm (φ : Module.Dual R E) (φ' : Module.Dual R E') (ψ : E →ₗ[R] E')
    (h : φ'.comp ψ = φ) (x : ExteriorAlgebra R E) :
    exteriorMap ψ (Koszul.contraction φ x) = Koszul.contraction φ' (exteriorMap ψ x)
Tag 0625, a lemma

Tag 0625 in the Stacks Project.

Koszul.seqComplex_mulVec_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Functoriality.lean, line 116.

Change of basis for a Koszul complex. If x is an invertible r × r matrix over R, then the Koszul complex of f is isomorphic to the Koszul complex of the sequence i ↦ ∑ j, x i j * f j.

public theorem seqComplex_mulVec_iso {R : Type u} [CommRing R] {r : ℕ}
    (f : Fin r → R) (x : Matrix (Fin r) (Fin r) R)
    (hx : IsUnit x) :
    Nonempty (Koszul.seqComplex f ≅ Koszul.seqComplex (Matrix.mulVec x f))
Tag 0626, a lemma

Tag 0626 in the Stacks Project.

koszul_scalar_eq_homotopy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Functoriality.lean, line 93. References: EGA III (1.1.7), “more general”.

Multiplication by φ e is null-homotopic on the Koszul complex. Let φ : E → R be an R-module map, let e ∈ E, and set f = φ e. As R-linear endomorphisms of K_•(φ) = ∧(E), f = d ∘ e + e ∘ d, i.e. for every a, f • a = d (e ∧ a) + e ∧ d a, where e ∧ - is left multiplication by ι R e in the exterior algebra.

theorem koszul_scalar_eq_homotopy (φ : Module.Dual R E) (e : E)
    (a : ExteriorAlgebra R E) :
    φ e • a =
      Koszul.contraction φ (ExteriorAlgebra.ι R e * a)
        + ExteriorAlgebra.ι R e * Koszul.contraction φ a
Tag 0663, a lemma

Tag 0663 in the Stacks Project.

Koszul.koszulSeq_smul_nullHomotopic_and_span_le_annihilator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Homotopy.lean, line 149.

Multiplication by each member of a finite sequence is null-homotopic on its Koszul complex, and the ideal generated by the sequence annihilates every Koszul homology module.

public theorem koszulSeq_smul_nullHomotopic_and_span_le_annihilator
    {R : Type*} [CommRing R] {r : ℕ} (f : Fin r → R) :
    (∀ i, Nonempty (Homotopy (f i • 𝟙 (Koszul.seqComplex f)) 0)) ∧
      ∀ n, Ideal.span (Set.range f) ≤
        Module.annihilator R ((Koszul.seqComplex f).homology n)
Tag 0627, an equation

Tag 0627 in the Stacks Project.

Declarations registered for the tag:

Tag 0628, a lemma

Tag 0628 in the Stacks Project.

Stacks.MappingCone.NatIndexed.koszulComplex_phiPrime_iso_cone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Cone.lean, line 613.

The cone of multiplication by f on the Koszul complex of phi is isomorphic, as a chain complex of R-modules, to the Koszul complex of phi' : E ⊕ R → R, by an isomorphism with the prescribed components Θₙ: the inclusion on the ⋀ⁿ E summand and wedging with e₀ = (0,1) on the ⋀^{n-1} E summand.

theorem koszulComplex_phiPrime_iso_cone (φ : Module.Dual R E) (f : R) :
    ∃ Θ : coneComplex (Koszul.complex φ) (Koszul.complex φ) (mulByF (Koszul.complex φ) f) ≅
        Koszul.complex (phiPrime φ f),
      (∀ x : (⋀[R]^0 E),
        (Θ.hom.f 0).hom (show ((Koszul.complex φ).X 0 : Type (max u v)) from x) = inclPow 0 x) ∧
      (∀ (n : ℕ) (b : (⋀[R]^(n+1) E)) (a : (⋀[R]^n E)),
        (Θ.hom.f (n+1)).hom
            (show ((Koszul.complex φ).X (n+1) × (Koszul.complex φ).X n : Type (max u v))
              from (b, a))
          = inclPow (n+1) b + wedgeE0Pow (n+1) a)
Tag 0629, a lemma

Tag 0629 in the Stacks Project.

Koszul.seqComplex_snoc_iso_cone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Cone.lean, line 742.

The Koszul complex of a sequence obtained by appending a is isomorphic to the cone of multiplication by a on the Koszul complex of the original sequence.

public theorem seqComplex_snoc_iso_cone {R : Type u} [CommRing R] {r : ℕ}
    (f : Fin r → R) (a : R) :
    Nonempty
      (Koszul.seqComplex (Fin.snoc f a) ≅
        Stacks.MappingCone.NatIndexed.coneComplex (Koszul.seqComplex f) (Koszul.seqComplex f)
          (Stacks.MappingCone.NatIndexed.mulByF (Koszul.seqComplex f) a))
Tag 062A, a lemma

Tag 062A in the Stacks Project.

Koszul.exists_homotopyEquiv_mappingCone_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/HomotopyCofiber.lean, line 81.

The cone of a composite of two endomorphisms is homotopy equivalent to the cone of a map from the shifted cone of the first endomorphism to the cone of the second.

theorem exists_homotopyEquiv_mappingCone_comp
    {C : Type u} [Category.{v} C] [Preadditive C] [HasZeroObject C]
    [HasBinaryBiproducts C]
    (A : CochainComplex C ℤ) (f g : A ⟶ A) :
    ∃ (φ : (CochainComplex.mappingCone f)⟦(-1 : ℤ)⟧ ⟶
        CochainComplex.mappingCone g),
      Nonempty
        (HomotopyEquiv (CochainComplex.mappingCone (g ≫ f))
          (CochainComplex.mappingCone φ))
Tag 062B, a lemma

Tag 062B in the Stacks Project.

Koszul.exists_homotopyEquiv_koszulComplex_coprod_mul_mappingCone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/HomotopyCofiber.lean, line 529.

After adjoining f * g to a linear functional, its Koszul complex is homotopy equivalent to the mapping cone of a map from the shifted complex obtained by adjoining f to the complex obtained by adjoining g.

theorem exists_homotopyEquiv_koszulComplex_coprod_mul_mappingCone
    {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E]
    (φ : E →ₗ[R] R) (f g : R) :
    let K (a : R) : CochainComplex (ModuleCat.{max u v} R) ℤ :=
      (ComplexShape.embeddingDownNat.extendFunctor (ModuleCat.{max u v} R)).obj
        (Koszul.complex (φ.coprod (a • LinearMap.id)))
    ∃ ψ : (K f)⟦(-1 : ℤ)⟧ ⟶ K g,
      Nonempty (HomotopyEquiv (K (f * g)) (CochainComplex.mappingCone ψ))
Tag 062C, a lemma

Tag 062C in the Stacks Project.

Koszul.exists_homotopyEquiv_koszulComplex_snoc_mul_mappingCone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/HomotopyCofiber.lean, line 597.

The Koszul complex on a finite sequence ending in f * g is homotopy equivalent to the mapping cone of a map from the shifted complex ending in f to the complex ending in g.

theorem exists_homotopyEquiv_koszulComplex_snoc_mul_mappingCone
    {R : Type u} [CommRing R] {n : ℕ} (s : Fin n → R) (f g : R) :
    let K (a : R) : CochainComplex (ModuleCat.{u} R) ℤ :=
      (ComplexShape.embeddingDownNat.extendFunctor (ModuleCat.{u} R)).obj
        (Koszul.complex (Fintype.linearCombination R (Fin.snoc s a)))
    ∃ ψ : (K f)⟦(-1 : ℤ)⟧ ⟶ K g,
      Nonempty (HomotopyEquiv (K (f * g)) (CochainComplex.mappingCone ψ))
Tag 0664, a lemma

Tag 0664 in the Stacks Project.

Koszul.seqComplex_append_iso_totTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Append.lean, line 607. References: EGA III (1.1.1), “(f)”.

Stacks Tag 0664. The Koszul complex on the concatenation of two sequences f_1, ..., f_r and g_1, ..., g_s (length r + s) is isomorphic, as a chain complex of R-modules, to the total complex of the tensor product of the Koszul complexes on f and on g; see seqComplexAppendIsoTotTensor for the isomorphism itself.

theorem seqComplex_append_iso_totTensor {r s : ℕ} (f : Fin r → R) (g : Fin s → R) :
    Nonempty
      (seqComplex (Fin.append f g) ≅ totTensor (seqComplex f) (seqComplex g))
Sources
LeanKoszul.differentialGradedAlgebra · Koszul.seqDual · Koszul.seqComplex · koszul_map_comm · Koszul.seqComplex_mulVec_iso · koszul_scalar_eq_homotopy · Koszul.koszulSeq_smul_nullHomotopic_and_span_le_annihilator · HomologicalComplex.homotopyCofiber.d_fstX

Section15.30 The extended alternating Čech complex#

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

Tag 0G6G, a lemma

Tag 0G6G in the Stacks Project.

ExtendedAlternatingCech.cechd_comp_cechd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Cech/Extended.lean, line 404.

Stacks 0G6G. For consecutive integer degrees i, j, k, the composition d_{j,k} ∘ d_{i,j} of the differentials of the extended alternating Čech complex vanishes.

theorem cechd_comp_cechd (i j k : ℤ) (hij : (ComplexShape.up ℤ).Rel i j)
    (hjk : (ComplexShape.up ℤ).Rel j k) :
    CategoryStruct.comp (cechd f M i j) (cechd f M j k) = 0
Tag 0G6H, a lemma

Tag 0G6H in the Stacks Project.

ExtendedCech.termTensorEquiv_comm_d, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Cech/Tensor.lean, line 199.

Stacks Lemma 15.30.2 (Tag 0G6H). The degreewise canonical isomorphisms termTensorEquiv (induced by M ⊗_R R_g ≅ M_g) commute with the Čech differentials, the differential of M ⊗_R Č•(R) being id_M ⊗ d_R = LinearMap.lTensor M (Cech.cechD f R p). Together with termTensorEquiv this exhibits the extended alternating Čech complex of M as M ⊗_R Č•(R), an isomorphism of cochain complexes of R-modules.

theorem termTensorEquiv_comm_d (p : ℕ) :
    (termTensorEquiv f M (p + 1)).toLinearMap.comp (cechD f M p)
      = (LinearMap.lTensor M (cechD f R p)).comp (termTensorEquiv f M p).toLinearMap
Tag 0G6I, a lemma

Tag 0G6I in the Stacks Project.

Stacks.CechBaseChange.exists_cechComplexBaseChange_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Cech/BaseChange.lean, line 504.

Stacks 0G6I. Let R → S be a ring map, g_i the image of f_i in S and N = S ⊗_R M. There is an isomorphism of cochain complexes of S-modules e : C^•(f; M) ⊗_R S ≅ C^•(g; N) (the target lifted to the universe of the source) whose degree-p component, after lowering the lift, is termBaseChangeS f M S p.

theorem exists_cechComplexBaseChange_iso :
    ∃ e : cechComplexBaseChange f M S ≅ cechComplexBaseChangeTarget f M S,
      ∀ p : ℕ, ULift.moduleEquiv.toLinearMap.comp (e.hom.f p).hom =
        termBaseChangeS f M S p
Tag 0G6J, a lemma

Tag 0G6J in the Stacks Project.

Stacks.CechContractible.cechComplex_nullHomotopic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Cech/Contractible.lean, line 677.

Stacks 0G6J. If some f i is a unit in R, then the extended alternating Čech complex of M is homotopy equivalent to 0: the identity chain map is chain homotopic to the zero chain map.

theorem cechComplex_nullHomotopic
    (hunit : ∃ i : Fin r, IsUnit (f i)) :
    Nonempty (Homotopy (𝟙 (cechComplex f M)) 0)
Tag 0G6K, a lemma

Tag 0G6K in the Stacks Project.

Cech.cechComplex_homology_torsion_support_vanishes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Cech/Cohomology.lean, line 271.

Stacks 0G6K. The cohomology of the extended alternating Čech complex is concentrated in degrees 0, …, r; every chosen element acts locally nilpotently on every cohomology class; its support lies in the common zero locus of the chosen elements; and all cohomology vanishes when an element of their generated ideal acts invertibly on the coefficient module.

theorem cechComplex_homology_torsion_support_vanishes
    {R : Type u} [CommRing R] {r : ℕ} (f : Fin r → R)
    (M : Type v) [AddCommGroup M] [Module R M] (q : ℤ) :
    let K : CochainComplex (ModuleCat.{max u v} R) ℤ :=
      (Cech.cechComplex f M).extend ComplexShape.embeddingUpNat
    ((q < 0 ∨ (r : ℤ) < q) → Subsingleton (K.homology q)) ∧
      (∀ (i : Fin r) (x : K.homology q),
        ∃ n : ℕ, 0 < n ∧ f i ^ n • x = 0) ∧
      Module.support R (K.homology q) ⊆
        PrimeSpectrum.zeroLocus (Ideal.span (Set.range f) : Set R) ∧
      ((∃ g ∈ Ideal.span (Set.range f),
          IsUnit (algebraMap R (Module.End R M) g)) →
        Subsingleton (K.homology q))
Tag 0913, a lemma

Tag 0913 in the Stacks Project.

Cech.cechComplex_isColimit_koszulPowerComplexes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Cech/KoszulColimit.lean, line 672.

The extended alternating Čech complex of a finite sequence f is the colimit of the regraded Koszul complexes on its positive powers. The transition maps multiply each standard exterior-basis vector by the product of the entries of f indexed by its complement, and the colimit cocone sends the basis vector indexed by s to the localized generator indexed by the complement t of s, with sign (-1) ^ (∑ i ∈ t, (i + 1) + p + r * p).

public theorem cechComplex_isColimit_koszulPowerComplexes
    {R : Type u} [CommRing R] {r : ℕ} (f : Fin r → R) :
    ∃ σ : ∀ n : ℕ,
        Koszul.seqComplex (fun i ↦ f i ^ (n + 1)) ⟶
          Koszul.seqComplex (fun i ↦ f i ^ (n + 2)),
      (∀ (n q : ℕ) (s : Finset (Fin r)) (hs : s.card = q),
        (σ n).f q
            ⟨ExteriorAlgebra.ιMulti R q
                (fun k ↦ Pi.single (s.orderEmbOfFin hs k) 1),
              Koszul.ιMulti_mem q _⟩ =
          (∏ i ∈ sᶜ, f i) •
            ⟨ExteriorAlgebra.ιMulti R q
                (fun k ↦ Pi.single (s.orderEmbOfFin hs k) 1),
              Koszul.ιMulti_mem q _⟩) ∧
      ∃ ι : ∀ n : ℕ, koszulPowerCochainComplex f n ⟶ Cech.cechComplex f R,
        ∃ hι : ∀ n : ℕ,
            (koszulPowerDiagram f σ).map (homOfLE (Nat.le_succ n)) ≫
              ι (n + 1) = ι n,
          (∀ (n p q : ℕ) (s t : Finset (Fin r)) (hs : s.card = q) (ht : t.card = p)
              (hcard : p + q = r) (_ : Disjoint s t) (_ : s ∪ t = Finset.univ),
            (ι n).f p
                (koszulRegradeHom f n p q hcard
                  ⟨ExteriorAlgebra.ιMulti R q
                      (fun k ↦ Pi.single (s.orderEmbOfFin hs k) 1),
                    Koszul.ιMulti_mem q _⟩) =
              DirectSum.lof R {w : Finset (Fin r) // w.card = p}
                (fun w ↦ Cech.cechMod f R w.1) ⟨t, ht⟩
                (LocalizedModule.mk
                  ((-1 : R) ^ ((∑ i ∈ t, (i.val + 1)) + p + r * p))
                  ⟨(∏ i ∈ t, f i) ^ (n + 1), n + 1, rfl⟩)) ∧
          Nonempty (IsColimit
            ({ pt := Cech.cechComplex f R
               ι := NatTrans.ofSequence
                 (F := koszulPowerDiagram f σ)
                 (G := (Functor.const ℕ).obj (Cech.cechComplex f R)) ι
                 (fun n ↦ (hι n).trans (Category.comp_id _).symm) } :
              Cocone (koszulPowerDiagram f σ)))
Sources
LeanExtendedAlternatingCech.cechd_comp_cechd · ExtendedCech.termTensorEquiv_comm_d · Stacks.CechBaseChange.exists_cechComplexBaseChange_iso · Stacks.CechContractible.cechComplex_nullHomotopic · Cech.cechComplex_homology_torsion_support_vanishes · Cech.cechComplex_isColimit_koszulPowerComplexes

Section15.31 Koszul regular sequences#

Section 15.31 of the Stacks Project, Tag 062D. 17 tags here are carried by 22 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 062E, a definition

Tag 062E in the Stacks Project.

Koszul.IsKoszulRegularOn, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Defs.lean, line 226. The attribute's comment: “(1)”.

A sequence f₁, …, f_r is M-Koszul-regular if Hᵢ(K_•(f) ⊗_R M) = 0 for all i ≠ 0.

def IsKoszulRegularOn (f : Fin r → R) (M : Type w) [AddCommGroup M] [Module R M] : Prop

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

A sequence f₁, …, f_r is M-H₁-regular if H₁(K_•(f) ⊗_R M) = 0.

def IsH1RegularOn (f : Fin r → R) (M : Type w) [AddCommGroup M] [Module R M] : Prop

Koszul.IsKoszulRegular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Defs.lean, line 236. The attribute's comment: “(3)”.

A sequence f₁, …, f_r is Koszul-regular if Hᵢ(K_•(f)) = 0 for all i ≠ 0.

def IsKoszulRegular (f : Fin r → R) : Prop

Koszul.IsH1Regular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Defs.lean, line 241. The attribute's comment: “(4)”.

A sequence f₁, …, f_r is H₁-regular if H₁(K_•(f)) = 0.

def IsH1Regular (f : Fin r → R) : Prop
Tag 062F, a lemma

Tag 062F in the Stacks Project.

Koszul.isKoszulRegularOn_and_isKoszulRegular_of_regular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Regular.lean, line 846.

If every term of a finite sequence acts injectively on the quotient of M by its predecessors, then the sequence is M-Koszul-regular. In particular, an M-regular sequence is M-Koszul-regular, and a regular sequence in R is Koszul-regular.

theorem isKoszulRegularOn_and_isKoszulRegular_of_regular
    {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
    {r : ℕ} {f : Fin r → R} :
    (RingTheory.Sequence.IsWeaklyRegular M (List.ofFn f) →
        Koszul.IsKoszulRegularOn f M) ∧
      (RingTheory.Sequence.IsRegular M (List.ofFn f) →
        Koszul.IsKoszulRegularOn f M) ∧
      (RingTheory.Sequence.IsRegular R (List.ofFn f) →
        Koszul.IsKoszulRegular f)
Tag 0CEM, a lemma

Tag 0CEM in the Stacks Project.

Koszul.IsKoszulRegularOn.isH1RegularOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Regular.lean, line 336. The attribute's comment: “(1)”.

If the sequence f_1, ..., f_r is M-Koszul-regular, then it is M-H_1-regular.

theorem IsKoszulRegularOn.isH1RegularOn {f : Fin r → R} {M : Type v} [AddCommGroup M]
    [Module R M] (h : IsKoszulRegularOn f M) : IsH1RegularOn f M

Koszul.IsKoszulRegular.isH1Regular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Regular.lean, line 342. The attribute's comment: “(2)”.

If the sequence f_1, ..., f_r is Koszul-regular, then it is H_1-regular.

theorem IsKoszulRegular.isH1Regular {f : Fin r → R} (h : IsKoszulRegular f) : IsH1Regular f
Tag 062G, a lemma

Tag 062G in the Stacks Project.

Koszul.isH1RegularOn_and_isKoszulRegularOn_snoc_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Regular.lean, line 1073.

Adjoining a product to a finite sequence preserves both M-H₁-regularity and M-Koszul-regularity when adjoining each factor separately has the corresponding property.

theorem isH1RegularOn_and_isKoszulRegularOn_snoc_mul
    {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
    {n : ℕ} (s : Fin n → R) (f g : R) :
    ((Koszul.IsH1RegularOn (Fin.snoc s f) M ∧
        Koszul.IsH1RegularOn (Fin.snoc s g) M) →
      Koszul.IsH1RegularOn (Fin.snoc s (f * g)) M) ∧
    ((Koszul.IsKoszulRegularOn (Fin.snoc s f) M ∧
        Koszul.IsKoszulRegularOn (Fin.snoc s g) M) →
      Koszul.IsKoszulRegularOn (Fin.snoc s (f * g)) M)
Tag 062H, a lemma

Tag 062H in the Stacks Project.

KoszulC.isH1Regular_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/FlatBaseChange.lean, line 597. The attribute's comment: “(1)”.

For a flat ring map φ : R → S, if f_1, ..., f_r is M-H_1-regular over R, then φ(f_1), ..., φ(f_r) is (S ⊗_R M)-H_1-regular over S.

theorem isH1Regular_baseChange {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Module.Flat R S] {r : ℕ} (f : Fin r → R) (M : Type*) [AddCommGroup M] [Module R M]
    (hf : IsH1RegularOn f M) :
    IsH1RegularOn (R := S) (fun i => algebraMap R S (f i)) (S ⊗[R] M)

KoszulC.isKoszulRegular_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/FlatBaseChange.lean, line 606. The attribute's comment: “(2)”. References: SGA 6 VII (1.5), “special case”; SGA 6 VIII (1.3), “VII 1.5, special case”.

For a flat ring map φ : R → S, if f_1, ..., f_r is M-Koszul-regular over R, then φ(f_1), ..., φ(f_r) is (S ⊗_R M)-Koszul-regular over S.

theorem isKoszulRegular_baseChange {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Module.Flat R S] {r : ℕ} (f : Fin r → R) (M : Type*) [AddCommGroup M] [Module R M]
    (hf : IsKoszulRegularOn f M) :
    IsKoszulRegularOn (R := S) (fun i => algebraMap R S (f i)) (S ⊗[R] M)
Tag 062I, a lemma

Tag 062I in the Stacks Project.

Koszul.isQuasiRegular_of_isH1RegularOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Quasiregular.lean, line 346.

Stacks 062I. An M-H₁-regular sequence is M-quasi-regular.

public theorem isQuasiRegular_of_isH1RegularOn
    {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
    {r : ℕ} {f : Fin r → R} (hf : Koszul.IsH1RegularOn f M) :
    RingTheory.Sequence.IsQuasiRegular M (List.ofFn f)
Tag 09CC, a lemma

Tag 09CC in the Stacks Project.

Koszul.regular_koszulRegular_h1Regular_quasiRegular_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Quasiregular.lean, line 374. References: EGA 0 (15.1.11), “(1) ⇔ (4), local case”; EGA IV (19.5.1), “a)–c), local case”; EGA 0 (15.2.2), “converse: q-reg ⇒ reg”; EGA 0 (15.1.10), “special case”; EGA 0 (15.1.9), “special case”; EGA IV (16.9.12), “parenthetical”.

Stacks 09CC. Let M be a nonzero finite module over a local Noetherian ring R, and let f be a finite sequence in the maximal ideal. Being M-regular, M-Koszul-regular, M-H₁-regular, and M-quasi-regular are equivalent. In particular, the corresponding four notions for the sequence in R are equivalent.

public theorem regular_koszulRegular_h1Regular_quasiRegular_tfae
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial M] [Module.Finite R M]
    {r : ℕ} (f : Fin r → R) (hf : ∀ i, f i ∈ IsLocalRing.maximalIdeal R) :
    List.TFAE
        [RingTheory.Sequence.IsRegular M (List.ofFn f),
          Koszul.IsKoszulRegularOn f M,
          Koszul.IsH1RegularOn f M,
          RingTheory.Sequence.IsQuasiRegular M (List.ofFn f)] ∧
      List.TFAE
        [RingTheory.Sequence.IsRegular R (List.ofFn f),
          Koszul.IsKoszulRegular f,
          Koszul.IsH1Regular f,
          RingTheory.Sequence.IsQuasiRegular R (List.ofFn f)]
Tag 0665, a lemma

Tag 0665 in the Stacks Project.

Koszul.inf_span_eq_smul_span, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Regular.lean, line 351.

Let A be a commutative ring, I an ideal of A, and g_1, ..., g_m elements of A. If the images of g_1, ..., g_m in A/I form an H_1-regular sequence, then I ⊓ (g_1, ..., g_m) = I (g_1, ..., g_m) as ideals of A.

theorem inf_span_eq_smul_span (I : Ideal A) (g : Fin m → A)
    (hreg : Koszul.IsH1Regular (fun i => Ideal.Quotient.mk I (g i))) :
    I ⊓ Ideal.span (Set.range g) = I * Ideal.span (Set.range g)
Tag 0666, a lemma

Tag 0666 in the Stacks Project.

Koszul.inf_sq_eq_mul_of_quotient_generated_by_isH1Regular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Regular.lean, line 451.

If I ⊆ J and J / I is generated by an H₁-regular sequence, then I ∩ J² = I J.

theorem inf_sq_eq_mul_of_quotient_generated_by_isH1Regular
    {A : Type*} [CommRing A] (I J : Ideal A) (hIJ : I ≤ J)
    {m : ℕ} (g : Fin m → A ⧸ I)
    (hspan : Ideal.span (Set.range g) = Ideal.map (Ideal.Quotient.mk I) J)
    (hreg : Koszul.IsH1Regular g) :
    I ⊓ J ^ 2 = I * J
Tag 0667, a lemma

Tag 0667 in the Stacks Project.

Koszul.isQuasiRegular_append_of_isH1Regular_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Concatenation/QuasiRegularAppend.lean, line 567.

Stacks 0667. If f is quasi-regular and the image of g modulo the ideal generated by f is H₁-regular, then the concatenation of f and g is quasi-regular.

public theorem isQuasiRegular_append_of_isH1Regular_quotient
    {A : Type*} [CommRing A] {n m : ℕ} (f : Fin n → A) (g : Fin m → A)
    (hf : RingTheory.Sequence.IsQuasiRegular A (List.ofFn f))
    (hg : Koszul.IsH1Regular
      (fun j => Ideal.Quotient.mk (Ideal.span (Set.range f)) (g j))) :
    RingTheory.Sequence.IsQuasiRegular A (List.ofFn (Fin.append f g))
Tag 0668, a lemma

Tag 0668 in the Stacks Project.

Koszul.isH1Regular_append, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Regular.lean, line 289.

Let A be a commutative ring, let f : Fin n → A be an H_1-regular sequence, let I = (f_0, ..., f_{n-1}) be the ideal it generates, and let g : Fin m → A be such that the images (Ideal.Quotient.mk I) ∘ g form an H_1-regular sequence in A/I. Then the concatenated sequence Fin.append f g : Fin (n + m) → A is H_1-regular in A.

theorem isH1Regular_append {A : Type*} [CommRing A] {n m : ℕ}
    (f : Fin n → A) (g : Fin m → A)
    (hf : Koszul.IsH1Regular f)
    (hg : Koszul.IsH1Regular
      (fun j => (Ideal.Quotient.mk (Ideal.span (Set.range f))) (g j))) :
    Koszul.IsH1Regular (Fin.append f g)
Tag 068L, a lemma

Tag 068L in the Stacks Project.

Koszul.isH1Regular_quotient_of_isH1Regular_append, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Regular.lean, line 421.

If f_1, ..., f_n, g_1, ..., g_m is an H₁-regular sequence in A, then the images ḡ_1, ..., ḡ_m of the g_j in the quotient A / (f_1, ..., f_n) form an H₁-regular sequence.

theorem isH1Regular_quotient_of_isH1Regular_append {A : Type*} [CommRing A] {n m : ℕ}
    (f : Fin n → A) (g : Fin m → A)
    (h : Koszul.IsH1Regular (Fin.append f g)) :
    Koszul.IsH1Regular
      (fun j : Fin m => Ideal.Quotient.mk (Ideal.span (Set.range f)) (g j))
Tag 0669, a lemma

Tag 0669 in the Stacks Project.

Koszul.koszul_regular_append, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Concatenation/KoszulRegularAppend.lean, line 706.

If f is Koszul-regular and the image of g modulo the ideal generated by f is Koszul-regular, then the concatenation of f and g is Koszul-regular.

public theorem koszul_regular_append {A : Type*} [CommRing A] {n m : ℕ}
    (f : Fin n → A) (g : Fin m → A)
    (hf : Koszul.IsKoszulRegular f)
    (hg : Koszul.IsKoszulRegular
      (fun j => Ideal.Quotient.mk (Ideal.span (Set.range f)) (g j))) :
    Koszul.IsKoszulRegular (Fin.append f g)
Tag 068M, a lemma

Tag 068M in the Stacks Project.

Koszul.koszulRegular_quotient_of_koszulRegular_append, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Concatenation/KoszulRegularQuotient.lean, line 172.

If f and the concatenation of f and g are Koszul-regular, then the image of g in the quotient by the ideal generated by f is Koszul-regular.

public theorem koszulRegular_quotient_of_koszulRegular_append
    {A : Type*} [CommRing A] {n m : ℕ} (f : Fin n → A) (g : Fin m → A)
    (hf : Koszul.IsKoszulRegular f)
    (hfg : Koszul.IsKoszulRegular (Fin.append f g)) :
    Koszul.IsKoszulRegular
      (fun j : Fin m => Ideal.Quotient.mk (Ideal.span (Set.range f)) (g j))
Tag 066A, a lemma

Tag 066A in the Stacks Project.

Koszul.regularity_of_generators_of_eq_span_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Concatenation/GeneratorIndependence.lean, line 434.

Stacks 066A. If an ideal generated by r elements admits a quasi-regular, H₁-regular, or Koszul-regular generating sequence of length r, then every generating sequence of length r has the corresponding property.

public theorem regularity_of_generators_of_eq_span_range
    {R : Type*} [CommRing R] {r : ℕ} (I : Ideal R) (f : Fin r → R)
    (hf : Ideal.span (Set.range f) = I) :
    ((∃ g : Fin r → R, Ideal.span (Set.range g) = I ∧
        RingTheory.Sequence.IsQuasiRegular R (List.ofFn g)) →
      RingTheory.Sequence.IsQuasiRegular R (List.ofFn f)) ∧
    ((∃ g : Fin r → R, Ideal.span (Set.range g) = I ∧ Koszul.IsH1Regular g) →
      Koszul.IsH1Regular f) ∧
    ((∃ g : Fin r → R, Ideal.span (Set.range g) = I ∧ Koszul.IsKoszulRegular g) →
      Koszul.IsKoszulRegular f)
Tag 068P, a lemma

Tag 068P in the Stacks Project.

Stacks.GenericLinearForm.linearForm_isNonZeroDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MvPolynomial/GenericLinearForm.lean, line 149.

Stacks 068P. If the only x ∈ R with x a_i = 0 for all i is x = 0, then f = ∑ a_i t_i is a nonzerodivisor in R[t_1, ..., t_n]: every g with f * g = 0 is zero.

theorem linearForm_isNonZeroDivisor (a : Fin n → R)
    (hinj : ∀ x : R, (∀ i, x * a i = 0) → x = 0) :
    ∀ g : MvPolynomial (Fin n) R, linearForm a * g = 0 → g = 0
Tag 068Q, a lemma

Tag 068Q in the Stacks Project.

Koszul.isRegular_upperTriangular_of_isKoszulRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Descent.lean, line 1466.

Stacks 068Q. A Koszul-regular sequence generating a proper ideal becomes a regular sequence after a generic invertible upper-triangular change of generators. The resulting polynomial localization is faithfully flat and smooth over the original ring, and the changed sequence generates the extension of the original ideal.

public theorem isRegular_upperTriangular_of_isKoszulRegular
    {R : Type*} [CommRing R] {n : ℕ} (f : Fin n → R)
    (hf : Koszul.IsKoszulRegular f)
    (hproper : Ideal.span (Set.range f) ≠ ⊤) :
    let σ := {ij : Fin n × Fin n // ij.1 ≤ ij.2}
    let P := MvPolynomial σ R
    let d : P := ∏ i : Fin n, MvPolynomial.X ⟨(i, i), le_rfl⟩
    let S := Localization.Away d
    let g : Fin n → S := fun i ↦
      ∑ j : Fin n, if hij : i ≤ j then
        algebraMap P S (MvPolynomial.X ⟨(i, j), hij⟩) * algebraMap R S (f j)
      else 0
    Module.FaithfullyFlat R S ∧ Algebra.Smooth R S ∧
      RingTheory.Sequence.IsRegular S (List.ofFn g) ∧
        Ideal.map (algebraMap R S) (Ideal.span (Set.range f)) =
          Ideal.span (Set.range g)
Sources
LeanKoszul.IsKoszulRegularOn · Koszul.IsH1RegularOn · Koszul.IsKoszulRegular · Koszul.IsH1Regular · Koszul.isKoszulRegularOn_and_isKoszulRegular_of_regular · Koszul.IsKoszulRegularOn.isH1RegularOn · Koszul.IsKoszulRegular.isH1Regular · Koszul.isH1RegularOn_and_isKoszulRegularOn_snoc_mul

Section15.32 More on Koszul regular sequences#

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

Tag 0G6L, a lemma

Tag 0G6L in the Stacks Project.

Cech.cechComplex_homology_isZero_of_isKoszulRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Cech/KoszulResolution.lean, line 233.

The extended alternating Čech complex of a Koszul-regular sequence has zero cohomology in every degree other than the length of the sequence.

public theorem cechComplex_homology_isZero_of_isKoszulRegular
    {R : Type u} [CommRing R] {r : ℕ} (f : Fin r → R) (hf : Koszul.IsKoszulRegular f)
    (p : ℕ) (hp : p ≠ r) :
    CategoryTheory.Limits.IsZero ((Cech.cechComplex f R).homology p)
Tag 0BIQ, a lemma

Tag 0BIQ in the Stacks Project.

Koszul.exists_affineBlowup_algEquiv_mvPolynomial_quotient_of_isH1Regular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Blowup.lean, line 199.

Stacks Project, Tag 0BIQ. The affine blowup algebra associated to an H₁-regular sequence is the polynomial algebra on the ratios of the remaining terms by the first term, modulo the evident linear relations.

public theorem exists_affineBlowup_algEquiv_mvPolynomial_quotient_of_isH1Regular
    {R : Type u} [CommRing R] {n : ℕ} (f : Fin (n + 1) → R)
    (hf : Koszul.IsH1Regular f) :
    Nonempty
      (affineBlowupAlgebraAway (Ideal.span (Set.range f)) (f 0) ≃ₐ[R]
        MvPolynomial (Fin n) R ⧸
          Ideal.span
            (Set.range fun i : Fin n ↦
              MvPolynomial.C (f 0) * MvPolynomial.X i - MvPolynomial.C (f i.succ)))
Tag 063Q, a lemma

Tag 063Q in the Stacks Project.

KoszulH1.cmp_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/H1BaseChange.lean, line 383.

Stacks Project, Tag 063Q. Let A → B be a ring map and f_1, …, f_r a sequence in B such that B/(f_1, …, f_r) is flat as an A-module. Let A → A' be a ring map and set B' = B ⊗_A A', f'_i = f_i ⊗ 1. Then the canonical comparison map

Φ : H_1(K_•(B, f_1, …, f_r)) ⊗_A A' ⟶ H_1(K_•(B', f'_1, …, f'_r))

is surjective.

Here the flatness hypothesis is stated as Module.Flat A (B ⧸ Ideal.span (Set.range f)), the quotient being viewed as an A-module by restriction of scalars along A → B.

theorem cmp_surjective
    {A B A' : Type*} [CommRing A] [CommRing B] [Algebra A B] [CommRing A'] [Algebra A A']
    {r : ℕ} (f : Fin r → B)
    (hflat : Module.Flat A (B ⧸ Ideal.span (Set.range f))) :
    Function.Surjective (cmp (A := A) (A' := A') f)
Tag 0CEP, a lemma

Tag 0CEP in the Stacks Project.

Koszul.quasiRegular_and_h1Regular_baseChange_of_quotient_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/FlatQuotient.lean, line 640.

Stacks Project, Tag 0CEP. Suppose that B / (f₁, …, fᵣ) is flat over A. If f is quasi-regular, then its image in B ⊗[A] A' is quasi-regular; if f is H₁-regular, then its image is H₁-regular.

public theorem quasiRegular_and_h1Regular_baseChange_of_quotient_flat
    {A B A' : Type*} [CommRing A] [CommRing B] [Algebra A B]
    [CommRing A'] [Algebra A A'] {r : ℕ} (f : Fin r → B)
    (hflat : Module.Flat A (B ⧸ Ideal.span (Set.range f))) :
    (IsQuasiRegular B (List.ofFn f) →
      IsQuasiRegular (B ⊗[A] A')
        (List.ofFn (KoszulH1.fp (A := A) (A' := A') f))) ∧
    (Koszul.IsH1Regular f →
      Koszul.IsH1Regular (KoszulH1.fp (A := A) (A' := A') f))
Tag 0CEQ, a lemma

Tag 0CEQ in the Stacks Project.

Koszul.flat_quotient_span_of_isQuasiRegular_of_locallyNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/FlatQuotient.lean, line 866.

Stacks Project, Tag 0CEQ. A flat, finitely presented algebra remains flat after quotienting by lifts of a quasi-regular sequence whose reduced quotient is flat.

public theorem flat_quotient_span_of_isQuasiRegular_of_locallyNilpotent
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Module.Flat R S] [Algebra.FinitePresentation R S]
    (I : Ideal R) (hI : I ≤ nilradical R) {r : ℕ} (f : Fin r → S)
    (hqr : IsQuasiRegular (S ⧸ I.map (algebraMap R S))
      (List.ofFn (fun i ↦ Ideal.Quotient.mk (I.map (algebraMap R S)) (f i))))
    (hflat : Module.Flat (R ⧸ I)
      ((S ⧸ I.map (algebraMap R S)) ⧸
        Ideal.span (Set.range (fun i ↦
          Ideal.Quotient.mk (I.map (algebraMap R S)) (f i))))) :
    Module.Flat R (S ⧸ Ideal.span (Set.range f))
Tag 0CER, a lemma

Tag 0CER in the Stacks Project.

Koszul.smooth_quotient_span_of_isQuasiRegular_of_locallyNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/FlatQuotient.lean, line 950.

Stacks Project, Tag 0CER. A flat, finitely presented algebra remains smooth after quotienting by lifts of a quasi-regular sequence whose reduced quotient is smooth.

public theorem smooth_quotient_span_of_isQuasiRegular_of_locallyNilpotent
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Module.Flat R S] [Algebra.FinitePresentation R S]
    (I : Ideal R) (hI : I ≤ nilradical R) {r : ℕ} (f : Fin r → S)
    (hqr : IsQuasiRegular (S ⧸ I.map (algebraMap R S))
      (List.ofFn (fun i ↦ Ideal.Quotient.mk (I.map (algebraMap R S)) (f i))))
    (hsmooth : Algebra.Smooth (R ⧸ I)
      ((S ⧸ I.map (algebraMap R S)) ⧸
        Ideal.span (Set.range (fun i ↦
          Ideal.Quotient.mk (I.map (algebraMap R S)) (f i))))) :
    Algebra.Smooth R (S ⧸ Ideal.span (Set.range f))
Sources
LeanCech.cechComplex_homology_isZero_of_isKoszulRegular · Koszul.exists_affineBlowup_algEquiv_mvPolynomial_quotient_of_isH1Regular · KoszulH1.cmp_surjective · Koszul.quasiRegular_and_h1Regular_baseChange_of_quotient_flat · Koszul.flat_quotient_span_of_isQuasiRegular_of_locallyNilpotent · Koszul.smooth_quotient_span_of_isQuasiRegular_of_locallyNilpotent

Section15.33 Regular ideals#

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

Tag 07CV, a definition

Tag 07CV in the Stacks Project.

Ideal.IsRegular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/Ideal.lean, line 67. The attribute's comment: “(1)”. References: EGA IV (16.9.7); EGA IV (19.3.1); SGA 1 II (4.14).

An ideal is regular if, at every prime containing it, some principal localization away from the prime is generated by a regular sequence.

public def IsRegular {R : Type*} [CommRing R] (I : Ideal R) : Prop

Ideal.IsKoszulRegular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/Ideal.lean, line 77. The attribute's comment: “(2)”.

An ideal is Koszul-regular if, at every prime containing it, some principal localization away from the prime is generated by a Koszul-regular sequence.

public def IsKoszulRegular {R : Type*} [CommRing R] (I : Ideal R) : Prop

Ideal.IsH1Regular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/Ideal.lean, line 87. The attribute's comment: “(3)”.

An ideal is H₁-regular if, at every prime containing it, some principal localization away from the prime is generated by an H₁-regular sequence.

public def IsH1Regular {R : Type*} [CommRing R] (I : Ideal R) : Prop

Declarations registered for the tag:

Tag 07CW, a lemma

Tag 07CW in the Stacks Project.

Quasiregular.isQuasiregularIdeal_fg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/Quasiregular.lean, line 835. References: EGA IV (16.9.4), “(i)”.

Stacks 07CW. A quasi-regular ideal is finitely generated.

theorem isQuasiregularIdeal_fg {I : Ideal R} (hI : IsQuasiregularIdeal' I) : I.FG
Tag 08RK, a lemma

Tag 08RK in the Stacks Project.

Quasiregular.cotangent_finite_projective_of_quasiregular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/Quasiregular.lean, line 827. References: EGA IV (16.9.4), “(ii)”; EGA IV (19.1.3), “special case”.

Stacks 08RK. If I \subseteq R is a quasi-regular ideal, then I/I^2 is a finite projective R/I-module.

theorem cotangent_finite_projective_of_quasiregular
    {R : Type*} [CommRing R] (I : Ideal R) (hI : IsQuasiregularIdeal' I) :
    Module.Finite (R ⧸ I) I.Cotangent ∧ Module.Projective (R ⧸ I) I.Cotangent
Tag 068N, a lemma

Tag 068N in the Stacks Project.

Koszul.regular_ideals_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/Descent.lean, line 830. References: SGA 6 VII (1.5), “converse, affine case”.

Stacks 068N. Koszul-regular, H₁-regular, and quasi-regular ideals descend along a faithfully flat homomorphism of commutative rings.

public theorem regular_ideals_of_faithfullyFlat
    {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B) (hf : f.FaithfullyFlat)
    (I : Ideal A) :
    (Ideal.IsKoszulRegular (I.map f) → Ideal.IsKoszulRegular I) ∧
      (Ideal.IsH1Regular (I.map f) → Ideal.IsH1Regular I) ∧
      (Quasiregular.IsQuasiregularIdeal' (I.map f) →
        Quasiregular.IsQuasiregularIdeal' I)
Tag 07CX, a lemma

Tag 07CX in the Stacks Project.

Ideal.inf_sq_eq_mul_of_quotient_isH1RegularIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/Ideal.lean, line 223.

If I ⊆ J and J / I is an H₁-regular ideal of A / I, then I ∩ J² = I J.

public theorem inf_sq_eq_mul_of_quotient_isH1RegularIdeal
    {A : Type*} [CommRing A] (I J : Ideal A) (hIJ : I ≤ J)
    (hreg : IsH1Regular (Ideal.map (Ideal.Quotient.mk I) J)) :
    I ⊓ J ^ 2 = I * J
Sources
LeanIdeal.IsRegular · Ideal.IsKoszulRegular · Ideal.IsH1Regular · Quasiregular.IsQuasiregularIdeal' · Quasiregular.isQuasiregularIdeal_fg · Quasiregular.cotangent_finite_projective_of_quasiregular · Koszul.regular_ideals_of_faithfullyFlat · Ideal.inf_sq_eq_mul_of_quotient_isH1RegularIdeal

Section15.34 Local complete intersection maps#

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

Tag 07CZ, a lemma

Tag 07CZ in the Stacks Project.

RingHom.isKoszulRegularIdeal_ker_of_surjective_mvPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/RingMap/Defs.lean, line 688.

The kernel of every finite polynomial presentation is a Koszul-regular ideal if the kernel of one such presentation is Koszul-regular.

public theorem isKoszulRegularIdeal_ker_of_surjective_mvPolynomial
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    {ι : Type w} [_root_.Finite ι] {κ : Type x} [_root_.Finite κ]
    (α : MvPolynomial ι A →ₐ[A] B) (hα : Function.Surjective α)
    (hI : Ideal.IsKoszulRegular (RingHom.ker α.toRingHom))
    (β : MvPolynomial κ A →ₐ[A] B) (hβ : Function.Surjective β) :
    Ideal.IsKoszulRegular (RingHom.ker β.toRingHom)
Tag 07D0, a definition

Tag 07D0 in the Stacks Project.

RingHom.IsLocalCompleteIntersection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/RingMap/Defs.lean, line 94.

A ring homomorphism is a local complete intersection if it is of finite type and some finite polynomial presentation has Koszul-regular kernel.

public def IsLocalCompleteIntersection {A : Type u} {B : Type v}
    [CommRing A] [CommRing B] (f : A →+* B) : Prop
Tag 07D1, a lemma

Tag 07D1 in the Stacks Project.

RingHom.isLocalCompleteIntersection_of_localization_away, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/RingMap/Criteria.lean, line 692.

Stacks 07D1. If finitely many elements g j generate the unit ideal of S and every composite from R to the localization S_{g j} is a local complete intersection, then the original ring homomorphism R → S is a local complete intersection.

public theorem isLocalCompleteIntersection_of_localization_away
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S)
    {m : ℕ} (g : Fin m → S) (hspan : Ideal.span (Set.range g) = ⊤)
    (hlocal : ∀ j, RingHom.IsLocalCompleteIntersection
      ((algebraMap S (Localization.Away (g j))).comp f)) :
    RingHom.IsLocalCompleteIntersection f
Tag 07D2, a lemma

Tag 07D2 in the Stacks Project.

RingHom.isKoszulRegular_relation_of_isRelativeGlobalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/RingMap/Criteria.lean, line 1298.

The relations in a polynomial presentation of a relative global complete intersection form a Koszul-regular sequence in the polynomial ring.

public theorem isKoszulRegular_relation_of_isRelativeGlobalCompleteIntersection
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    {ι : Type w} [_root_.Finite ι] {c : ℕ} (P : Algebra.Presentation R S ι (Fin c))
    (hP : P.IsRelativeGlobalCompleteIntersection) :
    Koszul.IsKoszulRegular P.relation
Tag 07D3, a lemma

Tag 07D3 in the Stacks Project.

RingHom.syntomic_iff_flat_and_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/RingMap/Criteria.lean, line 1693.

Stacks 07D3. A ring homomorphism is syntomic if and only if it is flat and a local complete intersection.

public theorem syntomic_iff_flat_and_isLocalCompleteIntersection
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) :
    letI := f.toAlgebra
    Algebra.Syntomic R S ↔ f.Flat ∧ RingHom.IsLocalCompleteIntersection f
Tag 07D4, a lemma

Tag 07D4 in the Stacks Project.

RingHom.cotangentMap_toComp_injective_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/RingMap/JacobiZariski.lean, line 249.

Let A → B → C be ring maps, let α : A[x_s] → B and β : B[y₁, ..., yₘ] → C be presentations, and write K for the kernel of the induced presentation β.comp α : A[x_s, y_t] → C. If B → C is a local complete intersection, then the canonical map C ⊗_B (I / I²) → K / K² is injective. Together with the canonical exact conormal/differential diagram and the Jacobi--Zariski exactness lemmas, this gives the exact sequence 0 → H₁(NL\_\{B/A} ⊗\_B C) → H₁(L\_\{C/A}) → H₁(L\_\{C/B}) → C ⊗\_B Ω[B⁄A] → Ω[C⁄A] → Ω[C⁄B] → 0.

public theorem cotangentMap_toComp_injective_of_isLocalCompleteIntersection
    {A : Type u₁} {B : Type u₂} [CommRing A] [CommRing B] [Algebra A B]
    {C : Type u₃} [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTower A B C]
    {S : Type w} {m : ℕ} (α : Generators A B S) (β : Generators B C (Fin m))
    (h : RingHom.IsLocalCompleteIntersection (algebraMap B C)) :
    Function.Injective
      ((Extension.Cotangent.map (β.toComp α).toExtensionHom).liftBaseChange C)
Tag 07D5, a lemma

Tag 07D5 in the Stacks Project.

RingHom.cotangentMap_toComp_injective_of_isFilteredColimit_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/RingMap/JacobiZariski.lean, line 792.

Let A → B → C be ring maps and suppose that B → C is exhibited as a filtered colimit of local complete intersection homomorphisms, with eB, eC, and hcomm identifying the directed system's colimit map with B → C. For presentations α : A[x_s] → B and β : B[y_t] → C, the canonical map C ⊗_B (I / I²) → K / K² from the conormal module of α to that of the induced presentation β.comp α is injective.

public theorem cotangentMap_toComp_injective_of_isFilteredColimit_isLocalCompleteIntersection
    {A : Type u₁} {B : Type u₂} [CommRing A] [CommRing B] [Algebra A B]
    {C : Type u₃} [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTower A B C]
    {S : Type w} {T : Type w'} (α : Generators A B S) (β : Generators B C T)
    {J : Type u₄} [Preorder J] [IsDirectedOrder J] [Nonempty J]
    (sys : RingMapSystemUnbundled.{u₅} J)
    (eB : sys.Rinf ≃+* B) (eC : sys.Sinf ≃+* C)
    (hcomm : eC.toRingHom.comp sys.gInf = (algebraMap B C).comp eB.toRingHom)
    (h : ∀ i : J, RingHom.IsLocalCompleteIntersection (sys.g i)) :
    Function.Injective
      ((Extension.Cotangent.map (β.toComp α).toExtensionHom).liftBaseChange C)
Tag 0D08, a lemma

Tag 0D08 in the Stacks Project.

Algebra.naiveCotangentComplex_quasiIso_henselization_and_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Henselization.lean, line 602.

Let A → B be a local homomorphism of local rings. For the induced local map between henselizations and the induced local map between strict henselizations associated to a compatible map of residue fields, the canonical maps NL_{B/A} ⊗_B Bʰ ⟶ NL_{Bʰ/Aʰ} and NL_{B/A} ⊗_B Bˢʰ ⟶ NL_{Bˢʰ/Aˢʰ} induce isomorphisms on all homology groups.

public theorem
    naiveCotangentComplex_quasiIso_henselization_and_strictHenselization
    (A Ah Ash : Type u) (B Bh Bsh : Type v) (kAsep : Type u) (kBsep : Type v)
    [CommRing A] [IsLocalRing A] [CommRing B] [IsLocalRing B]
    [Algebra A B] [IsLocalHom (algebraMap A B)]
    [CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
    [IsLocalRing.IsHenselization A (IsLocalRing.ResidueField A) Ah]
    [CommRing Bh] [IsLocalRing Bh] [Algebra B Bh]
    [IsLocalRing.IsHenselization B (IsLocalRing.ResidueField B) Bh]
    [Algebra A Bh] [IsScalarTower A B Bh] [Algebra Ah Bh] [IsScalarTower A Ah Bh]
    [IsLocalHom (algebraMap Ah Bh)]
    [Field kAsep] [Algebra (IsLocalRing.ResidueField A) kAsep]
    [IsSepClosure (IsLocalRing.ResidueField A) kAsep]
    [CommRing Ash] [IsLocalRing Ash] [Algebra A Ash]
    [IsLocalRing.IsHenselization A kAsep Ash]
    [Field kBsep] [Algebra (IsLocalRing.ResidueField B) kBsep]
    [IsSepClosure (IsLocalRing.ResidueField B) kBsep]
    [CommRing Bsh] [IsLocalRing Bsh] [Algebra B Bsh]
    [IsLocalRing.IsHenselization B kBsep Bsh]
    [Algebra A Bsh] [IsScalarTower A B Bsh] [Algebra Ash Bsh] [IsScalarTower A Ash Bsh]
    [IsLocalHom (algebraMap Ash Bsh)]
    (phi : IsLocalRing.ResidueField Ash →+* IsLocalRing.ResidueField Bsh)
    (_hphi : phi.comp ((IsLocalRing.residue Ash).comp (algebraMap A Ash)) =
      (IsLocalRing.residue Bsh).comp (algebraMap A Bsh))
    (_hinduced : (IsLocalRing.residue Bsh).comp (algebraMap Ash Bsh) =
      phi.comp (IsLocalRing.residue Ash)) :
    QuasiIso (Algebra.naiveCotangentComplexBaseChangeComparison A Ah B Bh) ∧
      QuasiIso (Algebra.naiveCotangentComplexBaseChangeComparison A Ash B Bsh)

Algebra.naiveCotangentComplex_quasiIso_henselizationPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Henselization.lean, line 672. The attribute's comment: “the henselization-of-pairs case, which Stacks 0DZC's proof cites 0D08 for although 0D08's own statement is about the local and strict henselizations of a local ring: the input to the source's proof is that both vertical maps are filtered colimits of étale maps, which ind_henselization supplies for the henselization of a pair”.

Stacks 0D08 for the henselization of a pair. Let P be an algebra over a commutative ring k, let J ⊆ P be an ideal and let (Pʰ, Jʰ) be the henselization of the pair (P, J), described by the henselian-pair condition on Pʰ together with its universal property. Then the canonical comparison map

NL_{P/k} ⊗_P Pʰ ⟶ NL_{Pʰ/k}

induces isomorphisms on all homology groups.

The source states Stacks 0D08 for the henselization and the strict henselization of a local ring, which is naiveCotangentComplex_quasiIso_henselization_and_strictHenselization. Its proof uses of those two only that they are filtered colimits of étale algebras over their bases, and the henselization of a pair is such a colimit by ind_henselization; this is the instance Stacks 0DZC's proof appeals to 0D08 for.

public theorem naiveCotangentComplex_quasiIso_henselizationPair
    (k : Type u) [CommRing k] (P : Type v) [CommRing P] [Algebra k P] (J : Ideal P)
    (Ph : Type v) [CommRing Ph] [Algebra P Ph] [Algebra k Ph] [IsScalarTower k P Ph]
    (hhens : HenselianPair Ph (J.map (algebraMap P Ph)))
    (huniv : ∀ (C : Type v) (_ : CommRing C) (JC : Ideal C), HenselianPair C JC →
      ∀ f : P →+* C, J ≤ JC.comap f →
        ∃! g : Ph →+* C, g.comp (algebraMap P Ph) = f ∧
          J.map (algebraMap P Ph) ≤ JC.comap g) :
    QuasiIso (naiveCotangentComplexBaseChangeComparison k k P Ph)
Sources
LeanRingHom.isKoszulRegularIdeal_ker_of_surjective_mvPolynomial · RingHom.IsLocalCompleteIntersection · RingHom.isLocalCompleteIntersection_of_localization_away · RingHom.isKoszulRegular_relation_of_isRelativeGlobalCompleteIntersection · RingHom.syntomic_iff_flat_and_isLocalCompleteIntersection · RingHom.cotangentMap_toComp_injective_of_isLocalCompleteIntersection · RingHom.cotangentMap_toComp_injective_of_isFilteredColimit_isLocalCompleteIntersection · Algebra.naiveCotangentComplex_quasiIso_henselization_and_strictHenselization

Section15.35 Cartier's equality and geometric regularity#

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

Tag 07E1, a lemma

Tag 07E1 in the Stacks Project.

trdeg_eq_finrank_kaehlerDifferential_sub_finrank_h1Cotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/KaehlerDifferential/CartierEquality.lean, line 337. References: EGA 0 (21.7.1); EGA 0 (21.7.2), “special case”.

Cartier's equality. For a finitely generated extension of fields K/k, the module of Kähler differentials and the first homology of the naive cotangent complex are finite-dimensional, and their dimensions differ by the transcendence degree.

public theorem trdeg_eq_finrank_kaehlerDifferential_sub_finrank_h1Cotangent
    (k : Type u) (K : Type v) [Field k] [Field K] [Algebra k K]
    [Algebra.EssFiniteType k K] :
    FiniteDimensional K Ω[K⁄k] ∧
      FiniteDimensional K (Algebra.H1Cotangent k K) ∧
        (Cardinal.toNat (Algebra.trdeg k K) : ℤ) =
          (Module.finrank K Ω[K⁄k] : ℤ) - Module.finrank K (Algebra.H1Cotangent k K)
Tag 07E2, a lemma

Tag 07E2 in the Stacks Project.

jacobiZariski_exact_of_fieldExtensions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/KaehlerDifferential/CartierEquality.lean, line 476.

Let M/L/K be a tower of field extensions. Then the canonical Jacobi--Zariski sequence

0 → H₁(L_{L/K}) ⊗[L] M → H₁(L_{M/K}) → H₁(L_{M/L}) → M ⊗[L] Ω[L⁄K] → Ω[M⁄K] → Ω[M⁄L] → 0

is exact.

public theorem jacobiZariski_exact_of_fieldExtensions
    (K : Type u₁) (L : Type u₂) (M : Type u₃)
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra L M] [Algebra K M] [IsScalarTower K L M] :
    let i := (Algebra.H1Cotangent.map K K L M).liftBaseChange M
    let p := Algebra.H1Cotangent.map K L M M
    let δ := Algebra.H1Cotangent.δ K L M
    let d := KaehlerDifferential.mapBaseChange K L M
    let q := KaehlerDifferential.map K L M M
    Function.Injective i ∧
      Function.Exact i p ∧
      Function.Exact p δ ∧
      Function.Exact δ d ∧
      Function.Exact d q ∧
      Function.Surjective q
Tag 07E3, a lemma

Tag 07E3 in the Stacks Project.

finrank_ker_sub_finrank_coker_kaehlerDifferential_map_sub_h1Cotangent_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/KaehlerDifferential/CartierEquality.lean, line 604. References: EGA 0 (21.7.1).

Given a commutative square of fields 

K  → K'
↑    ↑
k  → k'
whose horizontal extensions are finitely generated, the kernels and cokernels of the canonical maps on Kähler differentials and first cotangent homology are finite-dimensional. The alternating sum of their dimensions is the difference of the transcendence degrees of the horizontal extensions.

public theorem finrank_ker_sub_finrank_coker_kaehlerDifferential_map_sub_h1Cotangent_map
    (k : Type u₁) (K : Type u₂) (k' : Type u₃) (K' : Type u₄)
    [Field k] [Field K] [Field k'] [Field K']
    [Algebra k K] [Algebra k k'] [Algebra K K'] [Algebra k' K'] [Algebra k K']
    [IsScalarTower k K K'] [IsScalarTower k k' K']
    [Algebra.FiniteType k k'] [Algebra.FiniteType K K'] :
    let α := (KaehlerDifferential.map k k' K K').liftBaseChange K'
    let β := (Algebra.H1Cotangent.map k k' K K').liftBaseChange K'
    FiniteDimensional K' (LinearMap.ker α) ∧
      FiniteDimensional K' (Ω[K'⁄k'] ⧸ LinearMap.range α) ∧
      FiniteDimensional K' (LinearMap.ker β) ∧
      FiniteDimensional K' (Algebra.H1Cotangent k' K' ⧸ LinearMap.range β) ∧
      (Module.finrank K' (LinearMap.ker α) : ℤ) -
          Module.finrank K' (Ω[K'⁄k'] ⧸ LinearMap.range α) -
          Module.finrank K' (LinearMap.ker β) +
          Module.finrank K' (Algebra.H1Cotangent k' K' ⧸ LinearMap.range β) =
      (Cardinal.toNat (Algebra.trdeg k k') : ℤ) -
          Cardinal.toNat (Algebra.trdeg K K')
Sources
Leantrdeg_eq_finrank_kaehlerDifferential_sub_finrank_h1Cotangent · jacobiZariski_exact_of_fieldExtensions · finrank_ker_sub_finrank_coker_kaehlerDifferential_map_sub_h1Cotangent_map

Section15.36 Geometric regularity#

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

Tag 07E5, a proposition

Tag 07E5 in the Stacks Project.

geometricallyRegular_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/PurelyInseparableCriterion.lean, line 886. References: EGA 0 (22.5.8), “b) ⇔ b'), char p”.

Let A be a Noetherian local algebra over a field k of positive characteristic p. The following are equivalent:

  1. A is geometrically regular over k;
  2. A ⊗[k] k' is regular for every finite intermediate field k' of k¹ᵖ;
  3. A is regular and the canonical map from H¹(L_(K/k)) to 𝔪/𝔪² is injective;
  4. A is regular and the canonical map from Ω[k/ZMod p] ⊗[k] K to Ω[A/ZMod p] ⊗[A] K is injective,

where K is the residue field of A.

public theorem geometricallyRegular_tfae
    (p : ℕ) [Fact p.Prime] (k : Type u) (A : Type v)
    [Field k] [CharP k p] [CommRing A] [Algebra k A]
    [IsNoetherianRing A] [IsLocalRing A] :
    letI : Algebra (ZMod p) k := ZMod.algebra k p
    letI : Algebra (ZMod p) A :=
      ((algebraMap k A).comp (algebraMap (ZMod p) k)).toAlgebra
    letI : IsScalarTower (ZMod p) k A := IsScalarTower.of_algebraMap_eq' rfl
    letI : Algebra k (PerfectClosure k p) := (PerfectClosure.of k p).toAlgebra
    List.TFAE [
      Algebra.IsGeometricallyRegular k A,
      (∀ (k' : IntermediateField k (PerfectClosure k p)),
        FiniteDimensional k k' →
        (∀ x : k', (x : PerfectClosure k p) ^ p ∈
          Set.range (algebraMap k (PerfectClosure k p))) →
        IsRegularRing (A ⊗[k] k')),
      IsRegularLocalRing A ∧
        Function.Injective
          (Algebra.H1Cotangent.map k A (IsLocalRing.ResidueField A)
            (IsLocalRing.ResidueField A)),
      IsRegularLocalRing A ∧
        Function.Injective
          ((KaehlerDifferential.mapBaseChange (ZMod p) k A).baseChange
            (IsLocalRing.ResidueField A))]
Tag 07E6, a lemma

Tag 07E6 in the Stacks Project.

flat_localization_and_regular_quotient_of_basis_kaehlerDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/PurelyInseparableCriterion.lean, line 1206.

Let A be a Noetherian local algebra over a field k of positive characteristic, and assume that A is geometrically regular over k. Let F be a finitely generated intermediate field of the residue field of A. If yᵢ ∈ F have differentials forming a basis of Ω[F⁄k], and a map k[X₁, …, Xₘ] → A lifts the yᵢ, then A is flat over its localization at the inverse image of the maximal ideal, and the quotient of A by the extended prime is regular local.

public theorem flat_localization_and_regular_quotient_of_basis_kaehlerDifferential
    (p : ℕ) [Fact p.Prime] (k : Type u) (A : Type v)
    [Field k] [CharP k p] [CommRing A] [Algebra k A] [IsNoetherianRing A] [IsLocalRing A]
    [Algebra.IsGeometricallyRegular k A] (m : ℕ)
    (F : IntermediateField k (ResidueField A)) [Algebra.EssFiniteType k F]
    (y : Fin m → F) (b : Module.Basis (Fin m) F Ω[F⁄k])
    (hb : ∀ i, b i = KaehlerDifferential.D k F (y i))
    (φ : MvPolynomial (Fin m) k →ₐ[k] A)
    (hφ : ∀ i, residue A (φ (MvPolynomial.X i)) = algebraMap F (ResidueField A) (y i)) :
    letI : Algebra (MvPolynomial (Fin m) k) A := φ.toRingHom.toAlgebra
    ∀ (A₀ : Type w) [CommRing A₀] [Algebra (MvPolynomial (Fin m) k) A₀]
      [IsLocalization.AtPrime A₀ ((maximalIdeal A).comap φ)] [Algebra A₀ A]
      [IsScalarTower (MvPolynomial (Fin m) k) A₀ A],
      Module.Flat A₀ A ∧
        IsRegularLocalRing (A ⧸ Ideal.map φ ((maximalIdeal A).comap φ))
Sources
LeangeometricallyRegular_tfae · flat_localization_and_regular_quotient_of_basis_kaehlerDifferential

Section15.37 Topological rings and modules#

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

Tag 07E8, a definition

Tag 07E8 in the Stacks Project.

TopologicalRing.IsIdealOfDefinition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdmissibleRings.lean, line 91. The attribute's comment: “(4)”.

An ideal of definition is open and its powers are cofinal among the neighborhoods of zero.

public def IsIdealOfDefinition {R : Type u} [CommRing R] [TopologicalSpace R]
    (I : Ideal R) : Prop

TopologicalRing.IsPreAdmissible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdmissibleRings.lean, line 98. The attribute's comment: “(5)”.

A topological ring is pre-admissible if it has an ideal of definition.

public def IsPreAdmissible (R : Type u) [CommRing R] [TopologicalSpace R] : Prop

TopologicalRing.IsAdmissible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdmissibleRings.lean, line 107. The attribute's comment: “(6)”. References: EGA 0 (7.1.2), “admissible”.

A topological ring is admissible if it is pre-admissible and complete.

public def IsAdmissible (R : Type u) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] : Prop

TopologicalRing.IsPreAdic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdmissibleRings.lean, line 114. The attribute's comment: “(7)”.

A topological ring is pre-adic if an ideal of definition defines its topology through its powers.

public def IsPreAdic (R : Type u) [CommRing R] [TopologicalSpace R] : Prop

TopologicalRing.IsAdic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdmissibleRings.lean, line 119. The attribute's comment: “(8)”. References: EGA 0 (7.1.9), “preadic (J^n a basis)”.

A topological ring is adic if it is pre-adic and complete.

public def IsAdic (R : Type u) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] : Prop

TopologicalRing.preAdic_and_adic_iff_admissible_and_open_powers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdmissibleRings.lean, line 137. The attribute's comment: “equivalent characterization”.

A (pre-)adic topological ring is equivalently a (pre-)admissible topological ring possessing an ideal of definition all of whose positive powers are open.

public theorem preAdic_and_adic_iff_admissible_and_open_powers
    {R : Type u} [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [IsLinearTopology R R] :
    (IsPreAdic R ↔ IsPreAdmissible R ∧
      ∃ I : Ideal R, IsIdealOfDefinition I ∧
        ∀ n : ℕ, 1 ≤ n → IsOpen ((I ^ n : Ideal R) : Set R)) ∧
    (IsAdic R ↔ IsAdmissible R ∧
      ∃ I : Ideal R, IsIdealOfDefinition I ∧
        ∀ n : ℕ, 1 ≤ n → IsOpen ((I ^ n : Ideal R) : Set R))

Declarations registered for the tag:

Tag 07E9, a lemma

Tag 07E9 in the Stacks Project.

RingHom.continuous_adic_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Continuous.lean, line 29.

A ring homomorphism φ : R → S between commutative rings is continuous with respect to the I-adic topology on R and the J-adic topology on S if and only if there exists n ≥ 1 with φ(I ^ n) ⊆ J.

theorem RingHom.continuous_adic_iff {R S : Type*} [CommRing R] [CommRing S]
    (φ : R →+* S) (I : Ideal R) (J : Ideal S) :
    @Continuous R S I.adicTopology J.adicTopology φ ↔
      ∃ n : ℕ, 1 ≤ n ∧ ∀ x ∈ I ^ n, φ x ∈ J
Tag 0CQU, a lemma

Tag 0CQU in the Stacks Project.

dense_iInter_of_isOpen_of_complete_linearTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/BaireLinearTopology.lean, line 77.

The Baire category theorem for complete linearly topologized abelian groups with a countable fundamental system of neighbourhoods of zero.

public theorem dense_iInter_of_isOpen_of_complete_linearTopology
    {M : Type*} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M]
    [T2Space M] [IsLinearTopology ℤ M]
    (hcomplete : @CompleteSpace M (IsTopologicalAddGroup.rightUniformSpace M))
    (hcount : (nhds (0 : M)).IsCountablyGenerated)
    {U : ℕ → Set M} (hUopen : ∀ n, IsOpen (U n)) (hUdense : ∀ n, Dense (U n)) :
    Dense (⋂ n, U n)
Tag 0CQV, a lemma

Tag 0CQV in the Stacks Project.

exists_isOpen_of_iUnion_eq_univ_of_complete_linearTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/BaireLinearTopology.lean, line 112.

A countable closed-subgroup cover of a complete linearly topologized abelian group contains an open subgroup.

public theorem exists_isOpen_of_iUnion_eq_univ_of_complete_linearTopology
    {M : Type*} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M]
    [T2Space M] [IsLinearTopology ℤ M]
    (hcomplete : @CompleteSpace M (IsTopologicalAddGroup.rightUniformSpace M))
    (hcount : (nhds (0 : M)).IsCountablyGenerated)
    (N : ℕ → AddSubgroup M) (hNclosed : ∀ n, IsClosed (N n : Set M))
    (hNcover : (⋃ n, (N n : Set M)) = Set.univ) :
    ∃ n, IsOpen (N n : Set M)
Tag 0CQW, a lemma

Tag 0CQW in the Stacks Project.

open_mapping_lemma, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/OpenMapping.lean, line 288.

Let u : N → M be a continuous homomorphism of topological abelian groups. Assume that M is separated, and that N is complete (which, by IsGroupComplete, includes separatedness of N), linearly topologized, and has a countable fundamental system of neighbourhoods of 0. Then exactly one of the following two statements holds:

  1. u is open; or
  2. there exists an open subgroup N' ⊆ N such that the image u(N') is nowhere dense in M.
theorem open_mapping_lemma
    {N : Type*} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N]
    {M : Type*} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M]
    [T2Space M]
    (u : N →+ M) (hu : Continuous u)
    (hNcomplete : IsGroupComplete N)
    (hNlin : IsLinearlyTopologized N)
    (hNcount : HasCountableFundamentalSystem N) :
    Xor (IsOpenMap u)
      (∃ N' : AddSubgroup N, IsOpen (N' : Set N) ∧ IsNowhereDense (u '' (N' : Set N)))
Sources
LeanTopologicalRing.IsIdealOfDefinition · TopologicalRing.IsPreAdmissible · TopologicalRing.IsAdmissible · TopologicalRing.IsPreAdic · TopologicalRing.IsAdic · TopologicalRing.preAdic_and_adic_iff_admissible_and_open_powers · IsTopologicalRing · TopModuleCat

Section15.38 Formally smooth maps of topological rings#

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

Tag 07EB, a definition

Tag 07EB in the Stacks Project.

IsFormallySmooth, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/TopologicalRings/AdicCriterion.lean, line 96. References: EGA 0 (19.3.1), “linearly topologized”.

A homomorphism between linearly topologized rings is formally smooth if it is continuous and every compatible square-zero lifting problem with a discrete target ring has a continuous lift.

def IsFormallySmooth.{u, v, w} {R : Type v} {S : Type w}
    [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [IsLinearTopology R R]
    [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S]
    (φ : R →+* S) : Prop
Tag 07EC, a lemma

Tag 07EC in the Stacks Project.

RingHom.FormallySmoothTop.of_formallySmooth_of_isAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Algebraic.lean, line 25. References: EGA 0 (19.3.8), “discrete topologies”.

Algebraic formal smoothness implies topological formal smoothness for an adic target.

theorem of_formallySmooth_of_isAdic.{u, v, w}
    {R : Type v} {S : Type w} [CommRing R] [CommRing S]
    [TopologicalSpace R] [IsTopologicalRing R]
    [TopologicalSpace S] [IsTopologicalRing S]
    (phi : R →+* S) (n : Ideal S) (hn : IsAdic n)
    (hphi : @Algebra.FormallySmooth R S _ _ phi.toAlgebra) :
    RingHom.FormallySmoothTop.{u, v, w} phi

isFormallySmooth_of_formallySmooth_and_isAdic_and_iff_discrete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/TopologicalRings/AdicCriterion.lean, line 181.

Algebraic formal smoothness implies formal smoothness for any continuous map from a linearly topologized ring to a pre-adic ring. Moreover, for ideals m ⊆ R and n ⊆ S, a continuous map for the adic topologies is formally smooth if and only if it is formally smooth with the discrete topology on R.

public theorem isFormallySmooth_of_formallySmooth_and_isAdic_and_iff_discrete.{u, v, w}
    {R : Type v} {S : Type w} [CommRing R] [CommRing S] (φ : R →+* S) :
    (∀ (tR : TopologicalSpace R) (tS : TopologicalSpace S),
      letI := tR
      letI := tS
      ∀ [IsTopologicalRing R] [IsLinearTopology R R]
        [IsTopologicalRing S] [IsLinearTopology S S],
        (∃ n : Ideal S, IsAdic n) →
          @Algebra.FormallySmooth R S _ _ φ.toAlgebra → Continuous φ →
            IsFormallySmooth.{u} φ) ∧
      ∀ (m : Ideal R) (n : Ideal S),
        (letI := m.adicTopology
         letI : IsTopologicalRing R := m.ringFilterBasis.isTopologicalRing
         letI := n.adicTopology
         letI : IsTopologicalRing S := n.ringFilterBasis.isTopologicalRing
         @Continuous R S m.adicTopology n.adicTopology φ) →
          ((letI := m.adicTopology
            letI : IsTopologicalRing R := m.ringFilterBasis.isTopologicalRing
            letI : IsLinearTopology R R := m.isLinearTopology
            letI := n.adicTopology
            letI : IsTopologicalRing S := n.ringFilterBasis.isTopologicalRing
            letI : IsLinearTopology S S := n.isLinearTopology
            IsFormallySmooth.{u} φ) ↔
           (letI : TopologicalSpace R := ⊥
            letI : DiscreteTopology R := ⟨rfl⟩
            letI := n.adicTopology
            letI : IsTopologicalRing S := n.ringFilterBasis.isTopologicalRing
            letI : IsLinearTopology S S := n.isLinearTopology
            IsFormallySmooth.{u} φ))
Tag 07NI, a definition

Tag 07NI in the Stacks Project.

RingHom.FormallySmoothNAdic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Topological.lean, line 144.

φ : R →+* S is formally smooth for the n-adic topology, where n is an ideal of S: for every square-zero ideal J of a ring A, every ring map f : R → A, and every ring map ψ : S → A ⧸ J making the square commute and with ψ killing some power of n (some k ≥ 1 with n ^ k ≤ ker ψ), there exists a lift g : S → A with (Ideal.Quotient.mk J) ∘ g = ψ and g ∘ φ = f.

def FormallySmoothNAdic {R : Type v} {S : Type w} [CommRing R] [CommRing S]
    (φ : R →+* S) (n : Ideal S) : Prop
Tag 07ED, a lemma

Tag 07ED in the Stacks Project.

isFormallySmooth_iff_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/TopologicalRings/Completion.lean, line 465. References: EGA 0 (19.3.6), “adic top., f.g. ideals”; EGA 0 (19.9.4), “a) <=> b) <=> c)”; EGA IV (17.5.3), “d) ⇔ d')”.

Formal smoothness of a continuous homomorphism of adic rings is unchanged by completing the target, or by completing both source and target.

public theorem isFormallySmooth_iff_adicCompletion.{u, v, w}
    {R : Type v} {S : Type w} [CommRing R] [CommRing S]
    (m : Ideal R) (n : Ideal S) (hm : m.FG) (hn : n.FG) (f : R →+* S)
    (hf : @Continuous R S m.adicTopology n.adicTopology f) :
    letI : WithIdeal R := ⟨m⟩
    letI : WithIdeal S := ⟨n⟩
    let mhat : Ideal (Completion R) := m.map Completion.coeRingHom
    let nhat : Ideal (Completion S) := n.map Completion.coeRingHom
    let fhat : Completion R →+* Completion S := Completion.mapRingHom f hf
    let toShat : R →+* Completion S := Completion.coeRingHom.comp f
    letI : TopologicalSpace (Completion R) := mhat.adicTopology
    letI : IsTopologicalRing (Completion R) := mhat.nonarchimedean.toIsTopologicalRing
    letI : IsLinearTopology (Completion R) (Completion R) := mhat.isLinearTopology
    letI : TopologicalSpace (Completion S) := nhat.adicTopology
    letI : IsTopologicalRing (Completion S) := nhat.nonarchimedean.toIsTopologicalRing
    letI : IsLinearTopology (Completion S) (Completion S) := nhat.isLinearTopology
    (IsFormallySmooth.{u} f ↔ IsFormallySmooth.{u} toShat) ∧
      (IsFormallySmooth.{u} toShat ↔ IsFormallySmooth.{u} fhat)
Tag 07NJ, a lemma

Tag 07NJ in the Stacks Project.

RingHom.FormallySmoothTop.exists_continuous_lift_of_isAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/AdicLifting.lean, line 508.

A formally smooth homomorphism lifts continuously through a closed quotient of an adic complete ring, provided a positive power of the quotient ideal lies in an ideal of definition.

theorem exists_continuous_lift_of_isAdic
    {R : Type u} {S : Type v} {A : Type w}
    [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [IsLinearTopology R R]
    [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S]
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    (f : R →+* S) (n : Ideal S) (hn : IsAdic n)
    (hf : RingHom.FormallySmoothTop.{w} f)
    (I : Ideal A) (hI : IsAdic I) [IsAdicComplete I A]
    (J : Ideal A) (hJ : IsClosed (J : Set A))
    (t : ℕ) (ht : 1 ≤ t) (hJI : J ^ t ≤ I)
    (g : R →+* A) (hg : Continuous g)
    (ψ : S →+* A ⧸ J) (hψ : Continuous ψ)
    (hcomm : ψ.comp f = (Ideal.Quotient.mk J).comp g) :
    ∃ φ : S →+* A, Continuous φ ∧ φ.comp f = g ∧
      (Ideal.Quotient.mk J).comp φ = ψ

exists_continuous_lift_of_isFormallySmooth_of_isAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/TopologicalRings/AdicBaseChange.lean, line 129.

A formally smooth homomorphism for the n-adic topology lifts continuously through a closed quotient of an adic ring when a positive power of the quotient ideal lies in an ideal of definition.

public theorem exists_continuous_lift_of_isFormallySmooth_of_isAdic
    {R : Type u} {S : Type v} {A : Type w}
    [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [IsLinearTopology R R]
    [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S]
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    (f : R →+* S) (n : Ideal S) (hn : IsAdic n)
    (hf : IsFormallySmooth.{w} f)
    (I : Ideal A) (hI : IsAdic I) [IsAdicComplete I A]
    (J : Ideal A) (hJ : IsClosed (J : Set A))
    (t : ℕ) (ht : 1 ≤ t) (hJI : J ^ t ≤ I)
    (g : R →+* A) (hg : Continuous g)
    (ψ : S →+* A ⧸ J) (hψ : Continuous ψ)
    (hcomm : ψ.comp f = (Ideal.Quotient.mk J).comp g) :
    ∃ φ : S →+* A, Continuous φ ∧ φ.comp f = g ∧
      (Ideal.Quotient.mk J).comp φ = ψ
Tag 07EE, a lemma

Tag 07EE in the Stacks Project.

RingHom.FormallySmoothNAdic.mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Topological.lean, line 158. References: EGA 0 (19.3.8), “adic topologies on S”.

Stacks Tag 07EE, Lemma 15.38.6: if n ≤ n' are ideals of S and φ : R → S is formally smooth for the n-adic topology, then it is formally smooth for the n'-adic topology. Usable as h.mono hnn'.

theorem FormallySmoothNAdic.mono {R : Type v} {S : Type w} [CommRing R] [CommRing S]
    {φ : R →+* S} {n n' : Ideal S} (h : FormallySmoothNAdic.{u, v, w} φ n) (hnn' : n ≤ n') :
    FormallySmoothNAdic.{u, v, w} φ n'
Tag 07EF, a lemma

Tag 07EF in the Stacks Project.

RingHom.FormallySmoothTop.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Topological.lean, line 108.

Stacks Lemma 15.38.7 (Tag 07EF). A composition of formally smooth continuous ring homomorphisms of topological rings is formally smooth: if φ : R →+* S and ψ : S →+* T are formally smooth and ψ is continuous, then ψ.comp φ is formally smooth. Usable as hsφ.comp hsψ hψ. Continuity of ψ.comp φ is not part of the conclusion; it follows from Continuous.comp given that φ is continuous.

theorem FormallySmoothTop.comp {R : Type v} {S : Type w} {T : Type z}
    [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
    [CommRing T] [TopologicalSpace T] [IsTopologicalRing T] {φ : R →+* S} {ψ : S →+* T}
    (hsφ : FormallySmoothTop.{u, v, w} φ) (hsψ : FormallySmoothTop.{u, w, z} ψ)
    (hψ : Continuous ψ) : FormallySmoothTop.{u, v, z} (ψ.comp φ)
Tag 07EG, a lemma

Tag 07EG in the Stacks Project.

RingHom.formallySmoothTop_iff_formallySmoothNAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Adic.lean, line 69.

For a discrete source and an adic target, topological formal smoothness is equivalent to formal smoothness for the adic topology.

theorem formallySmoothTop_iff_formallySmoothNAdic.{u, v, w}
    {R : Type v} {S : Type w} [CommRing R] [CommRing S]
    [TopologicalSpace R] [IsTopologicalRing R] [DiscreteTopology R]
    [TopologicalSpace S] [IsTopologicalRing S]
    (phi : R →+* S) (n : Ideal S) (hn : IsAdic n) :
    FormallySmoothTop.{u, v, w} phi ↔ FormallySmoothNAdic.{u, v, w} phi n

RingHom.FormallySmoothNAdic.baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/BaseChange.lean, line 32. References: EGA 0 (19.3.5), “(iii)”; EGA 0 (19.9.3), “adic topology case”.

Formal smoothness for the n-adic topology is preserved by arbitrary base change from R to R'; on S ⊗[R] R', the adic ideal is the extension of n.

theorem baseChange.{u, v, w, z}
    {R : Type v} {S : Type w} {R' : Type z}
    [CommRing R] [CommRing S] [CommRing R'] [Algebra R S] [Algebra R R']
    (n : Ideal S) (h : RingHom.FormallySmoothNAdic.{u, v, w} (algebraMap R S) n) :
    RingHom.FormallySmoothNAdic.{u, z, max w z}
      (Algebra.TensorProduct.includeRight (R := R) (A := S) (B := R')).toRingHom
      (n.map (Algebra.TensorProduct.includeLeft (R := R) (S := R)
        (A := S) (B := R')).toRingHom)
Tag 07EH, a lemma

Tag 07EH in the Stacks Project.

isFormallySmooth_adic_of_split_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/TopologicalRings/AdicBaseChange.lean, line 375.

If R → R' admits an R-linear retraction and the base change R' → S ⊗[R] R' is formally smooth for the topology defined by the extension of n, then R → S is formally smooth for the n-adic topology.

public theorem isFormallySmooth_adic_of_split_baseChange.{u, v, w, z}
    {R : Type v} {S : Type w} {R' : Type z}
    [CommRing R] [CommRing S] [CommRing R'] [Algebra R S] [Algebra R R']
    (n : Ideal S)
    (hsplit : ∃ p : R' →ₗ[R] R,
      p.comp (Algebra.linearMap R R') = LinearMap.id)
    (hsmooth :
      letI : Algebra R' (S ⊗[R] R') :=
        Algebra.TensorProduct.rightAlgebra (R := R) (A := S) (B := R')
      let n' : Ideal (S ⊗[R] R') :=
        Ideal.map (Algebra.TensorProduct.includeLeft : S →ₐ[R] S ⊗[R] R') n
      letI : TopologicalSpace R' := ⊥
      letI : DiscreteTopology R' := ⟨rfl⟩
      letI : TopologicalSpace (S ⊗[R] R') := n'.adicTopology
      letI : IsTopologicalRing (S ⊗[R] R') := n'.ringFilterBasis.isTopologicalRing
      letI : IsLinearTopology (S ⊗[R] R') (S ⊗[R] R') := n'.isLinearTopology
      IsFormallySmooth.{max u z} (algebraMap R' (S ⊗[R] R'))) :
    letI : TopologicalSpace R := ⊥
    letI : DiscreteTopology R := ⟨rfl⟩
    letI : TopologicalSpace S := n.adicTopology
    letI : IsTopologicalRing S := n.ringFilterBasis.isTopologicalRing
    letI : IsLinearTopology S S := n.isLinearTopology
    IsFormallySmooth.{u} (algebraMap R S)
Sources
LeanIsFormallySmooth · RingHom.FormallySmoothTop.of_formallySmooth_of_isAdic · isFormallySmooth_of_formallySmooth_and_isAdic_and_iff_discrete · RingHom.FormallySmoothNAdic · isFormallySmooth_iff_adicCompletion · RingHom.FormallySmoothTop.exists_continuous_lift_of_isAdic · exists_continuous_lift_of_isFormallySmooth_of_isAdic · RingHom.FormallySmoothNAdic.mono

Section15.39 Formally smooth maps of local rings#

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

Tag 0DYG, a lemma

Tag 0DYG in the Stacks Project.

formallySmooth_adic_iff_lifts_local_squareZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/LocalRings/LiftingCriterion.lean, line 480. References: EGA 0 (22.1.4); SGA 1 III (2.2), “(iv ter)”; SGA 1 III (2.1), “(i) ⇔ (iv bis)”.

A local homomorphism of local rings is formally smooth for the adic topologies if and only if it lifts through all residually trivial square-zero quotients whose source has nilpotent maximal ideal. If the target is Noetherian, testing residually trivial small extensions suffices.

public theorem formallySmooth_adic_iff_lifts_local_squareZero
    {R : Type v} {S : Type w} [CommRing R] [IsLocalRing R]
    [CommRing S] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] :
    (FormallySmoothAdic.{u, v, w} φ ↔ LiftsLocalSquareZero.{u, v, w} φ) ∧
      (IsNoetherianRing S →
        (FormallySmoothAdic.{u, v, w} φ ↔ LiftsLocalSmallExtension.{u, v, w} φ))
Tag 07EI, a lemma

Tag 07EI in the Stacks Project.

isRegularLocalRing_of_isFormallySmooth_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/LocalRings/CoefficientFieldsAndRegularity.lean, line 199. References: EGA 0 (19.6.5), “A regular (k'=k)”; EGA 0 (22.5.8), “a) ⇒ A regular”.

A Noetherian local algebra over a field that is formally smooth for its maximal-ideal adic topology is a regular local ring.

public theorem isRegularLocalRing_of_isFormallySmooth_maximalIdeal.{v, w}
    {k : Type v} {A : Type w} [Field k] [CommRing A] [Algebra k A]
    [IsLocalRing A] [IsNoetherianRing A]
    (h : FormallySmoothDiscreteMaximalIdeal.{max v w, v, w} (algebraMap k A)) :
    IsRegularLocalRing A

RingHom.FormallySmoothTop.isRegularLocalRing_of_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/RegularLocal.lean, line 368. References: EGA 0 (19.6.5), “A regular (k'=k)”; EGA 0 (22.5.8), “a) ⇒ A regular”.

A Noetherian local algebra over a field is regular if its structure map is formally smooth for the maximal-ideal adic topology.

theorem isRegularLocalRing_of_maximalIdeal.{v, w}
    {k : Type v} {A : Type w} [Field k] [CommRing A] [Algebra k A]
    [IsLocalRing A] [IsNoetherianRing A]
    (h :
      let m := IsLocalRing.maximalIdeal A
      let : TopologicalSpace k := ⊥
      let : DiscreteTopology k := ⟨rfl⟩
      let : TopologicalSpace A := m.adicTopology
      let : IsTopologicalRing A := m.ringFilterBasis.isTopologicalRing
      let : IsLinearTopology A A := m.isLinearTopology
      RingHom.FormallySmoothTop.{max v w} (algebraMap k A)) :
    IsRegularLocalRing A
Tag 0C34, a lemma

Tag 0C34 in the Stacks Project.

exists_residueField_algHom_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/LocalRings/CoefficientFieldsAndRegularity.lean, line 106. References: EGA 0 (19.5.4.4), “special case”.

A complete local algebra over a field whose residue field is separable over the base field has a coefficient field: the residue homomorphism has a section by an algebra homomorphism.

public theorem exists_residueField_algHom_section
    {k : Type*} {A : Type*} [Field k] [CommRing A] [IsLocalRing A] [Algebra k A]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
    (hsep : Algebra.IsSeparableExtension k (IsLocalRing.ResidueField A)) :
    ∃ σ : IsLocalRing.ResidueField A →ₐ[k] A,
      (Ideal.Quotient.mkₐ k (IsLocalRing.maximalIdeal A)).comp σ =
        AlgHom.id k (IsLocalRing.ResidueField A)
Tag 0C35, a lemma

Tag 0C35 in the Stacks Project.

exists_algEquiv_mvPowerSeries_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/LocalRings/CoefficientFieldsAndRegularity.lean, line 144. References: EGA 0 (19.6.4), “special case”; EGA 0 (19.8.8), “(i), special case”; EGA 0 (21.9.2), “special case”; SGA 1 II (5.6), “(iii)”.

A complete regular local algebra over a field whose residue field is separable over the base field is isomorphic, as an algebra over that field, to a multivariable formal power series ring over its residue field.

public theorem exists_algEquiv_mvPowerSeries_residueField
    {k : Type u} {A : Type v} [Field k] [CommRing A] [Algebra k A]
    [IsRegularLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
    (hsep : Algebra.IsSeparableExtension k (IsLocalRing.ResidueField A)) :
    Nonempty
      (A ≃ₐ[k] MvPowerSeries
        (Fin (Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.CotangentSpace A)))
        (IsLocalRing.ResidueField A))
Tag 07EJ, a lemma

Tag 07EJ in the Stacks Project.

isFormallySmooth_maximalIdeal_of_isRegularLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/LocalRings/CoefficientFieldsAndRegularity.lean, line 565.

A regular local algebra over a field whose residue field is separable over the base field is formally smooth for its maximal-ideal adic topology.

public theorem isFormallySmooth_maximalIdeal_of_isRegularLocalRing.{u, v, w}
    {k : Type v} {A : Type w} [Field k] [CommRing A] [Algebra k A]
    [IsRegularLocalRing A]
    (hsep : Algebra.IsSeparableExtension k (IsLocalRing.ResidueField A)) :
    FormallySmoothDiscreteMaximalIdeal.{u, v, w} (algebraMap k A)
Tag 07VH, a lemma

Tag 07VH in the Stacks Project.

smoothAt_iff_formallySmoothNAdic_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/LocalRings/CoefficientFieldsAndRegularity.lean, line 671. References: EGA 0 (22.6.4), “c) <=> d)”; EGA IV (6.8.6), “a) ⇔ c)”; EGA IV (17.5.3), “a) ⇔ d)”; SGA 1 III (1.9), “Noetherian A”.

Let A → B be a finite type map with A Noetherian, and let the prime q ⊆ B lie over the prime p ⊆ A. Then the map is smooth at q if and only if the canonical local map A_p → B_q is formally smooth for the maximal-ideal-adic topology on B_q.

public theorem smoothAt_iff_formallySmoothNAdic_localization.{u, v}
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    [IsNoetherianRing A] [Algebra.FiniteType A B]
    (p : Ideal A) (q : Ideal B) [p.IsPrime] [q.IsPrime] [q.LiesOver p] :
    Algebra.SmoothAt A B q ↔
      RingHom.FormallySmoothNAdic.{max u v, u, v}
        (@algebraMap (Localization.AtPrime p) (Localization.AtPrime q) _ _
          (Localization.AtPrime.algebraOfLiesOver p q))
        (maximalIdeal (Localization.AtPrime q))
Sources
LeanformallySmooth_adic_iff_lifts_local_squareZero · isRegularLocalRing_of_isFormallySmooth_maximalIdeal · RingHom.FormallySmoothTop.isRegularLocalRing_of_maximalIdeal · exists_residueField_algHom_section · exists_algEquiv_mvPowerSeries_residueField · isFormallySmooth_maximalIdeal_of_isRegularLocalRing · smoothAt_iff_formallySmoothNAdic_localization

Section15.40 Some results on power series rings#

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

Tag 07NL, a lemma

Tag 07NL in the Stacks Project.

isFormallySmooth_mvPowerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/PowerSeriesFormallySmooth.lean, line 622.

Stacks 07NL. Formal power series rings over a characteristic-zero field, over a field of characteristic p, and over a Cohen ring are formally smooth over ℚ, 𝔽_p, and ℤ, respectively, for their maximal-ideal-adic topologies.

public theorem isFormallySmooth_mvPowerSeries.{u} (n p : ℕ)
    (K L Λ : Type*) [Field K] [CharZero K] [Field L] [Fact p.Prime] [CharP L p]
    [CommRing Λ] [IsDomain Λ] [IsCohenRing Λ] :
    letI : Algebra (ZMod p) L := ZMod.algebra L p
    @IsFormallySmooth.{u} ℚ (MvPowerSeries (Fin n) K) inferInstance
        (⊥ : Ideal ℚ).adicTopology (⊥ : Ideal ℚ).ringFilterBasis.isTopologicalRing
        (Ideal.isLinearTopology ⊥) inferInstance
        (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) K)).adicTopology
        (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) K)).ringFilterBasis.isTopologicalRing
        (Ideal.isLinearTopology _) (algebraMap ℚ (MvPowerSeries (Fin n) K)) ∧
      @IsFormallySmooth.{u} (ZMod p) (MvPowerSeries (Fin n) L) inferInstance
          (⊥ : Ideal (ZMod p)).adicTopology
          (⊥ : Ideal (ZMod p)).ringFilterBasis.isTopologicalRing
          (Ideal.isLinearTopology ⊥) inferInstance
          (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) L)).adicTopology
          (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) L)).ringFilterBasis.isTopologicalRing
          (Ideal.isLinearTopology _) (algebraMap (ZMod p) (MvPowerSeries (Fin n) L)) ∧
        @IsFormallySmooth.{u} ℤ (MvPowerSeries (Fin n) Λ) inferInstance
          (⊥ : Ideal ℤ).adicTopology (⊥ : Ideal ℤ).ringFilterBasis.isTopologicalRing
          (Ideal.isLinearTopology ⊥) inferInstance
          (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) Λ)).adicTopology
          (IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) Λ)).ringFilterBasis.isTopologicalRing
          (Ideal.isLinearTopology _) (algebraMap ℤ (MvPowerSeries (Fin n) Λ))
Tag 07NM, a lemma

Tag 07NM in the Stacks Project.

main_theorem_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/PowerSeriesMaps.lean, line 148. The attribute's comment: “(1)”. References: SGA 1 II (4.14), “special case”; SGA 1 III (2.3), “special case”; SGA 2 IV (5.5), “special case”; SGA 3 VIIB (5.5.2), “partial”.

Statement (1). If y_1, ..., y_n is a regular system of parameters of A = K[[x_1, ..., x_n]], then the canonical substitution map K[[Y_1, ..., Y_n]] → A, Y_i ↦ y_i, is an isomorphism.

The canonical map is MvPowerSeries.substAlgHom (hasSubst_of_mem_maximalIdeal y): the substitution X i ↦ y i, which is defined precisely because each y i lies in m_A and hence has zero constant coefficient, and which is the unique continuous K-algebra map sending X i to y i. The conclusion states that this map sends X i to y i and is bijective — i.e. is an isomorphism of K-algebras.

theorem main_theorem_one (K : Type*) [Field K] (n : ℕ)
    (y : Fin n → maximalIdeal (MvPowerSeries (Fin n) K)) (hy : IsRegularSystemOfParameters y) :
    (∀ i,
        (MvPowerSeries.substAlgHom (hasSubst_of_mem_maximalIdeal y) :
            MvPowerSeries (Fin n) K →ₐ[K] MvPowerSeries (Fin n) K)
          (MvPowerSeries.X i) = (y i : MvPowerSeries (Fin n) K)) ∧
      Function.Bijective
        ((MvPowerSeries.substAlgHom (hasSubst_of_mem_maximalIdeal y) :
          MvPowerSeries (Fin n) K →ₐ[K] MvPowerSeries (Fin n) K))

main_theorem_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/PowerSeriesMaps.lean, line 217. The attribute's comment: “(2)”. References: EGA 0 (17.1.4), “more general”; EGA 0 (17.1.7), “special case”.

Statement (2). If z_1, ..., z_r form part of a regular system of parameters for A = K[[x_1, ..., x_n]], then r <= n and A/(z_1, ..., z_r) is isomorphic (as a K-algebra) to the power series ring K[[Y_1, ..., Y_{n-r}]].

theorem main_theorem_two (K : Type*) [Field K] (n r : ℕ)
    (z : Fin r → maximalIdeal (MvPowerSeries (Fin n) K))
    (hz : FormsPartOfRegularSystemOfParameters z) :
    r ≤ n ∧
      Nonempty
        ((MvPowerSeries (Fin n) K ⧸
            Ideal.span (Set.range (fun i => (z i : MvPowerSeries (Fin n) K)))) ≃ₐ[K]
          MvPowerSeries (Fin (n - r)) K)

main_theorem_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/PowerSeriesMaps.lean, line 594. The attribute's comment: “(3)”. References: SGA 1 III (2.3), “special case”.

Statement (3). Let Lambda be a Cohen ring with uniformizer the prime number pr, and let B = Lambda[[x_1, ..., x_n]]. If p, y_1, ..., y_n is a regular system of parameters of B (where p = pr viewed in B via the coefficient inclusion), then the canonical Lambda-algebra homomorphism Lambda[[Y_1, ..., Y_n]] -> B sending Y_i to y_i — cohenSubstAlgHom, the m_Λ-adic translation followed by substitution of the normalized family — is an isomorphism: it sends X i to y i and it is bijective.

theorem main_theorem_three (Λ : Type*) [CommRing Λ] [IsDomain Λ] [IsDiscreteValuationRing Λ]
    (hΛ : IsCohenRing Λ) (n : ℕ) (pr : ℕ) (hunif : maximalIdeal Λ = Ideal.span {(pr : Λ)})
    (p : maximalIdeal (MvPowerSeries (Fin n) Λ))
    (hp : (p : MvPowerSeries (Fin n) Λ) = algebraMap Λ (MvPowerSeries (Fin n) Λ) (pr : Λ))
    (y : Fin n → maximalIdeal (MvPowerSeries (Fin n) Λ))
    (hrsp : IsRegularSystemOfParameters (Fin.cons p y)) :
    (∀ i, cohenSubstAlgHom hΛ y (MvPowerSeries.X i) = (y i : MvPowerSeries (Fin n) Λ)) ∧
      Function.Bijective (cohenSubstAlgHom hΛ y)

main_theorem_four, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/PowerSeriesMaps.lean, line 778. The attribute's comment: “(4)”. References: EGA 0 (17.1.7), “special case”.

Statement (4). Let Lambda be a Cohen ring with uniformizer the prime number pr, and let B = Lambda[[x_1, ..., x_n]]. If p, z_1, ..., z_r form part of a regular system of parameters for B (the length-(r+1) sequence p, z_1, ..., z_r, with p the uniformizer viewed in B), then r <= n and B/(z_1, ..., z_r) is isomorphic (as a Lambda-algebra) to the power series ring Lambda[[Y_1, ..., Y_{n-r}]].

theorem main_theorem_four (Λ : Type*) [CommRing Λ] [IsDomain Λ] [IsDiscreteValuationRing Λ]
    (hΛ : IsCohenRing Λ) (n r : ℕ) (pr : ℕ) (hunif : maximalIdeal Λ = Ideal.span {(pr : Λ)})
    (p : maximalIdeal (MvPowerSeries (Fin n) Λ))
    (hp : (p : MvPowerSeries (Fin n) Λ) = algebraMap Λ (MvPowerSeries (Fin n) Λ) (pr : Λ))
    (z : Fin r → maximalIdeal (MvPowerSeries (Fin n) Λ))
    (hz : FormsPartOfRegularSystemOfParameters (Fin.cons p z)) :
    r ≤ n ∧
      Nonempty
        ((MvPowerSeries (Fin n) Λ ⧸
            Ideal.span (Set.range (fun i => (z i : MvPowerSeries (Fin n) Λ)))) ≃ₐ[Λ]
          MvPowerSeries (Fin (n - r)) Λ)
Tag 07NN, a lemma

Tag 07NN in the Stacks Project.

exists_powerSeries_presentation_of_isLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/PowerSeriesFormallySmooth.lean, line 1087. References: EGA 0 (19.8.8), “more general”; SGA 2 IV (4.8), “more general”; SGA 2 IX (2.3), “more general”.

Stacks 07NN. A local homomorphism A → B of Noetherian complete local rings admits a commutative presentation by surjections from power series rings R and S. According to the residue characteristic, these are power series rings over fields or over Cohen rings. The map R → S carries a regular system of parameters to part of one, is flat, and has regular closed fibre.

public theorem exists_powerSeries_presentation_of_isLocalHom
    {A : Type u} {B : Type v}
    [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
    [CommRing B] [IsNoetherianRing B] [IsLocalRing B]
    [IsAdicComplete (IsLocalRing.maximalIdeal B) B]
    (f : A →+* B) [IsLocalHom f] :
    ∃ (R S : Type (max u v)) (_ : CommRing R) (_ : IsRegularLocalRing R)
      (_ : IsAdicComplete (IsLocalRing.maximalIdeal R) R)
      (_ : CommRing S) (_ : IsRegularLocalRing S)
      (_ : IsAdicComplete (IsLocalRing.maximalIdeal S) S)
      (g : R →+* S) (qA : R →+* A) (qB : S →+* B),
      Function.Surjective qA ∧ Function.Surjective qB ∧
      IsLocalHom g ∧ IsLocalHom qA ∧ IsLocalHom qB ∧
      f.comp qA = qB.comp g ∧
      (∃ (xs : List R) (ys : List S) (zs : List S),
        Ideal.ofList xs = IsLocalRing.maximalIdeal R ∧
        xs.length = (IsLocalRing.maximalIdeal R).spanFinrank ∧
        Ideal.ofList ys = IsLocalRing.maximalIdeal S ∧
        ys.length = (IsLocalRing.maximalIdeal S).spanFinrank ∧
        ys = xs.map g ++ zs ∧
        (ringChar (IsLocalRing.ResidueField A) = 0 →
          ∃ (nR nS : ℕ) (kR kS : Type (max u v)) (_ : Field kR) (_ : Field kS),
            Nonempty (R ≃+* MvPowerSeries (Fin nR) kR) ∧
            Nonempty (S ≃+* MvPowerSeries (Fin nS) kS)) ∧
        (∀ p : ℕ, 0 < p → ringChar (IsLocalRing.ResidueField A) = p →
          ∃ (nR nS : ℕ) (ΛR ΛS : Type (max u v))
            (_ : CommRing ΛR) (_ : IsDomain ΛR) (_ : IsCohenRing ΛR)
            (_ : CommRing ΛS) (_ : IsDomain ΛS) (_ : IsCohenRing ΛS),
            Nonempty (R ≃+* MvPowerSeries (Fin nR) ΛR) ∧
            Nonempty (S ≃+* MvPowerSeries (Fin nS) ΛS) ∧
            IsLocalRing.maximalIdeal ΛR = Ideal.span {(p : ΛR)} ∧
            IsLocalRing.maximalIdeal ΛS = Ideal.span {(p : ΛS)} ∧
            ∃ xs', xs = (p : R) :: xs')) ∧
      letI : Algebra R S := g.toAlgebra
      Module.Flat R S ∧
        IsRegularLocalRing (S ⧸ Ideal.map g (IsLocalRing.maximalIdeal R))
Tag 09Q8, a lemma

Tag 09Q8 in the Stacks Project.

isNoetherianCompleteLocalRing_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/PowerSeriesFormallySmooth.lean, line 1415. References: EGA IV (19.3.2.1), “(iii)”.

Stacks 09Q8. The pullback of two surjective maps of complete Noetherian local rings is again a complete Noetherian local ring.

public theorem isNoetherianCompleteLocalRing_pullback.{u, v, w}
    {R : Type u} {S : Type v} {S' : Type w}
    [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    [CommRing S] [IsLocalRing S] [IsNoetherianRing S]
    [IsAdicComplete (IsLocalRing.maximalIdeal S) S]
    [CommRing S'] [IsLocalRing S'] [IsNoetherianRing S']
    [IsAdicComplete (IsLocalRing.maximalIdeal S') S']
    (f : S →+* R) (f' : S' →+* R)
    (hf : Function.Surjective f) (hf' : Function.Surjective f') :
    ∃ hlocal : IsLocalRing (f.pullback f'),
      letI := hlocal
      IsNoetherianRing (f.pullback f') ∧
        IsAdicComplete (IsLocalRing.maximalIdeal (f.pullback f')) (f.pullback f')
Sources
LeanisFormallySmooth_mvPowerSeries · main_theorem_one · main_theorem_two · main_theorem_three · main_theorem_four · exists_powerSeries_presentation_of_isLocalHom · isNoetherianCompleteLocalRing_pullback

Section15.41 Geometric regularity and formal smoothness#

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

Tag 07EL, a theorem

Tag 07EL in the Stacks Project.

formalSmoothness_maximalIdeal_characterizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/FormalSmoothness.lean, line 1088. References: EGA 0 (19.6.6), “a) <=> c)”; EGA 0 (19.6.4), “char 0: a) ⇔ c)”; EGA 0 (19.6.5), “form. smooth ⟹ geom reg”; EGA 0 (22.1.2), “base a field, Noetherian”; EGA 0 (22.2.2), “(i)&(ii), char p”; EGA 0 (22.2.3), “a) (char p)”; EGA 0 (22.7.2), “a) <=> c) char 0”; EGA 0 (22.5.8); EGA 0 (22.6.7), “(i) b) ⇔ d)”; EGA 0 (19.0.2), “special case”; EGA 0 (19.6.7), “19.6.7(ii), special case”.

Let A be a Noetherian local algebra over a field k. In characteristic zero, A is a regular local ring if and only if k → A is formally smooth for the maximal-ideal adic topology. In prime characteristic p, the following are equivalent:

  1. A is geometrically regular over k;
  2. k → A is formally smooth for the maximal-ideal adic topology;
  3. every finite intermediate extension in k¹ᵖ gives a regular base change;
  4. A is regular and the canonical cotangent-complex map is injective;
  5. A is regular and the canonical map on Kähler differentials is injective.
public theorem formalSmoothness_maximalIdeal_characterizations
    (k : Type u) (A : Type v) [Field k] [CommRing A] [Algebra k A]
    [IsNoetherianRing A] [IsLocalRing A] :
    (let m := IsLocalRing.maximalIdeal A
     letI : TopologicalSpace k := ⊥
     letI : DiscreteTopology k := ⟨rfl⟩
     letI : TopologicalSpace A := m.adicTopology
     letI : IsTopologicalRing A := m.ringFilterBasis.isTopologicalRing
     letI : IsLinearTopology A A := m.isLinearTopology
     ∀ [CharZero k],
       IsRegularLocalRing A ↔
         IsFormallySmooth.{max u v} (algebraMap k A)) ∧
    (∀ (p : ℕ) [Fact p.Prime] [CharP k p],
      letI : Algebra (ZMod p) k := ZMod.algebra k p
      letI : Algebra (ZMod p) A :=
        ((algebraMap k A).comp (algebraMap (ZMod p) k)).toAlgebra
      letI : IsScalarTower (ZMod p) k A := IsScalarTower.of_algebraMap_eq' rfl
      letI : Algebra k (PerfectClosure k p) := (PerfectClosure.of k p).toAlgebra
      let m := IsLocalRing.maximalIdeal A
      letI : TopologicalSpace k := ⊥
      letI : DiscreteTopology k := ⟨rfl⟩
      letI : TopologicalSpace A := m.adicTopology
      letI : IsTopologicalRing A := m.ringFilterBasis.isTopologicalRing
      letI : IsLinearTopology A A := m.isLinearTopology
      List.TFAE [
        Algebra.IsGeometricallyRegular k A,
        IsFormallySmooth.{max u v} (algebraMap k A),
        (∀ (k' : IntermediateField k (PerfectClosure k p)),
          FiniteDimensional k k' →
          (∀ x : k', (x : PerfectClosure k p) ^ p ∈
            Set.range (algebraMap k (PerfectClosure k p))) →
          IsRegularRing (A ⊗[k] k')),
        IsRegularLocalRing A ∧
          Function.Injective
            (Algebra.H1Cotangent.map k A (IsLocalRing.ResidueField A)
              (IsLocalRing.ResidueField A)),
        IsRegularLocalRing A ∧
          Function.Injective
            ((KaehlerDifferential.mapBaseChange (ZMod p) k A).baseChange
              (IsLocalRing.ResidueField A))])
Tag 07EM, an example

Tag 07EM in the Stacks Project.

formallySmooth_adic_examples_with_inseparable_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/FormalSmoothness.lean, line 1745. References: EGA 0 (19.6.5.2), “existence of examples”.

In characteristic p, the local ring k[x, y]_(x, y ^ p - a) / (y ^ p - a - x) is geometrically regular over k, formally smooth both algebraically and for its maximal-ideal-adic topology, and has purely inseparable residue field. Closely relatedly, if K is the perfect closure of 𝔽ₚ(t), there is a map 𝔽ₚ(s) → K[[x]] sending s to t + x which is formally smooth for the (x)-adic topology. For the latter map, ds and dx are the indicated bases of the Kähler differentials and the map on differentials sends ds to dx.

public theorem formallySmooth_adic_examples_with_inseparable_residueField
    (p : ℕ) [Fact p.Prime] :
    (∀ (k : Type u) [Field k] [CharP k p] (a : k),
      a ∉ Set.range (fun b : k => b ^ p) →
      let P := MvPolynomial (Fin 2) k
      let m : Ideal P := Ideal.span
        {MvPolynomial.X 0, MvPolynomial.X 1 ^ p - MvPolynomial.C a}
      let g : P := MvPolynomial.X 1 ^ p - MvPolynomial.C a - MvPolynomial.X 0
      ∃ hm : m.IsPrime,
        letI : m.IsPrime := hm
        let B := Localization.AtPrime m
        let A := B ⧸ Ideal.span {algebraMap P B g}
        ∃ hlocal : IsLocalRing A,
          letI : IsLocalRing A := hlocal
          IsNoetherianRing A ∧
          Algebra.IsGeometricallyRegular k A ∧
          IsPurelyInseparable k (IsLocalRing.ResidueField A) ∧
          Algebra.FormallySmooth k A ∧
          let n := IsLocalRing.maximalIdeal A
          @IsAdicallyFormallySmooth k A _ _ n (algebraMap k A)) ∧
    (let k := RatFunc (ZMod p)
     let K := PerfectClosure k p
     letI : Algebra k K := (PerfectClosure.of k p).toAlgebra
     let A := PowerSeries K
     ∃ f : k →+* A,
       f RatFunc.X =
          PowerSeries.C (algebraMap k K RatFunc.X) + PowerSeries.X ∧
       letI : Algebra k A := f.toAlgebra
       letI : Algebra (ZMod p) A :=
         (f.comp (algebraMap (ZMod p) k)).toAlgebra
       letI : IsScalarTower (ZMod p) k A :=
         IsScalarTower.of_algebraMap_eq' rfl
       (∃ b : Module.Basis Unit k (KaehlerDifferential (ZMod p) k),
          b () = KaehlerDifferential.D (ZMod p) k RatFunc.X) ∧
       (∃ b : Module.Basis Unit A (KaehlerDifferential (ZMod p) A),
          b () = KaehlerDifferential.D (ZMod p) A PowerSeries.X) ∧
       KaehlerDifferential.map (ZMod p) (ZMod p) k A
           (KaehlerDifferential.D (ZMod p) k RatFunc.X) =
         KaehlerDifferential.D (ZMod p) A PowerSeries.X ∧
       let x : Ideal A := Ideal.span {PowerSeries.X}
       @IsAdicallyFormallySmooth k A _ _ x f)
Tag 07NP, a lemma

Tag 07NP in the Stacks Project.

flat_of_isFormallySmooth_maximalIdeal_adic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/FormalSmoothness.lean, line 595. References: SGA 1 III (1.7), “only if, flatness”.

Stacks 07NP. A formally smooth local homomorphism of Noetherian local rings, for the maximal-ideal-adic topologies on source and target, is flat.

public theorem flat_of_isFormallySmooth_maximalIdeal_adic.{v, w}
    {A : Type v} {B : Type w}
    [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    [CommRing B] [IsNoetherianRing B] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : RingHom.FormallySmoothNAdic.{max v w} f (maximalIdeal B)) :
    letI : Algebra A B := f.toAlgebra
    Module.Flat A B
Tag 0DYH, a lemma

Tag 0DYH in the Stacks Project.

exact_jacobiZariski_residueField_of_formallySmoothNAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/FormalSmoothness.lean, line 755. References: EGA 0 (20.6.23), “residue field, m-adic”.

Let A → B be a local homomorphism of Noetherian local rings which is formally smooth for the maximal-ideal-adic topology on B, and let K be the residue field of B. Then the canonical Jacobi–Zariski sequence

0 → H₁(L_{K/A}) → 𝔪_B/𝔪_B² → Ω[B⁄A] ⊗[B] K → Ω[K⁄A] → 0

is exact.

public theorem exact_jacobiZariski_residueField_of_formallySmoothNAdic
    {A : Type u} {B : Type v}
    [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    [CommRing B] [IsNoetherianRing B] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : RingHom.FormallySmoothNAdic.{max u v} f (maximalIdeal B)) :
    let K := ResidueField B
    letI : Algebra A B := f.toAlgebra
    letI : Algebra A K := ((residue B).comp f).toAlgebra
    letI : IsScalarTower A B K := IsScalarTower.of_algebraMap_eq' rfl
    let e : Algebra.H1Cotangent B K ≃ₗ[B] CotangentSpace B :=
      (h1Cotangent_equiv_cotangent_of_surjective B K residue_surjective).trans
        (Ideal.Cotangent.equivOfEq _ _ (ker_residue (R := B)))
    let i : Algebra.H1Cotangent A K → CotangentSpace B :=
      fun x ↦ e (Algebra.H1Cotangent.map A B K K x)
    let d : CotangentSpace B → K ⊗[B] Ω[B⁄A] :=
      fun x ↦ Algebra.H1Cotangent.δ A B K (e.symm x)
    Function.Injective i ∧
      Function.Exact i d ∧
      Function.Exact d (KaehlerDifferential.mapBaseChange A B K) ∧
      Function.Surjective (KaehlerDifferential.mapBaseChange A B K)
Tag 07NQ, a proposition

Tag 07NQ in the Stacks Project.

RingHom.FormallySmoothNAdic.of_flat_of_specialFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/SpecialFibre.lean, line 401. The attribute's comment: “(2) ⟹ (3)”. References: EGA 0 (19.0.2), “I, one direction”; EGA 0 (19.7.1), “b) ⇒ a)”; SGA 1 III (1.7), “if direction”; SGA 1 III (1.7), “if direction”.

Stacks 07NQ, (2) ⟹ (3). A flat local homomorphism of Noetherian local rings whose special fibre is adically formally smooth over the residue field of the source is itself formally smooth for the maximal-ideal-adic topology.

theorem FormallySmoothNAdic.of_flat_of_specialFibre
    (A : Type u) (B : Type v)
    [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    [CommRing B] [IsNoetherianRing B] [IsLocalRing B]
    [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Flat A B]
    (hbar : FormallySmoothNAdic.{max u v}
      (algebraMap (ResidueField A) (ResidueField A ⊗[A] B))
      (maximalIdeal (ResidueField A ⊗[A] B))) :
    FormallySmoothNAdic.{max u v} (algebraMap A B) (maximalIdeal B)

flat_geometricallyRegular_specialFiber_formallySmooth_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/FormalSmoothness.lean, line 2253. References: EGA 0 (19.0.2), “I”; EGA 0 (19.7.1), “more general”; SGA 1 III (1.7), “Noetherian local rings”; SGA 1 III (1.3), “more general”.

Let f : A → B be a local homomorphism of Noetherian local rings, let k be the residue field of A, and let B̄ = k ⊗[A] B be the special fibre. The following are equivalent:

  1. f is flat and B̄ is geometrically regular over k;
  2. f is flat and k → B̄ is formally smooth for the maximal-ideal-adic topology;
  3. f is formally smooth for the maximal-ideal-adic topology on B.
public theorem flat_geometricallyRegular_specialFiber_formallySmooth_tfae
    {A : Type u} {B : Type v}
    [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    [CommRing B] [IsNoetherianRing B] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f] :
    letI : Algebra A B := f.toAlgebra
    let k := ResidueField A
    let Bbar := k ⊗[A] B
    List.TFAE [
      Module.Flat A B ∧ Algebra.IsGeometricallyRegular k Bbar,
      Module.Flat A B ∧
        RingHom.FormallySmoothNAdic.{max u v}
          (algebraMap k Bbar) (maximalIdeal Bbar),
      RingHom.FormallySmoothNAdic.{max u v} f (maximalIdeal B)]
Tag 07NR, a lemma

Tag 07NR in the Stacks Project.

exists_completeLocal_formallySmooth_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/FormalSmoothness.lean, line 2512. References: EGA 0 (19.7.2), “existence, J = 𝔪”; EGA 0 (19.0.2), “III existence”; EGA 0 (19.7.1.3), “A complete, B geom reg”; EGA 0 (19.8.2), “(ii) existence”; EGA 0 (22.2.7), “(i)”.

Stacks 07NR. Let A be a Noetherian complete local ring and let B be a Noetherian complete local algebra over the residue field of A. If B is formally smooth for its maximal-ideal-adic topology, then it is the special fibre of a Noetherian complete local ring C that is adically formally smooth over A via a local homomorphism.

public theorem exists_completeLocal_formallySmooth_lift
    {A : Type u} {B : Type v}
    [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    [IsAdicComplete (maximalIdeal A) A]
    [CommRing B] [IsNoetherianRing B] [IsLocalRing B]
    [IsAdicComplete (maximalIdeal B) B]
    [Algebra (ResidueField A) B]
    (hB : RingHom.FormallySmoothNAdic.{max u v}
      (algebraMap (ResidueField A) B) (maximalIdeal B)) :
    ∃ (C : Type (max u v)) (_ : CommRing C) (_ : IsNoetherianRing C)
      (_ : IsLocalRing C) (_ : IsAdicComplete (maximalIdeal C) C)
      (f : A →+* C) (_ : IsLocalHom f),
      RingHom.FormallySmoothNAdic.{max u v} f (maximalIdeal C) ∧
        letI : Algebra A C := f.toAlgebra
        Nonempty ((ResidueField A ⊗[A] C) ≃ₐ[ResidueField A] B)
Tag 07NS, a remark

Tag 07NS in the Stacks Project.

exists_completeLocal_formallySmooth_lift_with_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/FormalSmoothness.lean, line 3531. References: EGA 0 (22.2.7), “(i)”.

Stacks 07NS. Consider local homomorphisms A → A' → B of Noetherian complete local rings such that A → A' induces an isomorphism on residue fields. If the special fibre of B over A' is formally smooth, then it is induced by an adically formally smooth Noetherian complete local A-algebra C mapping locally to B.

The completed base change of C to A' is again Noetherian, complete, local, and flat over A', and its induced map to B is surjective. Moreover, C → B is surjective when A → A' is, finite when A → A' is finite, and the completed base-change map is an isomorphism when A' → B is flat.

public theorem exists_completeLocal_formallySmooth_lift_with_baseChange
    {A : Type u} {A' : Type v} {B : Type w}
    [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    [IsAdicComplete (maximalIdeal A) A]
    [CommRing A'] [IsNoetherianRing A'] [IsLocalRing A']
    [IsAdicComplete (maximalIdeal A') A']
    [CommRing B] [IsNoetherianRing B] [IsLocalRing B]
    [IsAdicComplete (maximalIdeal B) B]
    (f : A →+* A') [IsLocalHom f]
    (g : A' →+* B) [IsLocalHom g]
    (hf : Function.Bijective (ResidueField.map f))
    (hB : letI : Algebra A' B := g.toAlgebra
      RingHom.FormallySmoothNAdic.{max u v w}
        (algebraMap (ResidueField A') (ResidueField A' ⊗[A'] B))
        (maximalIdeal (ResidueField A' ⊗[A'] B))) :
    ∃ (C : Type (max u v w)) (_ : CommRing C) (_ : IsNoetherianRing C)
      (_ : IsLocalRing C) (_ : IsAdicComplete (maximalIdeal C) C)
      (a : A →+* C) (_ : IsLocalHom a)
      (c : C →+* B) (_ : IsLocalHom c),
      c.comp a = g.comp f ∧
      RingHom.FormallySmoothNAdic.{max u v w} a (maximalIdeal C) ∧
      (letI : Algebra A A' := f.toAlgebra
       letI : Algebra A' B := g.toAlgebra
       letI : Algebra A C := a.toAlgebra
       letI : Algebra (ResidueField A) (ResidueField A') := (ResidueField.map f).toAlgebra
       ∃ e : (ResidueField A ⊗[A] C) ≃ₐ[ResidueField A]
           (ResidueField A' ⊗[A'] B),
         (∀ x : ResidueField A,
           e (Algebra.TensorProduct.includeLeft (R := A) (S := ResidueField A)
             (A := ResidueField A) (B := C) x) =
             Algebra.TensorProduct.includeLeft (R := A') (S := ResidueField A')
               (A := ResidueField A') (B := B) (ResidueField.map f x)) ∧
         (∀ y : C,
           e (Algebra.TensorProduct.includeRight (R := A)
             (A := ResidueField A) (B := C) y) =
           Algebra.TensorProduct.includeRight (R := A')
             (A := ResidueField A') (B := B) (c y))) ∧
      (letI : Algebra A A' := f.toAlgebra
       letI : Algebra A C := a.toAlgebra
       let T := C ⊗[A] A'
       let iA' : A' →+* T :=
         (Algebra.TensorProduct.includeRight (R := A) (A := C) (B := A')).toRingHom
       let J : Ideal T := (maximalIdeal A').map iA'
       let D := AdicCompletion J T
       ∃ (t : T →+* B) (q : D →+* B)
         (_ : IsNoetherianRing D) (_ : IsLocalRing D),
         t.comp (Algebra.TensorProduct.includeLeft (R := A) (S := A)
           (A := C) (B := A')).toRingHom = c ∧
         t.comp iA' = g ∧
         q.comp (algebraMap T D) = t ∧
         IsAdicComplete (maximalIdeal D) D ∧
         ((algebraMap T D).comp iA').Flat ∧
         Function.Surjective q ∧
         (Function.Surjective f → Function.Surjective c) ∧
         (f.Finite → c.Finite) ∧
         (g.Flat → Function.Bijective q))
Sources
LeanformalSmoothness_maximalIdeal_characterizations · formallySmooth_adic_examples_with_inseparable_residueField · flat_of_isFormallySmooth_maximalIdeal_adic · exact_jacobiZariski_residueField_of_formallySmoothNAdic · RingHom.FormallySmoothNAdic.of_flat_of_specialFibre · flat_geometricallyRegular_specialFiber_formallySmooth_tfae · exists_completeLocal_formallySmooth_lift · exists_completeLocal_formallySmooth_lift_with_baseChange

Section15.42 Regular ring maps#

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

Tag 07BZ, a definition

Tag 07BZ in the Stacks Project.

IsRegularRingHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/RegularRingHom.lean, line 92.

A ring homomorphism is regular if it is flat and, over every prime of its source, its residue-field fibre is Noetherian and geometrically regular over that residue field.

public def IsRegularRingHom {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    (f : R →+* S) : Prop
Tag 07C0, a lemma

Tag 07C0 in the Stacks Project.

isRegularRingHom_tfae_localizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/RegularRingHom.lean, line 469.

A ring homomorphism with Noetherian target is regular if and only if all its induced maps on local rings at corresponding prime ideals are regular, and if and only if this holds for maximal ideals of the target and their contractions.

public theorem isRegularRingHom_tfae_localizations
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    (f : R →+* S) [IsNoetherianRing S] :
    List.TFAE [
      IsRegularRingHom f,
      ∀ (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] (h : p = q.comap f),
        IsRegularRingHom (Localization.localRingHom p q f h),
      ∀ (m : Ideal R) [m.IsPrime] (m' : Ideal S) [m'.IsMaximal]
        (h : m = m'.comap f),
        IsRegularRingHom (Localization.localRingHom m m' f h)]
Tag 07C1, a lemma

Tag 07C1 in the Stacks Project.

isRegularRingHom_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/RegularRingHom.lean, line 554.

A finite-type base change of a regular ring homomorphism is regular.

public theorem isRegularRingHom_baseChange
    {R : Type u} {Λ : Type v} {R' : Type w}
    [CommRing R] [CommRing Λ] [CommRing R'] [Algebra R Λ] [Algebra R R']
    [Algebra.FiniteType R R']
    (h : IsRegularRingHom (algebraMap R Λ)) :
    IsRegularRingHom
      (Algebra.TensorProduct.includeRight (R := R) (A := Λ) (B := R')).toRingHom
Tag 07QI, a lemma

Tag 07QI in the Stacks Project.

isRegularRingHom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/RegularRingHom.lean, line 704.

The composite of two regular ring homomorphisms is regular if all its fibres are Noetherian.

public theorem isRegularRingHom_comp
    {A : Type u} {B : Type v} {C : Type w} [CommRing A] [CommRing B] [CommRing C]
    (f : A →+* B) (g : B →+* C)
    (hf : IsRegularRingHom f) (hg : IsRegularRingHom g)
    (hNoetherian : ∀ (p : Ideal A) [p.IsPrime],
      let : Algebra A C := (g.comp f).toAlgebra
      IsNoetherianRing (p.Fiber C)) :
    IsRegularRingHom (g.comp f)
Tag 07EP, a lemma

Tag 07EP in the Stacks Project.

isRegularRingHom_of_filteredColimit_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/RegularRingHom.lean, line 1181.

The colimit of a small nonempty directed system of smooth R-algebras, computed on underlying sets, whose residue-field fibres are Noetherian is regular over R.

public theorem isRegularRingHom_of_filteredColimit_smooth
    {R : Type u} [CommRing R]
    {J : Type w} [Preorder J] [IsDirectedOrder J] [Nonempty J] [Small.{max u v} J]
    (F : J ⥤ CommAlgCat.{v} R) (c : Cocone F) (hc : IsColimit c)
    [PreservesColimit (F ⋙ forget₂ (CommAlgCat.{v} R) CommRingCat.{v})
      (forget CommRingCat.{v})]
    (hsm : ∀ j, Algebra.Smooth R (F.obj j))
    (hnoeth : ∀ (p : Ideal R) [p.IsPrime], IsNoetherianRing (p.Fiber c.pt)) :
    IsRegularRingHom (algebraMap R c.pt)
Tag 07EQ, a lemma

Tag 07EQ in the Stacks Project.

isRegularRingHom_iff_isSeparableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/RegularRingHom.lean, line 1292.

A field extension is a regular ring map if and only if it is separable.

public theorem isRegularRingHom_iff_isSeparableExtension (k : Type u) (K : Type v)
    [Field k] [Field K] [Algebra k K] :
    IsRegularRingHom (algebraMap k K) ↔ Algebra.IsSeparableExtension k K
Tag 07NT, a lemma

Tag 07NT in the Stacks Project.

isRegularRingHom_of_comp_of_flat_of_surjectiveOnSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/RegularRingHom.lean, line 1314.

If a composite ring homomorphism is regular and the second homomorphism is flat and surjective on prime spectra, then the first homomorphism is regular.

public theorem isRegularRingHom_of_comp_of_flat_of_surjectiveOnSpec
    {A : Type u} {B : Type v} {C : Type w}
    [CommRing A] [CommRing B] [CommRing C]
    (f : A →+* B) (g : B →+* C)
    (hgf : IsRegularRingHom (g.comp f))
    (hgflat : g.Flat)
    (hgsurj : Function.Surjective (PrimeSpectrum.comap g)) :
    IsRegularRingHom f
Sources
LeanIsRegularRingHom · isRegularRingHom_tfae_localizations · isRegularRingHom_baseChange · isRegularRingHom_comp · isRegularRingHom_of_filteredColimit_smooth · isRegularRingHom_iff_isSeparableExtension · isRegularRingHom_of_comp_of_flat_of_surjectiveOnSpec

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.