10.125 Dimension of fibres to 10.135 Local complete…

Section10.125 Dimension of fibres#

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

Tag 00QD, a definition

Tag 00QD in the Stacks Project.

Algebra.relativeDimensionAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RelativeDimension/Defs.lean, line 123. The attribute's comment: “The fibre Spec (S ⊗_R κ(𝔭)) is the homeomorphic subspace comap (algebraMap R S) ⁻¹' {𝔭} of Spec S, in which the source's point q̄ is 𝔮 itself, and 𝔭 = R ∩ 𝔮 is not an argument; dim_q̄ is topologicalKrullDimAt. The source's finite type hypothesis is unused by the definition and is left to the lemmas. See the module docstring.”. References: EGA IV (17.10.1), “affine case”.

The relative dimension of S/R at a prime 𝔮 of S, dim_𝔮(S/R): the dimension of the fibre of Spec S → Spec R through 𝔮 at the point 𝔮. The fibre is the subspace comap (algebraMap R S) ⁻¹' {𝔭} of Spec S, where 𝔭 = R ∩ 𝔮, which is homeomorphic to Spec (S ⊗_R κ(𝔭)) by PrimeSpectrum.preimageHomeomorphFiber.

public noncomputable def relativeDimensionAt (R : Type*) {S : Type*} [CommRing R] [CommRing S]
    [Algebra R S] (𝔮 : Ideal S) [𝔮.IsPrime] : WithBot ℕ∞

Algebra.relativeDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RelativeDimension/Defs.lean, line 133. The attribute's comment: “The supremum of Algebra.relativeDimensionAt R 𝔮 over all primes 𝔮 of S, indexed by Spec S. See the module docstring.”.

The relative dimension of S/R, dim(S/R): the supremum of the relative dimensions dim_𝔮(S/R) over all primes 𝔮 of S. It is -∞ exactly when S is the zero ring.

public noncomputable def relativeDimension (R S : Type*) [CommRing R] [CommRing S]
    [Algebra R S] : WithBot ℕ∞

Tag 00QE, a lemma

Tag 00QE in the Stacks Project.

quasiFinite_over_polynomial_of_relativeDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RelativeDimension/QuasiFinite.lean, line 1216.

Stacks tag 00QE (Lemma 10.125.2). Let R → S be a finite type ring map, q ⊂ S a prime lying over p = q ∩ R, with corresponding point qbar of the fibre spectrum Spec(S ⊗_R κ(p)). If the relative dimension dim_q(S/R) equals n : ℕ, then there is g ∈ S, g ∉ q, and an R-algebra ring map φ : R[t_1, …, t_n] → S_g such that S_g = S[1/g] is finite type and quasi-finite over R[t_1, …, t_n] via φ.

theorem quasiFinite_over_polynomial_of_relativeDimension
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
    (q : PrimeSpectrum S)
    (p : Ideal R) [hp : p.IsPrime]
    (qbar : PrimeSpectrum (p.Fiber S))
    (hqbar : PrimeSpectrum.comap (fiberMap R S p) qbar = q)
    (n : ℕ)
    (hdim : relativeDimensionAt R S p qbar = (n : ℕ∞)) :
    ∃ (g : S), g ∉ q.asIdeal ∧
      ∃ (φ : MvPolynomial (Fin n) R →+* Localization.Away g),
        φ.comp (algebraMap R (MvPolynomial (Fin n) R)) = algebraMap R (Localization.Away g) ∧
        φ.FiniteType ∧ φ.QuasiFinite

Tag 0520, a lemma

Tag 0520 in the Stacks Project.

Algebra.exists_quasiFinite_mvPolynomial_away_comap_map_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RelativeDimension/QuasiFiniteAffineSpace.lean, line 417. The attribute's comment: “R_f[x_1, …, x_n] is MvPolynomial (Fin n) (Localization.Away f), with x_{i+1} indexed by i : Fin n; the ideal (𝔭, x_{r+1}, …, x_n) is the sum of the extension of 𝔭 along the constants and the ideal generated by the variables indexed by {i | r ≤ i}. Quasi-finite is RingHom.QuasiFinite together with RingHom.FiniteType, and φ is recorded to be an R-algebra map. The algebra κ(𝔭) → κ(𝔮) is any one compatible with R.”.

Stacks 0520. Let R → S be a ring map of finite type and let 𝔮 ⊂ S be a prime lying over 𝔭 ⊂ R with dim_𝔮(S/R) = n and trdeg_{κ(𝔭)} κ(𝔮) = r. Then there are f ∈ R, f ∉ 𝔭, g ∈ S, g ∉ 𝔮 and a quasi-finite R-algebra map φ : R_f[x_1, …, x_n] → S_g with φ⁻¹(𝔮S_g) = (𝔭, x_{r+1}, …, x_n).

theorem Algebra.exists_quasiFinite_mvPolynomial_away_comap_map_eq
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
    (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    [Algebra p.ResidueField q.ResidueField] [IsScalarTower R p.ResidueField q.ResidueField]
    {n r : ℕ} (hn : Algebra.relativeDimensionAt R q = n)
    (hr : Algebra.trdeg p.ResidueField q.ResidueField = r) :
    ∃ f ∉ p, ∃ g ∉ q, ∃ φ : MvPolynomial (Fin n) (Localization.Away f) →+* Localization.Away g,
      φ.comp (C.comp (algebraMap R (Localization.Away f))) =
        algebraMap R (Localization.Away g) ∧
      φ.FiniteType ∧ φ.QuasiFinite ∧
      (q.map (algebraMap S (Localization.Away g))).comap φ =
        Ideal.map C (p.map (algebraMap R (Localization.Away f))) ⊔
          Ideal.span (X '' {i : Fin n | r ≤ (i : ℕ)})

Tag 00QF, a lemma

Tag 00QF in the Stacks Project.

Ideal.height_le_height_of_liesOver_of_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/Dimension.lean, line 242. The attribute's comment: “dim(S_𝔮) and dim(R_𝔭) are 𝔮.height and 𝔭.height, model-independently by IsLocalization.AtPrime.ringKrullDim_eq_height; quasi-finiteness at 𝔮 (Definition 00PL) is Algebra.QuasiFiniteAt R 𝔮, which the source's finite type hypothesis identifies with the source's notion by Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber, and which the conclusion needs without it. See the module docstring.”.

Stacks 00QF. Let R → S be a ring map, let 𝔮 be a prime of S lying over the prime 𝔭 of R, and assume R → S is quasi-finite at 𝔮. Then dim(S_𝔮) = 𝔮.height is at most dim(R_𝔭) = 𝔭.height. The source's finite type hypothesis is not needed.

public theorem Ideal.height_le_height_of_liesOver_of_quasiFiniteAt {R S : Type*} [CommRing R]
    [CommRing S] [Algebra R S] (𝔭 : Ideal R) (𝔮 : Ideal S) [𝔭.IsPrime] [𝔮.IsPrime]
    [𝔮.LiesOver 𝔭] [Algebra.QuasiFiniteAt R 𝔮] : 𝔮.height ≤ 𝔭.height

Tag 00QG, a lemma

Tag 00QG in the Stacks Project.

ringKrullDim_le_natCard_of_quasiFinite_mvPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/QuasiFinite/AffineSpaceDimension.lean, line 167. The attribute's comment: “The source's k[t_1, …, t_n] ⊂ S with S of finite type over k and the map quasi-finite is weakened to Algebra.QuasiFinite (MvPolynomial σ k) S with Finite σ, which the source's hypotheses imply (tag 00PM); neither finite type nor injectivity is used. See the module docstring.”.

Stacks 00QG. Let k be a field and let S be a quasi-finite algebra over the polynomial ring k[t_i ; i ∈ σ] in n = #σ variables. Then dim(S) ≤ n: a quasi-finite cover of affine n-space has dimension at most n.

public theorem ringKrullDim_le_natCard_of_quasiFinite_mvPolynomial (k : Type*) [Field k]
    {σ S : Type*} [Finite σ] [CommRing S] [Algebra (MvPolynomial σ k) S]
    [Algebra.QuasiFinite (MvPolynomial σ k) S] : ringKrullDim S ≤ Nat.card σ

Tag 00QH, a lemma

Tag 00QH in the Stacks Project.

Algebra.isOpen_setOf_relativeDimensionAt_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RelativeDimension/Semicontinuity.lean, line 332. The attribute's comment: “The source's open neighbourhood V of a single prime 𝔮 with dim_𝔮(S/R) = n is pinned as the sublevel set {𝔮 | dim_𝔮(S/R) ≤ n}, whose openness the remark following the lemma in the source gives as an equivalent reading of it; dim_𝔮(S/R) is Algebra.relativeDimensionAt R 𝔮 (tag 00QD). See the module docstring.”.

Stacks 00QH. Let R → S be a finite type ring map and let n : ℕ. The set of primes 𝔮 of S at which the fibre of Spec S → Spec R has dimension at most n, that is dim_𝔮(S/R) ≤ n, is open in Spec S. Equivalently, every prime 𝔮 with dim_𝔮(S/R) = n has an open neighbourhood V in Spec S such that dim_{𝔮'}(S/R) ≤ n for all 𝔮' ∈ V.

public theorem isOpen_setOf_relativeDimensionAt_le {R S : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.FiniteType R S] (n : ℕ) :
    IsOpen {𝔮 : PrimeSpectrum S |
      Algebra.relativeDimensionAt R 𝔮.asIdeal ≤ (n : WithBot ℕ∞)}

Tag 00QI, a lemma

Tag 00QI in the Stacks Project.

Algebra.IsPushout.relativeDimensionAt_comap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RelativeDimension/BaseChange.lean, line 195. The attribute's comment: “The source's equality of sublevel sets, for a bound n ≥ 0, is stated as the pointwise equality dim_{𝔮'}(S'/R') = dim_{f(𝔮')}(S/R) of relative dimensions, to which it is equivalent for all n at once; S' = R' ⊗_R S is the abstract Algebra.IsPushout R S R' S' and f is PrimeSpectrum.comap (algebraMap S S'). See the module docstring.”.

Let R → S be a finite type ring map, let R → R' be any ring map, let S' = R' ⊗_R S and let f : Spec S' → Spec S be the induced map on spectra. Then relative dimension is invariant under this base change: dim_{𝔮'}(S'/R') = dim_{f(𝔮')}(S/R) for every prime 𝔮' of S'. In particular, for n : ℕ, the inverse image f⁻¹({𝔮 | dim_𝔮(S/R) ≤ n}) is {𝔮' | dim_{𝔮'}(S'/R') ≤ n}.

public theorem relativeDimensionAt_comap_eq (R S R' S' : Type*) [CommRing R]
    [CommRing S] [CommRing R'] [CommRing S'] [Algebra R S] [Algebra R R'] [Algebra R' S']
    [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
    [Algebra.IsPushout R S R' S'] [Algebra.FiniteType R S] (𝔮' : PrimeSpectrum S') :
    Algebra.relativeDimensionAt R (PrimeSpectrum.comap (algebraMap S S') 𝔮').asIdeal =
      Algebra.relativeDimensionAt R' 𝔮'.asIdeal

Tag 00QJ, a lemma

Tag 00QJ in the Stacks Project.

Algebra.isCompact_isOpen_setOf_relativeDimensionAt_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RelativeDimension/Semicontinuity.lean, line 589. The attribute's comment: “"Quasi-compact open" is IsCompact V ∧ IsOpen V, in the order and form PrimeSpectrum.isCompact_isOpen_iff consumes; the second conjunct is tag 00QH for the underlying finite type ring map, the first is the content here. dim_𝔮(S/R) is Algebra.relativeDimensionAt R 𝔮 (tag 00QD). See the module docstring.”.

Stacks 00QJ. Let R → S be a ring map of finite presentation and let n : ℕ. The set V_n = {𝔮 ∈ Spec S | dim_𝔮(S/R) ≤ n} of primes at which the fibre of Spec S → Spec R has dimension at most n is a quasi-compact open subset of Spec S.

public theorem isCompact_isOpen_setOf_relativeDimensionAt_le {R S : Type*} [CommRing R]
    [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S] (n : ℕ) :
    IsCompact {𝔮 : PrimeSpectrum S |
        Algebra.relativeDimensionAt R 𝔮.asIdeal ≤ (n : WithBot ℕ∞)} ∧
      IsOpen {𝔮 : PrimeSpectrum S |
        Algebra.relativeDimensionAt R 𝔮.asIdeal ≤ (n : WithBot ℕ∞)}

Tag 00QK, a lemma

Tag 00QK in the Stacks Project.

ValuationRing.ringKrullDim_fiber_maximalIdeal_eq_ringKrullDim_fiber_bot_and_equidimensional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RelativeDimension/ValuationRing.lean, line 809. The attribute's comment: “S ⊗_R k is the fibre (IsLocalRing.maximalIdeal R).Fiber S and S ⊗_R K the fibre (⊥ : Ideal R).Fiber S, the residue fields κ(𝔪_R) and κ(⊥) being k and K because R is a local domain; dim is ringKrullDim and equidimensionality is Definition 0058. S a domain containing R is [IsDomain S] with [FaithfulSMul R S]. See the module docstring.”. References: EGA IV (14.3.10), “affine case”.

Stacks 00QK. Let R be a valuation ring with residue field k and fraction field K, and let S be a domain containing R which is of finite type over R. If S ⊗_R k is not the zero ring, then dim (S ⊗_R k) = dim (S ⊗_R K), and in fact Spec (S ⊗_R k) is equidimensional, so that each of its irreducible components has dimension dim (S ⊗_R K).

public theorem ringKrullDim_fiber_maximalIdeal_eq_ringKrullDim_fiber_bot_and_equidimensional
    {R S : Type*} [CommRing R] [IsDomain R] [ValuationRing R] [CommRing S] [IsDomain S]
    [Algebra R S] [FaithfulSMul R S] [Algebra.FiniteType R S]
    (hfib : Nontrivial ((IsLocalRing.maximalIdeal R).Fiber S)) :
    ringKrullDim ((IsLocalRing.maximalIdeal R).Fiber S) =
        ringKrullDim ((⊥ : Ideal R).Fiber S) ∧
      TopologicalSpace.Equidimensional
        (PrimeSpectrum ((IsLocalRing.maximalIdeal R).Fiber S))

Sources

• Section 10.125, Tag 00QC
• AxiomMath/Stacks at 5ed82d14

LeanAlgebra.relativeDimensionAt · Algebra.relativeDimension · quasiFinite_over_polynomial_of_relativeDimension · Algebra.exists_quasiFinite_mvPolynomial_away_comap_map_eq · Ideal.height_le_height_of_liesOver_of_quasiFiniteAt · ringKrullDim_le_natCard_of_quasiFinite_mvPolynomial · Algebra.isOpen_setOf_relativeDimensionAt_le · Algebra.IsPushout.relativeDimensionAt_comap_eq

Section10.126 Algebras and modules of finite presentation#

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

Tag 00QP, a lemma

Tag 00QP in the Stacks Project.

Algebra.FiniteType.iff_finiteType_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Descent.lean, line 317. References: SGA 1 VIII (3.4); SGA 1 VIII (3.3), “finite type, affine”.

Stacks 00QP. Being of finite type descends along a faithfully flat base change: for a faithfully flat R-algebra R', an R-algebra S is of finite type if and only if R' ⊗[R] S is of finite type over R'.

theorem Algebra.FiniteType.iff_finiteType_tensorProduct
    (R S R' : Type*) [CommRing R] [CommRing S] [CommRing R']
    [Algebra R S] [Algebra R R'] [Module.FaithfullyFlat R R'] :
    Algebra.FiniteType R S ↔ Algebra.FiniteType R' (R' ⊗[R] S)

Tag 00QQ, a lemma

Tag 00QQ in the Stacks Project.

Declarations registered for the tag:

• Algebra.FinitePresentation.baseChange registered with add_to_stacks in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Descent.lean, line 331 (StacksFrontier): “a base change of an algebra of finite presentation is of finite presentation”. References: EGA IV (8.6.2), “special case”; EGA IV (1.4.1); EGA IV (1.4.3), “(iii), special case”; EGA IV (1.6.2), “(iii), special case”; SGA 1 VIII (3.6), “partial”; SGA 3 XIX (2.1), “special case”.
• Algebra.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat registered with add_to_stacks in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Descent.lean, line 333 (StacksFrontier): “finite presentation descends along a faithfully flat base change”. References: EGA IV (2.7.1), “special case”; EGA IV (2.7.1.1), “partial”; SGA 1 VIII (3.6), “affine case”; SGA 3 VIB (10.8), “special case”; SGA 3 XIX (2.1), “special case”; SGA 6 VIII (1.6), “special case”.

Tag 05N5, a lemma

Tag 05N5 in the Stacks Project.

Module.exists_finite_isBaseChange_of_surjective_algebraMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Descent.lean, line 667. The attribute's comment: “Stated for an arbitrary surjection Rₛ → R' from a localization Rₛ = S⁻¹R in place of R' = S⁻¹(R/I), of which it is the case R' = Rₛ ⧸ I·Rₛ; S⁻¹(M/IM) is the base change R' ⊗_R M, pinned by IsBaseChange R' g for the source's map g : M → M'. Items (1) and (2) are the two conjuncts.”.

Stacks 05N5. Let R be a ring, S ⊆ R a multiplicative subset, Rₛ = S⁻¹R and let R' be a quotient of Rₛ (for instance R' = S⁻¹(R/I) = Rₛ/I·Rₛ for an ideal I ⊆ R). For every finite R'-module M' there is a finite R-module M and an R-linear map g : M → M' exhibiting M' as the base change R' ⊗_R M, i.e. as S⁻¹(M/IM); and if M' is finitely presented over R', then M may be taken finitely presented over R.

theorem exists_finite_isBaseChange_of_surjective_algebraMap {R : Type u} [CommRing R]
    (S : Submonoid R) (Rₛ : Type v) [CommRing Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ]
    {R' : Type w} [CommRing R'] [Algebra R R'] [Algebra Rₛ R'] [IsScalarTower R Rₛ R']
    (M' : Type t) [AddCommGroup M'] [Module R M'] [Module R' M'] [IsScalarTower R R' M']
    [Module.Finite R' M'] (hsurj : Function.Surjective (algebraMap Rₛ R')) :
    ∃ (M : Type u) (_ : AddCommGroup M) (_ : Module R M) (g : M →ₗ[R] M'),
      Module.Finite R M ∧ IsBaseChange R' g ∧
        (Module.FinitePresentation R' M' → Module.FinitePresentation R M)

Tag 05N6, a lemma

Tag 05N6 in the Stacks Project.

Module.exists_finite_isLocalizedModule_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Descent.lean, line 478. The attribute's comment: “Localizations are abstract (IsLocalization S Rₛ, IsLocalizedModule S f); the induced isomorphism S⁻¹M' → S⁻¹M is pinned as IsLocalizedModule S (f ∘ₗ φ); M' is produced in the universe of R. Items (1) and (2) are the two conjuncts, (2) as an implication about the same M'.”.

Stacks 05N6. Let R be a ring, S ⊆ R a multiplicative subset, M an R-module and f : M → Mₛ a localization of M at S, over a localization Rₛ of R at S.

1. If Mₛ = S⁻¹M is a finite Rₛ-module, then there is a finite R-module M' and an R-linear map φ : M' → M inducing an isomorphism S⁻¹M' ≅ S⁻¹M, spelled IsLocalizedModule S (f ∘ₗ φ).
2. If Mₛ is moreover a finitely presented Rₛ-module, then M' is of finite presentation over R.

theorem exists_finite_isLocalizedModule_comp {R : Type u} [CommRing R] (S : Submonoid R)
    (Rₛ : Type v) [CommRing Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ]
    {M : Type w} [AddCommGroup M] [Module R M]
    {Mₛ : Type t} [AddCommGroup Mₛ] [Module R Mₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ]
    (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] [Module.Finite Rₛ Mₛ] :
    ∃ (M' : Type u) (_ : AddCommGroup M') (_ : Module R M') (φ : M' →ₗ[R] M),
      Module.Finite R M' ∧ IsLocalizedModule S (f ∘ₗ φ) ∧
        (Module.FinitePresentation Rₛ Mₛ → Module.FinitePresentation R M')

Tag 05GJ, a lemma

Tag 05GJ in the Stacks Project.

Module.exists_finite_isLocalizedModule_comp_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Descent.lean, line 527. The attribute's comment: “The case S = p.primeCompl of 05N6 (Module.exists_finite_isLocalizedModule_comp), stated in the same shape: localizations are abstract, the induced isomorphism M'ₚ → Mₚ is pinned as IsLocalizedModule p.primeCompl (f ∘ₗ φ), M' is produced in the universe of R, and items (1) and (2) are the two conjuncts, (2) as an implication about the same M'.”.

Stacks 05GJ. Let R be a ring, p ⊆ R a prime ideal, M an R-module and f : M → Mₚ a localization of M at p.primeCompl, over a localization Rₚ of R at p.

1. If Mₚ is a finite Rₚ-module, then there is a finite R-module M' and an R-linear map φ : M' → M inducing an isomorphism M'ₚ ≅ Mₚ, spelled IsLocalizedModule p.primeCompl (f ∘ₗ φ).
2. If Mₚ is moreover a finitely presented Rₚ-module, then M' is of finite presentation over R.

theorem exists_finite_isLocalizedModule_comp_atPrime {R : Type u} [CommRing R]
    (p : Ideal R) [p.IsPrime]
    (Rₚ : Type v) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p]
    {M : Type w} [AddCommGroup M] [Module R M]
    {Mₚ : Type t} [AddCommGroup Mₚ] [Module R Mₚ] [Module Rₚ Mₚ] [IsScalarTower R Rₚ Mₚ]
    (f : M →ₗ[R] Mₚ) [IsLocalizedModule p.primeCompl f] [Module.Finite Rₚ Mₚ] :
    ∃ (M' : Type u) (_ : AddCommGroup M') (_ : Module R M') (φ : M' →ₗ[R] M),
      Module.Finite R M' ∧ IsLocalizedModule p.primeCompl (f ∘ₗ φ) ∧
        (Module.FinitePresentation Rₚ Mₚ → Module.FinitePresentation R M')

Tag 00QR, a lemma

Tag 00QR in the Stacks Project.

exists_away_prod_of_localRingHom_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/SpreadingOut/LocalIsomorphism/ProductSplitting.lean, line 429.

Let φ : R → S be a ring map of commutative rings, and let q ⊆ S be a prime ideal lying over the prime p ⊆ R (i.e. p = q.comap φ). Assume S is of finite presentation over R, and that the induced map on localizations φ_p : R_p → S_q (Localization.localRingHom) is bijective. Then there exist f : R with f ∉ p and an R_f-algebra C such that S_f ≅ R_f × C as R_f-algebras, where S_f := Localization.Away (φ f) is given the R_f-algebra structure induced by Localization.awayMap φ f.

theorem exists_away_prod_of_localRingHom_bijective (R S : Type) [CommRing R] [CommRing S] [Algebra R
  S] (p : Ideal R) [p.IsPrime]
    (q : Ideal S) [q.IsPrime] (hpq : p = q.comap (algebraMap R S)) [Algebra.FinitePresentation R S]
    (hiso : Function.Bijective (Localization.localRingHom p q (algebraMap R S) hpq)) :
    ∃ f : R,
      f ∉ p ∧
        ∃ (C : Type) (_ : CommRing C) (_ : Algebra (Localization.Away f) C),
          letI : Algebra (Localization.Away f) (Localization.Away (algebraMap R S f)) :=
            (Localization.awayMap (algebraMap R S) f).toAlgebra
          Nonempty
            (Localization.Away (algebraMap R S f) ≃ₐ[Localization.Away f]
              (Localization.Away f × C))

Tag 00QS, a lemma

Tag 00QS in the Stacks Project.

Algebra.FinitePresentation.exists_algEquiv_localizationAway_of_algEquiv_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/SpreadingOut/LocalIsomorphism/AwayIsomorphism.lean, line 484. The attribute's comment: “The local rings S_q, S'_{q'} are abstract (IsLocalization.AtPrime Sq q with IsScalarTower R S Sq, so that the R-algebra structure is the composite R → S → Sq), which makes the hypothesis available for any model; the localizations S_g, S'_{g'} of the conclusion are the models Localization.Away g, Localization.Away g', a choice that costs no strength by uniqueness of localizations. As in the source only the existence of an R-algebra isomorphism is claimed, not the compatibility with the given isomorphism of local rings that the proof also produces. See the module docstring.”.

Let R be a ring, let S and S' be R-algebras of finite presentation, and let q ⊆ S, q' ⊆ S' be primes. If the local rings S_q and S'_{q'} are isomorphic as R-algebras, then there are g ∈ S, g ∉ q and g' ∈ S', g' ∉ q' such that S_g and S'_{g'} are isomorphic as R-algebras.

public theorem exists_algEquiv_localizationAway_of_algEquiv_atPrime {R : Type u} [CommRing R]
    {S : Type v} [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S] {S' : Type v'}
    [CommRing S'] [Algebra R S'] [Algebra.FinitePresentation R S'] (q : Ideal S) [q.IsPrime]
    (q' : Ideal S') [q'.IsPrime] (Sq : Type w) [CommRing Sq] [Algebra S Sq]
    [IsLocalization.AtPrime Sq q] [Algebra R Sq] [IsScalarTower R S Sq] (Sq' : Type w')
    [CommRing Sq'] [Algebra S' Sq'] [IsLocalization.AtPrime Sq' q'] [Algebra R Sq']
    [IsScalarTower R S' Sq'] (e : Sq ≃ₐ[R] Sq') :
    ∃ g ∉ q, ∃ g' ∉ q', Nonempty (Localization.Away g ≃ₐ[R] Localization.Away g')

Tag 0G8U, a lemma

Tag 0G8U in the Stacks Project.

finiteType_of_isNilpotent_quotient_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nilpotent/Descent.lean, line 437. References: SGA 3 VIB (1.3.0), “(i)”.

Stacks Tag 0G8U (Lemma 10.126.8). Let R be a ring, let I be a nilpotent ideal of R, and let S be an R-algebra such that the induced ring map R ⧸ I → S ⧸ IS is of finite type. Then the structure map R → S is of finite type.

theorem finiteType_of_isNilpotent_quotient_finiteType
    (R : Type*) [CommRing R] (I : Ideal R)
    (S : Type*) [CommRing S] [Algebra R S]
    (hI : IsNilpotent I)
    (hft : Algebra.FiniteType (R ⧸ I) (S ⧸ I.map (algebraMap R S))) :
    Algebra.FiniteType R S

Tag 07RD, a lemma

Tag 07RD in the Stacks Project.

surjective_of_surjective_mod_locallyNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nilpotent/Descent.lean, line 260.

Stacks Tag 07RD. Let R be a commutative ring, I ⊆ R a locally nilpotent ideal, and f : S →ₐ[R] S' an R-algebra map such that the induced map S → S'/IS' is surjective and S' is of finite type over R. Then f is surjective.

The proof is the Stacks 07RD argument, reorganized to avoid the R₀ reduction by observing that the finitely many nilpotent coefficients generate a nilpotent ideal directly via Tag 00IM with J = ⊥.

Let P := MvPolynomial ι R for a Fintype ι. Since S' is finite type over R, choose a surjective R-algebra hom φ : P →ₐ[R] S' (generators xⱼ := φ (X j)).

hsurj says π ∘ f is surjective, where π = Ideal.Quotient.mk (IS'). Hence for each j there is sⱼ ∈ S with π (xⱼ) = π (f sⱼ), i.e. xⱼ - f sⱼ ∈ IS' = Ideal.map (algebraMap R S') I.

An element of IS' is a finite sum Σ_k (algebraMap aₖ)·bₖ with aₖ ∈ I, bₖ ∈ S'. Lift each bₖ through φ to βₖ ∈ P, and set h j := Σ_k (C aₖ) · βₖ ∈ P, so that φ (h j) = xⱼ - f sⱼ. Define g j := X j - h j, whence φ (g j) = xⱼ - (xⱼ - f sⱼ) = f sⱼ ∈ range f.

Let 𝔫 ⊆ R be the ideal generated by the finite set {aₖ} of coefficients used above. Each aₖ ∈ I is nilpotent (hI), so 𝔫 ≤ (⊥ : Ideal R).radical (the nilradical); and 𝔫 is finitely generated. By Tag 00IM (Ideal.exists_pow_le_of_le_radical_of_fg) there is N with 𝔫 ^ N ≤ ⊥, i.e. 𝔫 ^ N = ⊥: 𝔫 is nilpotent. Put 𝔐 := Ideal.map C 𝔫 ⊆ P; then 𝔐 ^ N ≤ Ideal.map C (𝔫 ^ N) = ⊥, so 𝔐 is nilpotent, and each h j ∈ 𝔐 (it is a combination of C aₖ with aₖ ∈ 𝔫).

By aeval_sub_nilpotent_surjective, σ := aeval g : P →ₐ[R] P is surjective. Therefore the R-subalgebra of P generated by {g j} is ⊤ (it contains σ.range = ⊤, and Algebra.adjoin R {g j} = σ.range). Applying φ: S' = φ '' P = φ '' (adjoin R \{g j}) = Algebra.adjoin R \{φ (g j)} = Algebra.adjoin R \{f sⱼ} ≤ (f.range : Subalgebra R S'), since each f sⱼ ∈ f.range and f.range is an R-subalgebra. Hence f.range = ⊤, i.e. f is surjective. ∎

theorem surjective_of_surjective_mod_locallyNilpotent
    (I : Ideal R) (hI : I.IsLocallyNilpotent)
    (f : S →ₐ[R] S')
    (hsurj : Function.Surjective
      ((Ideal.Quotient.mk (extendedIdeal I S')).comp f.toRingHom))
    (hft : Algebra.FiniteType R S') :
    Function.Surjective f

Tag 087P, a lemma

Tag 087P in the Stacks Project.

isomorphism_of_flat_surjective_087P, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/SpreadingOut/Away.lean, line 334.

Stacks Tag 087P (Lemma 10.126.10). Under the stated hypotheses there is g ∈ S, g ∉ q, with φ_g : S_g → S'_g an isomorphism (i.e. bijective).

theorem isomorphism_of_flat_surjective_087P
    (hIq : I.map (algebraMap R S) ≤ q)
    (hsurj : Function.Surjective (φ : S → S'))
    (hiso : Function.Bijective (phiqBar I φ q Sq S'q))
    (hft : (algebraMap R S).FiniteType)
    (hfp : (algebraMap R S').FinitePresentation)
    (hflat : Module.Flat R S'q) :
    ∃ g : S, g ∉ q ∧ Function.Bijective (phig φ g)

Tag 07RE, a lemma

Tag 07RE in the Stacks Project.

AlgHom.bijective_of_bijective_quotientMapₐ_of_le_nilradical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Descent.lean, line 743. The attribute's comment: “That I consists of nilpotents is spelled I ≤ nilradical R, the source's S/IS → S'/IS' is Ideal.quotientMapₐ applied to f, and finite type, finite presentation and flatness are instance arguments.”. References: SGA 1 III (4.2), “affine case + finiteness”.

Stacks 07RE. Let I ⊆ R be an ideal all of whose elements are nilpotent, let S be of finite type over R and let S' be of finite presentation and flat over R. If an R-algebra map f : S →ₐ[R] S' induces a bijection S/IS → S'/IS', then f is bijective.

theorem AlgHom.bijective_of_bijective_quotientMapₐ_of_le_nilradical
    {R : Type u} [CommRing R] {S : Type v} [CommRing S] {S' : Type w} [CommRing S']
    [Algebra R S] [Algebra R S'] [Algebra.FiniteType R S] [Algebra.FinitePresentation R S']
    [Module.Flat R S'] (I : Ideal R) (hI : I ≤ nilradical R) (f : S →ₐ[R] S')
    (hf : Function.Bijective
      (Ideal.quotientMapₐ (I.map (algebraMap R S')) f
          (Ideal.map_le_iff_le_comap.mpr fun x hx ↦
            show f (algebraMap R S x) ∈ I.map (algebraMap R S') from
              f.commutes x ▸ Ideal.mem_map_of_mem _ hx) :
        S ⧸ I.map (algebraMap R S) →ₐ[R] S' ⧸ I.map (algebraMap R S'))) :
    Function.Bijective f

Sources

• Section 10.126, Tag 05N4
• AxiomMath/Stacks at 5ed82d14

LeanAlgebra.FiniteType.iff_finiteType_tensorProduct · Algebra.FinitePresentation.baseChange · Algebra.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat · Module.exists_finite_isBaseChange_of_surjective_algebraMap · Module.exists_finite_isLocalizedModule_comp · Module.exists_finite_isLocalizedModule_comp_atPrime · exists_away_prod_of_localRingHom_bijective · Algebra.FinitePresentation.exists_algEquiv_localizationAway_of_algEquiv_atPrime

Section10.127 Colimits and maps of finite presentation#

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

Tag 0BUF, a lemma

Tag 0BUF in the Stacks Project.

CommRingCat.isFiltered_costructuredArrow_and_isDenseAt_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ColimitPresentation/Canonical.lean, line 407. The attribute's comment: “The category 𝓘 is CostructuredArrow P.ι A for P the property of being of finite presentation over R, and "the colimit of the A' is A" is P.ι.isDenseAt A, which pins the colimit cocone to the tautological one. No smallness device is needed. See the module docstring.”. References: EGA IV (1.9.3.1), “more general”.

Let R → A be a ring map and let 𝓘 = CostructuredArrow P.ι A be the category of R-algebra maps A' → A with A' of finite presentation over R. Then 𝓘 is filtered, and A is the colimit of the A' over 𝓘, via the tautological cocone whose leg at A' → A is that map (which is what Functor.isDenseAt asserts).

public theorem isFiltered_costructuredArrow_and_isDenseAt_finitePresentation
    {R : CommRingCat.{u}} (A : Under R) :
    IsFiltered (CostructuredArrow
        (ObjectProperty.ι fun B : Under R ↦ B.hom.hom.FinitePresentation) A) ∧
      (ObjectProperty.ι fun B : Under R ↦ B.hom.hom.FinitePresentation).isDenseAt A

Tag 00QN, a lemma

Tag 00QN in the Stacks Project.

Algebra.exists_directedSystem_finitePresentation_lift_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Algebra/DirectLimit/FinitePresentation.lean, line 406. The attribute's comment: “Both sentences. The second is the implication Algebra.FiniteType R A → ∀ i j h, Function.Surjective (f i j h) inside the same existential, which is equivalent to stating it separately; A = colim G l is bijectivity of DirectLimit.Algebra.lift, which pins the comparison map. See the module docstring.”.

Every algebra is a direct limit of algebras of finite presentation. For a ring map R → A there is a directed system G of R-algebras of finite presentation, indexed by a directed partially ordered set Λ, together with a compatible family of R-algebra maps g l : G l →ₐ[R] A whose induced map colim_l G l → A is bijective. If A is of finite type over R, the system can moreover be chosen with all transition maps surjective.

public theorem Algebra.exists_directedSystem_finitePresentation_lift_bijective
    (R : Type u) [CommRing R] (A : Type v) [CommRing A] [Algebra R A] :
    ∃ (Λ : Type (max u v)) (_ : PartialOrder Λ) (_ : Nonempty Λ) (_ : IsDirectedOrder Λ)
      (G : Λ → Type (max u v)) (_ : ∀ l, CommRing (G l)) (_ : ∀ l, Algebra R (G l))
      (f : ∀ i j, i ≤ j → G i →ₐ[R] G j) (_ : DirectedSystem G fun i j h ↦ ⇑(f i j h))
      (g : ∀ l, G l →ₐ[R] A) (hg : ∀ i j h x, g j (f i j h x) = g i x),
      (∀ l, Algebra.FinitePresentation R (G l)) ∧
      (Algebra.FiniteType R A → ∀ i j (h : i ≤ j), Function.Surjective (f i j h)) ∧
      Function.Bijective (DirectLimit.Algebra.lift G f A g hg)

Tag 00QO, a lemma

Tag 00QO in the Stacks Project.

CommRingCat.isFinitelyPresentable_under_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/FinitePresentation.lean, line 293. The attribute's comment: “Item (2) is IsFinitelyPresentable in Under R, which is bijectivity of colim Homᵣ(S, A_λ) → Homᵣ(S, colim A_λ) for every filtered system (Lemma 0032 identifies these with directed ones); item (3) is the surjectivity of that map, spelled as factoring a map through a member of the system, for every partially ordered directed system, the form Lemma 00QN provides. Both departures strengthen the equivalence. See the module docstring.”. References: EGA IV (8.14.2.2), “more general”; EGA IV (8.8.2.3), “f.p. => bijective”; EGA IV (8.8.2.1), “f.p. case: bijective”; EGA IV (8.13.1), “affine case, bijective”; EGA IV (8.14.2), “X, S affine”; EGA IV (8.14.2.2), “more general”.

Algebras of finite presentation are the finitely presentable objects. For an R-algebra S, the following are equivalent: S is of finite presentation over R; S is a finitely presentable object of the category Under R of R-algebras, that is colim_λ Homᵣ(S, A_λ) → Homᵣ(S, colim_λ A_λ) is bijective for every filtered system of R-algebras; and every R-algebra map from S to the colimit of a directed system of R-algebras factors through one of its members, that is the same comparison map is merely surjective.

public theorem isFinitelyPresentable_under_tfae {R : CommRingCat.{u}} (S : Under R) :
    List.TFAE
      [ S.hom.hom.FinitePresentation,
        IsFinitelyPresentable.{u} S,
        ∀ (Λ : Type u) [PartialOrder Λ] [Nonempty Λ] [IsDirected Λ (· ≤ ·)]
          (A : Λ ⥤ Under R) (c : Cocone A), IsColimit c → ∀ g : S ⟶ c.pt,
            ∃ (l : Λ) (g' : S ⟶ A.obj l), g' ≫ c.ι.app l = g ]

Tag 07C3, a lemma

Tag 07C3 in the Stacks Project.

CommRingCat.ind_under_iff_exists_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/FinitePresentation.lean, line 514. The attribute's comment: “The family 𝓔 is an E : ObjectProperty (Under R) on the category Under R of R-algebras, and "Λ is a filtered colimit of members of 𝓔" is Mathlib's ObjectProperty.ind.{u} E Λ. E is not assumed small; the source's set-theoretic hypothesis is only a smallness device. See the module docstring.”.

Criterion for being a filtered colimit of algebras of a given family. Let R → Λ be a ring map and let E be a family of R-algebras of finite presentation over R. Then Λ is a filtered colimit of members of E if and only if every R-algebra map A → Λ with A of finite presentation over R factors as A → B → Λ with B in E.

public theorem ind_under_iff_exists_factorization {R : CommRingCat.{u}} (Λ : Under R)
    {E : ObjectProperty (Under R)} (hE : E ≤ fun B : Under R ↦ B.hom.hom.FinitePresentation) :
    ObjectProperty.ind.{u} E Λ ↔
      ∀ A : Under R, A.hom.hom.FinitePresentation → ∀ f : A ⟶ Λ,
        ∃ (B : Under R) (g : A ⟶ B) (h : B ⟶ Λ), g ≫ h = f ∧ E B

Tag 05LI, a lemma

Tag 05LI in the Stacks Project.

Stacks.FinitePresentation.ColimitDescent.statement_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/ModuleDescent/ColimitRing.lean, line 598. The attribute's comment: “(2)”.

Statement (2). If N is a finite A-module and u : M → N has surjective base change to R, then its base change to some R_i is surjective.

theorem statement_two
    (htrans : TransitionSystem φ) (hcocone : IsCoconeAlg φ ψ)
    (hcolimN : IsModuleColimit φ ψ N)
    (hN : Module.Finite A N)
    (u : M →ₗ[A] N)
    (h : Function.Surjective (LinearMap.baseChange S u)) :
    ∃ i : ι, Function.Surjective (LinearMap.baseChange (R i) u)

Stacks.FinitePresentation.ColimitDescent.statement_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/ModuleDescent/LinearMapDescent.lean, line 115. The attribute's comment: “(3)”.

Statement (3). If N is a finitely presented A-module and v : N ⊗_A R → M ⊗_A R is an R-module map, then there is some i and an R_i-module map v_i : N ⊗_A R_i → M ⊗_A R_i whose base change along ψ i : R_i → S (i.e. composition with the canonical identification maps) recovers v. Concretely, v composed with the canonical map for N equals the canonical map for M composed with v_i.

theorem statement_three
    (htrans : TransitionSystem φ) (hcocone : IsCoconeAlg φ ψ)
    (hcolimM : IsModuleColimit φ ψ M)
    (hN : Module.FinitePresentation A N)
    (v : S ⊗[A] N →ₗ[S] S ⊗[A] M) :
    ∃ (i : ι) (vi : (R i) ⊗[A] N →ₗ[R i] (R i) ⊗[A] M),
      (v.restrictScalars A) ∘ₗ (canonMod ψ N i)
        = (canonMod ψ M i) ∘ₗ (vi.restrictScalars A)

Stacks.FinitePresentation.ColimitDescent.statement_four, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/ModuleDescent/LinearMapDescent.lean, line 305. The attribute's comment: “(4)”.

Statement (4). If M is finite, N is finitely presented, and u : M → N has base change to R an isomorphism, then its base change to some R_i is an isomorphism.

theorem statement_four
    (htrans : TransitionSystem φ) (hcocone : IsCoconeAlg φ ψ)
    (hcolimM : IsModuleColimit φ ψ M) (hcolimN : IsModuleColimit φ ψ N)
    (hM : Module.Finite A M) (hN : Module.FinitePresentation A N)
    (u : M →ₗ[A] N)
    (h : Function.Bijective (LinearMap.baseChange S u)) :
    ∃ i : ι, Function.Bijective (LinearMap.baseChange (R i) u)

Stacks.FinitePresentation.ColimitDescent.statement_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/ModuleDescent/ModuleColimit.lean, line 233. The attribute's comment: “(1)”.

Statement (1). If M is a finite A-module and u, u' : M → N are A-module maps whose base changes to R agree, then their base changes to some R_i already agree.

theorem statement_one
    (hcolimN : IsModuleColimit φ ψ N)
    (hM : Module.Finite A M)
    (u u' : M →ₗ[A] N)
    (h : LinearMap.baseChange S u = LinearMap.baseChange S u') :
    ∃ i : ι, LinearMap.baseChange (R i) u = LinearMap.baseChange (R i) u'

Tag 05N7, a lemma

Tag 05N7 in the Stacks Project.

Module.exists_finitePresentation_and_baseChange_eq_of_lift_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/DirectLimit/FinitePresentation.lean, line 295. The attribute's comment: “The colimit is a DirectedSystem of A-algebras whose comparison map colim_j S j → R is bijective, as in 00QN; items (2) and (3) are stated over an arbitrary base ring A and with the finiteness hypotheses of 05LI (3) and (1), of which they are instances, the source's form being A = R_λ and the system restricted to μ ≥ λ; φ = φ_μ ⊗ 1_R is the commuting square with the canonical maps LinearMap.rTensor M (algebraMap (S j) R). See the module docstring.”. References: EGA IV (8.5.3), “affine case”.

Let A be a ring, let S be a directed system of A-algebras over a nonempty directed preorder J with transition maps f i j : S i →ₐ[A] S j, and let R be an A-algebra receiving compatible maps algebraMap (S j) R which exhibit it as the colimit colim_j S j. Then the category of finitely presented R-modules is the colimit of the categories of finitely presented S j-modules:

1. every finitely presented R-module M is isomorphic to the base change R ⊗[S j] M_j of a finitely presented S j-module, for some j;
2. for A-modules M, N with M finitely presented, every R-linear map R ⊗[A] M → R ⊗[A] N is the base change of an S j-linear map S j ⊗[A] M → S j ⊗[A] N for some j, in the sense that the square with the canonical maps S j ⊗[A] M → R ⊗[A] M commutes;
3. for A-modules M, N with M finite, two A-linear maps u, u' : M → N with u ⊗ 1_R = u' ⊗ 1_R satisfy u ⊗ 1_{S j} = u' ⊗ 1_{S j} for some j.

public theorem exists_finitePresentation_and_baseChange_eq_of_lift_bijective
    {J : Type w} [Preorder J] [Nonempty J] [IsDirectedOrder J] {A : Type u} [CommRing A]
    {S : J → Type v} [∀ j, CommRing (S j)] [∀ j, Algebra A (S j)]
    (f : ∀ i j, i ≤ j → S i →ₐ[A] S j) [DirectedSystem S fun i j h ↦ ⇑(f i j h)]
    {R : Type v} [CommRing R] [Algebra A R] [∀ j, Algebra (S j) R]
    [∀ j, IsScalarTower A (S j) R]
    (hf : ∀ i j (h : i ≤ j) (x : S i), algebraMap (S j) R (f i j h x) = algebraMap (S i) R x)
    (hR : Function.Bijective (DirectLimit.Algebra.lift S f R
      (fun j ↦ IsScalarTower.toAlgHom A (S j) R) hf)) :
    (∀ (M : Type t) [AddCommGroup M] [Module R M] [Module.FinitePresentation R M],
        ∃ (j : J) (Mj : Type v) (_ : AddCommGroup Mj) (_ : Module (S j) Mj),
          Module.FinitePresentation (S j) Mj ∧ Nonempty (R ⊗[S j] Mj ≃ₗ[R] M)) ∧
    (∀ (M : Type t) [AddCommGroup M] [Module A M] [Module.FinitePresentation A M]
        (N : Type t') [AddCommGroup N] [Module A N] (φ : R ⊗[A] M →ₗ[R] R ⊗[A] N),
        ∃ (j : J) (φj : S j ⊗[A] M →ₗ[S j] S j ⊗[A] N), ∀ x : S j ⊗[A] M,
          φ (LinearMap.rTensor M (IsScalarTower.toAlgHom A (S j) R).toLinearMap x) =
            LinearMap.rTensor N (IsScalarTower.toAlgHom A (S j) R).toLinearMap (φj x)) ∧
    (∀ (M : Type t) [AddCommGroup M] [Module A M] [Module.Finite A M]
        (N : Type t') [AddCommGroup N] [Module A N] (u u' : M →ₗ[A] N),
        u.baseChange R = u'.baseChange R →
          ∃ j : J, u.baseChange (S j) = u'.baseChange (S j))

Tag 05N8, a lemma

Tag 05N8 in the Stacks Project.

Algebra.TensorProduct.exists_of_directLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Algebra/DirectLimit/Hom.lean, line 757. The attribute's comment: “The four items are the four conjuncts, each carrying only its own finiteness hypothesis. B ⊗_A R is R ⊗[A] B and u ⊗ 1 is Algebra.TensorProduct.lTensor; R = colim_i R_i is bijectivity of DirectLimit.Algebra.lift, as in 00QN; item (3)'s v = v_i ⊗ 1 is the commuting square with the comparison maps rTensor _ (g i). See the module docstring.”.

Stacks 05N8. Let A be a ring, let B, C be A-algebras, and let R be the colimit of a directed system G of A-algebras with transition maps f and structure maps g i : G i →ₐ[A] R.

1. If B is of finite type over A and u, u' : B →ₐ[A] C satisfy u ⊗ 1 = u' ⊗ 1 over R, then u ⊗ 1 = u' ⊗ 1 over G i for some i.
2. If C is of finite type over A and u ⊗ 1 is surjective over R, then u ⊗ 1 is surjective over G i for some i.
3. If C is of finite presentation over A, then every R-algebra map v : R ⊗[A] C →ₐ[R] R ⊗[A] B is the base change of a G i-algebra map vᵢ : G i ⊗[A] C →ₐ[G i] G i ⊗[A] B for some i.
4. If B is of finite type and C of finite presentation over A and u ⊗ 1 is bijective over R, then u ⊗ 1 is bijective over G i for some i.

public theorem exists_of_directLimit {A : Type u} [CommRing A]
    {B : Type v} [CommRing B] [Algebra A B] {C : Type w} [CommRing C] [Algebra A C]
    {ι : Type t} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
    {G : ι → Type s} [∀ i, CommRing (G i)] [∀ i, Algebra A (G i)]
    (f : ∀ i j, i ≤ j → G i →ₐ[A] G j) [DirectedSystem G fun i j h ↦ ⇑(f i j h)]
    {R : Type r} [CommRing R] [Algebra A R] (g : ∀ i, G i →ₐ[A] R)
    (hg : ∀ i j h x, g j (f i j h x) = g i x)
    (hR : Function.Bijective (DirectLimit.Algebra.lift G f R g hg)) :
    (Algebra.FiniteType A B → ∀ u u' : B →ₐ[A] C,
        lTensor (S := R) R u = lTensor (S := R) R u' →
        ∃ i, lTensor (S := G i) (G i) u = lTensor (S := G i) (G i) u') ∧
    (Algebra.FiniteType A C → ∀ u : B →ₐ[A] C,
        Function.Surjective (lTensor (S := R) R u) →
        ∃ i, Function.Surjective (lTensor (S := G i) (G i) u)) ∧
    (Algebra.FinitePresentation A C → ∀ v : R ⊗[A] C →ₐ[R] R ⊗[A] B,
        ∃ (i : ι) (vᵢ : G i ⊗[A] C →ₐ[G i] G i ⊗[A] B),
          (v.restrictScalars A).comp (rTensor C (g i)) =
            (rTensor B (g i)).comp (vᵢ.restrictScalars A)) ∧
    (Algebra.FiniteType A B → Algebra.FinitePresentation A C → ∀ u : B →ₐ[A] C,
        Function.Bijective (lTensor (S := R) R u) →
        ∃ i, Function.Bijective (lTensor (S := G i) (G i) u))

Tag 05N9, a lemma

Tag 05N9 in the Stacks Project.

CommRingCat.exists_isPushout_and_exists_eq_comp_and_exists_comp_eq_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ColimitPresentation/FinitePresentation.lean, line 869. The attribute's comment: “The colimit is a colimit cocone in CommRingCat over a filtered category, an algebra is a ring map, and A ≅ A_λ ⊗_{R_λ} R is IsPushout, so no tensor product is constructed. Items (2) and (3) are transposed along that pushout, which is Mathlib's spelling and drops the source's finite presentation of B_λ; item (3) needs A_λ of finite type only. See the module docstring.”.

Stacks 05N9. Let R = colim_λ R_λ be a filtered colimit of rings, given by a filtered diagram F with colimit cocone c.

1. Every finitely presented R-algebra A is the base change of a finitely presented R_λ-algebra A', in the sense that the square R_λ → A', R_λ → R, A' → A, R → A is a pushout.
2. If A' is of finite presentation over R_λ and B is the base change to R of an R_λ-algebra B', then every R_λ-algebra map ρ : A' → B factors as ρ = σ ≫ t through the base change Bₖ of B' to some R_μ with μ ≥ λ, by an R_λ-algebra map σ and the canonical map t : Bₖ → B. Transposed along the pushout of item 1, this says that every R-algebra map A' ⊗_{R_λ} R → B' ⊗_{R_λ} R is the base change of an R_μ-algebra map A' ⊗_{R_λ} R_μ → B' ⊗_{R_λ} R_μ.
3. If A' is of finite type over R_λ and φ, ψ : A' → B' are R_λ-algebra maps whose base changes to R agree, then their base changes to R_μ agree for some μ ≥ λ.

public theorem exists_isPushout_and_exists_eq_comp_and_exists_comp_eq_of_isColimit
    {J : Type v} [Category.{w} J] [IsFiltered J] {F : J ⥤ CommRingCat.{u}} {c : Cocone F}
    (hc : IsColimit c) [PreservesColimit F (forget CommRingCat.{u})] :
    (∀ (A : CommRingCat.{u}) (f : c.pt ⟶ A), f.hom.FinitePresentation →
        ∃ (j : J) (A' : CommRingCat.{u}) (f' : F.obj j ⟶ A') (a : A' ⟶ A),
          f'.hom.FinitePresentation ∧ IsPushout f' (c.ι.app j) a f) ∧
    (∀ (j : J) (A' B' B : CommRingCat.{u}) (f' : F.obj j ⟶ A') (g' : F.obj j ⟶ B')
        (g : c.pt ⟶ B) (b : B' ⟶ B), f'.hom.FinitePresentation →
        IsPushout g' (c.ι.app j) b g →
        ∀ ρ : A' ⟶ B, f' ≫ ρ = c.ι.app j ≫ g →
          ∃ (k : J) (h : j ⟶ k) (Bₖ : CommRingCat.{u}) (gₖ : F.obj k ⟶ Bₖ) (bₖ : B' ⟶ Bₖ)
              (t : Bₖ ⟶ B) (σ : A' ⟶ Bₖ), IsPushout g' (F.map h) bₖ gₖ ∧ bₖ ≫ t = b ∧
            gₖ ≫ t = c.ι.app k ≫ g ∧ f' ≫ σ = F.map h ≫ gₖ ∧ ρ = σ ≫ t) ∧
    (∀ (j : J) (A' B' B : CommRingCat.{u}) (f' : F.obj j ⟶ A') (g' : F.obj j ⟶ B')
        (g : c.pt ⟶ B) (b : B' ⟶ B), f'.hom.FiniteType → IsPushout g' (c.ι.app j) b g →
        ∀ φ ψ : A' ⟶ B', f' ≫ φ = g' → f' ≫ ψ = g' → φ ≫ b = ψ ≫ b →
          ∃ (k : J) (h : j ⟶ k) (Bₖ : CommRingCat.{u}) (gₖ : F.obj k ⟶ Bₖ) (bₖ : B' ⟶ Bₖ),
            IsPushout g' (F.map h) bₖ gₖ ∧ φ ≫ bₖ = ψ ≫ bₖ)

Tag 00QT, a lemma

Tag 00QT in the Stacks Project.

exists_essFiniteType_directedSystem_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/EssentialFiniteness/Colimit.lean, line 450.

A local homomorphism φ : R → S of local rings is the colimit, over a directed set Λ, of a system of local homomorphisms ψ_λ : R_λ → S_λ of local rings such that each R_λ is essentially of finite type over ℤ and each S_λ is essentially of finite type over R_λ (via ψ_λ).

The data is bundled in the existential as: * Λ with a Preorder, Nonempty and IsDirectedOrder instance — the directed set; * Rl, Sl — the families of local rings, with their CommRing and IsLocalRing structure; * rf, sf — the transition maps, forming directed systems (dsR, dsS); * ψ — the family of local homomorphisms (instLH), commuting with the transition maps (hψ).

Condition (1) is encoded by the existence of ring isomorphisms eR : colim R_λ ≃+* R and eS : colim S_λ ≃+* S identifying the colimit map Ring.DirectLimit.map ψ hψ with φ, i.e. φ ∘ eR = eS ∘ (colim ψ).

theorem exists_essFiniteType_directedSystem_colimit
    (R S : Type u) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
    (φ : R →+* S) [IsLocalHom φ] :
    ∃ (Λ : Type u) (instP : Preorder Λ),
    ∃ (_ : Nonempty Λ) (_ : @IsDirectedOrder Λ instP.toLE)
      (Rl : Λ → Type u) (Sl : Λ → Type u)
      (_ : ∀ i, CommRing (Rl i)) (_ : ∀ i, CommRing (Sl i))
      (rf : ∀ i j, i ≤ j → (Rl i →+* Rl j))
      (sf : ∀ i j, i ≤ j → (Sl i →+* Sl j))
      (_ : ∀ i, @IsLocalRing (Rl i) _)
      (_ : ∀ i, @IsLocalRing (Sl i) _)
      (ψ : ∀ i, Rl i →+* Sl i)
      (_ : ∀ i, IsLocalHom (ψ i))
      -- `rf`, `sf` form directed systems of rings
      (_ : @DirectedSystem Λ instP Rl (fun i j h => ⇑(rf i j h)))
      (_ : @DirectedSystem Λ instP Sl (fun i j h => ⇑(sf i j h)))
      -- the squares commute: `ψ` is a morphism of directed systems
      (hψ : ∀ i j (h : i ≤ j), (ψ j).comp (rf i j h) = (sf i j h).comp (ψ i)),
      -- (1) the colimit of the system `R_λ → S_λ` is equal to `φ : R → S`
      (∃ (eR : Ring.DirectLimit Rl (fun i j h => ⇑(rf i j h)) ≃+* R)
         (eS : Ring.DirectLimit Sl (fun i j h => ⇑(sf i j h)) ≃+* S),
         φ.comp eR.toRingHom = eS.toRingHom.comp (Ring.DirectLimit.map ψ hψ)) ∧
      -- (2) each `R_λ` is essentially of finite type over `ℤ`
      (∀ i, (Int.castRingHom (Rl i)).EssFiniteType) ∧
      -- (3) each `S_λ` is essentially of finite type over `R_λ` (via `ψ_λ`)
      (∀ i, (ψ i).EssFiniteType)

Tag 00QU, a lemma

Tag 00QU in the Stacks Project.

exists_colimit_presentation_of_essFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/EssentialFiniteness/Colimit.lean, line 1374.

Let φ : R → S be a local homomorphism of local rings which is essentially of finite type. Then φ is a filtered colimit of a system of local homomorphisms φ_λ : R_λ → S_λ of local rings, where each R_λ is essentially of finite type over ℤ, each S_λ is essentially of finite type over R_λ, and for λ ≤ μ the map S_λ ⊗_{R_λ} R_μ → S_μ realizes S_μ as a localization of a quotient of S_λ ⊗_{R_λ} R_μ.

theorem exists_colimit_presentation_of_essFiniteType
    (R S : Type) [CommRing R] [CommRing S] [Algebra R S]
    [IsLocalRing R] [IsLocalRing S] (hφ : IsLocalHom (algebraMap R S))
    (hft : Algebra.EssFiniteType R S) :
    ∃ (Λ : Type) (_ : PartialOrder Λ) (_ : IsDirected Λ (· ≤ ·)) (_ : Nonempty Λ)
      (Rf Sf : Λ ⥤ CommRingCat) (φsys : Rf ⟶ Sf),
      -- each `R_λ`, `S_λ` is a local ring
      (∀ i, IsLocalRing (Rf.obj i)) ∧ (∀ i, IsLocalRing (Sf.obj i)) ∧
      -- each `φ_λ` is a local homomorphism
      (∀ i, IsLocalHom (φsys.app i).hom) ∧
      -- each transition map is a local homomorphism
      (∀ (i j : Λ) (h : i ≤ j), IsLocalHom (Rf.map h.hom).hom) ∧
      (∀ (i j : Λ) (h : i ≤ j), IsLocalHom (Sf.map h.hom).hom) ∧
      -- (1) the colimit of the system is `φ : R → S` (up to canonical isomorphism)
      (∃ (iR : colimit Rf ≅ CommRingCat.of R) (iS : colimit Sf ≅ CommRingCat.of S),
        iR.inv ≫ colimMap φsys ≫ iS.hom = CommRingCat.ofHom (algebraMap R S)) ∧
      -- (2) each `R_λ` is essentially of finite type over `ℤ`
      (∀ i, Algebra.EssFiniteType ℤ (Rf.obj i)) ∧
      -- (3) each `S_λ` is essentially of finite type over `R_λ`
      (∀ i, letI : Algebra (Rf.obj i) (Sf.obj i) := (φsys.app i).hom.toAlgebra
        Algebra.EssFiniteType (Rf.obj i) (Sf.obj i)) ∧
      -- (4) for `i ≤ j`, `S_j` is the localization of a quotient of `S_i ⊗_{R_i} R_j`
      (∀ (i j : Λ) (h : i ≤ j), Stacks.EssentialFiniteness.LocalColimit.LocalizationOfQuotient φsys
        h)

Tag 00QV, a lemma

Tag 00QV in the Stacks Project.

Stacks.EssentialFiniteness.ColimitPresentation.main_theorem_00qv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/EssentialFiniteness/ColimitFinitePresentation/BaseChangeLocalization.lean, line 599.

Stacks Project, Tag 00QV (Lemma 10.127.11).

Let φ : R → S be a local homomorphism of local rings. If S is essentially of finite presentation over R (via φ), then φ is a filtered colimit of a directed system of local homomorphisms ψ_λ : R_λ → S_λ between local rings, with local transition maps, such that: (1) the colimit of the system is φ; (2) each R_λ is essentially of finite type over ℤ; (3) each ψ_λ is essentially of finite type; (4) for λ ≤ μ, the canonical base-change map S_λ ⊗_{R_λ} R_μ → S_μ exhibits S_μ as a localization of S_λ ⊗_{R_λ} R_μ at a prime.

theorem main_theorem_00qv
    (R S : Type u) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
    (φ : R →+* S) (hφ : IsLocalHom φ)
    (hfp : φ.EssFinitePresentation) :
    ∃ (Λ : Type u) (_ : Preorder Λ) (_ : Nonempty Λ) (_ : IsDirected Λ (· ≤ ·))
      (Robj : Λ → Type u) (Sobj : Λ → Type u)
      (_ : ∀ i, CommRing (Robj i)) (_ : ∀ i, CommRing (Sobj i))
      (_ : ∀ i, IsLocalRing (Robj i)) (_ : ∀ i, IsLocalRing (Sobj i))
      (fR : ∀ i j, i ≤ j → Robj i →+* Robj j)
      (fS : ∀ i j, i ≤ j → Sobj i →+* Sobj j)
      (ψ : ∀ i, Robj i →+* Sobj i)
      (comm : ∀ i j (hij : i ≤ j), (ψ j).comp (fR i j hij) = (fS i j hij).comp (ψ i)),
      -- the transition maps form directed systems of rings
      (DirectedSystem Robj (fun i j h => (fR i j h : Robj i → Robj j))) ∧
      (DirectedSystem Sobj (fun i j h => (fS i j h : Sobj i → Sobj j))) ∧
      -- all transition maps and all `ψ_λ` are local homomorphisms
      (∀ i j (hij : i ≤ j), IsLocalHom (fR i j hij)) ∧
      (∀ i j (hij : i ≤ j), IsLocalHom (fS i j hij)) ∧
      (∀ i, IsLocalHom (ψ i)) ∧
      -- (1) the colimit of the system `R_λ → S_λ` recovers `φ : R → S`
      (∃ (eR : Ring.DirectLimit Robj (fun i j h => (fR i j h : Robj i → Robj j)) ≃+* R)
         (eS : Ring.DirectLimit Sobj (fun i j h => (fS i j h : Sobj i → Sobj j)) ≃+* S),
         φ.comp eR.toRingHom = eS.toRingHom.comp (Ring.DirectLimit.map ψ comm)) ∧
      -- (2) each `R_λ` is essentially of finite type over `ℤ`
      (∀ i, Algebra.EssFiniteType ℤ (Robj i)) ∧
      -- (3) each fiber map `ψ_λ` is essentially of finite type
      (∀ i, (ψ i).EssFiniteType) ∧
      -- (4) each transition map is a localization at a prime after base change
      (∀ i j (hij : i ≤ j),
        IsLocalizationAtPrimeOfBaseChange fR fS ψ comm i j hij)

Tag 00QX, a lemma

Tag 00QX in the Stacks Project.

RingHom.EssentiallyOfFinitePresentation.exists_isColimit_essFiniteType_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/SpreadingOut/ColimitSystem.lean, line 1365. The attribute's comment: “The system is a pair of functors A B : Λ ⥤ CommRingCat with a natural transformation φ : A ⟶ B, and a functor N : Λ ⥤ AddCommGrpCat with B.obj i-module structures compatible with the transition maps; S_λ ⊗_{R_λ} R_μ is the pushout in CommRingCat and (6) is IsBaseChange. Hypothesis (1) is RingHom.EssentiallyOfFinitePresentation (Definition 00QM (2)), Mathlib having no such predicate; (2) and (3) are Mathlib's EssFiniteType (Definition 00QM (1)). The conclusion also asserts that each structure map ρ_λ : A.obj i → R is local, which is the source's "system of local homomorphisms of local rings" read as a system in the category of local rings; it is realized by the construction of 00QU and is not implied by (1)–(6). See the module docstring.”.

Stacks 00QX. Let R → S be a local homomorphism of local rings which is essentially of finite presentation and let M be a finitely presented S-module. Then there are a nonempty directed set Λ, a system φ : A ⟶ B of local homomorphisms A.obj i → B.obj i of local rings, and B.obj i-modules N.obj i, such that (1) the colimits of A, B and N are R, S and M, compatibly with algebraMap R S and with the S-action on M; (2) each A.obj i is essentially of finite type over ℤ; (3) each A.obj i → B.obj i is essentially of finite type; (4) each N.obj i is a finite B.obj i-module; (5) for i ≤ j the ring B.obj j is a localization of B.obj i ⊗_{A.obj i} A.obj j at a prime ideal; (6) for i ≤ j the transition map N.obj i → N.obj j exhibits N.obj j as the base change of N.obj i along B.obj i → B.obj j. Moreover each structure map A.obj i → R of the colimit cocone is a local homomorphism, so that each transition map A.obj i → A.obj j is local too and each 𝔪_{A.obj i} is the contraction of the maximal ideal of R.

public theorem RingHom.EssentiallyOfFinitePresentation.exists_isColimit_essFiniteType_module
    {R S M : Type u} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
    [Algebra R S] [IsLocalHom (algebraMap R S)]
    [AddCommGroup M] [Module S M] [Module.FinitePresentation S M]
    (hS : (algebraMap R S).EssentiallyOfFinitePresentation) :
    ∃ (Λ : Type u) (_ : Preorder Λ) (_ : Nonempty Λ) (_ : IsDirected Λ (· ≤ ·))
      (A B : Λ ⥤ CommRingCat.{u}) (φ : A ⟶ B) (N : Λ ⥤ AddCommGrpCat.{u})
      (_ : ∀ i, Module (B.obj i) (N.obj i))
      (hsmul : ∀ ⦃i j : Λ⦄ (h : i ⟶ j) (b : B.obj i) (m : N.obj i),
        N.map h (b • m) = B.map h b • N.map h m)
      (ρ : A ⟶ (Functor.const Λ).obj (CommRingCat.of R))
      (σ : B ⟶ (Functor.const Λ).obj (CommRingCat.of S))
      (ν : N ⟶ (Functor.const Λ).obj (AddCommGrpCat.of M))
      (_ : IsColimit (Cocone.mk (CommRingCat.of R) ρ))
      (_ : IsColimit (Cocone.mk (CommRingCat.of S) σ))
      (_ : IsColimit (Cocone.mk (AddCommGrpCat.of M) ν)),
      (∀ i, φ.app i ≫ σ.app i = ρ.app i ≫ CommRingCat.ofHom (algebraMap R S)) ∧
      (∀ (i : Λ) (b : B.obj i) (m : N.obj i),
        (ν.app i (b • m) : M) = HSMul.hSMul (α := S) (β := M) (σ.app i b) (ν.app i m)) ∧
      (∀ i, IsLocalRing (A.obj i)) ∧ (∀ i, IsLocalRing (B.obj i)) ∧
      (∀ i, IsLocalHom (φ.app i).hom) ∧
      (∀ i, IsLocalHom (ρ.app i).hom) ∧
      (∀ i, Algebra.EssFiniteType ℤ (A.obj i)) ∧
      (∀ i, (φ.app i).hom.EssFiniteType) ∧
      (∀ i, Module.Finite (B.obj i) (N.obj i)) ∧
      (∀ ⦃i j : Λ⦄ (h : i ⟶ j),
        letI := (pushout.desc (B.map h) (φ.app j) (φ.naturality h).symm).hom.toAlgebra
        ∃ (q : Ideal ↑(pushout (φ.app i) (A.map h))) (_ : q.IsPrime),
          IsLocalization q.primeCompl ↑(B.obj j)) ∧
      (∀ ⦃i j : Λ⦄ (h : i ⟶ j),
        letI : Algebra ↑(B.obj i) ↑(B.obj j) := (B.map h).hom.toAlgebra
        letI : Module ↑(B.obj i) ↑(N.obj j) := Module.compHom _ (B.map h).hom
        letI : IsScalarTower ↑(B.obj i) ↑(B.obj j) ↑(N.obj j) :=
          .of_algebraMap_smul fun _ _ => rfl
        IsBaseChange ↑(B.obj j)
          (⟨(N.map h).hom.toAddHom, hsmul h⟩ :
            ↑(N.obj i) →ₗ[↑(B.obj i)] ↑(N.obj j)))

Tag 00QY, a lemma

Tag 00QY in the Stacks Project.

CommRingCat.exists_colimitPresentation_arrow_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ColimitPresentation/FiniteType.lean, line 406. The attribute's comment: “A ring map is an object of Arrow CommRingCat, and the source's item (1) is the bundled Limits.ColimitPresentation Λ X (diagram, cocone, colimiting), colimits in an arrow category being computed entrywise. The index is the source's nonempty directed poset; Mathlib's ObjectProperty.ind form follows from this one. See the module docstring.”.

A ring map is a directed colimit of finite type ring maps between ℤ-algebras of finite type. Given a ring map X : R ⟶ S, there are a nonempty directed poset Λ and a diagram of ring maps R_λ ⟶ S_λ over Λ, together with a colimit cocone exhibiting R ⟶ S as its colimit, such that each R_λ is of finite type over ℤ and each R_λ ⟶ S_λ is of finite type.

public theorem exists_colimitPresentation_arrow_finiteType (X : Arrow CommRingCat.{u}) :
    ∃ (Λ : Type u) (_ : PartialOrder Λ) (_ : IsDirected Λ (· ≤ ·)) (_ : Nonempty Λ)
      (pres : ColimitPresentation Λ X), ∀ i : Λ,
        Algebra.FiniteType ℤ (pres.diag.obj i).left ∧ (pres.diag.obj i).hom.hom.FiniteType

Tag 0BTG, a lemma

Tag 0BTG in the Stacks Project.

integral_isColimit_directed_finite_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/Colimit.lean, line 641.

If S is integral over R, then the algebra map R → S is a filtered colimit of a directed system of module-finite ring maps f_λ : R_λ → S_λ whose bases R_λ are of finite type over ℤ.

theorem integral_isColimit_directed_finite_of_finiteType
    (R S : Type) [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] :
    ∃ D : DirectedRingMapSystem,
      -- (1) Colimit: the colimit of the system equals the structural map `R → S`.
      D.IsColimitEqual (algebraMap R S) ∧
      -- (2) Finite type base: each `R_λ` is of finite type over `Z`.
      (∀ a : D.Λ, Algebra.FiniteType ℤ (D.FR.obj a)) ∧
      -- (3) Module-finite: each `f_λ : R_λ → S_λ` is finite.
      (∀ a : D.Λ, RingHom.Finite (D.f.app a).hom)

Tag 00QZ, a lemma

Tag 00QZ in the Stacks Project.

exists_ringHomDirectedSystem_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FiniteType/Colimit.lean, line 430.

Let φ : R → S be a ring map with S of finite type over R. Then there exist a directed set (Λ, ≤) and a system of ring maps φ_λ : R_λ → S_λ over Λ such that:

1. the colimit of the system recovers φ : R → S (there are ring isomorphisms α : colim R_λ ≅ R, β : colim S_λ ≅ S with β ∘ (colim φ_λ) = φ ∘ α);
2. each R_λ is of finite type over ℤ;
3. each φ_λ : R_λ → S_λ is of finite type;
4. for each λ ≤ μ, the base-change map θ_{λμ} : S_λ ⊗_{R_λ} R_μ → S_μ is surjective.

theorem exists_ringHomDirectedSystem_of_finiteType
    (R S : Type u) [CommRing R] [CommRing S] (φ : R →+* S)
    (hft : φ.FiniteType) :
    ∃ (Λ : Type u) (_ : Preorder Λ) (_ : IsDirected Λ (· ≤ ·)) (_ : Nonempty Λ)
      (sys : RingHomDirectedSystem Λ),
      -- (1) the colimit recovers `φ : R → S`
      (∃ (α : sys.colimR ≃+* R) (β : sys.colimS ≃+* S),
        (β : sys.colimS →+* S).comp sys.colimφ = φ.comp (α : sys.colimR →+* R)) ∧
      -- (2) each `R_λ` is of finite type over `ℤ`
      (∀ l, (algebraMap ℤ (sys.R l)).FiniteType) ∧
      -- (3) each `φ_λ` is of finite type
      (∀ l, (sys.φ l).FiniteType) ∧
      -- (4) each base-change map `θ_{λμ}` is surjective
      (∀ ⦃i j : Λ⦄ (h : i ≤ j), Function.Surjective (sys.baseChangeMap h))

Tag 00R0, a lemma

Tag 00R0 in the Stacks Project.

exists_ringMapSystem_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/Colimit.lean, line 962.

Let f : R →+* S be a ring map with S of finite presentation over R. Then there is a directed index set Λ and a system of ring maps R_λ → S_λ (packaged as 𝓟 : RingMapSystem Λ) such that:

1. there are ring isomorphisms eR : colim R_λ ≃+* R and eS : colim S_λ ≃+* S intertwining the colimit map colim ψ with the given map f (f ∘ eR = eS ∘ colim ψ);
2. each R_λ is of finite type over ℤ;
3. each ψ_λ : R_λ →+* S_λ is of finite type;
4. for each λ ≤ μ the base change map S_λ ⊗_{R_λ} R_μ →+* S_μ is bijective (an isomorphism of rings).

theorem exists_ringMapSystem_of_finitePresentation {R S : Type u} [CommRing R] [CommRing S] (f : R
  →+* S)
    (hf : f.FinitePresentation) :
    ∃ (Λ : Type u) (_ : PartialOrder Λ) (_ : Nonempty Λ) (_ : IsDirected Λ (· ≤ ·))
      (𝓟 : RingMapSystem.{u, u} Λ)
      (eR : 𝓟.source.colimit ≃+* R) (eS : 𝓟.target.colimit ≃+* S),
      -- (1) Colimit: the square commutes (`f ∘ eR = eS ∘ colim ψ`).
      (∀ x, f (eR x) = eS (𝓟.colimitMap x)) ∧
      -- (2) Finite type base: each `R_λ` is of finite type over `ℤ`.
      (∀ i, Algebra.FiniteType ℤ (𝓟.source.R i)) ∧
      -- (3) Finite type fibers: each `ψ_λ` is of finite type.
      (∀ i, (𝓟.ψ i).FiniteType) ∧
      -- (4) Cartesian transitions: the base change maps are isomorphisms.
      (∀ ⦃i j : Λ⦄ (hij : i ≤ j), Function.Bijective (𝓟.baseChange hij))

Tag 00R1, a lemma

Tag 00R1 in the Stacks Project.

Algebra.exists_subring_finiteType_int_isPushout_isBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/ModuleDescent/SubringDescent.lean, line 390. The attribute's comment: “Stated as a descent along a single subring R₀ ⊆ R of finite type over ℤ rather than as a directed system: the six clauses of the source are recovered by taking for Λ the subrings of R of finite type over ℤ containing R₀ and base changing S₀ and M₀ along R₀ → R_λ, and conversely the source's system gives such an R₀ as the image of any R_λ in R. See the module docstring.”.

A finitely presented algebra with a finitely presented module descends to a subring of finite type over ℤ. Let R → S be of finite presentation and let M be a finitely presented S-module. Then there are a subring R₀ ⊆ R of finite type over ℤ, an R₀-algebra S₀ of finite type and a finite S₀-module M₀, together with an algebra map S₀ → S and an S₀-linear map f : M₀ → M, presenting S as R ⊗_{R₀} S₀ and M as S ⊗_{S₀} M₀.

public theorem Algebra.exists_subring_finiteType_int_isPushout_isBaseChange
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S]
    (M : Type v) [AddCommGroup M] [Module S M] [Module.FinitePresentation S M] :
    ∃ (R₀ : Subring R) (S₀ M₀ : Type u) (_ : CommRing S₀) (_ : Algebra R₀ S₀)
      (_ : Algebra S₀ S) (_ : IsScalarTower R₀ S₀ S) (_ : AddCommGroup M₀)
      (_ : Module S₀ M₀) (_ : Module S₀ M) (_ : IsScalarTower S₀ S M) (f : M₀ →ₗ[S₀] M),
      Algebra.FiniteType ℤ R₀ ∧ Algebra.FiniteType R₀ S₀ ∧ Module.Finite S₀ M₀ ∧
        Algebra.IsPushout R₀ R S₀ S ∧ IsBaseChange S f

Sources

• Section 10.127, Tag 00QL
• AxiomMath/Stacks at 5ed82d14

LeanCommRingCat.isFiltered_costructuredArrow_and_isDenseAt_finitePresentation · Algebra.exists_directedSystem_finitePresentation_lift_bijective · CommRingCat.isFinitelyPresentable_under_tfae · CommRingCat.ind_under_iff_exists_factorization · Stacks.FinitePresentation.ColimitDescent.statement_two · Stacks.FinitePresentation.ColimitDescent.statement_three · Stacks.FinitePresentation.ColimitDescent.statement_four · Stacks.FinitePresentation.ColimitDescent.statement_one

Section10.128 More flatness criteria#

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

Tag 00R4, a lemma

Tag 00R4 in the Stacks Project.

Module.Flat.of_isMaximalCohenMacaulay_of_ringKrullDim_eq_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/MiracleFlatness.lean, line 292. The attribute's comment: “Regularity of the Noetherian local ring R is IsRegularLocalRing R; Cohen-Macaulayness of S (Definition 00N8) is Module.IsMaximalCohenMacaulay S S, i.e. depth_{𝔪_S}(S) = dim S; and dim(S/𝔪_R S) is the Krull dimension of the quotient of S by the image ideal of the maximal ideal of R. See the module docstring.”. References: EGA IV (6.1.5), “case M = B”; EGA IV (15.4.2), “e′)⇒b), partial”.

Miracle flatness, Stacks 00R4. Let R → S be a local homomorphism of Noetherian local rings with R regular and S Cohen–Macaulay, i.e. depth_{𝔪_S}(S) = dim(S). If dim(S) = dim(R) + dim(S/𝔪_R S), then S is flat over R.

public theorem Module.Flat.of_isMaximalCohenMacaulay_of_ringKrullDim_eq_add
    {R S : Type*} [CommRing R] [IsRegularLocalRing R] [CommRing S] [IsLocalRing S]
    [IsNoetherianRing S] [Algebra R S] [IsLocalHom (algebraMap R S)]
    (hS : Module.IsMaximalCohenMacaulay S S)
    (hdim : ringKrullDim S =
      ringKrullDim R + ringKrullDim (S ⧸ (maximalIdeal R).map (algebraMap R S))) :
    Module.Flat R S

Tag 07DY, a lemma

Tag 07DY in the Stacks Project.

Module.Flat.of_ofList_eq_maximalIdeal_of_isWeaklyRegular_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/RegularSequence.lean, line 214. The attribute's comment: “Stated for a finite S-module M in place of S itself, the source's statement being the case M = S; a regular system of parameters is a list generating the maximal ideal whose length is its minimal number of generators; and the source's regular sequence is weakened to RingTheory.Sequence.IsWeaklyRegular, its nonvanishing clause being replaced by IsLocalHom. See the module docstring.”.

Let R be a regular local ring, let xs = x₁, …, x_d be a regular system of parameters of R, that is, a list generating 𝔪_R whose length is the minimal number of generators of 𝔪_R, let S be a Noetherian local ring receiving a local homomorphism from R and let M be a finite S-module. If the images of x₁, …, x_d in S form a weakly M-regular sequence, then M is flat over R. Taking M = S shows that R → S is flat.

public theorem Module.Flat.of_ofList_eq_maximalIdeal_of_isWeaklyRegular_map
    {R : Type*} (S : Type*) (M : Type*) [CommRing R] [IsRegularLocalRing R] [CommRing S]
    [IsLocalRing S] [IsNoetherianRing S] [Algebra R S] [IsLocalHom (algebraMap R S)]
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Module.Finite S M]
    (xs : List R) (hxs : Ideal.ofList xs = maximalIdeal R)
    (hmin : xs.length = (maximalIdeal R).spanFinrank)
    (hreg : IsWeaklyRegular M (xs.map (algebraMap R S))) :
    Module.Flat R M

Tag 00R6, a lemma

Tag 00R6 in the Stacks Project.

Module.Flat.exists_ge_flat_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/SpreadingOut/Flat.lean, line 101. The attribute's comment: “The system "as in Lemma 00QX" is spelled out as the data and the six conditions concluded by RingHom.EssentiallyOfFinitePresentation.exists_isColimit_essFiniteType_module, together with locality of the transition maps A i → A j, which is the source's "system of local homomorphisms of local rings" read as a system in the category of local rings and is what 00MO needs to know (𝔪 i) A j is proper. The hypotheses of 00QX are not assumed, being either unused or consequences of the system. The conclusion is the cofinal form (∀ i, ∃ j ≥ i), which is what the source's proof produces and what the dependents use. See the module docstring.”.

Let (A i → B i, N i) be a directed system as in 00QX, with colimits R → S and M: each A i is essentially of finite type over ℤ, each A i → B i is a local homomorphism of local rings essentially of finite type, each transition map A i → A j is local, each N i is a finite B i-module, each B j is a localization of B i ⊗_{A i} A j at a prime ideal, and each N j is the base change of N i along B i → B j. If M is flat over R, then for every index i there is j ≥ i such that N j is flat over A j.

public theorem exists_ge_flat_of_isColimit
    {R S M : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Module.Flat R M]
    {Λ : Type u} [Preorder Λ] [Nonempty Λ] [IsDirected Λ (· ≤ ·)]
    {A B : Λ ⥤ CommRingCat.{u}} {φ : A ⟶ B} {N : Λ ⥤ AddCommGrpCat.{u}}
    (mod : ∀ i, Module (B.obj i) (N.obj i))
    (hsmul : ∀ ⦃i j : Λ⦄ (h : i ⟶ j) (b : B.obj i) (m : N.obj i),
      N.map h (b • m) = B.map h b • N.map h m)
    {ρ : A ⟶ (Functor.const Λ).obj (CommRingCat.of R)}
    {σ : B ⟶ (Functor.const Λ).obj (CommRingCat.of S)}
    {ν : N ⟶ (Functor.const Λ).obj (AddCommGrpCat.of M)}
    (hR : IsColimit (Cocone.mk (CommRingCat.of R) ρ))
    (_hS : IsColimit (Cocone.mk (CommRingCat.of S) σ))
    (hM : IsColimit (Cocone.mk (AddCommGrpCat.of M) ν))
    (hφ : ∀ i, φ.app i ≫ σ.app i = ρ.app i ≫ CommRingCat.ofHom (algebraMap R S))
    (hν : ∀ (i : Λ) (b : B.obj i) (m : N.obj i),
      (ν.app i (b • m) : M) = HSMul.hSMul (α := S) (β := M) (σ.app i b) (ν.app i m))
    (hAlocal : ∀ i, IsLocalRing (A.obj i)) (hBlocal : ∀ i, IsLocalRing (B.obj i))
    (hφlocal : ∀ i, IsLocalHom (φ.app i).hom)
    (hAmaplocal : ∀ ⦃i j : Λ⦄ (h : i ⟶ j), IsLocalHom (A.map h).hom)
    (hAft : ∀ i, Algebra.EssFiniteType ℤ (A.obj i))
    (hφft : ∀ i, (φ.app i).hom.EssFiniteType)
    (hNfin : ∀ i, Module.Finite (B.obj i) (N.obj i))
    (hBloc : ∀ ⦃i j : Λ⦄ (h : i ⟶ j),
      letI := (pushout.desc (B.map h) (φ.app j) (φ.naturality h).symm).hom.toAlgebra
      ∃ (q : Ideal ↑(pushout (φ.app i) (A.map h))) (_ : q.IsPrime),
        IsLocalization q.primeCompl ↑(B.obj j))
    (hNbc : ∀ ⦃i j : Λ⦄ (h : i ⟶ j),
      letI : Algebra ↑(B.obj i) ↑(B.obj j) := (B.map h).hom.toAlgebra
      letI : Module ↑(B.obj i) ↑(N.obj j) := Module.compHom _ (B.map h).hom
      letI : IsScalarTower ↑(B.obj i) ↑(B.obj j) ↑(N.obj j) :=
        .of_algebraMap_smul fun _ _ => rfl
      IsBaseChange ↑(B.obj j)
        (⟨(N.map h).hom.toAddHom, hsmul h⟩ : ↑(N.obj i) →ₗ[↑(B.obj i)] ↑(N.obj j)))
    (i : Λ) :
    ∃ j, i ≤ j ∧
      (letI : Module ↑(A.obj j) ↑(N.obj j) := Module.compHom _ (φ.app j).hom
       Module.Flat ↑(A.obj j) ↑(N.obj j))

Tag 046Y, a lemma

Tag 046Y in the Stacks Project.

Module.Flat.injective_and_flat_quotient_range_of_injective_mapQ_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriterionNonNoetherian.lean, line 279. The attribute's comment: “M/𝔪M is M ⧸ 𝔪 • (⊤ : Submodule R M) and ū the canonical Submodule.mapQ of u. Hypothesis (1) is RingHom.EssentiallyOfFinitePresentation (Definition 00QM (2)), Mathlib having no such predicate. The cokernel N/u(M) is N ⧸ LinearMap.range u, and the two conclusions are conjoined; see the module docstring.”. References: SGA 1 IV (5.7), “(ii) ⟹ (i)”.

Let R → S be a local homomorphism of local rings with S essentially of finite presentation over R, let 𝔪 be the maximal ideal of R, and let u : M → N be a map of S-modules with M, N of finite presentation over S and N flat over R. If the induced map ū : M/𝔪M → N/𝔪N is injective, then u is injective and N/u(M) is flat over R.

Here M/𝔪M is M ⧸ 𝔪 • ⊤ and ū is the canonical Submodule.mapQ, which sends the class of x to the class of u x.

public theorem Module.Flat.injective_and_flat_quotient_range_of_injective_mapQ_maximalIdeal
    {R S M N : Type*} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N]
    [Module.FinitePresentation S M] [Module.FinitePresentation S N] [Module.Flat R N]
    (hS : (algebraMap R S).EssentiallyOfFinitePresentation) (u : M →ₗ[S] N)
    (hu :
      Function.Injective
        (Submodule.mapQ (maximalIdeal R • (⊤ : Submodule R M))
          (maximalIdeal R • (⊤ : Submodule R N)) (u.restrictScalars R)
          (Submodule.smul_top_le_comap_smul_top (maximalIdeal R) (u.restrictScalars R)))) :
    Function.Injective u ∧ Module.Flat R (N ⧸ LinearMap.range u)

Tag 046Z, a lemma

Tag 046Z in the Stacks Project.

Module.Flat.isSMulRegular_and_flat_quotient_span_of_isSMulRegular_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/SliceRegularParameter.lean, line 238. The attribute's comment: “the case M := S, spelled with ring quotients by ideals”. References: EGA IV (11.3.8), “(c) ⇒ (a), special case”.

Stacks 046Z with both quotients taken by ideals. Let R → S be a local homomorphism of local rings which is essentially of finite presentation and makes S flat over R. If a ∈ S is a nonzerodivisor on the fibre S ⧸ 𝔪S, then a is a nonzerodivisor on S and S ⧸ (a) is again flat over R.

This is the M = S case of Module.Flat.isSMulRegular_and_flat_quotient_smul_of_isSMulRegular_maximalIdeal, restated with the fibre and the quotient written as quotients of the ring by ideals rather than as quotients of the module S by I • ⊤. The two agree because extending an ideal to the top submodule of the ring returns the ideal, and that identification is an equality of submodules, so the hypothesis and the conclusion are transported along Submodule.quotEquivOfEq rather than compared as types.

public theorem Module.Flat.isSMulRegular_and_flat_quotient_span_of_isSMulRegular_quotient
    {R S : Type*} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] [Module.Flat R S]
    (hS : (algebraMap R S).EssentiallyOfFinitePresentation) {a : S}
    (ha : IsSMulRegular (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) a) :
    IsSMulRegular S a ∧ Module.Flat R (S ⧸ Ideal.span {a})

Module.Flat.isSMulRegular_and_flat_quotient_smul_of_isSMulRegular_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/RegularSequenceOverBase.lean, line 70. The attribute's comment: “Stated in module form (the source's case is M := S), with 𝔪M spelled Ideal.map (algebraMap R S) (maximalIdeal R) • (⊤ : Submodule S M) and fM spelled Ideal.span {f} • ⊤, and "nonzerodivisor" spelled IsSMulRegular. Hypothesis (1) is RingHom.EssentiallyOfFinitePresentation (Definition 00QM (2)), Mathlib having no such predicate. The two conclusions are conjoined; see the module docstring.”. References: EGA IV (11.3.8), “(c) ⇒ (a), special case”.

Stacks 046Z. Let R → S be a local homomorphism of local rings with S essentially of finite presentation over R, let 𝔪 be the maximal ideal of R, and let M be an S-module of finite presentation which is flat over R. If f ∈ S is a nonzerodivisor on the fibre M/𝔪M, then f is a nonzerodivisor on M and M/fM is flat over R.

The source is the case M = S: f is a nonzerodivisor in S and S/fS is flat over R. Here 𝔪M is 𝔪S • ⊤ and fM is Ideal.span {f} • ⊤; see the module docstring.

public theorem Module.Flat.isSMulRegular_and_flat_quotient_smul_of_isSMulRegular_maximalIdeal
    {R S M : Type*} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.FinitePresentation S M] [Module.Flat R M]
    (hS : (algebraMap R S).EssentiallyOfFinitePresentation) {f : S}
    (hf :
      IsSMulRegular (M ⧸ (Ideal.map (algebraMap R S) (maximalIdeal R) • (⊤ : Submodule S M))) f) :
    IsSMulRegular M f ∧ Module.Flat R (M ⧸ (Ideal.span {f} • (⊤ : Submodule S M)))

Tag 0470, a lemma

Tag 0470 in the Stacks Project.

Module.Flat.isRegular_and_flat_quotient_ofList_smul_of_isRegular_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/RegularSequenceOverBase.lean, line 172. The attribute's comment: “Stated in module form (the source's case is M := S), with the sequence a List S, 𝔪M spelled Ideal.map (algebraMap R S) (maximalIdeal R) • (⊤ : Submodule S M) and the partial quotients spelled M ⧸ Ideal.ofList (fs.take i) • ⊤. "Regular sequence" is Mathlib's RingTheory.Sequence.IsRegular, which is Definition 00LF verbatim (nonvanishing clause included). Hypothesis (1) is RingHom.EssentiallyOfFinitePresentation (Definition 00QM (2)), Mathlib having no such predicate. The two conclusions are conjoined; see the module docstring.”. References: EGA 0 (15.1.16), “c)=>a), ess fin pres”; EGA 0 (15.1.17), “(f_i) is M-regular”; EGA IV (11.3.8), “c) ⇒ a)”.

Stacks 0470. Let R → S be a local homomorphism of local rings with S essentially of finite presentation over R, let 𝔪 be the maximal ideal of R, and let M be an S-module of finite presentation which is flat over R. If a sequence f₁, …, f_c of elements of S is regular on the fibre M/𝔪M, then it is regular on M and every partial quotient M/(f₁, …, f_i)M is flat over R.

The source is the case M = S: f₁, …, f_c is a regular sequence in S and each S/(f₁, …, f_i) is flat over R. Here 𝔪M is 𝔪S • ⊤ and M/(f₁, …, f_i)M is M ⧸ Ideal.ofList (fs.take i) • ⊤; see the module docstring.

public theorem Module.Flat.isRegular_and_flat_quotient_ofList_smul_of_isRegular_maximalIdeal
    {R S M : Type*} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.FinitePresentation S M] [Module.Flat R M]
    (hS : (algebraMap R S).EssentiallyOfFinitePresentation) (fs : List S)
    (hfs :
      RingTheory.Sequence.IsRegular
        (M ⧸ (Ideal.map (algebraMap R S) (maximalIdeal R) • (⊤ : Submodule S M))) fs) :
    RingTheory.Sequence.IsRegular M fs ∧
      ∀ i, Module.Flat R (M ⧸ (Ideal.ofList (fs.take i) • (⊤ : Submodule S M)))

Tag 0471, a lemma

Tag 0471 in the Stacks Project.

Module.Flat.of_rTensor_subtype_injective_of_flat_quotient_of_essentiallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriterionEssFP.lean, line 351. The attribute's comment: “The hypothesis Tor_1^R(M, R/I) = 0 is stated in the form Remark 00M6 identifies it with, the injectivity of I ⊗_R M → R ⊗_R M, as in the Noetherian sibling 00ML; this is the form the source's proof produces and the form 00ML consumes, and unlike Tor_1 it puts R and M in no common universe. Hypothesis (1) is RingHom.EssentiallyOfFinitePresentation (Definition 00QM (2)), Mathlib having no such predicate. See the module docstring.”. References: EGA IV (11.3.12), “b⇒a, b⇒a for arbitrary A”; SGA 1 IV (5.6), “(ii)⇒(i), special case”.

The local criterion for flatness for local maps essentially of finite presentation. Let R → S be a local homomorphism of local rings with S essentially of finite presentation over R, let I ≠ R be an ideal of R and let M be an S-module of finite presentation. If Tor₁^R(R/I, M) = 0 and M/IM is flat over R/I, then M is flat over R.

Here the Tor hypothesis appears in the form of Remark 00M6, as the injectivity of I ⊗_R M → R ⊗_R M, and M/IM is M ⧸ I • ⊤ with its canonical R ⧸ I-module structure. No ring is assumed Noetherian; the Noetherian variant is 00ML.

public theorem of_rTensor_subtype_injective_of_flat_quotient_of_essentiallyOfFinitePresentation
    {R : Type u} (S : Type v) (M : Type w) [CommRing R] [CommRing S] [IsLocalRing R]
    [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [AddCommGroup M] [Module R M]
    [Module S M] [IsScalarTower R S M] [Module.FinitePresentation S M]
    (hS : (algebraMap R S).EssentiallyOfFinitePresentation) (I : Ideal R) (hI : I ≠ ⊤)
    (hTor : Function.Injective (I.subtype.rTensor M))
    (hflat : Module.Flat (R ⧸ I) (M ⧸ (I • (⊤ : Submodule R M)))) :
    Module.Flat R M

Tag 00R7, a lemma

Tag 00R7 in the Stacks Project.

Module.flat_algebra_and_flat_of_flat_quotient_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FibrewiseCriterionEssFP.lean, line 351. The attribute's comment: “Hypothesis (1) is RingHom.EssentiallyOfFinitePresentation (Definition 00QM (2)) applied to algebraMap R S and algebraMap R S', Mathlib having no such predicate. The fibre is M ⧸ (𝔪S) • (⊤ : Submodule S M) over the ring S ⧸ 𝔪S, as in 06A5, and the two conclusions are conjoined; see the module docstring.”. References: EGA IV (11.3.10), “special case”; SGA 1 I (5.9), “partial”; SGA 1 IV (5.9), “(ii) ⇒ (i)”; SGA 3 VIB (1.3.0), “special case”; SGA 3 VIB (12.7), “special case”; SGA 3 VIB (2.5), “flatness clause”; SGA 3 X (3.5), “Flat case”.

Critère de platitude par fibres. Let R → S → S' be local homomorphisms of local rings with R → S and R → S' essentially of finite presentation, let 𝔪 be the maximal ideal of R, and let M be a nonzero S'-module of finite presentation over S'. If the fibre M/𝔪M is flat over S/𝔪S and M is flat over R, then S is flat over R and M is flat over S.

Here 𝔪S is Ideal.map (algebraMap R S) (maximalIdeal R) and M/𝔪M is M ⧸ 𝔪S • ⊤ taken over S, so that it is a module over S/𝔪S.

public theorem Module.flat_algebra_and_flat_of_flat_quotient_maximalIdeal
    {R S S' M : Type*} [CommRing R] [CommRing S] [CommRing S']
    [IsLocalRing R] [IsLocalRing S] [IsLocalRing S']
    [Algebra R S] [Algebra S S'] [Algebra R S'] [IsScalarTower R S S']
    [IsLocalHom (algebraMap R S)] [IsLocalHom (algebraMap S S')]
    [AddCommGroup M] [Module R M] [Module S M] [Module S' M]
    [IsScalarTower R S M] [IsScalarTower S S' M]
    [Module.FinitePresentation S' M] [Nontrivial M]
    [Module.Flat (S ⧸ (maximalIdeal R).map (algebraMap R S))
      (M ⧸ ((maximalIdeal R).map (algebraMap R S) • (⊤ : Submodule S M)))]
    [Module.Flat R M]
    (hS : (algebraMap R S).EssentiallyOfFinitePresentation)
    (hS' : (algebraMap R S').EssentiallyOfFinitePresentation) :
    Module.Flat R S ∧ Module.Flat S M

Tag 05UV, a lemma

Tag 05UV in the Stacks Project.

Module.essentiallyOfFinitePresentation_and_flat_and_flat_of_flat_quotient_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FibrewiseCriterionEssFPBase.lean, line 463. The attribute's comment: “"Essentially of finite type" is Mathlib's Algebra.EssFiniteType (Definition 00QM (1)); "essentially of finite presentation" is RingHom.EssentiallyOfFinitePresentation (Definition 00QM (2)), Mathlib having no such predicate. The chain R → S → S' is IsScalarTower R S S', 𝔪S is (maximalIdeal R).map (algebraMap R S) and 𝔪M is 𝔪S • ⊤ over S, so that the fibre M/𝔪M is a module over the ring S/𝔪S. "M is not zero" is Nontrivial M. The three conclusions are conjoined; see the module docstring.”. References: EGA IV (11.3.10), “special case”; SGA 1 I (5.9), “partial”; SGA 1 IV (5.9), “(ii) ⇒ (i)”; SGA 3 VIB (1.3.0), “special case”; SGA 3 VIB (12.7), “special case”; SGA 3 VIB (2.5), “flatness clause”; SGA 3 X (3.5), “Flat case”.

Let R → S → S' be local homomorphisms of local rings, let 𝔪 be the maximal ideal of R, and let M be a nonzero S'-module of finite presentation. Assume R → S' is essentially of finite presentation, R → S is essentially of finite type, M is flat over R, and the fibre M/𝔪M is flat over S/𝔪S. Then R → S is essentially of finite presentation, S is flat over R, and M is flat over S.

Here 𝔪S is (maximalIdeal R).map (algebraMap R S) and 𝔪M is 𝔪S • ⊤, so that M/𝔪M is a module over the fibre ring S/𝔪S.

public theorem
    Module.essentiallyOfFinitePresentation_and_flat_and_flat_of_flat_quotient_maximalIdeal
    {R S S' M : Type*} [CommRing R] [CommRing S] [CommRing S']
    [IsLocalRing R] [IsLocalRing S] [IsLocalRing S']
    [Algebra R S] [Algebra S S'] [Algebra R S'] [IsScalarTower R S S']
    [IsLocalHom (algebraMap R S)] [IsLocalHom (algebraMap S S')]
    [AddCommGroup M] [Module R M] [Module S M] [Module S' M]
    [IsScalarTower R S M] [IsScalarTower S S' M]
    [Algebra.EssFiniteType R S] [Module.FinitePresentation S' M] [Nontrivial M] [Module.Flat R M]
    [Module.Flat (S ⧸ (maximalIdeal R).map (algebraMap R S))
      (M ⧸ ((maximalIdeal R).map (algebraMap R S) • (⊤ : Submodule S M)))]
    (hS' : (algebraMap R S').EssentiallyOfFinitePresentation) :
    (algebraMap R S).EssentiallyOfFinitePresentation ∧ Module.Flat R S ∧ Module.Flat S M

Tag 0CEL, a lemma

Tag 0CEL in the Stacks Project.

Module.flat_and_flat_localization_of_flat_quotient_of_locallyNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FibreCriterionNilpotent.lean, line 373. The attribute's comment: “"Locally nilpotent" is ∀ x ∈ I, IsNilpotent x. IM is written as IS • ⊤ over S, S_q is an abstract localization of S at q, and "essentially of finite presentation" is RingHom.EssentiallyOfFinitePresentation; see the module docstring.”. References: EGA IV (11.3.11), “(a) ⇒ (b), special case”; SGA 1 IV (5.9), “(ii) ⇒ (i), special case”; SGA 3 VIB (1.3.0), “special case”; SGA 3 VIB (2.5), “flatness clause”.

Let R → S → S' be ring maps with R → S of finite type and R → S' of finite presentation, let I ⊆ R be an ideal all of whose elements are nilpotent, and let M be a finitely presented S'-module. If M/IM is flat over S/IS and M is flat over R, then M is flat over S, and S_q is flat and essentially of finite presentation over R for every prime q ⊆ S with M ⊗_S κ(q) nonzero.

theorem Module.flat_and_flat_localization_of_flat_quotient_of_locallyNilpotent
    {R S S' : Type*} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra S S']
    [Algebra R S'] [IsScalarTower R S S']
    {M : Type*} [AddCommGroup M] [Module R M] [Module S M] [Module S' M]
    [IsScalarTower R S M] [IsScalarTower S S' M]
    (I : Ideal R) (hI : ∀ x ∈ I, IsNilpotent x)
    [Algebra.FiniteType R S] [Algebra.FinitePresentation R S'] [Module.FinitePresentation S' M]
    [Module.Flat (S ⧸ I.map (algebraMap R S))
      (M ⧸ (I.map (algebraMap R S) • (⊤ : Submodule S M)))]
    [Module.Flat R M] :
    Module.Flat S M ∧
      ∀ (q : Ideal S) [q.IsPrime] (Sq : Type*) [CommRing Sq] [Algebra S Sq]
        [IsLocalization.AtPrime Sq q] [Algebra R Sq] [IsScalarTower R S Sq],
        Nontrivial (M ⊗[S] q.ResidueField) →
          Module.Flat R Sq ∧ (algebraMap R Sq).EssentiallyOfFinitePresentation

Sources

• Section 10.128, Tag 00R3
• AxiomMath/Stacks at 5ed82d14

LeanModule.Flat.of_isMaximalCohenMacaulay_of_ringKrullDim_eq_add · Module.Flat.of_ofList_eq_maximalIdeal_of_isWeaklyRegular_map · Module.Flat.exists_ge_flat_of_isColimit · Module.Flat.injective_and_flat_quotient_range_of_injective_mapQ_maximalIdeal · Module.Flat.isSMulRegular_and_flat_quotient_span_of_isSMulRegular_quotient · Module.Flat.isSMulRegular_and_flat_quotient_smul_of_isSMulRegular_maximalIdeal · Module.Flat.isRegular_and_flat_quotient_ofList_smul_of_isRegular_maximalIdeal · Module.Flat.of_rTensor_subtype_injective_of_flat_quotient_of_essentiallyOfFinitePresentation

Section10.129 Openness of the flat locus#

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

Tag 00R9, a lemma

Tag 00R9 in the Stacks Project.

Module.IsMaximalCohenMacaulay.ringKrullDim_quotient_add_length_eq_and_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Equidimensional.lean, line 360. The attribute's comment: “Cohen-Macaulayness of a Noetherian local ring is Module.IsMaximalCohenMacaulay A A (Definition 00N8); that of the Noetherian ring S (Definition 00NC) is spelled out over its localizations at primes, as in tag 00ND. dim V(f₁, …, f_i) is ringKrullDim (S ⧸ Ideal.ofList f) (ringKrullDim_quotient), and ≤ d - i is written + f.length ≤ d in WithBot ℕ∞, the source's truncating subtraction being false as stated. The extra hypothesis Ideal.ofList f ≠ ⊤ excludes the empty locus, where the source's equality fails. See the module docstring.”.

Stacks 00R9. Let k be a field and S a finite type k-algebra which is Cohen–Macaulay (every local ring S_𝔭 satisfies depth_{𝔪}(S_𝔭) = dim S_𝔭) and equidimensional of dimension d. Let f = f₁, …, f_i be elements of S cutting out a nonempty closed subset V(f₁, …, f_i) of Spec S of dimension at most d - i. Then that dimension is exactly d - i, and f₁, …, f_i is a regular sequence in S_𝔮 for every prime 𝔮 ⊇ (f₁, …, f_i).

public theorem ringKrullDim_quotient_add_length_eq_and_isRegular
    {k S : Type*} [Field k] [CommRing S] [Algebra k S] [Algebra.FiniteType k S]
    (hS : ∀ (p : Ideal S) [p.IsPrime],
      Module.IsMaximalCohenMacaulay (Localization.AtPrime p) (Localization.AtPrime p))
    (hequi : TopologicalSpace.Equidimensional (PrimeSpectrum S)) (d : ℕ)
    (hd : ringKrullDim S = d) (f : List S) (hf : Ideal.ofList f ≠ ⊤)
    (hdim : ringKrullDim (S ⧸ Ideal.ofList f) + f.length ≤ (d : WithBot ℕ∞)) :
    ringKrullDim (S ⧸ Ideal.ofList f) + f.length = (d : WithBot ℕ∞) ∧
      ∀ (q : Ideal S) [q.IsPrime], Ideal.ofList f ≤ q →
        ∀ (Sq : Type*) [CommRing Sq] [Algebra S Sq] [IsLocalization.AtPrime Sq q],
          RingTheory.Sequence.IsRegular Sq (f.map (algebraMap S Sq))

Tag 00RA, a lemma

Tag 00RA in the Stacks Project.

Algebra.isOpen_setOf_isRegular_fiber_of_isMaximalCohenMacaulay_of_equidimensional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/RegularLocus.lean, line 861. The attribute's comment: “V(f₁, …, f_i) is the subspace PrimeSpectrum.zeroLocus ↑(Ideal.ofList f) of Spec S and openness is for its subspace topology. S_𝔮/𝔭S_𝔮 is the quotient of Localization.AtPrime 𝔮 by the ideal generated by 𝔭 = 𝔮.under R, which is the fibre κ(𝔭) ⊗_R S_𝔮 of tag 00PK by Ideal.Fiber.ringEquivQuotient but carries the canonical S-algebra structure. Cohen-Macaulayness of the fibre (Definition 00NC) is spelled out over its primes at Localization.AtPrime and equidimensionality of dimension d as Definition 0058 plus ringKrullDim = d, as in tags 00ND and 00R9; the hypothesis is guarded by the fibre being nonzero, where the source's condition on its components has content. See the module docstring.”.

Stacks 00RA. Let R → S be a finite type ring map and let d be such that every nonempty fibre S ⊗_R κ(𝔭) is Cohen–Macaulay (each of its local rings A satisfies depth_{𝔪_A}(A) = dim A) and equidimensional of dimension d. Let f = f₁, …, f_i be elements of S. Then the set of points 𝔮 of V(f₁, …, f_i) at which f₁, …, f_i is a regular sequence in S_𝔮/𝔭S_𝔮, where 𝔭 = R ∩ 𝔮, is open in V(f₁, …, f_i).

public theorem isOpen_setOf_isRegular_fiber_of_isMaximalCohenMacaulay_of_equidimensional
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S] (d : ℕ)
    (hfib : ∀ (p : Ideal R) [p.IsPrime], Nontrivial (p.Fiber S) →
      (∀ (Q : Ideal (p.Fiber S)) [Q.IsPrime],
          Module.IsMaximalCohenMacaulay (Localization.AtPrime Q) (Localization.AtPrime Q)) ∧
        TopologicalSpace.Equidimensional (PrimeSpectrum (p.Fiber S)) ∧
        ringKrullDim (p.Fiber S) = (d : WithBot ℕ∞))
    (f : List S) :
    IsOpen {q : ↥(PrimeSpectrum.zeroLocus (Ideal.ofList f : Set S)) |
      RingTheory.Sequence.IsRegular
        (Localization.AtPrime q.1.asIdeal ⧸
          (q.1.asIdeal.under R).map (algebraMap R (Localization.AtPrime q.1.asIdeal)))
        (f.map (algebraMap S (Localization.AtPrime q.1.asIdeal ⧸
          (q.1.asIdeal.under R).map (algebraMap R (Localization.AtPrime q.1.asIdeal)))))}

Tag 00RB, a lemma

Tag 00RB in the Stacks Project.

Algebra.isOpen_setOf_injective_and_exact_baseChange_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/OpenFibreExactLocus.lean, line 579. The attribute's comment: “The complex is indexed as in 00N1: φ k : S^{n (k+1)} → S^{n k}, read for k ≤ e, and exactness is injectivity of φ e and exactness at S^{n_e}, …, S^{n_1}. F_𝔮 ⊗_R κ(𝔭) is the base change of F along S → S_𝔮/𝔭S_𝔮, the ring of 00RA, which is S_𝔮 ⊗_R κ(𝔭). The fibre hypothesis is spelled out as in 00RA. See the module docstring.”.

Let R → S be a flat ring map of finite type with R Noetherian, whose nonzero fibres S ⊗_R κ(𝔭) are Cohen–Macaulay and equidimensional of dimension d, and let 0 → S^{n_{e+1}} →[φ e] S^{n_e} → ⋯ → S^{n_1} →[φ 0] S^{n_0} be a complex of finite free S-modules. Then the set of primes 𝔮 of S at which the complex F_𝔮 ⊗_R κ(𝔭) = F ⊗_S S_𝔮/𝔭S_𝔮, 𝔭 = 𝔮 ∩ R, is exact is open in Spec S.

public theorem Algebra.isOpen_setOf_injective_and_exact_baseChange_fiber
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [IsNoetherianRing R]
    [Algebra.FiniteType R S] [Module.Flat R S] (d : ℕ)
    (hfib : ∀ (p : Ideal R) [p.IsPrime], Nontrivial (p.Fiber S) →
      (∀ (Q : Ideal (p.Fiber S)) [Q.IsPrime],
          Module.IsMaximalCohenMacaulay (Localization.AtPrime Q) (Localization.AtPrime Q)) ∧
        TopologicalSpace.Equidimensional (PrimeSpectrum (p.Fiber S)) ∧
        ringKrullDim (p.Fiber S) = (d : WithBot ℕ∞))
    (e : ℕ) (n : ℕ → ℕ) (φ : ∀ i, (Fin (n (i + 1)) → S) →ₗ[S] (Fin (n i) → S))
    (hφ : ∀ k < e, φ k ∘ₗ φ (k + 1) = 0) :
    IsOpen {q : PrimeSpectrum S |
      Function.Injective ((φ e).baseChange (Localization.AtPrime q.asIdeal ⧸
          (q.asIdeal.under R).map (algebraMap R (Localization.AtPrime q.asIdeal)))) ∧
      ∀ k < e, Function.Exact
        ((φ (k + 1)).baseChange (Localization.AtPrime q.asIdeal ⧸
          (q.asIdeal.under R).map (algebraMap R (Localization.AtPrime q.asIdeal))))
        ((φ k).baseChange (Localization.AtPrime q.asIdeal ⧸
          (q.asIdeal.under R).map (algebraMap R (Localization.AtPrime q.asIdeal))))}

Tag 00RC, a theorem

Tag 00RC in the Stacks Project.

Module.isOpen_setOf_flat_localizedModule_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/OpenFlatLocus.lean, line 1056. References: EGA IV (11.3.1), “U open, affine case”; EGA IV (11.1.6), “case C = B”; EGA IV (11.3.3), “case C = B”; SGA 1 IV (6.10), “affine case”.

For a finitely presented ring map R → S and a finitely presented S-module M, the locus of primes q of S at which M_q is flat over R is open.

public theorem Module.isOpen_setOf_flat_localizedModule_atPrime
    {R : Type*} {S : Type*} {M : Type*}
    [CommRing R] [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S]
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.FinitePresentation S M] :
    IsOpen {q : PrimeSpectrum S | Module.Flat R (LocalizedModule.AtPrime q.asIdeal M)}

Sources

• Section 10.129, Tag 00R8
• AxiomMath/Stacks at 5ed82d14

LeanModule.IsMaximalCohenMacaulay.ringKrullDim_quotient_add_length_eq_and_isRegular · Algebra.isOpen_setOf_isRegular_fiber_of_isMaximalCohenMacaulay_of_equidimensional · Algebra.isOpen_setOf_injective_and_exact_baseChange_fiber · Module.isOpen_setOf_flat_localizedModule_atPrime

Section10.130 Openness of Cohen-Macaulay loci#

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

Tag 00RE, a lemma

Tag 00RE in the Stacks Project.

Module.Flat.atPrime_iff_isMaximalCohenMacaulay_and_relativeDimensionAt_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Locus.lean, line 398. The attribute's comment: “Cohen-Macaulayness of the Noetherian local ring S_𝔮 (Definition 00N8) is Module.IsMaximalCohenMacaulay Sq Sq; k[y_1, …, y_d] is MvPolynomial σ k with d = Nat.card σ; the localization is an abstract IsLocalization.AtPrime; and the equality of subsets of Spec S is stated pointwise at 𝔮, with the source's global quasi-finiteness of φ weakened to quasi-finiteness at 𝔮 (Definition 00PL). See the module docstring.”.

Stacks 00RE. Let S be a finite type algebra over a field k, let φ : k[y_1, …, y_d] → S be a map of k-algebras from a polynomial ring in d = Nat.card σ variables, and let 𝔮 be a prime of S at which φ is quasi-finite, with localization S_𝔮 = Sq. Then S_𝔮 is flat over k[y_1, …, y_d] if and only if S_𝔮 is Cohen–Macaulay and dim_𝔮(S/k) = d. Taking Sq = Localization.AtPrime 𝔮 and Set.ext, this is the source's equality of the flat locus and the Cohen–Macaulay locus of relative dimension d inside Spec(S).

public theorem Module.Flat.atPrime_iff_isMaximalCohenMacaulay_and_relativeDimensionAt_eq
    {k S : Type*} [Field k] [CommRing S] [Algebra k S] [Algebra.FiniteType k S] {σ : Type*}
    [Finite σ] [Algebra (MvPolynomial σ k) S] [IsScalarTower k (MvPolynomial σ k) S]
    (𝔮 : Ideal S) [𝔮.IsPrime] [Algebra.QuasiFiniteAt (MvPolynomial σ k) 𝔮] (Sq : Type*)
    [CommRing Sq] [Algebra S Sq] [IsLocalization.AtPrime Sq 𝔮] [IsLocalRing Sq]
    [Algebra (MvPolynomial σ k) Sq] [IsScalarTower (MvPolynomial σ k) S Sq] :
    Module.Flat (MvPolynomial σ k) Sq ↔
      Module.IsMaximalCohenMacaulay Sq Sq ∧ Algebra.relativeDimensionAt k 𝔮 = Nat.card σ

Tag 00RF, a lemma

Tag 00RF in the Stacks Project.

PrimeSpectrum.isOpen_setOf_isMaximalCohenMacaulay_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/OpenLocus.lean, line 722. The attribute's comment: “Cohen-Macaulayness of the local ring S_𝔮 (Definition 00N8) is Module.IsMaximalCohenMacaulay of Localization.AtPrime 𝔮 over itself. The proof is the case R = k of Lemma 00RH; see the module docstring.”. References: EGA IV (6.11.3), “affine over field, F=O_X”; EGA IV (12.1.7), “(iii), over a field”.

Stacks 00RF. Let S be a finite type algebra over a field k. The set of primes 𝔮 of S such that the local ring S_𝔮 is Cohen–Macaulay is open in Spec S.

theorem PrimeSpectrum.isOpen_setOf_isMaximalCohenMacaulay_localization (k S : Type*) [Field k]
    [CommRing S] [Algebra k S] [Algebra.FiniteType k S] :
    IsOpen {q : PrimeSpectrum S |
      Module.IsMaximalCohenMacaulay (Localization.AtPrime q.asIdeal)
        (Localization.AtPrime q.asIdeal)}

Tag 00RG, a lemma

Tag 00RG in the Stacks Project.

PrimeSpectrum.isOpen_and_dense_setOf_isMaximalCohenMacaulay_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/OpenLocus.lean, line 750. The attribute's comment: “Cohen-Macaulayness of S_𝔮 is Module.IsMaximalCohenMacaulay of Localization.AtPrime 𝔮 over itself; "dense open" is the conjunction of IsOpen and Dense.”. References: EGA IV (6.11.3), “affine over field, F=O_X”; EGA IV (12.1.7), “(iii), over a field”.

Stacks 00RG. Let S be a finite type algebra over a field k. The set of primes 𝔮 of S at which S_𝔮 is Cohen–Macaulay is a dense open subset of Spec S: it is open by Lemma 00RF and contains every minimal prime, where the local ring has dimension zero.

theorem PrimeSpectrum.isOpen_and_dense_setOf_isMaximalCohenMacaulay_localization (k S : Type*)
    [Field k] [CommRing S] [Algebra k S] [Algebra.FiniteType k S] :
    IsOpen {q : PrimeSpectrum S |
        Module.IsMaximalCohenMacaulay (Localization.AtPrime q.asIdeal)
          (Localization.AtPrime q.asIdeal)} ∧
      Dense {q : PrimeSpectrum S |
        Module.IsMaximalCohenMacaulay (Localization.AtPrime q.asIdeal)
          (Localization.AtPrime q.asIdeal)}

Tag 00RH, a lemma

Tag 00RH in the Stacks Project.

Algebra.isOpen_setOf_isMaximalCohenMacaulay_fiber_and_relativeDimensionAt_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/OpenLocus.lean, line 626. The attribute's comment: “The fibre ring S_𝔮/𝔭S_𝔮 is Localization.AtPrime of the image of 𝔮 in S/𝔭S, 𝔭 = 𝔮.under R, as in 00RK; Cohen-Macaulayness of a local ring (Definition 00N8) is Module.IsMaximalCohenMacaulay A A, and dim_𝔮(S/R) is Algebra.relativeDimensionAt R 𝔮.”. References: EGA IV (12.1.7), “(iii)”.

Stacks 00RH. Let R → S be flat of finite presentation and let d ≥ 0. The set of primes 𝔮 of S such that, with 𝔭 = R ∩ 𝔮, the fibre ring S_𝔮/𝔭S_𝔮 is Cohen–Macaulay and dim_𝔮(S/R) = d is open in Spec S. The fibre ring is spelled as the localization of S/𝔭S at the image of 𝔮.

theorem Algebra.isOpen_setOf_isMaximalCohenMacaulay_fiber_and_relativeDimensionAt_eq
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S]
    [Algebra.FinitePresentation R S] (d : ℕ) :
    IsOpen {q : PrimeSpectrum S |
      Module.IsMaximalCohenMacaulay
          (Localization.AtPrime (q.asIdeal.map (Ideal.Quotient.mk
            ((q.asIdeal.under R).map (algebraMap R S)))))
          (Localization.AtPrime (q.asIdeal.map (Ideal.Quotient.mk
            ((q.asIdeal.under R).map (algebraMap R S))))) ∧
        Algebra.relativeDimensionAt R q.asIdeal = d}

Tag 00RI, a lemma

Tag 00RI in the Stacks Project.

Algebra.isOpen_setOf_isMaximalCohenMacaulay_fiber_and_dense_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/OpenLocus.lean, line 772. The attribute's comment: “The fibre ring is Localization.AtPrime of the image of 𝔮 in S/𝔭S, as in 00RH and 00RK. The fibre over 𝔭 is the subspace comap (algebraMap R S) ⁻¹' {𝔭} of Spec S and density is for its subspace topology; openness is asserted in all of Spec S, which implies openness in each fibre. See the module docstring.”. References: EGA IV (12.1.1), “(vi), affine, F=O_X”; EGA IV (12.1.7), “(iii), affine flat”; SGA 4 XVIII (2.3), “affine case”.

Stacks 00RI. Let R → S be flat of finite presentation. The set W of primes 𝔮 of S at which the fibre ring S_𝔮 ⊗_R κ(𝔭), 𝔭 = R ∩ 𝔮, is Cohen–Macaulay is open in Spec S, and for every prime 𝔭 of R its trace on the fibre Spec S ×_{Spec R} {𝔭} of Spec S → Spec R is dense in that fibre.

theorem Algebra.isOpen_setOf_isMaximalCohenMacaulay_fiber_and_dense_fiber
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S]
    [Algebra.FinitePresentation R S] :
    IsOpen {q : PrimeSpectrum S |
      Module.IsMaximalCohenMacaulay
          (Localization.AtPrime (q.asIdeal.map (Ideal.Quotient.mk
            ((q.asIdeal.under R).map (algebraMap R S)))))
          (Localization.AtPrime (q.asIdeal.map (Ideal.Quotient.mk
            ((q.asIdeal.under R).map (algebraMap R S)))))} ∧
    ∀ p : PrimeSpectrum R,
      Dense ((↑) ⁻¹' {q : PrimeSpectrum S |
        Module.IsMaximalCohenMacaulay
          (Localization.AtPrime (q.asIdeal.map (Ideal.Quotient.mk
            ((q.asIdeal.under R).map (algebraMap R S)))))
          (Localization.AtPrime (q.asIdeal.map (Ideal.Quotient.mk
            ((q.asIdeal.under R).map (algebraMap R S)))))} :
        Set (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}))

Tag 00RJ, a lemma

Tag 00RJ in the Stacks Project.

Algebra.IsPushout.isMaximalCohenMacaulay_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/LocusBaseChange.lean, line 159. The attribute's comment: “Cohen-Macaulayness of a Noetherian local ring A (Definition 00N8) is Module.IsMaximalCohenMacaulay A A (tag 00NF); the base change K ⊗_k S is an arbitrary pushout square of k-algebras Algebra.IsPushout k K S T, as in the sibling 00P4; the two local rings are abstract IsLocalization.AtPrimes; and 𝔮_K lying over 𝔮 is Ideal.LiesOver. See the module docstring.”. References: EGA IV (6.7.1), “(i), CM, affine”; SGA 3 VIA (1.1.1), “special case”.

Let k be a field, let S be a finite type k-algebra, let K/k be a field extension and let T = K ⊗_k S be the base change, presented as a pushout square. Let 𝔮K be a prime of T lying over the prime 𝔮 of S, and let Sq = S_𝔮 and TqK = T_{𝔮K} be the local rings at them. Then S_𝔮 is Cohen–Macaulay if and only if T_{𝔮K} is Cohen–Macaulay.

public theorem isMaximalCohenMacaulay_iff (k K S T : Type*) [Field k] [Field K] [CommRing S]
    [CommRing T] [Algebra k K] [Algebra k S] [Algebra k T] [Algebra K T] [Algebra S T]
    [IsScalarTower k K T] [IsScalarTower k S T] [Algebra.IsPushout k K S T]
    [Algebra.FiniteType k S] (𝔮 : Ideal S) [𝔮.IsPrime] (𝔮K : Ideal T) [𝔮K.IsPrime]
    [𝔮K.LiesOver 𝔮] (Sq : Type*) [CommRing Sq] [Algebra S Sq] [IsLocalization.AtPrime Sq 𝔮]
    [IsLocalRing Sq] (TqK : Type*) [CommRing TqK] [Algebra T TqK]
    [IsLocalization.AtPrime TqK 𝔮K] [IsLocalRing TqK] :
    Module.IsMaximalCohenMacaulay Sq Sq ↔ Module.IsMaximalCohenMacaulay TqK TqK

Tag 00RK, a lemma

Tag 00RK in the Stacks Project.

Algebra.IsPushout.setOf_isMaximalCohenMacaulay_fiber_eq_preimage_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/LocusBaseChange.lean, line 401. The attribute's comment: “The base change is an arbitrary pushout square Algebra.IsPushout R R' S S', as in the siblings 00P3, 00P4 and 00SS, so f is PrimeSpectrum.comap (algebraMap S S'). The fibre ring S_𝔮 ⊗_R κ(𝔭) is Localization.AtPrime of the image of 𝔮 in S/𝔭S, with 𝔭 = 𝔮.under R, as in 00RH and 00RI, and Cohen-Macaulayness of a local ring (Definition 00N8) is Module.IsMaximalCohenMacaulay A A (tag 00NF). The conclusion is the source's equality of sets of primes; Set.ext_iff gives the pointwise form. See the module docstring.”.

Let R → S be of finite type, let R → R' be any ring map and let S' = R' ⊗_R S, presented as a pushout square. Let f : Spec S' → Spec S be the map of the ring map S → S'. Then the set W' of primes 𝔮' of S' whose fibre ring S'_{𝔮'} ⊗_{R'} κ(𝔭'), 𝔭' = R' ∩ 𝔮', is Cohen–Macaulay is the preimage f ⁻¹' W of the corresponding set W for S over R. The fibre ring is the localization of S/𝔭S at the prime 𝔮/𝔭S.

public theorem setOf_isMaximalCohenMacaulay_fiber_eq_preimage_comap (R R' S S' : Type*)
    [CommRing R] [CommRing R'] [CommRing S] [CommRing S'] [Algebra R R'] [Algebra R S]
    [Algebra R S'] [Algebra R' S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
    [Algebra.IsPushout R R' S S'] [Algebra.FiniteType R S] :
    {𝔮' : PrimeSpectrum S' |
        Module.IsMaximalCohenMacaulay
          (Localization.AtPrime (𝔮'.asIdeal.map (Ideal.Quotient.mk
            ((𝔮'.asIdeal.under R').map (algebraMap R' S')))))
          (Localization.AtPrime (𝔮'.asIdeal.map (Ideal.Quotient.mk
            ((𝔮'.asIdeal.under R').map (algebraMap R' S')))))} =
      PrimeSpectrum.comap (algebraMap S S') ⁻¹'
        {𝔮 : PrimeSpectrum S |
          Module.IsMaximalCohenMacaulay
            (Localization.AtPrime (𝔮.asIdeal.map (Ideal.Quotient.mk
              ((𝔮.asIdeal.under R).map (algebraMap R S)))))
            (Localization.AtPrime (𝔮.asIdeal.map (Ideal.Quotient.mk
              ((𝔮.asIdeal.under R).map (algebraMap R S)))))}

Tag 00RL, a lemma

Tag 00RL in the Stacks Project.

Algebra.exists_algEquiv_pi_of_isMaximalCohenMacaulay_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/OpenLocus.lean, line 816. The attribute's comment: “The fibre ring is Localization.AtPrime of the image of 𝔮 in S/𝔭S, as in 00RH. "All fibres equidimensional of dimension d" is Algebra.relativeDimensionAt R 𝔮 = d at every prime 𝔮 of S_d, which is equivalent over a field by Lemma 00OT. The factors are indexed by Fin (n + 1) and live in the universe of S. See the module docstring.”.

Stacks 00RL. Let R → S be flat, of finite presentation and with Cohen–Macaulay fibres, that is with every fibre ring S_𝔮/𝔭S_𝔮 Cohen–Macaulay. Then S ≅ S_0 × ⋯ × S_n as R-algebras, where each S_d is flat, of finite presentation and with Cohen–Macaulay fibres over R, and all fibres of R → S_d are equidimensional of dimension d: the relative dimension dim_𝔮(S_d/R) is d at every prime 𝔮 of S_d.

theorem Algebra.exists_algEquiv_pi_of_isMaximalCohenMacaulay_fiber (R : Type u) (S : Type v)
    [CommRing R]
    [CommRing S] [Algebra R S] [Module.Flat R S] [Algebra.FinitePresentation R S]
    (hCM : ∀ q : PrimeSpectrum S,
      Module.IsMaximalCohenMacaulay
          (Localization.AtPrime (q.asIdeal.map (Ideal.Quotient.mk
            ((q.asIdeal.under R).map (algebraMap R S)))))
          (Localization.AtPrime (q.asIdeal.map (Ideal.Quotient.mk
            ((q.asIdeal.under R).map (algebraMap R S)))))) :
    ∃ (n : ℕ) (S' : Fin (n + 1) → Type v) (_ : ∀ d, CommRing (S' d)) (_ : ∀ d, Algebra R (S' d)),
      Nonempty (S ≃ₐ[R] Π d, S' d) ∧ ∀ d, Module.Flat R (S' d) ∧
        Algebra.FinitePresentation R (S' d) ∧
        (∀ q : PrimeSpectrum (S' d),
          Module.IsMaximalCohenMacaulay
            (Localization.AtPrime (q.asIdeal.map (Ideal.Quotient.mk
              ((q.asIdeal.under R).map (algebraMap R (S' d))))))
            (Localization.AtPrime (q.asIdeal.map (Ideal.Quotient.mk
              ((q.asIdeal.under R).map (algebraMap R (S' d))))))) ∧
        ∀ q : PrimeSpectrum (S' d), Algebra.relativeDimensionAt R q.asIdeal = (d : ℕ)

Sources

• Section 10.130, Tag 00RD
• AxiomMath/Stacks at 5ed82d14

LeanModule.Flat.atPrime_iff_isMaximalCohenMacaulay_and_relativeDimensionAt_eq · PrimeSpectrum.isOpen_setOf_isMaximalCohenMacaulay_localization · PrimeSpectrum.isOpen_and_dense_setOf_isMaximalCohenMacaulay_localization · Algebra.isOpen_setOf_isMaximalCohenMacaulay_fiber_and_relativeDimensionAt_eq · Algebra.isOpen_setOf_isMaximalCohenMacaulay_fiber_and_dense_fiber · Algebra.IsPushout.isMaximalCohenMacaulay_iff · Algebra.IsPushout.setOf_isMaximalCohenMacaulay_fiber_eq_preimage_comap · Algebra.exists_algEquiv_pi_of_isMaximalCohenMacaulay_fiber

Section10.131 Differentials#

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

Tag 00RN, a definition

Tag 00RN in the Stacks Project.

Declarations registered for the tag:

• Derivation registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Defs.lean, line 32 (StacksFrontier): “derivations”. References: EGA 0 (20.1.1), “special case”; EGA 0 (20.1.2), “commutative, 1-sided mod”; SGA 3 VIIA (1.2.0), “special case”; SGA 3 VIIA (5.2), “special case”; SGA 7 X (2.26).
• Derivation.mk registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Defs.lean, line 38 (StacksFrontier): “the constructor”. References: EGA 0 (20.1.2), “commutative, 1-sided mod”.
• Derivation.map_algebraMap registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Defs.lean, line 40 (StacksFrontier): “annihilates the image of the base ring map”. References: EGA 0 (20.1.2), “vanishes on image of A”.
• Derivation.leibniz registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Defs.lean, line 42 (StacksFrontier): “the Leibniz rule”. References: EGA 0 (20.1.2), “Leibniz rule (ii)”.

Tag 07BK, a definition

Tag 07BK in the Stacks Project.

Declarations registered for the tag:

• KaehlerDifferential registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Defs.lean, line 46 (StacksFrontier): “the module of differentials”. References: EGA 0 (20.4.3), “special case”; EGA IV (16.3.1), “affine Ω¹_{X/S}”; EGA IV (16.3.7); EGA IV (17.13.5), “Affine case”; EGA IV (17.15.8); SGA 1 II (5.7); SGA 1 II (5.9); SGA 6 0 (2.1), “special case”; SGA 6 VIII (2.2); SGA 6 VIII (2.4); SGA 7 VI (1.17), “Ω when K is a field”; SGA 7 VI (5.1), “special case”; SGA 7 VI (5.5), “special case”.
• KaehlerDifferential.D registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Defs.lean, line 60 (StacksFrontier): “its universal derivation”. References: EGA 0 (20.4.8), “(ii), derivation clause”; EGA IV (16.3.6), “special case”; EGA IV (16.5.3), “(i), affine case”; SGA 7 VI (1.17), “d, special case”.

Tag 00RO, a lemma

Tag 00RO in the Stacks Project.

Declarations registered for the tag:

• KaehlerDifferential.linearMapEquivDerivation registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Defs.lean, line 67 (StacksFrontier). References: EGA IV (16.5.14), “partial”; EGA IV (16.5.7), “special case”; EGA IV (16.5.3), “(ii), affine case”; EGA 0 (20.4.8), “(ii), discrete case”; EGA IV (16.5.3), “(ii), affine/ring case”; SGA 1 III (5.2), “special case”; SGA 3 VIIA (1.3.1), “special case”; SGA 3 II (3.14), “affine case”.
• KaehlerDifferential.linearMapEquivDerivation_apply_apply registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Defs.lean, line 74 (StacksFrontier): “the map is α ↦ α ∘ d”.

Tag 00RP, a lemma

Tag 00RP in the Stacks Project.

Declarations registered for the tag:

• KaehlerDifferential.subsingleton_of_surjective registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Basic.lean, line 84 (StacksFrontier): “Ω[S⁄R] vanishes when R → S is surjective”. References: EGA 0 (20.4.12), “discrete case”.

Tag 0H2F, an equation

Tag 0H2F in the Stacks Project.

Stacks.KaehlerDifferential.Presentation.presentation_square_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/Presentation.lean, line 131.

Stacks Tag 0H2F. Given a commutative square of commutative rings φ ∘ α = β ∘ ψ (here phrased as φ.comp α = β.comp ψ), the square of presentations of Kähler differentials commutes: Φ_F ∘ ∂_{S/R} = ∂_{S'/R'} ∘ Φ_P as φ-semilinear maps P_{S/R} → F_{S'/R'}.

theorem presentation_square_comm
    {R S R' S' : Type*} [CommRing R] [CommRing S] [CommRing R'] [CommRing S']
    (α : R →+* S) (β : R' →+* S') (φ : S →+* S') (ψ : R →+* R')
    (hcomm : φ.comp α = β.comp ψ) :
    (PhiF φ).comp (presentationMap α)
      = (presentationMap β).comp (PhiP φ ψ)

Tag 031G, a lemma

Tag 031G in the Stacks Project.

Stacks.KaehlerDifferential.Colimit.main_theorem_031g, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/Colimit.lean, line 949.

Stacks Tag 031G. For a system of ring maps over a directed set I, the canonical comparison map Θ : colim_i Ω[S_i⁄R_i] → Ω[S⁄R] is bijective (an isomorphism of abelian groups, equivalently of S-modules).

theorem main_theorem_031g (hsq : IsCompatible fR fS)
    (hdirS : DirectedSystem S (fun _ _ h => (fS h : S _ → S _))) :
    Function.Bijective (Theta fR fS hsq)

Tag 00RR, a lemma

Tag 00RR in the Stacks Project.

KaehlerDifferential.map_surjective_and_ker_eq_span_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/KernelOfSurjection.lean, line 74.

In a commutative square of rings

S --φ--> S'
↑        ↑
|        |
R -----> R'

with φ : S → S' surjective, the map Ω[S⁄R] → Ω[S'⁄R'] is surjective and its kernel is the S-submodule generated by the da with a ∈ S such that φ(a) lies in the image of R' (among them the di with i ∈ ker φ).

theorem map_surjective_and_ker_eq_span_of_surjective
    (h : Function.Surjective (algebraMap S S')) :
    Function.Surjective (map R R' S S') ∧
      LinearMap.ker (map R R' S S') =
        Submodule.span S (⇑(D R S) '' {a | algebraMap S S' a ∈ Set.range (algebraMap R' S')})

Tag 00RS, a lemma

Tag 00RS in the Stacks Project.

Declarations registered for the tag:

• KaehlerDifferential.exact_mapBaseChange_map registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Basic.lean, line 90 (StacksFrontier): “exactness at the middle term of the sequence of a tower”. References: EGA 0 (20.5.7), “partial”; EGA IV (16.4.19), “exact at Ω, affine”; EGA 0 (20.6.17), “exact at Ω¹_{C/A}”; EGA 0 (20.6.5), “H_0 = Ω_{C/B}”; EGA 0 (20.6.17), “second assertion”; EGA IV (16.4.19), “second assertion”; SGA 1 II (4.3), “(i)”; SGA 6 VIII (2.2), “partial”; SGA 6 VIII (2.6), “partial”; SGA 6 VIII (5.2), “partial”.
• KaehlerDifferential.map_surjective registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Basic.lean, line 100 (StacksFrontier): “surjectivity of Ω[C⁄A] → Ω[C⁄B]”. References: EGA 0 (20.5.7), “partial”; SGA 6 VIII (5.2), “partial”.

Tag 00RT, a lemma

Tag 00RT in the Stacks Project.

omega_localization_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/BaseChange.lean, line 87. The attribute's comment: “(1)”. References: EGA 0 (20.5.5), “special case”.

Let A → B be a ring map and let S ⊆ A be a multiplicative subset whose image consists of units of B, so that B is an Aₛ = S⁻¹A-algebra. Then the canonical B-linear map Ω_{B/A} → Ω_{B/Aₛ} is bijective.

theorem omega_localization_base
    (A : Type*) [CommRing A] (B : Type*) [CommRing B] [Algebra A B]
    (S : Submonoid A) (Aₛ : Type*) [CommRing Aₛ] [Algebra A Aₛ] [IsLocalization S Aₛ]
    [Algebra Aₛ B] [IsScalarTower A Aₛ B] :
    Function.Bijective (KaehlerDifferential.map A Aₛ B B)

omega_localization_total, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/BaseChange.lean, line 106. The attribute's comment: “(2)”. References: EGA 0 (20.5.9).

Let A → B be a ring map, let S ⊆ B be a multiplicative subset and Bₛ = S⁻¹B. Then the canonical map Ω_{B/A} → Ω_{Bₛ/A} exhibits Ω_{Bₛ/A} as the localization S⁻¹ Ω_{B/A}.

theorem omega_localization_total
    (A : Type*) [CommRing A] (B : Type*) [CommRing B] [Algebra A B]
    (S : Submonoid B) (Bₛ : Type*) [CommRing Bₛ] [Algebra B Bₛ] [IsLocalization S Bₛ]
    [Algebra A Bₛ] [IsScalarTower A B Bₛ] :
    IsLocalizedModule S (KaehlerDifferential.map A A B Bₛ)

Tag 00RU, a lemma

Tag 00RU in the Stacks Project.

Stacks.KaehlerDifferential.Conormal.conormalSequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/KerCotangentToTensor.lean, line 55. The attribute's comment: “exactness at the middle”. References: EGA 0 (20.5.12), “(i)”; EGA 0 (20.6.23), “partial”; EGA 0 (20.6.9), “partial”; EGA 0 (22.4.4.2), “partial”; SGA 3 III (4.25), “exactness at middle”.

Exactness at B ⊗[A] Ω[A⁄R]. The kernel of the base-change map mapBaseChange is the range of the conormal map kerCotangentToTensor.

theorem conormalSequence_exact (R A B : Type*) [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B]
    (hφ : Function.Surjective (algebraMap A B)) :
    Function.Exact (kerCotangentToTensor R A B) (mapBaseChange R A B)

Stacks.KaehlerDifferential.Conormal.conormalSequence_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/KerCotangentToTensor.lean, line 68. The attribute's comment: “surjectivity on the right”. References: EGA 0 (20.5.12), “(i)”; EGA 0 (20.6.23), “partial”; EGA 0 (20.6.9), “partial”; EGA 0 (22.4.4.2), “partial”; SGA 3 III (4.25), “surjectivity in (+)”.

Exactness at Ω[B⁄R]. The base-change map mapBaseChange is surjective.

theorem conormalSequence_surjective (R A B : Type*) [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B]
    (hφ : Function.Surjective (algebraMap A B)) :
    Function.Surjective (mapBaseChange R A B)

Stacks.KaehlerDifferential.Conormal.kerCotangentToTensor_class, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/KerCotangentToTensor.lean, line 84. The attribute's comment: “the formula for the left-hand map”. References: EGA 0 (20.5.11), “formula on classes”; EGA 0 (22.6.4), “partial”; SGA 1 II (5.9), “partial”; SGA 3 III (4.8), “special case”; SGA 6 VIII (2.1), “special case”.

The left-hand map of the conormal sequence on classes of sections of the ideal. The class of f ∈ I in I/I² maps to 1 ⊗ₜ d f, which is the source's d f ⊗ 1.

theorem kerCotangentToTensor_class (R A B : Type*) [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B]
    (x : RingHom.ker (algebraMap A B)) :
    kerCotangentToTensor R A B ((RingHom.ker (algebraMap A B)).toCotangent x)
      = 1 ⊗ₜ[A] (D R A) x

Declarations registered for the tag:

• KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Basic.lean, line 107 (StacksFrontier): “exactness at the middle term”. References: EGA 0 (20.5.12), “partial”; EGA 0 (20.6.23), “partial”; EGA 0 (22.4.8), “partial”; EGA IV (16.4.21), “special case”; EGA IV (17.2.5), “affine middle exactness”.
• KaehlerDifferential.mapBaseChange_surjective registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Basic.lean, line 115 (StacksFrontier): “surjectivity onto Ω[B⁄R]”. References: EGA IV (17.13.1), “special case”.

Tag 02HP, a lemma

Tag 02HP in the Stacks Project.

KaehlerDifferential.split_exact_kerCotangentToTensor_mapBaseChange_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/Basic.lean, line 355. The attribute's comment: “Recorded in full, as the decomposition of the middle term of the sequence of 00RU carrying its two maps to LinearMap.inl and LinearMap.snd. The hypothesis is a section of P ⧸ I² → S rather than of P → S, and surjectivity of P → S is derived from it rather than assumed.”. References: EGA 0 (20.6.22), “Case Λ = A”.

Let R → P → S be commutative rings, let I = ker(P → S), and suppose there is an R-algebra map g : S → P ⧸ I² that is a right inverse to P ⧸ I² → S. Then the exact sequence 0 → I/I² → S ⊗[P] Ω[P⁄R] → Ω[S⁄R] → 0 is split short exact: it is isomorphic to the trivial sequence, by an isomorphism S ⊗[P] Ω[P⁄R] ≃ I/I² × Ω[S⁄R] carrying KaehlerDifferential.kerCotangentToTensor R P S to LinearMap.inl and KaehlerDifferential.mapBaseChange R P S to LinearMap.snd. Nothing is required of P.

theorem split_exact_kerCotangentToTensor_mapBaseChange_of_section {R P S : Type*}
    [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S]
    [IsScalarTower R P S] (g : S →ₐ[R] P ⧸ RingHom.ker (algebraMap P S) ^ 2)
    (hg : (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S) :
    ∃ e : S ⊗[P] Ω[P⁄R] ≃ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent × Ω[S⁄R],
      kerCotangentToTensor R P S =
          e.symm ∘ₗ LinearMap.inl P (RingHom.ker (algebraMap P S)).Cotangent Ω[S⁄R] ∧
        (mapBaseChange R P S).restrictScalars P =
          LinearMap.snd P (RingHom.ker (algebraMap P S)).Cotangent Ω[S⁄R] ∘ₗ e.toLinearMap

Tag 02HQ, a lemma

Tag 02HQ in the Stacks Project.

kaehlerReductionMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/AdicQuotient.lean, line 402.

Stacks Tag 02HQ (Lemma 10.131.11). For a ring map R → S, an ideal I ⊆ S, and an integer n ≥ 1, with S' = S/I^{n+1}, the comparison map

Φ : Ω[S/R] ⊗[S] (S/I^n) → Ω[S'/R] ⊗[S'] (S/I^n)

induced by the functoriality map dπ : Ω[S/R] → Ω[S'/R] is bijective (an isomorphism).

theorem kaehlerReductionMap_bijective :
    Function.Bijective (kaehlerReductionMap R S I n)

Tag 00RV, a lemma

Tag 00RV in the Stacks Project.

Declarations registered for the tag:

• KaehlerDifferential.tensorKaehlerEquivBase registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/BaseChange.lean, line 122 (StacksFrontier): “for an arbitrary pushout square, with the tensor factors in the other order”. References: EGA 0 (21.3.6), “partial”; EGA 0 (22.4.4.7), “more general”; EGA 0 (22.4.8), “more general”; EGA IV (16.4.5), “special case”; EGA IV (16.5.10), “(16.5.10.1) affine case”; EGA 0 (20.5.5); SGA 3 III (0.12), “special case”; SGA 3 III (4.8), “(iii), special case”; SGA 3 VIA (1.3.2), “Differentials clause”; SGA 5 III (6.9), “special case”; SGA 7 VI (5.5), “special case”.
• KaehlerDifferential.tensorKaehlerEquiv registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/BaseChange.lean, line 134 (StacksFrontier): “the variant over the base-changed algebra”. References: EGA 0 (20.5.5); EGA 0 (21.3.6), “partial”; EGA 0 (22.4.4.7), “more general”; EGA 0 (22.4.8), “more general”; EGA IV (16.5.10), “(16.5.10.1) affine case”.

Tag 00RW, a lemma

Tag 00RW in the Stacks Project.

Declarations registered for the tag:

• KaehlerDifferential registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Defs.lean, line 81 (StacksFrontier): “Ω[S⁄R] is J / J ^ 2”. References: EGA 0 (20.4.3), “special case”; EGA IV (16.3.1), “affine Ω¹_{X/S}”; EGA IV (16.3.7); EGA IV (17.13.5), “Affine case”; EGA IV (17.15.8); SGA 1 II (5.7); SGA 1 II (5.9); SGA 6 0 (2.1), “special case”; SGA 6 VIII (2.2); SGA 6 VIII (2.4); SGA 7 VI (1.17), “Ω when K is a field”; SGA 7 VI (5.1), “special case”; SGA 7 VI (5.5), “special case”.
• KaehlerDifferential.ideal registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Defs.lean, line 82 (StacksFrontier): “the ideal J”. References: EGA 0 (20.4.1); SGA 3 VIIA (1.4.1), “special case”.
• KaehlerDifferential.D_apply registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Defs.lean, line 85 (StacksFrontier): “d b = 1 ⊗ b - b ⊗ 1”. References: EGA IV (16.3.6), “special case”.

Tag 00RX, a lemma

Tag 00RX in the Stacks Project.

Declarations registered for the tag:

• KaehlerDifferential.mvPolynomialBasis registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Basic.lean, line 125 (StacksFrontier): “the basis d x_i of Ω[R[x_1, …, x_n]⁄R]”. References: EGA 0 (20.4.13); EGA 0 (21.2.5), “special case”; EGA IV (16.5.8), “affine space over a ring”; EGA IV (16.6.5), “special case”; SGA 6 VIII (5.2), “special case”; SGA 1 II (4.2), “second assertion”; SGA 1 II (4.2), “exact at Ω¹_{C/A}”.
• KaehlerDifferential.mvPolynomialBasis_apply registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Basic.lean, line 133 (StacksFrontier): “the basis consists of the d x_i”. References: EGA 0 (20.4.13); EGA 0 (21.2.5), “special case”; SGA 1 II (4.2), “second assertion”; SGA 1 II (4.2), “exact at Ω, affine”.

Tag 00RY, a lemma

Tag 00RY in the Stacks Project.

Declarations registered for the tag:

• Algebra.instFinitePresentationKaehlerDifferentialOfFinitePresentation registered with add_to_stacks in StacksFrontier/RingTheory/Kaehler/Basic.lean, line 144 (StacksFrontier): “Ω[S⁄R] is finitely presented when S is a finitely presented algebra”. References: EGA IV (16.4.22), “Ω¹ only, affine”; SGA 3 III (0.14), “special case”; SGA 7 VI (5.1), “special case”.

Tag 00RZ, a lemma

Tag 00RZ in the Stacks Project.

Declarations registered for the tag:

• KaehlerDifferential.finite registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch10.lean, line 244 (StacksFrontier). References: EGA 0 (21.7.1), “more general”; EGA IV (17.4.1.2), “special case”; SGA 7 VI (5.5), “Coherence of Ω_{X|S}”.

Sources

• Section 10.131, Tag 00RM
• AxiomMath/Stacks at 5ed82d14

LeanDerivation · Derivation.mk · Derivation.map_algebraMap · Derivation.leibniz · KaehlerDifferential · KaehlerDifferential.D · KaehlerDifferential.linearMapEquivDerivation · KaehlerDifferential.linearMapEquivDerivation_apply_apply

Section10.132 The de Rham complex#

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

Tag 0FKF, the section

Tag 0FKF in the Stacks Project.

KaehlerDifferential.deRhamDifferential_comp_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DeRham/Basic.lean, line 720. The attribute's comment: “the complex property d ∘ d = 0 of the de Rham complex of a ring map, on the exterior powers of the Kaehler differentials”.

The de Rham differential of B over A squares to zero. The elements b₀ · (d b₁ ∧ ⋯ ∧ d b_p) span Ω^p_{B/A} over A, and on such an element the defining rule computes the composite as a wedge whose first factor is d 1 = 0.

public theorem deRhamDifferential_comp_self (p : ℕ) (ξ : ⋀[B]^p (Ω[B⁄A])) :
    deRhamDifferential (A := A) (p + 1) (deRhamDifferential p ξ) = 0

KaehlerDifferential.deRhamDifferential_comp_deRhamDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DeRham/Basic.lean, line 738. The attribute's comment: “the complex property d ∘ d = 0 of the de Rham complex of a ring map, as an equality of A-linear maps”.

Consecutive de Rham differentials compose to zero, as an equality of A-linear maps. This is the complex property of the de Rham complex of B over A.

public theorem deRhamDifferential_comp_deRhamDifferential (p : ℕ) :
    (deRhamDifferential (A := A) (B := B) (p + 1)).comp (deRhamDifferential p) = 0

Stacks.DeRham.DifferentialDescent.sourceDeRham, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DeRham/Basic.lean, line 1087. The attribute's comment: “the de Rham complex of a ring map A → B, as the family of A-linear differentials on the exterior powers of the Kaehler differentials together with the defining rule on generators and the complex property d ∘ d = 0; this construction has no hypothesis”.

The de Rham complex of B over A, as a term of SourceDeRham A B: the de Rham differentials KaehlerDifferential.deRhamDifferential on the exterior powers of Ω[B⁄A], which obey the defining rule on generators by KaehlerDifferential.deRhamDifferential_smul_ιMulti_D. Nothing is supposed: the descent datum of Tag 07HY is produced here, and its complex property is the theorem KaehlerDifferential.deRhamDifferential_comp_deRhamDifferential, reached through the default value of the field complex.

noncomputable def sourceDeRham (A B : Type u) [CommRing A] [CommRing B] [Algebra A B] :
    SourceDeRham A B

KaehlerDifferential.deRhamComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DeRham/Complex.lean, line 77. The attribute's comment: “the de Rham complex Ω^0_{B/A} → Ω^1_{B/A} → ⋯ of a ring map A → B, as a CochainComplex of A-modules indexed by ℕ; the construction has no hypothesis”.

The de Rham complex Ω^0_{B/A} → Ω^1_{B/A} → Ω^2_{B/A} → ⋯ of B over A: the exterior powers of Ω[B⁄A], as A-modules, with the de Rham differentials as its arrows. The construction has no hypothesis — the arrows are deRhamDifferential and the square-zero condition is deRhamDifferential_comp_deRhamDifferential.

public noncomputable def deRhamComplex (A B : Type u) [CommRing A] [CommRing B]
    [Algebra A B] : CochainComplex (ModuleCat.{u} A) ℕ

Tag 0FKG, an equation

Tag 0FKG in the Stacks Project.

KaehlerDifferential.deRhamDifferential, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DeRham/Basic.lean, line 667. The attribute's comment: “the differential itself”.

The de Rham differential d : Ω^p_{B/A} → Ω^{p+1}_{B/A} in degree p: the A-linear map with d (b₀ · d b₁ ∧ ⋯ ∧ d b_p) = d b₀ ∧ d b₁ ∧ ⋯ ∧ d b_p for all b₀, …, b_p ∈ B, where d : B → Ω[B⁄A] is the universal A-derivation. That rule is deRhamDifferential_smul_ιMulti_D and deRhamDifferential_unique says it pins the map down.

public noncomputable def deRhamDifferential (p : ℕ) :
    ⋀[B]^p (Ω[B⁄A]) →ₗ[A] ⋀[B]^(p + 1) (Ω[B⁄A])

KaehlerDifferential.deRhamDifferential_smul_ιMulti_D, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DeRham/Basic.lean, line 678. The attribute's comment: “the defining rule of deRhamDifferential”.

The defining rule of the de Rham differential: d (b₀ · d b₁ ∧ ⋯ ∧ d b_p) = d b₀ ∧ d b₁ ∧ ⋯ ∧ d b_p. The leading scalar b₀ contributes the factor d b₀ through dp_apply_smul, and G_exact kills the wedge of exact forms.

public lemma deRhamDifferential_smul_ιMulti_D (p : ℕ) (b : Fin (p + 1) → B) :
    deRhamDifferential p (b 0 • exteriorPower.ιMulti B p fun i ↦ D A B (b i.succ)) =
      exteriorPower.ιMulti B (p + 1) fun i ↦ D A B (b i)

KaehlerDifferential.deRhamDifferential_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DeRham/Basic.lean, line 696. The attribute's comment: “uniqueness of deRhamDifferential”.

deRhamDifferential p is the only A-linear map Ω^p_{B/A} → Ω^{p+1}_{B/A} with d (b₀ · d b₁ ∧ ⋯ ∧ d b_p) = d b₀ ∧ d b₁ ∧ ⋯ ∧ d b_p, because those elements span Ω^p_{B/A} over A.

public theorem deRhamDifferential_unique (p : ℕ)
    (d : ⋀[B]^p (Ω[B⁄A]) →ₗ[A] ⋀[B]^(p + 1) (Ω[B⁄A]))
    (hd : ∀ b : Fin (p + 1) → B,
      d (b 0 • exteriorPower.ιMulti B p fun i ↦ D A B (b i.succ)) =
        exteriorPower.ιMulti B (p + 1) fun i ↦ D A B (b i)) :
    d = deRhamDifferential p

Tag 0H8Y, a lemma

Tag 0H8Y in the Stacks Project.

KaehlerDifferential.isBaseChange_exteriorPower_and_deRhamDifferential_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DeRham/Basic.lean, line 962. References: EGA IV (16.6.4), “affine case”.

Stacks 0H8Y. Let A → A' and A → B be ring maps, let B' = B ⊗_A A', and let ψ be the canonical map ⋀^p (KaehlerDifferential.map A A' B B'). Then ψ exhibits Ω^•_{B'/A'} as the base change of Ω^•_{B/A} along A → A', i.e. Ω^•_{B/A} ⊗_A A' = Ω^•_{B'/A'}, and it is a map of complexes for the de Rham differentials of B over A and of B' over A'.

public theorem isBaseChange_exteriorPower_and_deRhamDifferential_comm
    {A A' B B' : Type*} [CommRing A] [CommRing A'] [CommRing B] [CommRing B']
    [Algebra A A'] [Algebra A B] [Algebra A B'] [Algebra A' B'] [Algebra B B']
    [IsScalarTower A A' B'] [IsScalarTower A B B'] [Algebra.IsPushout A A' B B']
    (ψ : ∀ p : ℕ, ⋀[B]^p (Ω[B⁄A]) →ₗ[B] ⋀[B']^p (Ω[B'⁄A']))
    (hψ : ∀ (p : ℕ) (ω : Fin p → Ω[B⁄A]),
      ψ p (exteriorPower.ιMulti B p ω) =
        exteriorPower.ιMulti B' p fun i ↦ map A A' B B' (ω i)) :
    (∀ p : ℕ, IsBaseChange A' ((ψ p).restrictScalars A)) ∧
      ∀ (p : ℕ) (ω : ⋀[B]^p (Ω[B⁄A])), ψ (p + 1) (deRhamDifferential p ω) =
        deRhamDifferential (A := A') (B := B') p (ψ p ω)

Tag 07HY, a lemma

Tag 07HY in the Stacks Project.

exists_unique_quotient_deRhamDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DeRham/Basic.lean, line 1842.

Stacks 07HY. Let S be the de Rham complex of B over A and let π : Ω[B⁄A] → Ω be a surjection of B-modules whose kernel is generated by elements ω with π ω = 0 and (⋀^2 π) (d ω) = 0. Then there is exactly one family of A-linear maps Ω^p = ⋀[B]^p Ω → Ω^{p+1} making the squares d ∘ (⋀^p π) = (⋀^{p+1} π) ∘ d_{B/A} commute; it obeys the same rule d (f₀ · d f₁ ∧ ⋯ ∧ d f_p) = d f₀ ∧ ⋯ ∧ d f_p on generators, with d f = π (d_{B/A} f), and it is again a complex.

theorem exists_unique_quotient_deRhamDifferential
    (S : SourceDeRham A B)
    {Ω : Type u} [AddCommGroup Ω] [Module B Ω] (π : Ω[B⁄A] →ₗ[B] Ω)
    (hπ : Function.Surjective π)
    (hgen : S.GenerationHypothesis π) :
    ∃ dΩ : (∀ p, TgtA A B Ω p →ₗ[A] TgtA A B Ω (p + 1)),
      S.Commutes π dΩ ∧
      SatisfiesRule π dΩ ∧
      (∀ dΩ' : (∀ p, TgtA A B Ω p →ₗ[A] TgtA A B Ω (p + 1)), S.Commutes π dΩ' → dΩ' = dΩ) ∧
      (∀ p, (dΩ (p + 1)).comp (dΩ p) = 0)

Sources

• Section 10.132, Tag 0FKF
• AxiomMath/Stacks at 5ed82d14

LeanKaehlerDifferential.deRhamDifferential_comp_self · KaehlerDifferential.deRhamDifferential_comp_deRhamDifferential · Stacks.DeRham.DifferentialDescent.sourceDeRham · KaehlerDifferential.deRhamComplex · KaehlerDifferential.deRhamDifferential · KaehlerDifferential.deRhamDifferential_smul_ιMulti_D · KaehlerDifferential.deRhamDifferential_unique · KaehlerDifferential.isBaseChange_exteriorPower_and_deRhamDifferential_comm

Section10.133 Finite order differential operators#

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

Tag 09CI, a definition

Tag 09CI in the Stacks Project.

LinearMap.IsDifferentialOperatorOfOrderLE, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/Defs.lean, line 110. The attribute's comment: “The source's k bounds the order: Diff⁰ ⊆ Diff¹ ⊆ …, whence LE in the name. The commutator m ↦ D (g • m) - g • D m is the difference of the two composites of D with Algebra.lsmul R R _ g, multiplication by g. The S-module Diffᵏ_{S/R}(M, N) of the paragraph following the definition is a separate statement. See the module docstring.”. References: EGA IV (16.8.1), “affine (module) case”; SGA 3 VIIA (1.4), “affine case”; SGA 6 II (AppII.1.2.2), “Diff^n, affine case”; SGA 3 VIIA (1.1.1), “partial”.

Let R → S be a ring map, let M and N be S-modules, and let k : ℕ. D.IsDifferentialOperatorOfOrderLE S k says that the R-linear map D : M → N is a differential operator of order at most k relative to R → S. By induction on k: order at most 0 means S-linear, and order at most k + 1 means that for every g : S the commutator m ↦ D (g • m) - g • D m is a differential operator of order at most k.

public def IsDifferentialOperatorOfOrderLE (S : Type*) [Semiring S] [Algebra R S] [Module S M]
    [IsScalarTower R S M] [Module S N] [IsScalarTower R S N] : ℕ → (M →ₗ[R] N) → Prop

Tag 09CJ, a lemma

Tag 09CJ in the Stacks Project.

isDiffOpOfOrder_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/Defs.lean, line 458. References: EGA IV (16.8.9), “affine case”; SGA 3 VIIA (1.2), “affine, deviations of id”; SGA 3 VIIA (1.4), “partial”.

The composition of a differential operator of order k with one of order k' is a differential operator of order k + k'.

theorem isDiffOpOfOrder_comp
    {L : Type*} [AddCommGroup L] [Module S L] [Module R L] [IsScalarTower R S L]
    (k k' : ℕ) (D : L →ₗ[R] M) (D' : M →ₗ[R] N)
    (hD : IsDiffOpOfOrder S k D) (hD' : IsDiffOpOfOrder S k' D') :
    IsDiffOpOfOrder S (k + k') (D'.comp D)

Tag 09CK, a lemma

Tag 09CK in the Stacks Project.

LinearMap.exists_universal_isDifferentialOperatorOfOrderLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/PrincipalParts.lean, line 335. The attribute's comment: “Stated in the universal-object form of the paragraph following the lemma: the isomorphism Diffᵏ_{S/R}(M, N) = Hom_S(Pᵏ_{S/R}(M), N) is the map α ↦ α ∘ D_univ, so the universal operator is pinned and functoriality in N is automatic. See the module docstring.”. References: EGA IV (16.8.3), “affine case”; SGA 6 II (AppII.1.2.3), “affine (module) case”; SGA 6 II (AppII.1.2.2), “affine case”.

Stacks 09CK. Let R → S be a ring map, let M be an S-module and let k : ℕ. There exist an S-module P and a differential operator D_univ : M → P of order at most k relative to R → S such that, for every S-module N, precomposition with D_univ is a bijection from the S-linear maps P → N onto the differential operators M → N of order at most k. Thus P = Pᵏ_{S/R}(M) represents Diffᵏ_{S/R}(M, -), functorially in N.

public theorem exists_universal_isDifferentialOperatorOfOrderLE (k : ℕ) :
    ∃ (P : Type (max v w)) (_ : AddCommGroup P) (_ : Module R P) (_ : Module S P)
      (_ : IsScalarTower R S P) (Duniv : M →ₗ[R] P),
      Duniv.IsDifferentialOperatorOfOrderLE S k ∧
        ∀ (N : Type x) [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N],
          Function.Injective (fun α : P →ₗ[S] N => α.restrictScalars R ∘ₗ Duniv) ∧
            Set.range (fun α : P →ₗ[S] N => α.restrictScalars R ∘ₗ Duniv) =
              {D : M →ₗ[R] N | D.IsDifferentialOperatorOfOrderLE S k}

Tag 09CL, a definition

Tag 09CL in the Stacks Project.

LinearMap.IsUniversalDifferentialOperatorOfOrderLE, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/Defs.lean, line 387. The attribute's comment: “The source names the module Pᵏ_{S/R}(M) it has just constructed; defined here is the property of a pair (P, D) of being one, which determines it up to unique isomorphism and so applies to every construction. Existence of such a pair is Lemma 09CK. See the module docstring.”. References: SGA 6 II (AppII.1.2.2), “affine case”.

Let R → S be a ring map, let M be an S-module and let k : ℕ. For an R-linear map D : M → P into an S-module P, the property D.IsUniversalDifferentialOperatorOfOrderLE S k says that D is a differential operator of order at most k relative to R → S and that every differential operator E : M → N of order at most k into an S-module factors as E = α ∘ D for a unique S-linear map α : P → N. Equivalently α ↦ α ∘ D is the canonical isomorphism Hom_S(P, N) = Diffᵏ_{S/R}(M, N) of Lemma 09CK: that is, P is a module of principal parts of order k of M, written Pᵏ_{S/R}(M), and D is its universal differential operator. Such a pair is unique up to unique isomorphism.

public def IsUniversalDifferentialOperatorOfOrderLE (S : Type v) [Semiring S] [Algebra R S]
    [Module S M] [IsScalarTower R S M] [Module S P] [IsScalarTower R S P] (k : ℕ)
    (D : M →ₗ[R] P) : Prop

Tag 09CM, an example

Tag 09CM in the Stacks Project.

diff1EquivDerProd, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/OrderOne.lean, line 177. References: SGA 3 VIIA (1.3.1), “Dev≤1 ≃ O_S ⊕ Der_S”.

The S-module isomorphism Diff¹(S, N) ≃ₗ[S] Der_R(S, N) × N given by D ↦ (σ_D, D 1), where σ_D g = D g - g · D 1, with inverse (σ, x) ↦ σ + λ_x.

def diff1EquivDerProd : Diff1 R S N ≃ₗ[S] (Derivation R S N × N)

Tag 09CN, a lemma

Tag 09CN in the Stacks Project.

LinearMap.IsDifferentialOperatorOfOrderLE.exists_shortExact_principalParts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/PrincipalParts.lean, line 897. The attribute's comment: “Stated for an arbitrary universal order-≤ 1 differential operator D : M → P rather than for a chosen construction of P¹_{S/R}(M), whose existence is Lemma 09CK; both maps of the sequence are pinned by equations, from which functoriality in M is formal. See the module docstring.”. References: SGA 6 II (AppII.1.2.4), “n = 1, ring setting”.

Stacks 09CN. Let R → S be a ring map and let M be an S-module. Let D : M → P be a universal differential operator of order at most 1 on M, i.e. D has order at most 1 and every order-≤ 1 operator out of M factors uniquely through D by an S-linear map, so that P is a module of principal parts P¹_{S/R}(M). Then there is a short exact sequence 0 → Ω[S⁄R] ⊗[S] M → P → M → 0, the sequence of principal parts, whose first map sends d b ⊗ₜ m to D (b • m) - b • D m and whose second map is the retraction of D.

public theorem exists_shortExact_principalParts {R : Type*} {S : Type u} {M : Type v} {P : Type w}
    [CommRing R] [CommRing S] [Algebra R S]
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [AddCommGroup P] [Module R P] [Module S P] [IsScalarTower R S P]
    (D : M →ₗ[R] P) (hD : D.IsDifferentialOperatorOfOrderLE S 1)
    (huniv : ∀ (N : Type (max u v w)) [AddCommGroup N] [Module R N] [Module S N]
      [IsScalarTower R S N] (E : M →ₗ[R] N), E.IsDifferentialOperatorOfOrderLE S 1 →
      ∃! α : P →ₗ[S] N, ∀ m : M, α (D m) = E m) :
    ∃ (ι : Ω[S⁄R] ⊗[S] M →ₗ[S] P) (π : P →ₗ[S] M),
      (∀ (b : S) (m : M), ι (KaehlerDifferential.D R S b ⊗ₜ[S] m) = D (b • m) - b • D m) ∧
      (∀ m : M, π (D m) = m) ∧
      Function.Injective ι ∧ Function.Exact ι π ∧ Function.Surjective π

Tag 0H8Z, a lemma

Tag 0H8Z in the Stacks Project.

LinearMap.IsUniversalDifferentialOperatorOfOrderLE.isBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/BaseChange.lean, line 880. The attribute's comment: “Modules of principal parts appear through the universal property of Definition 09CL rather than as chosen constructions, and both base changes in Mathlib's IsBaseChange form. The map of Remark 09CP is the hypothesis hψ, which pins it since a universal D generates P over B. See the module docstring.”.

Stacks 0H8Z. Let A → A' and A → B be ring maps, let B' = B ⊗_A A', let M be a B-module and let M' = M ⊗_A A', a B'-module, with φ : M → M' the canonical map. Let D : M → P be a universal differential operator of order at most k relative to A → B and let D' : M' → P' be one relative to A' → B', so that P = Pᵏ_{B/A}(M) and P' = Pᵏ_{B'/A'}(M') are modules of principal parts. Then the map ψ : P → P' of Remark 09CP, i.e. the unique B-linear map with ψ ∘ D = D' ∘ φ, exhibits P' as the base change of P along A → A': Pᵏ_{B/A}(M) ⊗_A A' = Pᵏ_{B'/A'}(M').

public theorem isBaseChange
    [CommRing A] [CommRing A'] [CommRing B] [CommRing B']
    [Algebra A A'] [Algebra A B] [Algebra A B'] [Algebra A' B'] [Algebra B B']
    [IsScalarTower A A' B'] [IsScalarTower A B B'] [Algebra.IsPushout A A' B B']
    [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M]
    [AddCommGroup M'] [Module A M'] [Module A' M'] [Module B M'] [Module B' M']
    [IsScalarTower A A' M'] [IsScalarTower A B M'] [IsScalarTower A' B' M']
    [IsScalarTower B B' M']
    [AddCommGroup P] [Module A P] [Module B P] [IsScalarTower A B P]
    [AddCommGroup P'] [Module A P'] [Module A' P'] [Module B P'] [Module B' P']
    [IsScalarTower A A' P'] [IsScalarTower A B P'] [IsScalarTower A' B' P']
    [IsScalarTower B B' P']
    {k : ℕ} {D : M →ₗ[A] P} {D' : M' →ₗ[A'] P'}
    (hD : D.IsUniversalDifferentialOperatorOfOrderLE B k)
    (φ : M →ₗ[B] M') (hφ : IsBaseChange A' (φ.restrictScalars A))
    (hD' : D'.IsUniversalDifferentialOperatorOfOrderLE B' k)
    (ψ : P →ₗ[B] P') (hψ : ∀ m : M, ψ (D m) = D' (φ m)) :
    IsBaseChange A' (ψ.restrictScalars A)

Tag 0H90, a lemma

Tag 0H90 in the Stacks Project.

LinearMap.isUniversalDifferentialOperatorOfOrderLE_mkQ_comp_mk_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/PrincipalParts.lean, line 1357. The attribute's comment: “Stated as: the quotient, with the map m ↦ class of 1 ⊗ₜ m, is a module of principal parts of order k (Definition 09CL), which supplies the source's canonical isomorphism by uniqueness of a representing pair and pins the map. The S ⊗[R] S-action on S ⊗[R] M is the hypothesis hsmul, which determines it; it cannot be an instance, as it restricts to two different Module S (S ⊗[R] M) structures. See the module docstring.”. References: EGA IV (16.8.2), “factorization of D”; EGA IV (16.8.1), “special case”; SGA 3 VIIA (1.4.1), “affine case”.

Stacks 0H90. Let R → S be a ring map, let M be an S-module, let k : ℕ and let J = Ker(S ⊗[R] S → S) be the kernel of the multiplication map. Then the S-module (S ⊗[R] M)/J^{k + 1}(S ⊗[R] M), with s acting as multiplication by s ⊗ₜ 1, together with the R-linear map m ↦ class of 1 ⊗ₜ m, is a module of principal parts of order k of M: that map is a differential operator of order at most k relative to R → S and every such operator out of M factors uniquely S-linearly through it. Equivalently, there is a canonical isomorphism Pᵏ_{S/R}(M) → (S ⊗[R] M)/J^{k + 1}(S ⊗[R] M) carrying the universal differential operator of order k to m ↦ class of 1 ⊗ₜ m.

public theorem isUniversalDifferentialOperatorOfOrderLE_mkQ_comp_mk_one
    [Module (S ⊗[R] S) (S ⊗[R] M)] [IsScalarTower S (S ⊗[R] S) (S ⊗[R] M)]
    (hsmul : ∀ (a b t : S) (m : M), (a ⊗ₜ[R] b) • (t ⊗ₜ[R] m) = (a * t) ⊗ₜ[R] (b • m)) (k : ℕ) :
    (((KaehlerDifferential.ideal R S ^ (k + 1) •
          (⊤ : Submodule (S ⊗[R] S) (S ⊗[R] M))).restrictScalars S).mkQ.restrictScalars R ∘ₗ
        TensorProduct.mk R S M 1).IsUniversalDifferentialOperatorOfOrderLE S k

Tag 0G34, a lemma

Tag 0G34 in the Stacks Project.

deRham_isDiffOpOfOrder_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/OrderOne.lean, line 310.

Let A → B be a ring map and i ≥ 0. The de Rham differential d : Ωⁱ_{B/A} → Ωⁱ⁺¹_{B/A}, an additive map that is A-linear (hAlin) and satisfies d (b₀ · db₁ ∧ ⋯ ∧ dbᵢ) = db₀ ∧ db₁ ∧ ⋯ ∧ dbᵢ (hChar), is a differential operator of order 1 relative to A → B: for every b ∈ B the map ω ↦ d (b · ω) - b · d ω is B-linear.

theorem deRham_isDiffOpOfOrder_one (i : ℕ)
    (d : (⋀[B]^i (Ω[B⁄A])) →+ (⋀[B]^(i + 1) (Ω[B⁄A])))
    (hAlin : IsALinear A B d)
    (hChar : ∀ b : Fin (i+1) → B, d (deRhamGen i b) = deRhamTop i b) :
    IsDiffOpLE A B 1 d

Tag 0G35, a lemma

Tag 0G35 in the Stacks Project.

isDiffOpLE_succ_of_comm_isDiffOpLE_on_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/Defs.lean, line 763.

Let A → B be a ring map, let (g i) generate B as an A-algebra, let M, N be B-modules and D : M →+ N an A-linear map. Fix k ≥ 1 (written k + 1 here). If for every i the commutator diffOpComm (g i) D is a differential operator of order ≤ k, then D is a differential operator of order ≤ k + 1.

theorem isDiffOpLE_succ_of_comm_isDiffOpLE_on_generators
    {ι : Type*} (g : ι → B)
    (hgen : Algebra.adjoin A (Set.range g) = ⊤)
    {M N : Type*} [AddCommGroup M] [AddCommGroup N] [Module B M] [Module B N]
    (D : M →+ N) (hD : IsALinear A B D) (k : ℕ)
    (hcomm : ∀ i : ι, IsDiffOpLE A B k (diffOpComm (g i) D)) :
    IsDiffOpLE A B (k + 1) D

Tag 0G36, a lemma

Tag 0G36 in the Stacks Project.

LinearMap.IsDifferentialOperatorOfOrderLE.existsUnique_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/Localization.lean, line 632. The attribute's comment: “Stated for abstract localizations IsLocalization T S', IsLocalizedModule T f, IsLocalizedModule T g rather than for Localization T and LocalizedModule T. The order of the extension is relative to R → S', as in the source's proof. extends is spelled as the equation E ∘ₗ f.restrictScalars R = g.restrictScalars R ∘ₗ D, so the source's canonical maps are pinned; the case k = 0 is IsLocalizedModule.lift. See the module docstring.”.

Stacks 0G36. Let R → S be a ring map, let M and N be S-modules and let T ⊆ S be a multiplicative subset. A differential operator D : M → N of order at most k relative to R → S extends uniquely to a differential operator of order at most k relative to R → T⁻¹S on the localizations: there is a unique R-linear map E : T⁻¹M → T⁻¹N which is a differential operator of order at most k and satisfies E ∘ f = g ∘ D for the localization maps f : M → T⁻¹M and g : N → T⁻¹N.

public theorem existsUnique_extension {k : ℕ} {D : M →ₗ[R] N}
    (hD : D.IsDifferentialOperatorOfOrderLE S k) (T : Submonoid S) [IsLocalization T S']
    (f : M →ₗ[S] M') (g : N →ₗ[S] N') [IsLocalizedModule T f] [IsLocalizedModule T g] :
    ∃! E : M' →ₗ[R] N', E.IsDifferentialOperatorOfOrderLE S' k ∧
      E ∘ₗ f.restrictScalars R = g.restrictScalars R ∘ₗ D

Tag 0G37, a lemma

Tag 0G37 in the Stacks Project.

LinearMap.IsDifferentialOperatorOfOrderLE.rTensorB, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/BaseChange.lean, line 363. The attribute's comment: “the operator D ⊗ id_N itself; rTensorB_tmul is its values on pure tensors, order_rTensorB the order bound and eq_rTensorB its uniqueness. The B-algebra structure on A ⊗[R] B and the actions on M ⊗[R] N, M' ⊗[R] N are hypotheses because Mathlib has no such instances; halg, hsmul and hsmul' pin them to the canonical ones. See the module docstring.”.

The operator D ⊗ id_N. The tensor product of an R-linear map D : M →ₗ[R] M' with the identity of a B-module N, as a B-linear map M ⊗[R] N → M' ⊗[R] N. Its underlying R-linear map is LinearMap.rTensor N D; the content of the definition is the B-linearity, B acting through algebraMap B (A ⊗[R] B) b = 1 ⊗ₜ b on the factor N that D ⊗ id_N leaves alone. Here hsmul and hsmul' say that A ⊗[R] B acts on the tensor products by (a ⊗ b) • (m ⊗ n) = (a • m) ⊗ (b • n), and halg that B → A ⊗[R] B is b ↦ 1 ⊗ b.

public def rTensorB
    (halg : ∀ b : B, algebraMap B (A ⊗[R] B) b = 1 ⊗ₜ[R] b)
    (hsmul : ∀ (a : A) (b : B) (m : M) (n : N),
      (a ⊗ₜ[R] b) • (m ⊗ₜ[R] n) = (a • m) ⊗ₜ[R] (b • n))
    (hsmul' : ∀ (a : A) (b : B) (m : M') (n : N),
      (a ⊗ₜ[R] b) • (m ⊗ₜ[R] n) = (a • m) ⊗ₜ[R] (b • n))
    (D : M →ₗ[R] M') : M ⊗[R] N →ₗ[B] M' ⊗[R] N

LinearMap.IsDifferentialOperatorOfOrderLE.rTensorB_tmul, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/BaseChange.lean, line 375. The attribute's comment: “the values of rTensorB on pure tensors”.

D ⊗ id_N sends m ⊗ n to D m ⊗ n.

public lemma rTensorB_tmul
    (halg : ∀ b : B, algebraMap B (A ⊗[R] B) b = 1 ⊗ₜ[R] b)
    (hsmul : ∀ (a : A) (b : B) (m : M) (n : N),
      (a ⊗ₜ[R] b) • (m ⊗ₜ[R] n) = (a • m) ⊗ₜ[R] (b • n))
    (hsmul' : ∀ (a : A) (b : B) (m : M') (n : N),
      (a ⊗ₜ[R] b) • (m ⊗ₜ[R] n) = (a • m) ⊗ₜ[R] (b • n))
    (D : M →ₗ[R] M') (m : M) (n : N) :
    rTensorB halg hsmul hsmul' D (m ⊗ₜ[R] n) = D m ⊗ₜ[R] n

LinearMap.IsDifferentialOperatorOfOrderLE.order_rTensorB, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/BaseChange.lean, line 389. The attribute's comment: “the order bound on rTensorB”.

If D is a differential operator of order at most k relative to R → A, then D ⊗ id_N is one of order at most k relative to B → A ⊗[R] B.

public lemma order_rTensorB {k : ℕ} {D : M →ₗ[R] M'}
    (hD : D.IsDifferentialOperatorOfOrderLE A k)
    (halg : ∀ b : B, algebraMap B (A ⊗[R] B) b = 1 ⊗ₜ[R] b)
    (hsmul : ∀ (a : A) (b : B) (m : M) (n : N),
      (a ⊗ₜ[R] b) • (m ⊗ₜ[R] n) = (a • m) ⊗ₜ[R] (b • n))
    (hsmul' : ∀ (a : A) (b : B) (m : M') (n : N),
      (a ⊗ₜ[R] b) • (m ⊗ₜ[R] n) = (a • m) ⊗ₜ[R] (b • n)) :
    (rTensorB halg hsmul hsmul' D).IsDifferentialOperatorOfOrderLE (A ⊗[R] B) k

LinearMap.IsDifferentialOperatorOfOrderLE.eq_rTensorB, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DifferentialOperator/BaseChange.lean, line 402. The attribute's comment: “uniqueness of rTensorB”.

D ⊗ id_N is the only B-linear map M ⊗[R] N → M' ⊗[R] N carrying m ⊗ n to D m ⊗ n.

public lemma eq_rTensorB {D : M →ₗ[R] M'}
    (halg : ∀ b : B, algebraMap B (A ⊗[R] B) b = 1 ⊗ₜ[R] b)
    (hsmul : ∀ (a : A) (b : B) (m : M) (n : N),
      (a ⊗ₜ[R] b) • (m ⊗ₜ[R] n) = (a • m) ⊗ₜ[R] (b • n))
    (hsmul' : ∀ (a : A) (b : B) (m : M') (n : N),
      (a ⊗ₜ[R] b) • (m ⊗ₜ[R] n) = (a • m) ⊗ₜ[R] (b • n))
    (D' : M ⊗[R] N →ₗ[B] M' ⊗[R] N)
    (hD' : ∀ (m : M) (n : N), D' (m ⊗ₜ[R] n) = D m ⊗ₜ[R] n) :
    D' = rTensorB halg hsmul hsmul' D

Sources

• Section 10.133, Tag 09CH
• AxiomMath/Stacks at 5ed82d14

LeanLinearMap.IsDifferentialOperatorOfOrderLE · isDiffOpOfOrder_comp · LinearMap.exists_universal_isDifferentialOperatorOfOrderLE · LinearMap.IsUniversalDifferentialOperatorOfOrderLE · diff1EquivDerProd · LinearMap.IsDifferentialOperatorOfOrderLE.exists_shortExact_principalParts · LinearMap.IsUniversalDifferentialOperatorOfOrderLE.isBaseChange · LinearMap.isUniversalDifferentialOperatorOfOrderLE_mkQ_comp_mk_one

Section10.134 The naive cotangent complex#

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

Tag 07BL, an equation

Tag 07BL in the Stacks Project.

Declarations registered for the tag:

• Algebra.Generators.self registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch10.lean, line 261 (StacksFrontier): “the canonical surjection R[S] → S, [s] ↦ s: the generators of S indexed by S itself, whose map MvPolynomial S R → S is aeval id”.

Tag 07BM, an equation

Tag 07BM in the Stacks Project.

Declarations registered for the tag:

• Algebra.Extension.cotangentComplex registered with add_to_stacks in StacksFrontier/RingTheory/NaiveCotangent/Defs.lean, line 569 (StacksFrontier): “the naive cotangent differential”. References: EGA IV (17.15.9); SGA 1 II (5.9), “more general”; SGA 6 0 (4.4), “special case”; SGA 6 VIII (2.1), “affine case”.

Tag 07BN, a definition

Tag 07BN in the Stacks Project.

Algebra.naiveCotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Defs.lean, line 161. The attribute's comment: “The complex itself; Mathlib has its differential (Algebra.Extension.cotangentComplex at Algebra.Generators.self R S) and its degree-1 homology (Algebra.H1Cotangent), but not the two-term complex. See the module docstring.”. References: SGA 6 VIII (2.1), “affine case, R[S]”.

The naive cotangent complex (Stacks 07BN): for a ring map R → S, the two-term chain complex of S-modules

NL_{S/R} = (I/I² ⟶ Ω_{R[S]/R} ⊗_{R[S]} S)

where I is the kernel of the canonical surjection R[S] → S, [s] ↦ s, with I/I² in homological degree 1, Ω_{R[S]/R} ⊗_{R[S]} S in homological degree 0, and the canonical map of Stacks 07BM, sending the class of f ∈ I to df ⊗ 1, as its differential. It is zero in all other degrees. Its degree-0 homology is Ω_{S/R} and its degree-1 homology is H₁(L_{S/R}) = Algebra.H1Cotangent R S.

public noncomputable def Algebra.naiveCotangentComplex (R : Type u) (S : Type v) [CommRing R]
    [CommRing S] [Algebra R S] : ChainComplex (ModuleCat.{max u v} S) ℕ

Tag 06RQ, an equation

Tag 06RQ in the Stacks Project.

Algebra.Generators.defaultHom_comp_defaultHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Functoriality.lean, line 221. The attribute's comment: “The display is the datum for functoriality of NL; what is stated is the compatibility with composition of the canonical maps it produces, at the level of morphisms of presentations. See the module docstring.”.

Functoriality of the naive cotangent complex in a square of rings (Stacks 06RQ): given two commutative squares of rings side by side,

S --φ--> S' --φ'--> S''
↑        ↑          ↑
R -----> R' ------> R''

a presentation P of S over R, a presentation P'' of S'' over R'', and the canonical presentation R'[S'] → S' of the intermediate algebra, the composite of the canonical comparison morphisms of presentations P → R'[S'] and R'[S'] → P'' is the canonical comparison morphism P → P'' of the outer square. Hence the canonical maps of naive cotangent complexes NL_{S/R} → NL_{S'/R'} → NL_{S''/R''} compose to the canonical map NL_{S/R} → NL_{S''/R''}.

public theorem defaultHom_comp_defaultHom (P : Generators R S ι) (P'' : Generators R'' S'' ι'') :
    (defaultHom (self R' S') P'').comp (defaultHom P (self R' S')) = defaultHom P P''

Tag 00S1, a lemma

Tag 00S1 in the Stacks Project.

Deformation.Artin.derivedNaiveCotangentComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveCotangentPresentation.lean, line 348. The attribute's comment: “presentation independence in the derived category: the comparison with the canonical presentation is an isomorphism in D(A)”. References: SGA 6 0 (4.3), “partial”; SGA 6 0 (4.4), “special case”; SGA 6 VIII (2.2), “special case”.

For any presentation of A over Λ, the comparison with the canonical presentation is an isomorphism NL(α) ≅ NL_{A/Λ} in the derived category of A-modules.

public def derivedNaiveCotangentComplexIso (P : Algebra.Generators Λ A ι)
    (φ : P.Hom (canonicalGenerators Λ A)) :
    DerivedCategory.Q.obj (twoTermComplex (nlRestrict A P)) ≅
      derivedNaiveCotangentComplex Λ A

NaiveCotangent.exists_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Defs.lean, line 417. The attribute's comment: “(1)”.

Existence. There exists a morphism of presentations varphi from α to α' covering the square.

theorem exists_hom (P : Generators R S ι) (P' : Generators R' S' ι') : Nonempty (P.Hom P')

NaiveCotangent.nlMap_homotopic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Defs.lean, line 427. The attribute's comment: “(2)”.

Homotopy uniqueness. Any two morphisms of presentations varphi, varphi' from α to α' induce homotopic chain maps NL(varphi), NL(varphi') (over the source base S). The homotopy is the S-linear map h : Ω_{P/R} ⊗_P S → I'/(I')² (= P.CotangentSpace →ₗ[S] P'.Cotangent) given by Algebra.Extension.Hom.sub of the two extension homs; the two homotopy relations are Cotangent.map_sub_map and CotangentSpace.map_sub_map.

theorem nlMap_homotopic (P : Generators R S ι) (P' : Generators R' S' ι') (φ φ' : P.Hom P') :
    Homotopic (nlMap P P' φ) (nlMap P P' φ')

NaiveCotangent.nlMapBase_comp_nlMapBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Defs.lean, line 436. The attribute's comment: “(3)”.

Compatibility with composition. Given a commutative diagram of two squares and compatible morphisms of presentations varphi : P → P', varphi' : P' → P'', the composite varphi' ∘ varphi is a morphism of presentations from α to α'' and, viewing everything over the base ring S, NL(varphi') ∘ NL(varphi) = NL(varphi' ∘ varphi).

theorem nlMapBase_comp_nlMapBase {R'' S'' ι'' : Type*} [CommRing R''] [CommRing S'']
    [Algebra R'' S''] [Algebra R' R''] [Algebra R' S''] [Algebra S' S''] [Algebra S S'']
    [IsScalarTower R' R'' S''] [IsScalarTower R' S' S''] [IsScalarTower S S' S''] [Algebra R R'']
    [Algebra R S''] [IsScalarTower R R' R''] [IsScalarTower R R'' S''] [IsScalarTower R S S'']
    (P : Generators R S ι) (P' : Generators R' S' ι') (P'' : Generators R'' S'' ι'') (φ : P.Hom P')
    (φ' : P'.Hom P'') :
    (nlMapBase S P' P'' φ').comp (nlMapBase S P P' φ) = nlMapBase S P P'' (φ'.comp φ)

NaiveCotangent.nlMap_isHomotopyEquiv_and_isQuasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Defs.lean, line 516. The attribute's comment: “(4)”.

Isomorphism case. If R → R' and φ : S → S' are isomorphisms, then for any morphism of presentations varphi from α to α' the induced chain map NL(varphi) (over S) is both a homotopy equivalence and a quasi-isomorphism.

theorem nlMap_isHomotopyEquiv_and_isQuasiIso (hR : Function.Bijective (algebraMap R R'))
    (hS : Function.Bijective (algebraMap S S')) (P : Generators R S ι) (P' : Generators R' S' ι')
    (φ : P.Hom P') : IsHomotopyEquiv (nlMap P P' φ) ∧ IsQuasiIso (nlMap P P' φ)

NaiveCotangent.nlMap_canonical_isQuasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Defs.lean, line 559.

Comparison with the canonical complex. Any morphism of presentations varphi from a presentation α of S/R to the canonical presentation α_can : R[S] → S induces a quasi-isomorphism NL(α) → NL_{S/R}.

theorem nlMap_canonical_isQuasiIso (P : Generators R S ι) (φ : P.Hom (canonicalGenerators R S)) :
    IsQuasiIso (nlMap P (canonicalGenerators R S) φ)

Tag 08Q1, a lemma

Tag 08Q1 in the Stacks Project.

natExt_cotangent_subsingleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Localization.lean, line 1228. The attribute's comment: “Ingredient only, and only for the variables presentation B = MvPolynomial ι A: the degree-1 term vanishes. The homotopy equivalence NL_{B/A} ≃ (0 → Ω_{B/A}) is not stated.”.

The degree one module of NL_{B/A} vanishes for the presentation natExt A ι of B = MvPolynomial ι A.

theorem natExt_cotangent_subsingleton (A : Type*) [CommRing A] (ι : Type*) :
    Subsingleton ((natExt A ι).Cotangent)

natExt_toKaehler_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Localization.lean, line 1246. The attribute's comment: “Ingredient only, and only for the variables presentation B = MvPolynomial ι A: the degree-0 term is Ω via the augmentation. The homotopy equivalence NL_{B/A} ≃ (0 → Ω_{B/A}) is not stated.”.

The augmentation P.toKaehler is a B-linear isomorphism of P.CotangentSpace onto Ω[B⁄A] for the presentation P = natExt A ι.

theorem natExt_toKaehler_bijective (A : Type*) [CommRing A] (ι : Type*) :
    Function.Bijective (natExt A ι).toKaehler

Tag 00S2, a lemma

Tag 00S2 in the Stacks Project.

Algebra.Generators.Cotangent.map_ker_baseChange_cotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/JacobiZariski.lean, line 144. The attribute's comment: “Exactness at H₁(L_{C/A}), the one node of the six term sequence that is not in Mathlib; the term on the left is the source's H₁(NL_{B/A} ⊗_B C), so no Tor vanishing hypothesis is needed. See the module docstring.”.

The Jacobi-Zariski sequence is exact at H₁(L_{C/A}): let A → B → C be ring maps, let α : A[x_s, s ∈ S] → B be a presentation with kernel I, let β : B[y_t, t ∈ T] → C be a presentation with kernel J, and let γ : A[x_s, y_t] → C be the induced presentation of C with kernel K. Then the image in K/K² of H₁(NL_{B/A} ⊗_B C) = Ker(I/I² ⊗_B C → Ω_{A[x_s]/A} ⊗ C), under the map I/I² ⊗_B C → K/K² induced by A[x_s] → A[x_s, y_t], is the intersection of H₁(L_{C/A}) = Ker(K/K² → Ω_{A[x_s, y_t]/A} ⊗ C) with the kernel of the map K/K² → J/J² induced by A[x_s, y_t] → B[y_t], i.e. with the kernel of H₁(L_{C/A}) → H₁(L_{C/B}).

public theorem map_ker_baseChange_cotangentComplex (Q : Generators S T ι)
    (P : Generators R S σ) :
    Submodule.map ((Extension.Cotangent.map (Q.toComp P).toExtensionHom).liftBaseChange T)
        (LinearMap.ker (P.toExtension.cotangentComplex.baseChange T)) =
      LinearMap.ker (Q.comp P).toExtension.cotangentComplex ⊓
        LinearMap.ker (Extension.Cotangent.map (Q.ofComp P).toExtensionHom)

NaiveCotangent.jacobiZariski_sixTerm_exact_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/JacobiZariskiPresentations.lean, line 272. The attribute's comment: “the six-term exact sequence with its middle column an ARBITRARY presentation of C over A, rather than the presentation Q.comp P induced by the other two, which is what NaiveCotangent.jacobiZariski_sixTerm_exact gives; the two are compared by Stacks 00S1 (4), which this statement uses but does not state”.

The Jacobi-Zariski six-term exact sequence over three independently chosen presentations (Stacks 00S2 together with Stacks 00S1). Let A → B → C be ring maps, let α : A[x_s] → B be a presentation of B over A, let β : B[y_t] → C be a presentation of C over B and let N be any presentation of C over A. Choose morphisms of extensions varphi : α ⟶ N over the square with vertical morphisms id_A and B → C, and psi : N ⟶ β over the square with vertical morphisms A → B and id_C. Then

H₁(NL(α) ⊗_B C) → H₁(NL(N)) → H₁(NL(β)) --δ--> H₀(NL(α) ⊗_B C) → H₀(NL(N)) → H₀(NL(β)) → 0

is exact at each of its five interior nodes, δ being NaiveCotangent.jacobiZariskiConnecting.

The two comparison maps do not depend on the choice of varphi and psi (NaiveCotangent.homotopic_nlExtensionBaseChangeMap and NaiveCotangent.homotopic_nlExtensionOverMap, which are Stacks 00S1 (2)), so the sequence is canonical.

theorem jacobiZariski_sixTerm_exact_extension (Q : Generators S T ι)
    (P : Generators R S σ) (N : Generators R T τ)
    (φ : P.toExtension.Hom N.toExtension) (ψ : N.toExtension.Hom Q.toExtension) :
    Exact (nlExtensionBaseChangeMap (T := T) φ).onH₁ (nlExtensionOverMap ψ).onH₁ ∧
      Exact (nlExtensionOverMap ψ).onH₁ (jacobiZariskiConnecting Q P) ∧
      Exact (jacobiZariskiConnecting Q P) (nlExtensionBaseChangeMap (T := T) φ).onH₀ ∧
      Exact (nlExtensionBaseChangeMap (T := T) φ).onH₀ (nlExtensionOverMap ψ).onH₀ ∧
      Surjective (nlExtensionOverMap ψ).onH₀

NaiveCotangent.jacobiZariski_sixTerm_exact_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/JacobiZariskiPresentations.lean, line 326. The attribute's comment: “the six-term exact sequence between the naive cotangent complexes of the three CANONICAL presentations of Stacks 07BL, rather than of the three presentations of the source's own proof”.

The Jacobi-Zariski six-term exact sequence over the canonical presentations of Stacks 07BL. For ring maps A → B → C,

H₁(NL_{B/A} ⊗_B C) → H₁(NL_{C/A}) → H₁(NL_{C/B}) --δ--> C ⊗_B Ω_{B/A} → Ω_{C/A} → Ω_{C/B} → 0

is exact at each of its five interior nodes, the three complexes being the naive cotangent complexes of the canonical presentations A[B] → B, A[C] → C and B[C] → C, and the two comparison maps those attached to any morphisms of extensions between them, on which they do not depend.

This is NaiveCotangent.jacobiZariski_sixTerm_exact_extension at the canonical presentation of C over A; it is the form in which the stalkwise statements of Stacks 0E1Y need it, the stalk of the naive cotangent complex being the naive cotangent complex of the canonical presentation of the stalk (Stacks 0D09), and the stalk of the canonical map c₁ of Stacks 0E1Y being NaiveCotangent.nlExtensionBaseChangeMap of a morphism of those canonical presentations (Stacks.NaiveCotangentStalkBaseChange.stalkLegZeroLinear_baseChangeNaiveCotangentMap).

theorem jacobiZariski_sixTerm_exact_canonical
    (φ : (canonicalGenerators R S).toExtension.Hom (canonicalGenerators R T).toExtension)
    (ψ : (canonicalGenerators R T).toExtension.Hom (canonicalGenerators S T).toExtension) :
    Exact (nlExtensionBaseChangeMap (T := T) φ).onH₁ (nlExtensionOverMap ψ).onH₁ ∧
      Exact (nlExtensionOverMap ψ).onH₁
        (jacobiZariskiConnecting (canonicalGenerators S T) (canonicalGenerators R S)) ∧
      Exact (jacobiZariskiConnecting (canonicalGenerators S T) (canonicalGenerators R S))
        (nlExtensionBaseChangeMap (T := T) φ).onH₀ ∧
      Exact (nlExtensionBaseChangeMap (T := T) φ).onH₀ (nlExtensionOverMap ψ).onH₀ ∧
      Surjective (nlExtensionOverMap ψ).onH₀

NaiveCotangent.jacobiZariskiConnecting, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/JacobiZariskiSixTerm.lean, line 146. The attribute's comment: “The connecting map of the six-term sequence, for the naive cotangent complexes of three presentations as in the source's own proof.”.

The Jacobi-Zariski connecting map (Stacks 00S2): for ring maps A → B → C and presentations α : A[x_s] → B, β : B[y_t] → C with induced presentation γ : A[x_s, y_t] → C, the snake-lemma map δ : H₁(NL(β)) ⟶ H₀(NL(α) ⊗_B C), that is H₁(L_{C/B}) → C ⊗_B Ω_{B/A}.

public noncomputable def jacobiZariskiConnecting (Q : Generators S T ι) (P : Generators R S σ) :
    H₁ (NL Q) →ₗ[T] H₀ (nlBaseChange T P)

NaiveCotangent.jacobiZariski_sixTerm_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/JacobiZariskiSixTerm.lean, line 167. The attribute's comment: “The six-term exact sequence for the naive cotangent complex, over the three presentations of the source's own proof; Stacks.KaehlerDifferential.JacobiZariski records only exactness at H₁(L_{C/A}), and for the full cotangent complex.”.

The Jacobi-Zariski six-term exact sequence (Stacks 00S2) for the naive cotangent complex. Let A → B → C be ring maps, let α : A[x_s] → B and β : B[y_t] → C be presentations and let γ : A[x_s, y_t] → C be the induced presentation of C over A. Then

H₁(NL(α) ⊗_B C) → H₁(NL(γ)) → H₁(NL(β)) --δ--> H₀(NL(α) ⊗_B C) → H₀(NL(γ)) → H₀(NL(β)) → 0

is exact at each of its five interior nodes, δ being NaiveCotangent.jacobiZariskiConnecting. In the notation of the source this is 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 jacobiZariski_sixTerm_exact (Q : Generators S T ι) (P : Generators R S σ) :
    Exact (nlToComp Q P).onH₁ (nlOfComp Q P).onH₁ ∧
      Exact (nlOfComp Q P).onH₁ (jacobiZariskiConnecting Q P) ∧
      Exact (jacobiZariskiConnecting Q P) (nlToComp Q P).onH₀ ∧
      Exact (nlToComp Q P).onH₀ (nlOfComp Q P).onH₀ ∧
      Surjective (nlOfComp Q P).onH₀

NaiveCotangent.exists_jacobiZariski_sixTerm_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/JacobiZariskiSixTerm.lean, line 190. The attribute's comment: “The existential form of the six-term sequence for the naive cotangent complex.”.

Stacks 00S2 in the form in which the source states it: there exists a six-term exact sequence

H₁(NL(α) ⊗_B C) → H₁(NL(γ)) → H₁(NL(β)) → H₀(NL(α) ⊗_B C) → H₀(NL(γ)) → H₀(NL(β)) → 0

of C-modules, for ring maps A → B → C, presentations α : A[x_s] → B, β : B[y_t] → C and the induced presentation γ : A[x_s, y_t] → C.

public theorem exists_jacobiZariski_sixTerm_exact (Q : Generators S T ι)
    (P : Generators R S σ) :
    ∃ δ : H₁ (NL Q) →ₗ[T] H₀ (nlBaseChange T P),
      Exact (nlToComp Q P).onH₁ (nlOfComp Q P).onH₁ ∧
        Exact (nlOfComp Q P).onH₁ δ ∧
        Exact δ (nlToComp Q P).onH₀ ∧
        Exact (nlToComp Q P).onH₀ (nlOfComp Q P).onH₀ ∧
        Surjective (nlOfComp Q P).onH₀

Tag 07VC, a remark

Tag 07VC in the Stacks Project.

NaiveCotangent.towerChainMap_homotopic_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/CompositionNullHomotopy.lean, line 216. The attribute's comment: “the composition is homotopy equivalent to zero”.

Stacks 07VC. The composition NL_{B/A} ⟶ NL_{C/A} ⟶ NL_{C/B} of the two functoriality maps of the naive cotangent complex is homotopic to the zero chain map.

public theorem towerChainMap_homotopic_zero :
    Homotopic (towerChainMap A B C)
      (ChainMap.zero (nlRestrict B (Generators.self A B))
        (nlRestrict B (Generators.self B C)))

NaiveCotangent.towerNullHomotopy_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/CompositionNullHomotopy.lean, line 227. The attribute's comment: “the displayed map is an explicit homotopy”.

The two homotopy relations satisfied by towerNullHomotopy: it is a null homotopy of the composition NL_{B/A} ⟶ NL_{C/A} ⟶ NL_{C/B}.

public theorem towerNullHomotopy_spec :
    (towerChainMap A B C).f₁ = towerNullHomotopy A B C ∘ₗ
        (nlRestrict B (Generators.self A B)).d ∧
      (towerChainMap A B C).f₀ =
        (nlRestrict B (Generators.self B C)).d ∘ₗ towerNullHomotopy A B C

NaiveCotangent.towerNullHomotopy_cotangentSpaceBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/CompositionNullHomotopy.lean, line 259. The attribute's comment: “the value of the homotopy on the basis element d[b]”.

Stacks 07VC. The homotopy sends the basis element d[b] of Ω_{A[B]/A} ⊗_{A[B]} B to the class of [φ(b)] - b in J/J².

public theorem towerNullHomotopy_cotangentSpaceBasis (b : B) :
    towerNullHomotopy A B C ((Generators.self A B).cotangentSpaceBasis b) =
      Extension.Cotangent.mk
        ⟨X (algebraMap B C b) - MvPolynomial.C b, X_sub_C_mem_ker B C b⟩

Tag 07BP, a lemma

Tag 07BP in the Stacks Project.

h1Cotangent_equiv_cotangent_of_surjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/H1.lean, line 116.

For a surjective ring map A → B with kernel I := RingHom.ker (algebraMap A B), the A-linear isomorphism Algebra.H1Cotangent A B ≃ₗ[A] I.Cotangent.

noncomputable def h1Cotangent_equiv_cotangent_of_surjective
    (h : Function.Surjective (algebraMap A B)) :
    Algebra.H1Cotangent A B ≃ₗ[A] (RingHom.ker (algebraMap A B)).Cotangent

Tag 065V, a lemma

Tag 065V in the Stacks Project.

exact_mapCotangent_kerCotangentToTensor_and_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Conormal.lean, line 697. References: EGA 0 (20.5.12), “(i), special case”.

Stacks Tag 065V (Lemma 10.134.7). Let A → B → C be ring maps with A → C surjective, and set I = ker (A → C) and J = ker (B → C). Then the sequence I/I² → J/J² → Ω[B⁄A] ⊗_B B/J → 0 is exact: the image of Ideal.mapCotangent is the kernel of KaehlerDifferential.kerCotangentToTensor, and the latter is surjective.

theorem exact_mapCotangent_kerCotangentToTensor_and_surjective
    (A B C : Type*) [CommRing A] [CommRing B] [CommRing C]
    [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
    (hAC : Function.Surjective (algebraMap A C))
    (hle : RingHom.ker (algebraMap A C) ≤
      Ideal.comap (Algebra.ofId A B) (RingHom.ker (algebraMap B C))) :
    Function.Exact
      (Ideal.mapCotangent (RingHom.ker (algebraMap A C)) (RingHom.ker (algebraMap B C))
        (Algebra.ofId A B) hle)
      (KaehlerDifferential.kerCotangentToTensor A B C) ∧
    Function.Surjective (KaehlerDifferential.kerCotangentToTensor A B C)

Tag 00S4, a lemma

Tag 00S4 in the Stacks Project.

FlatBaseChangeNL.statement2_complex_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/BaseChange.lean, line 763. References: EGA IV (16.2.2), “(iii)”; EGA IV (16.2.4), “affine case”; SGA 3 I (6.8.5), “special case”; SGA 3 III (0.14), “partial”.

Statement 2, part (b): the canonical comparison is an isomorphism.

If R → R' is flat, the canonical comparison NL(α) ⊗_S S' → NL(α') is an isomorphism of two-term complexes of S' = R' ⊗_R S-modules, with degree-1 component cotComparison1 (bijective by flatness) and degree-0 component cotComparison0 (always bijective).

theorem statement2_complex_iso [Module.Flat R R'] (P : Algebra.Extension R S) :
    ∃ iso : TwoComplexEquiv (cotDiffBaseChangeS R' P)
        (P.baseChange (T := R')).cotangentComplex,
      (iso.e1 : _ →ₗ[R' ⊗[R] S] _) = cotComparison1 R' P ∧
        (iso.e0 : _ →ₗ[R' ⊗[R] S] _) = cotComparison0 R' P

FlatBaseChangeNL.statement3_homotopy_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/BaseChange.lean, line 1470.

Statement 3: under flatness of R → R', the canonical comparison chain map of naive cotangent complexes NL_{S/R} ⊗_S S' → NL_{S'/R'} (with NL_{S'/R'} the canonical presentation of S' = R' ⊗_R S over R') is a homotopy equivalence of two-term complexes of S'-modules; in particular a quasi-isomorphism.

The asserted homotopy equivalence has as its forward chain map the canonical comparison, i.e. the ChainMap whose degree-1/0 components are the canonical comparisons statement3_f1/statement3_f0 (the S'-linear lifts of Cotangent.map (canHom), CotangentSpace.map (canHom)).

theorem statement3_homotopy_equiv [Module.Flat R R'] :
    ∃ he : HtpyEquiv (nlCanDiffBaseChange R')
        ((Algebra.Generators.self R' (R' ⊗[R] S)).toExtension).cotangentComplex,
      he.toFun.f1 = statement3_f1 R' ∧ he.toFun.f0 = statement3_f0 R'

Tag 07BQ, a lemma

Tag 07BQ in the Stacks Project.

RingMapSystemUnbundled.isIso_colim_NL, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Colimit.lean, line 1697.

Stacks Tag 07BQ, Lemma 10.134.9 (packaged). The canonical comparison morphism colim_λ NL_{S_λ/R_λ} → NL_{S/R} is an isomorphism of two-term complexes: it is a bijection in each homological degree (degree 1 and degree 0) and the two degreewise comparison maps commute with the differentials (the colimit differential colimDifferential and the differential NL_{S/R}.cotangentComplex). This bundles the three theorems above.

theorem isIso_colim_NL [IsDirected Λ (· ≤ ·)] [Nonempty Λ] :
    Function.Bijective sys.comparisonCotangent ∧
    Function.Bijective sys.comparisonCotangentSpace ∧
    (∀ x : sys.colimCotangent,
      sys.comparisonCotangentSpace (sys.colimDifferential x)
        = sys.NLinf.cotangentComplex (sys.comparisonCotangent x))

Tag 07BR, a lemma

Tag 07BR in the Stacks Project.

kaehlerDifferential_subsingleton_of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Localization.lean, line 853.

H₀(NL_{S⁻¹A/A}) = Ω_{S⁻¹A/A} = 0: the module of Kähler differentials of a localization S⁻¹A over A vanishes.

theorem kaehlerDifferential_subsingleton_of_isLocalization
    [IsLocalization S B] :
    Subsingleton (Ω[B⁄A])

h1Cotangent_subsingleton_of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Localization.lean, line 862.

H₁(NL_{S⁻¹A/A}) = 0: the first naive cotangent homology of a localization S⁻¹A over A vanishes.

theorem h1Cotangent_subsingleton_of_isLocalization
    [IsLocalization S B] :
    Subsingleton (Algebra.H1Cotangent A B)

Tag 07BS, a lemma

Tag 07BS in the Stacks Project.

naiveCotangentComplex_localization_base_homotopyEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Localization.lean, line 1161.

With Aₘ a localization of A at the multiplicative subset M and a ring map Aₘ → B, the canonical chain map φ = (φ₁, φ₀) : NL_{B/A} → NL_{B/Aₘ}, given by Algebra.Extension.Cotangent.map h and Algebra.Extension.CotangentSpace.map h for the morphism of extensions h induced by the tower A → Aₘ → B, is a homotopy equivalence of the two term naive cotangent complexes of B-modules.

theorem naiveCotangentComplex_localization_base_homotopyEquiv
    (A : Type*) (Aₘ : Type*) (B : Type*)
    [CommRing A] [CommRing Aₘ] [CommRing B]
    [Algebra A Aₘ] [Algebra A B] [Algebra Aₘ B]
    [IsScalarTower A Aₘ B]
    (M : Submonoid A) [IsLocalization M Aₘ] :
    let P := (Generators.self A B).toExtension
    let Q := (Generators.self Aₘ B).toExtension
    let h : P.Hom Q :=
      ((Generators.self A B).defaultHom (Generators.self Aₘ B)).toExtensionHom
    let φ₁ := Algebra.Extension.Cotangent.map h
    let φ₀ := Algebra.Extension.CotangentSpace.map h
    ∃ (ψ₁ : Q.Cotangent →ₗ[B] P.Cotangent)
      (ψ₀ : Q.CotangentSpace →ₗ[B] P.CotangentSpace)
      (s : P.CotangentSpace →ₗ[B] P.Cotangent)
      (t : Q.CotangentSpace →ₗ[B] Q.Cotangent),
      Q.cotangentComplex ∘ₗ φ₁ = φ₀ ∘ₗ P.cotangentComplex ∧
      P.cotangentComplex ∘ₗ ψ₁ = ψ₀ ∘ₗ Q.cotangentComplex ∧
      ψ₁ ∘ₗ φ₁ - LinearMap.id = s ∘ₗ P.cotangentComplex ∧
      ψ₀ ∘ₗ φ₀ - LinearMap.id = P.cotangentComplex ∘ₗ s ∧
      φ₁ ∘ₗ ψ₁ - LinearMap.id = t ∘ₗ Q.cotangentComplex ∧
      φ₀ ∘ₗ ψ₀ - LinearMap.id = Q.cotangentComplex ∘ₗ t

NaiveCotangent.isQuasiIso_nlExtensionOverMap_of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/LocalizationBaseAndTarget.lean, line 479. The attribute's comment: “the canonical map NL_{T/R} ⟶ NL_{T/R'} is bijective in both degrees, hence a quasi-isomorphism; the homotopy equivalence itself is naiveCotangentComplex_localization_base_homotopyEquiv.”.

Localizing the base: for a localization R' = N⁻¹R of R at a multiplicative subset N ⊆ R and a ring map R' → T, the canonical map of two-term complexes NL_{T/R} ⟶ NL_{T/R'} is bijective in both degrees, hence a quasi-isomorphism.

theorem isQuasiIso_nlExtensionOverMap_of_isLocalization (N : Submonoid R) [IsLocalization N R'] :
    IsQuasiIso (nlExtensionOverMap
      ((Generators.self R T).defaultHom (Generators.self R' T)).toExtensionHom)

Tag 08JZ, a lemma

Tag 08JZ in the Stacks Project.

Algebra.Generators.exists_cotangentComplex_comp_localizationAway_eq_prodMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Localization.lean, line 521. The attribute's comment: “Item (3), which contains items (1) and (2): splittings of both rows of the source's diagram that are simultaneously compatible with the differentials. Mathlib has each row separately, but not compatibly. See the module docstring.”.

The naive cotangent complex commutes with localization at an element: let A → B be a ring map, let α : P = A[x_i, i ∈ ι] → B be a presentation with kernel I, let g ∈ B and let B_g be a localization of B away from g. Write β : P[x] → B_g, x ↦ 1/g for the induced presentation of B_g over A, with kernel J, and B[x] → B_g for the canonical presentation of B_g over B. Then there are splittings J/J² ≅ (I/I²) ⊗_B B_g ⊕ (gx-1)/(gx-1)² and Ω_{P[x]/A} ⊗ B_g ≅ (Ω_{P/A} ⊗_P B) ⊗_B B_g ⊕ Ω_{B[x]/B} ⊗ B_g of the two canonical exact rows which are compatible with the differentials, i.e. which identify the two term complex NL(β) with the direct sum of NL(α) ⊗_B B_g and of the complex NL(B[x] → B_g) = (B_g --g--> B_g).

public theorem exists_cotangentComplex_comp_localizationAway_eq_prodMap
    (g : S) [IsLocalization.Away g T] (P : Generators R S ι) :
    ∃ (e : ((localizationAway T g).comp P).toExtension.Cotangent ≃ₗ[T]
        T ⊗[S] P.toExtension.Cotangent × (localizationAway T g).toExtension.Cotangent)
      (e' : ((localizationAway T g).comp P).toExtension.CotangentSpace ≃ₗ[T]
        T ⊗[S] P.toExtension.CotangentSpace ×
          (localizationAway T g).toExtension.CotangentSpace),
      e'.toLinearMap ∘ₗ ((localizationAway T g).comp P).toExtension.cotangentComplex =
          (P.toExtension.cotangentComplex.baseChange T).prodMap
            (localizationAway T g).toExtension.cotangentComplex ∘ₗ e.toLinearMap ∧
        e.symm.toLinearMap ∘ₗ LinearMap.inl T _ _ =
          (Extension.Cotangent.map
            ((localizationAway T g).toComp P).toExtensionHom).liftBaseChange T ∧
        LinearMap.snd T _ _ ∘ₗ e.toLinearMap =
          Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom ∧
        e'.symm.toLinearMap ∘ₗ LinearMap.inl T _ _ =
          (Extension.CotangentSpace.map
            ((localizationAway T g).toComp P).toExtensionHom).liftBaseChange T ∧
        LinearMap.snd T _ _ ∘ₗ e'.toLinearMap =
          Extension.CotangentSpace.map ((localizationAway T g).ofComp P).toExtensionHom

Tag 00S7, a lemma

Tag 00S7 in the Stacks Project.

Algebra.Extension.Cotangent.bijOn_ker_liftBaseChange_map_of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Localization.lean, line 180. The attribute's comment: “The H₁ half at the level of the complexes, where the homology is ker (d ⊗ T) rather than T ⊗ ker d. The H₀ half is KaehlerDifferential.isLocalizedModule_map and the H¹(L)-level H₁ half is Algebra.H1Cotangent.isLocalizedModule. See the module docstring.”.

The naive cotangent complex commutes with localization, on H₁: let A → B be a ring map, let M ⊆ B be a multiplicative subset with localization M⁻¹B, and let α, β be presentations of B and of M⁻¹B over A with a compatible map f between them. Then the map M⁻¹B ⊗_B I/I² → J/J² induced by f carries the kernel of the base changed differential of NL(α) bijectively onto the kernel of the differential of NL(β).

public theorem Algebra.Extension.Cotangent.bijOn_ker_liftBaseChange_map_of_isLocalization
    {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
    (M : Submonoid S) [IsLocalization M T] {ι κ : Type*} {P : Algebra.Generators R S ι}
    {Q : Algebra.Generators R T κ} (f : P.toExtension.Hom Q.toExtension) :
    Set.BijOn ((Algebra.Extension.Cotangent.map f).liftBaseChange T)
      (LinearMap.ker (P.toExtension.cotangentComplex.baseChange T))
      (LinearMap.ker Q.toExtension.cotangentComplex)

NaiveCotangent.isQuasiIso_nlExtensionBaseChangeMap_of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/LocalizationBaseAndTarget.lean, line 446. The attribute's comment: “the whole lemma at the level of the complexes: the canonical map NL_{S/R} ⊗_S T ⟶ NL_{T/R} is a quasi-isomorphism. The H₁ half alone is Algebra.Extension.Cotangent.bijOn_ker_liftBaseChange_map_of_isLocalization.”.

Localizing the target: for a localization T = M⁻¹S of S at a multiplicative subset M ⊆ S, the canonical map of two-term complexes NL_{S/R} ⊗_S T ⟶ NL_{T/R} is a quasi-isomorphism.

theorem isQuasiIso_nlExtensionBaseChangeMap_of_isLocalization (M : Submonoid S) [IsLocalization M T]
    (h : (Generators.self R S).toExtension.Hom (Generators.self R T).toExtension) :
    IsQuasiIso (nlExtensionBaseChangeMap (T := T) h)

Tag 00S3, a lemma

Tag 00S3 in the Stacks Project.

main_theorem_00s3, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/TwoTermComplex.lean, line 155.

Stacks Tag 00S3 (Lemma 10.134.14). Let R be a ring and let A_• : A_1 →[d_A] A_0 and B_• : B_1 →[d_B] B_0 be two term complexes of R-modules. Suppose there are morphisms of complexes φ : A_• → B_• and ψ : B_• → A_• such that φ ∘ ψ is homotopic to id_{B_•} and ψ ∘ φ is homotopic to id_{A_•}. Then there is an isomorphism of R-modules A_1 ⊕ B_0 ≅ B_1 ⊕ A_0.

theorem main_theorem_00s3 (A B : TwoComplex R)
    (φ : ComplexHom A B) (ψ : ComplexHom B A)
    (hB : Homotopic (φ.comp ψ) (ComplexHom.id B))
    (hA : Homotopic (ψ.comp φ) (ComplexHom.id A)) :
    Nonempty ((A.A1 × B.A0) ≃ₗ[R] (B.A1 × A.A0))

Tag 00S5, a lemma

Tag 00S5 in the Stacks Project.

NaiveCotangent.Conormal.conormal_stable_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Conormal.lean, line 269.

Stacks Tag 00S5 (Lemma 10.134.15). Let R → S be a ring map of finite type, and let P : Algebra.Generators R S (Fin n) (with kernel I) and Q : Algebra.Generators R S (Fin m) (with kernel J) be two finite-type presentations of S over R. Then there is an isomorphism of S-modules I/I² ⊕ S^{⊕m} ≅ J/J² ⊕ S^{⊕n}.

theorem conormal_stable_iso [Algebra.FiniteType R S]
    {n m : ℕ} (P : Algebra.Generators R S (Fin n)) (Q : Algebra.Generators R S (Fin m)) :
    Nonempty ((Conormal P × FreeModule S m) ≃ₗ[S] (Conormal Q × FreeModule S n))

Tag 00S6, a lemma

Tag 00S6 in the Stacks Project.

Algebra.Generators.nonempty_cotangent_baseChange_prod_linearEquiv_of_isLocalizationAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Localization.lean, line 815. The attribute's comment: “The isomorphism is non-canonical: Nonempty of a linear equivalence is the whole statement. See the module docstring.”.

The conormal module up to free summands, after localizing at an element: let R → S be a ring map, let g ∈ S and let S_g be a localization of S away from g. Let α : R[x₁, …, xₙ] → S be a presentation of S over R with kernel I and let β : R[y₁, …, y_m] → S_g be a presentation of S_g over R with kernel J. Then there is an isomorphism of S_g-modules (I/I²)_g ⊕ S_g^{⊕m} ≅ J/J² ⊕ S_g^{⊕n}.

public theorem nonempty_cotangent_baseChange_prod_linearEquiv_of_isLocalizationAway
    (g : S) [IsLocalization.Away g T] {n m : ℕ}
    (P : Generators R S (Fin n)) (Q : Generators R T (Fin m)) :
    Nonempty (((T ⊗[S] P.toExtension.Cotangent) × (Fin m → T)) ≃ₗ[T]
      (Q.toExtension.Cotangent × (Fin n → T)))

Sources

• Section 10.134, Tag 00S0
• AxiomMath/Stacks at 5ed82d14

LeanAlgebra.Generators.self · Algebra.Extension.cotangentComplex · Algebra.naiveCotangentComplex · Algebra.Generators.defaultHom_comp_defaultHom · Deformation.Artin.derivedNaiveCotangentComplexIso · NaiveCotangent.exists_hom · NaiveCotangent.nlMap_homotopic · NaiveCotangent.nlMapBase_comp_nlMapBase

Section10.135 Local complete intersections#

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

Tag 00S9, a definition

Tag 00S9 in the Stacks Project.

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

Let k be a field. A k-algebra S is a global complete intersection over k if either S is the zero ring (Subsingleton S), or there are n, c ≥ 0 and an isomorphism of k-algebras S ≃ₐ[k] k[x_1, …, x_n]/(f_1, …, f_c) with dim S = n - c.

Here k[x_1, …, x_n] is MvPolynomial (Fin n) k, the relations (f_1, …, f_c) are the ideal Ideal.span (Set.range f) for f : Fin c → MvPolynomial (Fin n) k, and the dimension condition is c ≤ n together with ringKrullDim S = ((n - c : ℕ) : WithBot ℕ∞).

public def IsGlobalCompleteIntersection (k : Type*) [Field k] (S : Type*) [CommRing S]
    [Algebra k S] : Prop

IsLocalCompleteIntersection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Defs.lean, line 107. The attribute's comment: “(2)”. References: EGA IV (19.3.6); SGA 6 0 (3.2), “special case”.

Let k be a field. A k-algebra S is a local complete intersection over k if there is a set s ⊆ S whose standard opens D(g) cover Spec S, and such that S_g = Localization.Away g is a global complete intersection over k for every g ∈ s.

The covering condition is recorded algebraically as Ideal.span s = ⊤; localCompleteIntersection_cover_iff is its equivalence with ⨆ g ∈ s, D(g) = ⊤.

public def IsLocalCompleteIntersection (k : Type*) [Field k] (S : Type*) [CommRing S]
    [Algebra k S] : Prop

Tag 00SA, a lemma

Tag 00SA in the Stacks Project.

Declarations registered for the tag:

• isGlobalCompleteIntersection_localization, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/CompleteIntersection/Criteria.lean, line 176 (StacksFrontier): “part (1): a localization of a global complete intersection over a field is a global complete intersection over that field”.
• isLocalCompleteIntersection_localization, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/CompleteIntersection/Criteria.lean, line 179 (StacksFrontier): “part (2): a localization of a local complete intersection over a field is a local complete intersection over that field”.

Tag 00SB, a lemma

Tag 00SB in the Stacks Project.

IsCompleteIntersection.isMaximalCohenMacaulay, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Local.lean, line 232. The attribute's comment: “The pointwise half of the lemma: Cohen-Macaulayness of a single complete intersection local ring over k, stated as Module.IsMaximalCohenMacaulay over itself as in 00ND.”. References: EGA 0 (17.1.3), “Cohen–Macaulay”.

A complete intersection over a field is a Cohen–Macaulay local ring. Writing the ring as R/(f_1, …, f_c) with R regular local and f_1, …, f_c a regular sequence, R is Cohen–Macaulay (Lemma 00NQ) and the quotient of a Cohen–Macaulay local ring by a regular sequence is again Cohen–Macaulay (Proposition 02JN).

theorem IsCompleteIntersection.isMaximalCohenMacaulay {k : Type*} [Field k] {A : Type*}
    [CommRing A] [IsNoetherianRing A] [IsLocalRing A] [Algebra k A]
    (h : IsCompleteIntersection k A) : Module.IsMaximalCohenMacaulay A A

IsLocalCompleteIntersection.isMaximalCohenMacaulay_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Local.lean, line 252. The attribute's comment: “Cohen-Macaulayness of the Noetherian ring S (Definition 00NC) is spelled out as a condition on its localizations at primes, each being Module.IsMaximalCohenMacaulay over itself, as in 00ND. The finite type hypothesis is omitted, being a consequence of IsLocalCompleteIntersection. See the module docstring.”.

A local complete intersection over a field is Cohen–Macaulay. Let k be a field and let S be a local complete intersection over k. Then every local ring S_𝔮 of S at a prime is a Cohen–Macaulay local ring, depth(S_𝔮) = dim(S_𝔮).

theorem IsLocalCompleteIntersection.isMaximalCohenMacaulay_localization
    {k : Type*} [Field k] {S : Type*} [CommRing S] [Algebra k S]
    (h : IsLocalCompleteIntersection k S) (q : Ideal S) [q.IsPrime] :
    Module.IsMaximalCohenMacaulay (Localization.AtPrime q) (Localization.AtPrime q)

Tag 00SC, a lemma

Tag 00SC in the Stacks Project.

Algebra.Generators.tfae_isGlobalCompleteIntersection_away, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/AtPrime/Criterion.lean, line 495. The attribute's comment: “Items (1)-(5) are the five entries of the List.TFAE, in order. The source's c, defined there as height 𝔮' - height 𝔮, is the hypothesis height 𝔮' = height 𝔮 + c, the additive form (see the module docstring); the source's parenthetical dim_𝔮(S) = n - c is a consequence of it, by Stacks 00P2. Items (3) and (4) are stated for the conormal module of I_A = I_{𝔮'} over A/I_A rather than for (I/I²)_𝔮 over S_𝔮; the two agree under the canonical identification of A/I_A with S_𝔮, localization being flat. The closing assertion of the lemma is the second conjunct of Algebra.Generators.spanFinrank_ker_map_le_iff_exists_isRegular, which carries this tag as well.”.

The complete intersection criterion at a prime. Let k be a field, let S = k[x_i]/I be a presented k-algebra with finitely many variables, let q be a prime of S, let q' be the corresponding prime of k[x_i] and let c be the codimension, height q' = height q + c. Write A = k[x_i]_{q'} and I_A = I_{q'}. Then the following are equivalent:

1. there is a g ∈ S, g ∉ q, such that S_g is a global complete intersection over k;
2. the ideal I_A can be generated by c elements;
3. the conormal module I_A/I_A² can be generated by c elements over A/I_A;
4. the conormal module I_A/I_A² is a free A/I_A-module of rank c;
5. the ideal I_A can be generated by a regular sequence in the regular local ring A.

Items (3) and (4) are stated for the conormal module of I_A over A/I_A, which agrees with (I/I²)_q over S_q: A/I_A is the localization S_q (this is ringKrullDim_quotient_map_ker_eq_height), and I_A/I_A² is (I/I²)_q, localization being flat.

The closing assertion of the lemma, that any c elements of I_A generating I_A/q'I_A form a regular sequence in A, is the second conjunct of Algebra.Generators.spanFinrank_ker_map_le_iff_exists_isRegular.

theorem Algebra.Generators.tfae_isGlobalCompleteIntersection_away
    (k : Type u) [Field k] (S : Type v) [CommRing S] [Algebra k S]
    {ι : Type w} [Finite ι] (P : Algebra.Generators k S ι)
    (q : Ideal S) [q.IsPrime] (c : ℕ)
    (hc : (q.comap (algebraMap P.Ring S)).height = q.height + c)
    (A : Type*) [CommRing A] [Algebra P.Ring A]
    [IsLocalization.AtPrime A (q.comap (algebraMap P.Ring S))] :
    List.TFAE
      [∃ g ∉ q, IsGlobalCompleteIntersection k (Localization.Away g),
        Submodule.spanFinrank (P.ker.map (algebraMap P.Ring A)) ≤ c,
        (⊤ : Submodule (A ⧸ P.ker.map (algebraMap P.Ring A))
            (P.ker.map (algebraMap P.Ring A)).Cotangent).spanFinrank ≤ c,
        Module.Free (A ⧸ P.ker.map (algebraMap P.Ring A))
              (P.ker.map (algebraMap P.Ring A)).Cotangent ∧
          Module.finrank (A ⧸ P.ker.map (algebraMap P.Ring A))
            (P.ker.map (algebraMap P.Ring A)).Cotangent = c,
        ∃ rs : List A, IsRegular A rs ∧
          Ideal.ofList rs = P.ker.map (algebraMap P.Ring A)]

Algebra.Generators.spanFinrank_ker_map_le_iff_exists_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/AtPrime/LocalCriterion.lean, line 510. The attribute's comment: “The equivalence of items (2) and (5) is the first conjunct, and the closing assertion of the lemma — that any c elements of I_{𝔮'} generating I_{𝔮'}/𝔮'I_{𝔮'} form a regular sequence — is the second. The five equivalent conditions themselves are Algebra.Generators.tfae_isGlobalCompleteIntersection_away, which carries this tag as well; this declaration is on the covering set for the closing assertion.”.

The equivalence of items (2) and (5), together with the closing assertion.

Let k be a field, let S = k[x_i]/I be a presented k-algebra with finitely many variables, let q be a prime of S, let q' be the corresponding prime of k[x_i], and let c be the codimension, height q' = height q + c. Then the ideal I_{q'} of A = k[x_i]_{q'} can be generated by c elements if and only if it can be generated by a regular sequence; and any c elements of I_{q'} generating I_{q'}/q'I_{q'} form a regular sequence.

theorem Algebra.Generators.spanFinrank_ker_map_le_iff_exists_isRegular
    (k : Type u) [Field k] (S : Type v) [CommRing S] [Algebra k S]
    {ι : Type w} [Finite ι] (P : Algebra.Generators k S ι)
    (q : Ideal S) [q.IsPrime] (c : ℕ)
    (hc : (q.comap (algebraMap P.Ring S)).height = q.height + c)
    (A : Type*) [CommRing A] [Algebra P.Ring A]
    [IsLocalization.AtPrime A (q.comap (algebraMap P.Ring S))] :
    (Submodule.spanFinrank (P.ker.map (algebraMap P.Ring A)) ≤ c ↔
        ∃ rs : List A, IsRegular A rs ∧
          Ideal.ofList rs = P.ker.map (algebraMap P.Ring A)) ∧
      ∀ rs : List A, rs.length = c →
        Ideal.ofList rs ⊔ (q.comap (algebraMap P.Ring S)).map (algebraMap P.Ring A) *
            P.ker.map (algebraMap P.Ring A) = P.ker.map (algebraMap P.Ring A) →
          IsRegular A rs

Tag 00SD, a definition

Tag 00SD in the Stacks Project.

IsCompleteIntersectionLocalRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Criteria.lean, line 86.

A k-algebra S is a complete intersection over k if there exist a k-algebra R and a list f = f₁, …, f_c of elements of R such that

• R is a regular local ring,
• R is essentially of finite type over k,
• every fᵢ lies in the maximal ideal of R,
• f₁, …, f_c is a regular sequence in R, and
• S ≅ R/(f₁, …, f_c) as k-algebras.

The source states this for a local k-algebra S essentially of finite type over k; both hypotheses are consequences here, see IsCompleteIntersectionLocalRing.isLocalRing and IsCompleteIntersectionLocalRing.essFiniteType. The length c of f is unconstrained, and is forced to be the codimension dim R - dim S by IsCompleteIntersectionLocalRing.exists_witness.

def IsCompleteIntersectionLocalRing (k : Type u) [Field k] (S : Type v) [CommRing S]
    [Algebra k S] : Prop

IsCompleteIntersection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Defs.lean, line 168. The attribute's comment: “Items (1)-(4) are the four clauses of the body, in order. The source's condition f_1, …, f_c ∈ 𝔪_R is not stated separately: over the local ring R it is equivalent, given item (3), to the nonvanishing of R/(f_1, …, f_c) that Mathlib's RingTheory.Sequence.IsRegular already carries. The source's hypotheses that S be local and essentially of finite type over k are omitted, both being consequences of the existence of R, as with the finite type hypothesis in Definition 00S9. The witness R is quantified in the universe of k. See the module docstring.”.

Let k be a field. A k-algebra S is a complete intersection over k if there are a regular local k-algebra R, essentially of finite type over k, and a regular sequence f_1, …, f_c in R such that S ≃ₐ[k] R/(f_1, …, f_c). The condition f_1, …, f_c ∈ 𝔪_R is contained in RingTheory.Sequence.IsRegular, which asks the quotient R/(f_1, …, f_c) to be nonzero.

public def IsCompleteIntersection (k : Type u) [Field k] (S : Type v) [CommRing S]
    [Algebra k S] : Prop

Tag 00SE, a lemma

Tag 00SE in the Stacks Project.

IsRegularLocalRing.exists_isRegular_ker_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/Basic.lean, line 2066. The attribute's comment: “Items (1)-(4) are the four items of the list, in the source's order. Ker(A → C) is RingHom.ker (g.comp f). Generated by dim A - dim C elements is the equality ringKrullDim C + (RingHom.ker (g.comp f)).spanFinrank = ringKrullDim A: subtraction in WithBot ℕ∞ is truncated, while the inequality ≤ always holds here by Krull's height theorem, so the equality says exactly that the minimal number of generators attains dim A - dim C. The source's hypotheses that the maps be local homomorphisms and that C be local are omitted, all three being consequences of surjectivity. See the module docstring.”.

Stacks 00SE. Let A → B → C be surjective local ring homomorphisms with A and B regular local rings. Then the following are equivalent: Ker(A → C) is generated by a regular sequence; Ker(A → C) is generated by dim A - dim C elements; Ker(B → C) is generated by a regular sequence; Ker(B → C) is generated by dim B - dim C elements.

Being generated by n elements is Submodule.spanFinrank ≤ n, stated here in the equivalent additive form dim C + spanFinrank (Ker) = dim A (respectively = dim B), since the reverse inequality is Krull's height theorem. See the module docstring.

public theorem IsRegularLocalRing.exists_isRegular_ker_tfae
    {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
    [IsRegularLocalRing A] [IsRegularLocalRing B] [Nontrivial C]
    {f : A →+* B} {g : B →+* C} (hf : Function.Surjective f) (hg : Function.Surjective g) :
    List.TFAE
      [∃ rs : List A, RingTheory.Sequence.IsRegular A rs ∧
          Ideal.ofList rs = RingHom.ker (g.comp f),
        ringKrullDim C + (RingHom.ker (g.comp f)).spanFinrank = ringKrullDim A,
        ∃ rs : List B, RingTheory.Sequence.IsRegular B rs ∧ Ideal.ofList rs = RingHom.ker g,
        ringKrullDim C + (RingHom.ker g).spanFinrank = ringKrullDim B]

Tag 00SF, a lemma

Tag 00SF in the Stacks Project.

IsCompleteIntersection.tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/LocalRing.lean, line 896. The attribute's comment: “Items (1)-(5) are the five items of the list, in the source's order. Essentially of finite presentation over k is Algebra.EssFiniteType k R, the two notions agreeing over a field; the source's proof states item (2) with essentially of finite type as well. Generated by dim R - dim S elements is ringKrullDim S + (RingHom.ker f).spanFinrank = ringKrullDim R, the reading of Lemma 00SE: subtraction in WithBot ℕ∞ is truncated while the inequality ≥ holds unconditionally, so the equality says the minimal number of generators attains dim R - dim S. In items (4) and (5) the isomorphism S ≅ A_𝔞 is stated abstractly, as IsLocalization.AtPrime S a for an A-algebra structure on S compatible with k. Item (2) quantifies over rings in Type (max u w) for a universe parameter w: that asserts it in every universe and still lets it be instantiated at the localization k[x_1, …, x_n]_𝔮 of the source's proof of (2) ⇒ (1), which a free Type w would not. The existential items (3)-(5) put their witnesses in the universe of k, where the source's are. The hypothesis that the surjections be local ring homomorphisms is omitted, being a consequence of surjectivity. See the module docstring.”. References: EGA IV (19.3.2), “ess. f.t. over a field”.

Let k be a field and let S be a local k-algebra essentially of finite type over k. The following are equivalent: S is a complete intersection over k; for every surjection f : R →ₐ[k] S with R a regular local k-algebra essentially of finite type over k the ideal Ker f is generated by a regular sequence; for some such surjection Ker f is generated by dim R - dim S elements; S is a localization of a global complete intersection over k at a prime; and S is a localization of a local complete intersection over k at a prime.

Generated by dim R - dim S elements is the additive equality dim S + spanFinrank (Ker f) = dim R, and items (4) and (5) exhibit S as a localization by an instance rather than by an isomorphism with Localization.AtPrime.

public theorem IsCompleteIntersection.tfae (k : Type u) [Field k] (S : Type v) [CommRing S]
    [Algebra k S] [IsLocalRing S] [Algebra.EssFiniteType k S] :
    List.TFAE
      [IsCompleteIntersection k S,
        ∀ (R : Type (max u w)) (_ : CommRing R) (_ : Algebra k R) (_ : IsRegularLocalRing R)
          (_ : Algebra.EssFiniteType k R) (f : R →ₐ[k] S),
          Function.Surjective f →
            ∃ rs : List R, RingTheory.Sequence.IsRegular R rs ∧ Ideal.ofList rs = RingHom.ker f,
        ∃ (R : Type u) (_ : CommRing R) (_ : Algebra k R) (_ : IsRegularLocalRing R) (_ :
          Algebra.EssFiniteType k R) (f : R →ₐ[k] S),
          Function.Surjective f ∧ ringKrullDim S + (RingHom.ker f).spanFinrank = ringKrullDim R,
        ∃ (A : Type u) (_ : CommRing A) (_ : Algebra k A) (_ : Algebra A S) (_ :
          IsScalarTower k A S) (a : Ideal A) (_ : a.IsPrime),
          IsGlobalCompleteIntersection k A ∧ IsLocalization.AtPrime S a,
        ∃ (A : Type u) (_ : CommRing A) (_ : Algebra k A) (_ : Algebra A S) (_ :
          IsScalarTower k A S) (a : Ideal A) (_ : a.IsPrime),
          IsLocalCompleteIntersection k A ∧ IsLocalization.AtPrime S a]

Tag 00SG, a lemma

Tag 00SG in the Stacks Project.

IsCompleteIntersection.localization_atPrime_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/LocalRing.lean, line 559. The attribute's comment: “Item (1) is IsCompleteIntersection k Sq for an abstract localization Sq of S at q, items (2) and (3) use Localization.Away g as Definition 00S9 does, and item (4) is a universally quantified statement over presentations Algebra.Generators k S ι with ι finite, transcribing condition (5) of Lemma 00SC — the only one of its conditions (1)-(5) that mentions neither the codimension c nor the conormal module, and interchangeable with the others by that lemma. See the module docstring.”. References: EGA IV (19.3.2), “special case”.

Let k be a field, let S be a finite type k-algebra and let q be a prime of S. Then: the local ring S_q is a complete intersection over k; S_g is a local complete intersection over k for some g ∉ q; S_g is a global complete intersection over k for some g ∉ q; and, for every presentation S = k[x_i]/I in finitely many variables, the ideal I_{q'} of k[x_i]_{q'} is generated by a regular sequence — are all equivalent.

public theorem IsCompleteIntersection.localization_atPrime_tfae (k : Type u) [Field k] (S : Type v)
    [CommRing S] [Algebra k S] [Algebra.FiniteType k S] (q : Ideal S) [q.IsPrime] (Sq : Type*)
    [CommRing Sq] [Algebra S Sq] [IsLocalization.AtPrime Sq q] [Algebra k Sq]
    [IsScalarTower k S Sq] :
    List.TFAE
      [IsCompleteIntersection k Sq, ∃ g ∉ q, IsLocalCompleteIntersection k (Localization.Away g),
        ∃ g ∉ q, IsGlobalCompleteIntersection k (Localization.Away g),
        ∀ (ι : Type w) [Finite ι] (P : Algebra.Generators k S ι) (A : Type (max u w)) [CommRing A]
          [Algebra P.Ring A] [IsLocalization.AtPrime A (q.comap (algebraMap P.Ring S))],
          ∃ rs : List A,
            RingTheory.Sequence.IsRegular A rs ∧
              Ideal.ofList rs = P.ker.map (algebraMap P.Ring A)]

Tag 00SH, a lemma

Tag 00SH in the Stacks Project.

IsLocalCompleteIntersection.tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/LocalRing.lean, line 703. The attribute's comment: “Item (1) is IsLocalCompleteIntersection k S (Definition 00S9 (2)), and items (2) and (3) say that IsCompleteIntersection k Sq (Definition 00SD) holds for every localization of S at a prime, resp. at a maximal ideal, quantified over abstract localizations Sq in the universe of S with the k-algebra structure induced from S — the hypothesis block of item (1) of Lemma 00SG. The source's finite type hypothesis is kept: items (2) and (3) do not imply it, as ℚ(x) over ℚ shows. The source's appeal to quasi-compactness of Spec S is absent, IsLocalCompleteIntersection asking for a covering by an arbitrary set of elements generating the unit ideal. See the module docstring.”.

Let k be a field and let S be a finite type k-algebra. Then: S is a local complete intersection over k; every local ring of S is a complete intersection over k; and every localization of S at a maximal ideal is a complete intersection over k — are all equivalent. The local rings in the last two items are abstract localizations of S, carrying the k-algebra structure induced from S.

public theorem IsLocalCompleteIntersection.tfae (k : Type u) [Field k] (S : Type v) [CommRing S]
    [Algebra k S] [Algebra.FiniteType k S] :
    List.TFAE
      [IsLocalCompleteIntersection k S,
        ∀ (q : Ideal S) [q.IsPrime] (Sq : Type v) [CommRing Sq] [Algebra S Sq]
          [IsLocalization.AtPrime Sq q] [Algebra k Sq] [IsScalarTower k S Sq],
          IsCompleteIntersection k Sq,
        ∀ (m : Ideal S) [m.IsMaximal] (Sm : Type v) [CommRing Sm] [Algebra S Sm]
          [IsLocalization.AtPrime Sm m] [Algebra k Sm] [IsScalarTower k S Sm],
          IsCompleteIntersection k Sm]

Tag 00SI, a lemma

Tag 00SI in the Stacks Project.

Algebra.IsPushout.isCompleteIntersection_localization_atPrime_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/BaseChange.lean, line 360. The attribute's comment: “The base change S' = K ⊗_k S is an arbitrary pushout square Algebra.IsPushout k K S S', the shape of the sibling 00SJ; the source's literal form satisfies it. The source's corresponding prime q is the contraction of q', spelled Ideal.LiesOver, and the two local rings are abstract localizations at q, resp. q', with the k-, resp. K-algebra structure induced from S, resp. S', as in item (1) of Lemma 00SG. A complete intersection over a field (Definition 00SD) is IsCompleteIntersection. See the module docstring.”. References: EGA IV (19.3.4), “affine case”.

Let K/k be a field extension, let S be a finite type k-algebra and let S' be the base change of S along k → K, so S' = K ⊗_k S. Let q' be a prime of S' and let q be the prime of S it lies over. Then the local ring S'_{q'} is a complete intersection over K if and only if the local ring S_q is a complete intersection over k.

public theorem Algebra.IsPushout.isCompleteIntersection_localization_atPrime_iff
    (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K]
    (S : Type*) [CommRing S] [Algebra k S] [Algebra.FiniteType k S]
    (S' : Type*) [CommRing S'] [Algebra k S'] [Algebra K S'] [Algebra S S']
    [IsScalarTower k K S'] [IsScalarTower k S S'] [Algebra.IsPushout k K S S']
    (q : Ideal S) [q.IsPrime] (q' : Ideal S') [q'.IsPrime] [q'.LiesOver q]
    (Sq : Type*) [CommRing Sq] [Algebra S Sq] [IsLocalization.AtPrime Sq q]
    [Algebra k Sq] [IsScalarTower k S Sq]
    (S'q' : Type*) [CommRing S'q'] [Algebra S' S'q'] [IsLocalization.AtPrime S'q' q']
    [Algebra K S'q'] [IsScalarTower K S' S'q'] :
    IsCompleteIntersection K S'q' ↔ IsCompleteIntersection k Sq

Tag 00SJ, a lemma

Tag 00SJ in the Stacks Project.

Algebra.IsPushout.isLocalCompleteIntersection_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/FieldExtension.lean, line 154. The attribute's comment: “The base change S' = S ⊗_k K is an arbitrary pushout square Algebra.IsPushout k K S S', the orientation of the sibling 00SM; the source's literal form is inferInstance. The source's finite type hypothesis on S is omitted: each side of the equivalence implies it. A local complete intersection over a field (Definition 00S9 (2)) is IsLocalCompleteIntersection. See the module docstring.”.

Let k → K be a field extension, let S be a k-algebra and let S' be the base change of S along k → K, so S' = S ⊗_k K. Then S' is a local complete intersection over K if and only if S is a local complete intersection over k.

public theorem Algebra.IsPushout.isLocalCompleteIntersection_iff (k K S S' : Type*) [Field k]
    [Field K] [CommRing S] [CommRing S'] [Algebra k K] [Algebra k S] [Algebra k S'] [Algebra K S']
    [Algebra S S'] [IsScalarTower k K S'] [IsScalarTower k S S'] [Algebra.IsPushout k K S S'] :
    IsLocalCompleteIntersection K S' ↔ IsLocalCompleteIntersection k S

Tag 02JP, a lemma

Tag 02JP in the Stacks Project.

exists_isRegular_ofList_eq_ker_algebraMap_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Local.lean, line 616. The attribute's comment: “The square is IsScalarTower R A B and IsScalarTower R S B with R → A and S → B surjective, I and J being their kernels, and J̄ is the image of J in S ⧸ 𝔪_R S. Stated more generally than the source: R is only assumed Cohen-Macaulay (regular local rings are, by 00NQ), and S̄ is not assumed regular, which the argument does not use. S is assumed Noetherian, as the source's appeals to 00MG and 00ME require. See the module docstring.”.

Descent of regular sequences along a flat square of local rings. Let

B ← S
↑   ↑
A ← R

be a commutative square of rings in which R is a Cohen–Macaulay Noetherian local ring, S is a Noetherian local ring, A = R/I and B = S/J are quotients, and R → S and A → B are flat. If J is generated by a regular sequence, and the image J̄ of J in S̄ = S/𝔪_R S is generated by a regular sequence, then I is generated by a regular sequence.

The quotients are encoded by the surjectivity of R → A and S → B, the ideals I and J being their kernels. See the module docstring.

theorem exists_isRegular_ofList_eq_ker_algebraMap_of_flat
    {R S A B : Type*} [CommRing R] [CommRing S] [CommRing A] [CommRing B]
    [Algebra R S] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B]
    [IsScalarTower R A B] [IsScalarTower R S B]
    [IsLocalRing R] [IsNoetherianRing R] [IsLocalRing S] [IsNoetherianRing S]
    [Module.Flat R S] [Module.Flat A B]
    (hR : Module.IsMaximalCohenMacaulay R R)
    (hA : Function.Surjective (algebraMap R A)) (hB : Function.Surjective (algebraMap S B))
    (hJ : ∃ rs : List S, IsRegular S rs ∧ Ideal.ofList rs = RingHom.ker (algebraMap S B))
    (hJbar : ∃ rs : List (S ⧸ (maximalIdeal R).map (algebraMap R S)),
      IsRegular (S ⧸ (maximalIdeal R).map (algebraMap R S)) rs ∧
        Ideal.ofList rs = (RingHom.ker (algebraMap S B)).map (Ideal.Quotient.mk _)) :
    ∃ rs : List R, IsRegular R rs ∧ Ideal.ofList rs = RingHom.ker (algebraMap R A)

Sources

• Section 10.135, Tag 00S8
• AxiomMath/Stacks at 5ed82d14

LeanIsGlobalCompleteIntersection · IsLocalCompleteIntersection · isGlobalCompleteIntersection_localization · isLocalCompleteIntersection_localization · IsCompleteIntersection.isMaximalCohenMacaulay · IsLocalCompleteIntersection.isMaximalCohenMacaulay_localization · Algebra.Generators.tfae_isGlobalCompleteIntersection_away · Algebra.Generators.spanFinrank_ker_map_le_iff_exists_isRegular

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.