15.43 Ascending properties… to 15.63 Spectral sequences for Tor

Section15.43 Ascending properties along regular ring maps#

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

Tag 07QK, a lemma

Tag 07QK in the Stacks Project.

isReduced_of_isRegularRingHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/AscentAlongRegularRingHom.lean, line 79.

If f : R →+* S is regular, R and S are Noetherian, and R is reduced, then S is reduced.

public theorem isReduced_of_isRegularRingHom {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    (f : R →+* S) (hf : IsRegularRingHom f) [IsNoetherianRing R]
    [IsReduced R] : IsReduced S
Tag 0BFK, a lemma

Tag 0BFK in the Stacks Project.

isNormalRing_of_flat_of_isGeometricallyRegular_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/AscentAlongRegularRingHom.lean, line 114. References: EGA IV (6.5.4), “(ii), regular fibres”.

Let R → S be a regular map of Noetherian rings. If R is normal, then S is normal.

public theorem isNormalRing_of_flat_of_isGeometricallyRegular_fiber
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
    [IsNoetherianRing R] [IsNoetherianRing S] [Module.Flat R S]
    (hR : IsNormalRing R)
    (hfiber : ∀ (p : Ideal R) [p.IsPrime],
      Algebra.IsGeometricallyRegular p.ResidueField (p.Fiber S)) :
    IsNormalRing S
Tag 0H7S, a lemma

Tag 0H7S in the Stacks Project.

isRegularRing_of_isRegularRingHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/AscentAlongRegularRingHom.lean, line 143.

The Noetherian target of a regular ring homomorphism from a regular ring is regular.

public theorem isRegularRing_of_isRegularRingHom
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    (f : R →+* S) (hf : IsRegularRingHom f)
    [IsNoetherianRing S] [IsRegularRing R] : IsRegularRing S
Tag 0H7T, a lemma

Tag 0H7T in the Stacks Project.

isCohenMacaulayRing_of_isRegularRingHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/AscentAlongRegularRingHom.lean, line 211.

If f : R →+* S is regular, S is Noetherian, and R is Noetherian and Cohen–Macaulay, then S is Cohen–Macaulay.

public theorem isCohenMacaulayRing_of_isRegularRingHom
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsNoetherianRing R] [IsNoetherianRing S] (f : R →+* S)
    (hf : IsRegularRingHom f) (hR : IsCohenMacaulayRing R) :
    IsCohenMacaulayRing S
Sources
LeanisReduced_of_isRegularRingHom · isNormalRing_of_flat_of_isGeometricallyRegular_fiber · isRegularRing_of_isRegularRingHom · isCohenMacaulayRing_of_isRegularRingHom

Section15.44 Permanence of properties under completion#

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

Tag 07NU, the section

Tag 07NU in the Stacks Project.

AdicCompletion.noetherian_completeLocal_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/PermanenceUnderCompletion.lean, line 34. The attribute's comment: “the completion of a Noetherian local ring”.

The completion of a Noetherian local ring (A, 𝔪) is a Noetherian local ring with maximal ideal 𝔪 A^∧, complete with respect to it, and faithfully flat over A.

theorem noetherian_completeLocal_faithfullyFlat (A : Type*) [CommRing A] [IsNoetherianRing A]
    [IsLocalRing A] :
    IsNoetherianRing (AdicCompletion (maximalIdeal A) A) ∧
      IsLocalRing (AdicCompletion (maximalIdeal A) A) ∧
      maximalIdeal (AdicCompletion (maximalIdeal A) A) =
        (maximalIdeal A).map (algebraMap A (AdicCompletion (maximalIdeal A) A)) ∧
      IsAdicComplete (maximalIdeal (AdicCompletion (maximalIdeal A) A))
        (AdicCompletion (maximalIdeal A) A) ∧
      Module.FaithfullyFlat A (AdicCompletion (maximalIdeal A) A)
Tag 07NV, a lemma

Tag 07NV in the Stacks Project.

ringKrullDim_adicCompletion_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/PermanenceOfProperties.lean, line 306. References: EGA IV (7.3.19), “partial”.

Stacks 07NV. A Noetherian local ring and its completion at the maximal ideal have the same Krull dimension.

public theorem ringKrullDim_adicCompletion_maximalIdeal {A : Type*} [CommRing A]
    [IsNoetherianRing A] [IsLocalRing A] :
    ringKrullDim A = ringKrullDim (AdicCompletion (maximalIdeal A) A)
Tag 07NW, a lemma

Tag 07NW in the Stacks Project.

depth_adicCompletion_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/PermanenceOfProperties.lean, line 372.

Stacks 07NW. A Noetherian local ring and its completion at the maximal ideal have the same depth.

public theorem depth_adicCompletion_maximalIdeal {A : Type*} [CommRing A]
    [IsNoetherianRing A] [IsLocalRing A] :
    Module.depth A (maximalIdeal A) A =
      Module.depth (AdicCompletion (maximalIdeal A) A)
        (maximalIdeal (AdicCompletion (maximalIdeal A) A))
        (AdicCompletion (maximalIdeal A) A)
Tag 07NX, a lemma

Tag 07NX in the Stacks Project.

isMaximalCohenMacaulay_iff_adicCompletion_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/PermanenceOfProperties.lean, line 397.

Stacks 07NX. A Noetherian local ring is Cohen–Macaulay if and only if its completion at the maximal ideal is Cohen–Macaulay.

public theorem isMaximalCohenMacaulay_iff_adicCompletion_maximalIdeal {A : Type*} [CommRing A]
    [IsNoetherianRing A] [IsLocalRing A] :
    Module.IsMaximalCohenMacaulay A A ↔
      Module.IsMaximalCohenMacaulay (AdicCompletion (IsLocalRing.maximalIdeal A) A)
        (AdicCompletion (IsLocalRing.maximalIdeal A) A)
Tag 07NY, a lemma

Tag 07NY in the Stacks Project.

isRegularLocalRing_iff_adicCompletion_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/PermanenceOfProperties.lean, line 419. References: EGA 0 (17.1.5); EGA 0 (17.3.8.1), “local, J = maximal ideal”.

Stacks 07NY. A Noetherian local ring is regular if and only if its completion at the maximal ideal is regular.

public theorem isRegularLocalRing_iff_adicCompletion_maximalIdeal {A : Type*} [CommRing A]
    [IsNoetherianRing A] [IsLocalRing A] :
    IsRegularLocalRing A ↔
      IsRegularLocalRing (AdicCompletion (IsLocalRing.maximalIdeal A) A)
Tag 0AP1, a lemma

Tag 0AP1 in the Stacks Project.

isDiscreteValuationRing_iff_adicCompletion_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/PermanenceOfProperties.lean, line 440.

Stacks 0AP1. A Noetherian local ring is a discrete valuation ring if and only if its completion at the maximal ideal is a discrete valuation ring.

public theorem isDiscreteValuationRing_iff_adicCompletion_maximalIdeal {A : Type*} [CommRing A]
    [IsNoetherianRing A] [IsLocalRing A] :
    (∃ _ : IsDomain A, IsDiscreteValuationRing A) ↔
      ∃ _ : IsDomain (AdicCompletion (IsLocalRing.maximalIdeal A) A),
        IsDiscreteValuationRing (AdicCompletion (IsLocalRing.maximalIdeal A) A)
Tag 07NZ, a lemma

Tag 07NZ in the Stacks Project.

reducedness_and_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/PermanenceOfProperties.lean, line 515. References: EGA IV (7.6.1), “more general”.

Stacks 07NZ. For a Noetherian local ring A, a reduced completion forces A to be reduced. The converse fails, even for a Noetherian local domain. If A is Nagata, then A is reduced if and only if its completion is reduced.

public theorem reducedness_and_adicCompletion (A : Type u) [CommRing A] [IsLocalRing A]
    [IsNoetherianRing A] :
    (IsAnalyticallyUnramified A → IsReduced A) ∧
      (∃ (B : Type v) (_ : CommRing B) (_ : IsLocalRing B) (_ : IsNoetherianRing B)
        (_ : IsDomain B), ¬ IsAnalyticallyUnramified B) ∧
      (IsNagataRing A → (IsReduced A ↔ IsAnalyticallyUnramified A))
Tag 0FIZ, a lemma

Tag 0FIZ in the Stacks Project.

isNormalRing_of_isNormalRing_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/PermanenceOfProperties.lean, line 547.

A Noetherian local ring is normal if its completion at the maximal ideal is normal.

public theorem isNormalRing_of_isNormalRing_adicCompletion
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (hA : IsNormalRing (AdicCompletion (IsLocalRing.maximalIdeal A) A)) :
    IsNormalRing A
Tag 0C4G, a lemma

Tag 0C4G in the Stacks Project.

adicCompletionMap_flat_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/PermanenceOfProperties.lean, line 684. References: SGA 3 VIIB (1.3.4), “partial”.

Stacks 0C4G. A local homomorphism of Noetherian local rings is flat if and only if the induced homomorphism between their completions at the maximal ideals is flat.

public theorem adicCompletionMap_flat_iff {A : Type u} {B : Type v}
    [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B]
    [IsNoetherianRing A] [IsNoetherianRing B] (f : A →+* B) [IsLocalHom f] :
    (adicCompletionMap f (IsLocalRing.maximalIdeal A) (IsLocalRing.maximalIdeal B)
      (IsLocalRing.map_maximalIdeal_le f)).Flat ↔ f.Flat
Tag 0AGX, a lemma

Tag 0AGX in the Stacks Project.

exists_adicCompletion_ringEquiv_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/PermanenceOfProperties.lean, line 784.

Stacks 0AGX. A flat local homomorphism which identifies the maximal ideals and induces an isomorphism of residue fields induces an isomorphism of adic completions.

public theorem exists_adicCompletion_ringEquiv_of_flat
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B]
    [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Flat A B]
    (hfg : (maximalIdeal A).FG)
    (hmax : (maximalIdeal A).map (algebraMap A B) = maximalIdeal B)
    (hres : Function.Bijective (ResidueField.map (algebraMap A B))) :
    ∃ e : AdicCompletion (maximalIdeal A) A ≃+* AdicCompletion (maximalIdeal B) B,
      ∀ a : A,
        e (algebraMap A (AdicCompletion (maximalIdeal A) A) a) =
          algebraMap B (AdicCompletion (maximalIdeal B) B) (algebraMap A B a)
Sources
LeanAdicCompletion.noetherian_completeLocal_faithfullyFlat · ringKrullDim_adicCompletion_maximalIdeal · depth_adicCompletion_maximalIdeal · isMaximalCohenMacaulay_iff_adicCompletion_maximalIdeal · isRegularLocalRing_iff_adicCompletion_maximalIdeal · isDiscreteValuationRing_iff_adicCompletion_maximalIdeal · reducedness_and_adicCompletion · isNormalRing_of_isNormalRing_adicCompletion

Section15.45 Permanence of properties under étale maps#

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

Tag 0AGY, the section

Tag 0AGY in the Stacks Project.

RingHom.Etale.ringKrullDim_localization_atPrime_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Height.lean, line 95. The tag is given by the attribute command at StacksFrontier/RingTheory/Etale/Height.lean, line 103. The attribute's comment: “Lemma 07QP of the section: for an étale ring map A → B and a prime 𝔮 ⊂ B lying over 𝔭 ⊂ A, dim A_𝔭 = dim B_𝔮.”. References: EGA IV (17.6.4), “affine/ring case”; EGA IV (6.1.3), “special case”.

Stacks Tag 07QP. For an étale ring map f : A →+* B, if q is a prime of B lying over the prime p of A, then the Krull dimensions of the localizations A_p and B_q agree.

theorem RingHom.Etale.ringKrullDim_localization_atPrime_eq {A B : Type*} [CommRing A] [CommRing B]
    {f : A →+* B} (hf : f.Etale) (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime]
    (hlo : p = q.comap f) :
    ringKrullDim (Localization.AtPrime p) = ringKrullDim (Localization.AtPrime q)

isNoetherianRing_localization_iff_of_etale, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/PermanenceOfProperties.lean, line 100. The attribute's comment: “Lemma 0AGZ of the section: for an étale ring map A → B and a prime 𝔮 ⊂ B lying over 𝔭 ⊂ A, A_𝔭 is Noetherian if and only if B_𝔮 is.”.

For an étale map, the local rings at primes lying over one another are Noetherian simultaneously.

public lemma isNoetherianRing_localization_iff_of_etale
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [Algebra.Etale A B]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p] :
    IsNoetherianRing (Localization.AtPrime p) ↔
      IsNoetherianRing (Localization.AtPrime q)

isRegularLocalRing_localization_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/PermanenceOfProperties.lean, line 132. The tag is given by the attribute command at StacksFrontier/RingTheory/Etale/PermanenceOfProperties.lean, line 161. The attribute's comment: “Lemma 0AH0 of the section: for an étale ring map A → B and a prime 𝔮 ⊂ B lying over 𝔭 ⊂ A, A_𝔭 is regular if and only if B_𝔮 is.”.

Local rings at corresponding primes under an étale ring map are regular simultaneously.

public theorem isRegularLocalRing_localization_iff_of_etale
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [Algebra.Etale A B]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p] :
    IsRegularLocalRing (Localization.AtPrime p) ↔
      IsRegularLocalRing (Localization.AtPrime q)

exists_ringEquiv_pi_isDedekindDomain_and_isDiscreteValuationRing_atPrime_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/PermanenceOfProperties.lean, line 277. The tag is given by the attribute command at StacksFrontier/RingTheory/Etale/PermanenceOfProperties.lean, line 288. The attribute's comment: “Lemma 0AP2 of the section, its localization clause in corrected form: an étale algebra B over a Dedekind domain A is a finite product of Dedekind domains, and B_𝔮 is a discrete valuation ring for every maximal ideal 𝔮 ⊂ B with 𝔮 ∩ A ≠ (0). As written the clause asserts this for every maximal ideal, which is false: at a prime over (0) the local ring has dimension 0 by Lemma 07QP, see not_isDiscreteValuationRing_localization_of_etale_of_comap_eq_bot and the instance not_forall_isDiscreteValuationRing_localization_rat for the étale map ℚ → ℚ. The source's proof, through Lemmas 07QP, 0AH0 and Algebra 00PD, establishes the corrected clause.”.

An étale algebra over a Dedekind domain is a finite product of Dedekind domains, and its localizations at maximal ideals with nonzero contraction to the base are discrete valuation rings.

public theorem exists_ringEquiv_pi_isDedekindDomain_and_isDiscreteValuationRing_atPrime_of_etale
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [Algebra.Etale A B]
    [IsDedekindDomain A] :
    (∃ (n : ℕ) (D : Fin n → Type v) (_ : ∀ i, CommRing (D i)),
      (∀ i, IsDedekindDomain (D i)) ∧ Nonempty (B ≃+* ∀ i, D i)) ∧
      ∀ q : MaximalSpectrum B, q.asIdeal.comap (algebraMap A B) ≠ ⊥ →
        ∃ _ : IsDomain (Localization.AtPrime q.asIdeal),
          IsDiscreteValuationRing (Localization.AtPrime q.asIdeal)
Tag 0AGZ, a lemma

Tag 0AGZ in the Stacks Project.

isNoetherianRing_localization_iff_of_flat_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/PermanenceOfProperties.lean, line 67.

For a flat finite type map, the local rings at primes lying over one another are Noetherian simultaneously.

public theorem isNoetherianRing_localization_iff_of_flat_of_finiteType
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
    [Module.Flat A B] [Algebra.FiniteType A B]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p] :
    IsNoetherianRing (Localization.AtPrime p) ↔
      IsNoetherianRing (Localization.AtPrime q)
Tag 07QP, a lemma

Tag 07QP in the Stacks Project.

RingHom.Etale.ringKrullDim_localization_atPrime_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Height.lean, line 95. References: EGA IV (17.6.4), “affine/ring case”; EGA IV (6.1.3), “special case”.

Stacks Tag 07QP. For an étale ring map f : A →+* B, if q is a prime of B lying over the prime p of A, then the Krull dimensions of the localizations A_p and B_q agree.

theorem RingHom.Etale.ringKrullDim_localization_atPrime_eq {A B : Type*} [CommRing A] [CommRing B]
    {f : A →+* B} (hf : f.Etale) (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime]
    (hlo : p = q.comap f) :
    ringKrullDim (Localization.AtPrime p) = ringKrullDim (Localization.AtPrime q)
Tag 0AH0, a lemma

Tag 0AH0 in the Stacks Project.

isRegularLocalRing_localization_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/PermanenceOfProperties.lean, line 132.

Local rings at corresponding primes under an étale ring map are regular simultaneously.

public theorem isRegularLocalRing_localization_iff_of_etale
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [Algebra.Etale A B]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p] :
    IsRegularLocalRing (Localization.AtPrime p) ↔
      IsRegularLocalRing (Localization.AtPrime q)
Tag 0AP2, a lemma

Tag 0AP2 in the Stacks Project.

exists_ringEquiv_pi_isDedekindDomain_and_isDiscreteValuationRing_atPrime_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/PermanenceOfProperties.lean, line 277.

An étale algebra over a Dedekind domain is a finite product of Dedekind domains, and its localizations at maximal ideals with nonzero contraction to the base are discrete valuation rings.

public theorem exists_ringEquiv_pi_isDedekindDomain_and_isDiscreteValuationRing_atPrime_of_etale
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [Algebra.Etale A B]
    [IsDedekindDomain A] :
    (∃ (n : ℕ) (D : Fin n → Type v) (_ : ∀ i, CommRing (D i)),
      (∀ i, IsDedekindDomain (D i)) ∧ Nonempty (B ≃+* ∀ i, D i)) ∧
      ∀ q : MaximalSpectrum B, q.asIdeal.comap (algebraMap A B) ≠ ⊥ →
        ∃ _ : IsDomain (Localization.AtPrime q.asIdeal),
          IsDiscreteValuationRing (Localization.AtPrime q.asIdeal)
Sources
LeanRingHom.Etale.ringKrullDim_localization_atPrime_eq · isNoetherianRing_localization_iff_of_etale · isRegularLocalRing_localization_iff_of_etale · exists_ringEquiv_pi_isDedekindDomain_and_isDiscreteValuationRing_atPrime_of_etale · isNoetherianRing_localization_iff_of_flat_of_finiteType

Section15.46 Permanence of properties under henselization#

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

Tag 07QM, a lemma

Tag 07QM in the Stacks Project.

henselization_faithfullyFlat_and_quotient_basis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/PermanenceOfProperties/FlatnessAndReducedness.lean, line 322. The attribute's comment: “The identification _hRsh_res of ResidueField Rsh with κsep is carried, for faithfulness to the source statement, but is not needed by the proof: the basis comes from ind-étaleness of R → Rsh together with [IsSepClosed (ResidueField Rsh)]. Hence the leading underscore on that binder.”.

Stacks 07QM. Let Rh and Rsh be respectively a henselization and a strict henselization of a local ring R, with residue field of Rsh identified with a separable closure κsep of the residue field of R. Then R → Rh → Rsh is faithfully flat, the maximal ideals are generated by those below them, reduction modulo every power of the maximal ideal is unchanged by henselization, and the corresponding reduction of Rsh has a basis obtained by reducing one fixed family of elements of Rsh.

public theorem henselization_faithfullyFlat_and_quotient_basis.{u, v, w, t}
    {R : Type u} {Rh : Type w} {Rsh : Type t} {κsep : Type v}
    [CommRing R] [IsLocalRing R]
    [CommRing Rh] [Algebra R Rh] [HenselianLocalRing Rh]
    [IsLocalHom (algebraMap R Rh)]
    [CommRing Rsh] [Algebra R Rsh] [Algebra Rh Rsh]
    [IsScalarTower R Rh Rsh] [HenselianLocalRing Rsh]
    [IsLocalHom (algebraMap Rh Rsh)]
    [Field κsep] [Algebra (ResidueField R) κsep]
    [IsSepClosure (ResidueField R) κsep] [IsSepClosed (ResidueField Rsh)]
    (hRh_ind : (CommAlgCat.etale.{w} R).ind.{w} (CommAlgCat.of R Rh))
    (hRh_res : Function.Bijective (ResidueField.map (algebraMap R Rh)))
    (hRsh_ind : (CommAlgCat.etale.{t} R).ind.{t} (CommAlgCat.of R Rsh))
    (_hRsh_res : ∃ e : κsep ≃+* ResidueField Rsh, ∀ x : R,
      e (algebraMap (ResidueField R) κsep (residue R x)) =
        residue Rsh (algebraMap R Rsh x)) :
    Module.FaithfullyFlat R Rh ∧
      Module.FaithfullyFlat Rh Rsh ∧
      (maximalIdeal R).map (algebraMap R Rh) = maximalIdeal Rh ∧
      (maximalIdeal R).map (algebraMap R Rsh) = maximalIdeal Rsh ∧
      (maximalIdeal Rh).map (algebraMap Rh Rsh) = maximalIdeal Rsh ∧
      (∀ n : ℕ, Function.Bijective
        (Ideal.quotientMap ((maximalIdeal R ^ n).map (algebraMap R Rh))
          (algebraMap R Rh) Ideal.le_comap_map)) ∧
      ∃ (ι : Type t) (x : ι → Rsh), ∀ n : ℕ,
        letI : Algebra (R ⧸ maximalIdeal R ^ n)
            (Rsh ⧸ (maximalIdeal R ^ n).map (algebraMap R Rsh)) :=
          Ideal.Quotient.algebraQuotientOfLEComap Ideal.le_comap_map
        ∃ b : Module.Basis ι (R ⧸ maximalIdeal R ^ n)
            (Rsh ⧸ (maximalIdeal R ^ n).map (algebraMap R Rsh)),
          ∀ i, b i = Ideal.Quotient.mk _ (x i)
Tag 07QN, a lemma

Tag 07QN in the Stacks Project.

henselization_formallyEtale_and_isFormallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/PermanenceOfProperties/FlatnessAndReducedness.lean, line 503.

The maps from a local ring to its henselization, from its henselization to its strict henselization, and from the original ring to its strict henselization are formally étale. With the discrete topology on each source, they are formally smooth for the adic topology defined by the maximal ideal of the corresponding target.

public theorem henselization_formallyEtale_and_isFormallySmooth
    (R Rh Rsh : Type u)
    [CommRing R] [IsLocalRing R]
    [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
    [CommRing Rsh] [IsLocalRing Rsh] [Algebra R Rsh] [Algebra Rh Rsh]
    [IsScalarTower R Rh Rsh]
    (κsep : Type v)
    [Field κsep] [Algebra (ResidueField R) κsep]
    [IsSepClosure (ResidueField R) κsep]
    [IsHenselization R (ResidueField R) Rh]
    [IsHenselization R κsep Rsh]
    [IsLocalHom (algebraMap Rh Rsh)] :
    Algebra.FormallyEtale R Rh ∧
      Algebra.FormallyEtale Rh Rsh ∧
      Algebra.FormallyEtale R Rsh ∧
      (letI : TopologicalSpace R := ⊥
       letI : DiscreteTopology R := ⟨rfl⟩
       letI := (maximalIdeal Rh).adicTopology
       letI : IsTopologicalRing Rh := (maximalIdeal Rh).ringFilterBasis.isTopologicalRing
       letI : IsLinearTopology Rh Rh := (maximalIdeal Rh).isLinearTopology
       IsFormallySmooth (algebraMap R Rh)) ∧
      (letI : TopologicalSpace Rh := ⊥
       letI : DiscreteTopology Rh := ⟨rfl⟩
       letI := (maximalIdeal Rsh).adicTopology
       letI : IsTopologicalRing Rsh := (maximalIdeal Rsh).ringFilterBasis.isTopologicalRing
       letI : IsLinearTopology Rsh Rsh := (maximalIdeal Rsh).isLinearTopology
       IsFormallySmooth (algebraMap Rh Rsh)) ∧
      (letI : TopologicalSpace R := ⊥
       letI : DiscreteTopology R := ⟨rfl⟩
       letI := (maximalIdeal Rsh).adicTopology
       letI : IsTopologicalRing Rsh := (maximalIdeal Rsh).ringFilterBasis.isTopologicalRing
       letI : IsLinearTopology Rsh Rsh := (maximalIdeal Rsh).isLinearTopology
       IsFormallySmooth (algebraMap R Rsh))
Tag 06LJ, a lemma

Tag 06LJ in the Stacks Project.

isNoetherianRing_iff_henselizations_and_completion_properties, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/PermanenceOfProperties/NoetherianCompletions.lean, line 641. References: EGA IV (18.6.6), “(iv), (v)”; EGA IV (18.8.8), “(iv)”.

A local ring is Noetherian if and only if its henselization is, if and only if its strict henselization is. In that case the latter two rings have complete Noetherian local completions; completion does not change the henselization, both completion maps are flat, the map from the completed ring to the completed strict henselization is formally smooth, strict henselization commutes with base change to the completion, and completing once more gives the completed strict henselization.

public theorem isNoetherianRing_iff_henselizations_and_completion_properties.{u, v, w}
    (R Rh Rsh : Type u)
    [CommRing R] [IsLocalRing R]
    [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
    [CommRing Rsh] [IsLocalRing Rsh] [Algebra R Rsh]
    (κsep : Type v) [Field κsep] [Algebra (ResidueField R) κsep]
    [IsSepClosure (ResidueField R) κsep]
    [IsHenselization R (ResidueField R) Rh]
    [IsHenselization R κsep Rsh] :
    let Rhat := AdicCompletion (maximalIdeal R) R
    let Rhhat := AdicCompletion (maximalIdeal Rh) Rh
    let Rshhat := AdicCompletion (maximalIdeal Rsh) Rsh
    ((IsNoetherianRing R ↔ IsNoetherianRing Rh) ∧
      (IsNoetherianRing R ↔ IsNoetherianRing Rsh)) ∧
    (∀ [Algebra Rh Rsh] [IsScalarTower R Rh Rsh]
      [IsLocalHom (algebraMap Rh Rsh)], IsNoetherianRing R →
      ∃ (hRhatLocal : IsLocalRing Rhat)
        (hRhhatLocal : IsLocalRing Rhhat)
        (hRshhatLocal : IsLocalRing Rshhat),
      letI : IsLocalRing Rhat := hRhatLocal
      letI : IsLocalRing Rhhat := hRhhatLocal
      letI : IsLocalRing Rshhat := hRshhatLocal
      IsNoetherianRing Rhhat ∧ IsNoetherianRing Rshhat ∧
      IsAdicComplete (maximalIdeal Rhhat) Rhhat ∧
      IsAdicComplete (maximalIdeal Rshhat) Rshhat ∧
      ∃ e : Rhat ≃+* Rhhat,
        (∀ x : R, e (algebraMap R Rhat x) =
          algebraMap Rh Rhhat (algebraMap R Rh x)) ∧
        RingHom.Flat (algebraMap Rh Rhhat) ∧
        RingHom.Flat (algebraMap Rsh Rshhat) ∧
        (∃ f : Rhat →+* Rshhat,
          (∀ x : R, f (algebraMap R Rhat x) =
            algebraMap Rsh Rshhat (algebraMap R Rsh x)) ∧
          (letI : TopologicalSpace Rhat := (maximalIdeal Rhat).adicTopology
           letI : IsTopologicalRing Rhat :=
             (maximalIdeal Rhat).nonarchimedean.toIsTopologicalRing
           letI : IsLinearTopology Rhat Rhat := (maximalIdeal Rhat).isLinearTopology
           letI : TopologicalSpace Rshhat := (maximalIdeal Rshhat).adicTopology
           letI : IsTopologicalRing Rshhat :=
             (maximalIdeal Rshhat).nonarchimedean.toIsTopologicalRing
           letI : IsLinearTopology Rshhat Rshhat := (maximalIdeal Rshhat).isLinearTopology
           IsFormallySmooth.{w} f)) ∧
        (let algRhRhat : Algebra Rh Rhat :=
            (e.symm.toRingHom.comp (algebraMap Rh Rhhat)).toAlgebra
         letI : Algebra Rh Rhat := algRhRhat
         ∃ hRhatMapLocal : IsLocalHom (algebraMap R Rhat),
           letI : IsLocalHom (algebraMap R Rhat) := hRhatMapLocal
           ∃ algKhat : Algebra (ResidueField Rhat) κsep,
           letI : Algebra (ResidueField Rhat) κsep := algKhat
           (∀ x : ResidueField R,
             algebraMap (ResidueField Rhat) κsep
                 (ResidueField.map (algebraMap R Rhat) x) =
               algebraMap (ResidueField R) κsep x) ∧
           IsSepClosure (ResidueField Rhat) κsep ∧
           ∃ hTensorLocal : IsLocalRing (Rhat ⊗[Rh] Rsh),
           letI : IsLocalRing (Rhat ⊗[Rh] Rsh) := hTensorLocal
           IsHenselization Rhat κsep (Rhat ⊗[Rh] Rsh) ∧
           ∃ ef : AdicCompletion (maximalIdeal (Rhat ⊗[Rh] Rsh))
               (Rhat ⊗[Rh] Rsh) ≃+* Rshhat,
             ∀ x : Rsh,
               ef (algebraMap (Rhat ⊗[Rh] Rsh)
                   (AdicCompletion (maximalIdeal (Rhat ⊗[Rh] Rsh))
                     (Rhat ⊗[Rh] Rsh))
                   (Algebra.TensorProduct.includeRight x)) =
                 algebraMap Rsh Rshhat x))
Tag 06DH, a lemma

Tag 06DH in the Stacks Project.

isReduced_tfae_henselization_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/PermanenceOfProperties/FlatnessAndReducedness.lean, line 696. References: EGA IV (18.6.9), “(i), special case”; EGA IV (18.8.12), “(i), special case”.

Reducedness of a local ring, its henselization, and its strict henselization are equivalent.

public theorem isReduced_tfae_henselization_strictHenselization
    (R Rh Rsh : Type u) [CommRing R] [CommRing Rh] [CommRing Rsh]
    [IsLocalRing R] [IsLocalRing Rh] [IsLocalRing Rsh]
    [Algebra R Rh] [Algebra R Rsh]
    [IsLocalRing.IsHenselization R (IsLocalRing.ResidueField R) Rh]
    (κsep : Type v) [Field κsep] [Algebra (IsLocalRing.ResidueField R) κsep]
    [IsSepClosure (IsLocalRing.ResidueField R) κsep]
    [IsLocalRing.IsHenselization R κsep Rsh] :
    List.TFAE [IsReduced R, IsReduced Rh, IsReduced Rsh]
Tag 0ASE, a lemma

Tag 0ASE in the Stacks Project.

nilradical_map_eq_henselization_and_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/PermanenceOfProperties/FlatnessAndReducedness.lean, line 778.

The nilradical of a henselization or strict henselization of a local ring is the extension of the nilradical of the base ring.

public theorem nilradical_map_eq_henselization_and_strictHenselization
    (R Rh Rsh : Type u) [CommRing R] [CommRing Rh] [CommRing Rsh]
    [IsLocalRing R] [IsLocalRing Rh] [IsLocalRing Rsh]
    [Algebra R Rh] [Algebra R Rsh]
    [IsLocalRing.IsHenselization R (IsLocalRing.ResidueField R) Rh]
    (κsep : Type v) [Field κsep] [Algebra (IsLocalRing.ResidueField R) κsep]
    [IsSepClosure (IsLocalRing.ResidueField R) κsep]
    [IsLocalRing.IsHenselization R κsep Rsh] :
    Ideal.map (algebraMap R Rh) (nilradical R) = nilradical Rh ∧
      Ideal.map (algebraMap R Rsh) (nilradical R) = nilradical Rsh
Tag 06DI, a lemma

Tag 06DI in the Stacks Project.

isNormalDomain_tfae_henselization_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/PermanenceOfProperties/NormalityAndDimension.lean, line 239. References: EGA IV (18.6.9), “(i), special case”; EGA IV (18.8.12), “(i), special case”.

Normality of a local ring, its henselization, and its strict henselization are equivalent.

public theorem isNormalDomain_tfae_henselization_strictHenselization
    (R Rh Rsh : Type u) [CommRing R] [CommRing Rh] [CommRing Rsh]
    [IsLocalRing R] [IsLocalRing Rh] [IsLocalRing Rsh]
    [Algebra R Rh] [Algebra R Rsh]
    [IsLocalRing.IsHenselization R (IsLocalRing.ResidueField R) Rh]
    (κsep : Type v) [Field κsep] [Algebra (IsLocalRing.ResidueField R) κsep]
    [IsSepClosure (IsLocalRing.ResidueField R) κsep]
    [IsLocalRing.IsHenselization R κsep Rsh] :
    List.TFAE [IsDomain R ∧ IsIntegrallyClosed R,
      IsDomain Rh ∧ IsIntegrallyClosed Rh,
      IsDomain Rsh ∧ IsIntegrallyClosed Rsh]
Tag 06LK, a lemma

Tag 06LK in the Stacks Project.

ringKrullDim_eq_henselization_eq_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/PermanenceOfProperties/NormalityAndDimension.lean, line 351. References: SGA 5 I (3.1.3), “more general”.

A local ring, its henselization, and its strict henselization have equal Krull dimension.

public theorem ringKrullDim_eq_henselization_eq_strictHenselization
    (R Rh Rsh : Type u)
    [CommRing R] [IsLocalRing R]
    [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
    [CommRing Rsh] [IsLocalRing Rsh] [Algebra R Rsh]
    (κpsep : Type v) [Field κpsep] [Algebra (ResidueField R) κpsep]
    [IsSepClosure (ResidueField R) κpsep]
    [IsHenselization R (ResidueField R) Rh]
    [IsHenselization R κpsep Rsh] :
    ringKrullDim R = ringKrullDim Rh ∧ ringKrullDim Rh = ringKrullDim Rsh
Tag 06LL, a lemma

Tag 06LL in the Stacks Project.

ringDepth_eq_henselization_eq_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/PermanenceOfProperties/DepthRegularityAndFibres.lean, line 193.

A Noetherian local ring, its henselization, and its strict henselization have equal depth.

public theorem ringDepth_eq_henselization_eq_strictHenselization
    (R Rh Rsh : Type u)
    [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
    [CommRing Rsh] [IsLocalRing Rsh] [Algebra R Rsh]
    (κsep : Type v) [Field κsep] [Algebra (ResidueField R) κsep]
    [IsSepClosure (ResidueField R) κsep]
    [IsHenselization R (ResidueField R) Rh]
    [IsHenselization R κsep Rsh] :
    ringDepth R = ringDepth Rh ∧ ringDepth Rh = ringDepth Rsh
Tag 06LM, a lemma

Tag 06LM in the Stacks Project.

isMaximalCohenMacaulay_iff_henselizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/PermanenceOfProperties/DepthRegularityAndFibres.lean, line 231. References: EGA IV (18.6.10), “a)”; EGA IV (18.8.13), “a)”.

A Noetherian local ring is Cohen–Macaulay if and only if its henselization is, and if and only if its strict henselization is.

public theorem isMaximalCohenMacaulay_iff_henselizations
    (R Rh Rsh : Type u)
    [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
    [CommRing Rsh] [IsLocalRing Rsh] [Algebra R Rsh]
    (ksep : Type v) [Field ksep] [Algebra (ResidueField R) ksep]
    [IsSepClosure (ResidueField R) ksep]
    [IsHenselization R (ResidueField R) Rh]
    [IsHenselization R ksep Rsh] :
    (Module.IsMaximalCohenMacaulay R R ↔ Module.IsMaximalCohenMacaulay Rh Rh) ∧
      (Module.IsMaximalCohenMacaulay R R ↔ Module.IsMaximalCohenMacaulay Rsh Rsh)
Tag 06LN, a lemma

Tag 06LN in the Stacks Project.

isRegularLocalRing_iff_henselizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/PermanenceOfProperties/DepthRegularityAndFibres.lean, line 291. References: EGA IV (18.6.10); EGA IV (18.8.13).

A Noetherian local ring is regular if and only if its henselization is regular, and if and only if its strict henselization is regular.

public theorem isRegularLocalRing_iff_henselizations
    (R Rh Rsh : Type u)
    [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
    [CommRing Rsh] [IsLocalRing Rsh] [Algebra R Rsh]
    (κsep : Type v) [Field κsep] [Algebra (ResidueField R) κsep]
    [IsSepClosure (ResidueField R) κsep]
    [IsHenselization R (ResidueField R) Rh]
    [IsHenselization R κsep Rsh] :
    (IsRegularLocalRing R ↔ IsRegularLocalRing Rh) ∧
      (IsRegularLocalRing R ↔ IsRegularLocalRing Rsh)
Tag 0AP3, a lemma

Tag 0AP3 in the Stacks Project.

isDiscreteValuationRing_iff_henselizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/PermanenceOfProperties/DepthRegularityAndFibres.lean, line 375.

A Noetherian local ring is a discrete valuation ring if and only if its henselization is a discrete valuation ring, and if and only if its strict henselization is a discrete valuation ring.

public theorem isDiscreteValuationRing_iff_henselizations
    (R Rh Rsh : Type u)
    [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
    [CommRing Rsh] [IsLocalRing Rsh] [Algebra R Rsh]
    (κsep : Type v) [Field κsep] [Algebra (ResidueField R) κsep]
    [IsSepClosure (ResidueField R) κsep]
    [IsHenselization R (ResidueField R) Rh]
    [IsHenselization R κsep Rsh] :
    ((∃ _ : IsDomain R, IsDiscreteValuationRing R) ↔
      ∃ _ : IsDomain Rh, IsDiscreteValuationRing Rh) ∧
      ((∃ _ : IsDomain R, IsDiscreteValuationRing R) ↔
        ∃ _ : IsDomain Rsh, IsDiscreteValuationRing Rsh)
Tag 0AH1, a lemma

Tag 0AH1 in the Stacks Project.

IsFilteredColimitEtale.exists_fiber_algEquiv_pi_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/IndEtaleFibres.lean, line 532. References: EGA IV (18.6.9), “more general”; SGA 1 IX (1.8), “decomposition direction”; SGA 1 IX (1.9), “partial, special case”; SGA 4½ Arcata (2.4.2), “Only-if direction”.

Let A be a commutative ring and B an A-algebra which is a filtered colimit of étale A-algebras and which is a Noetherian ring. Let p be a prime of A. Then there are finitely many primes q : Fin r → Ideal B, all lying over p, such that:

  • the fiber B ⊗_A κ(p) is isomorphic, as a κ(p)-algebra, to the (finite) product ∏ᵢ κ(qᵢ) of the residue fields;
  • each extension κ(qᵢ)/κ(p) is separable algebraic;
  • the qᵢ are exactly the primes of B lying over p (q is injective and its range is the set of primes lying over p).

The κ(p)-algebra structure on each residue field κ(qᵢ) is the canonical one induced by Ideal.ResidueField.map from the structure map A → B.

theorem IsFilteredColimitEtale.exists_fiber_algEquiv_pi_residueField
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsNoetherianRing B]
    (hcolim : IsFilteredColimitEtale.{u, v, x, y} A B) (p : Ideal A) [p.IsPrime] :
    ∃ (r : ℕ) (q : Fin r → Ideal B) (hq : ∀ i, (q i).IsPrime)
      (hlo : ∀ i, (q i).LiesOver p),
      -- (1) product decomposition of the fiber algebra, and
      -- (2) separable algebraicity of each factor:
      (letI : ∀ i, (q i).IsPrime := hq
       letI : ∀ i, Algebra p.ResidueField (q i).ResidueField := fun i =>
         (Ideal.ResidueField.map p (q i) (algebraMap A B) (hlo i).over).toAlgebra
       Nonempty
         (TensorProduct A p.ResidueField B ≃ₐ[p.ResidueField]
           (∀ i, (q i).ResidueField)) ∧
       (∀ i, Algebra.IsSeparable p.ResidueField (q i).ResidueField) ∧
       (∀ i, Algebra.IsAlgebraic p.ResidueField (q i).ResidueField)) ∧
      -- the `qᵢ` are precisely the primes of `B` lying over `p`:
      Function.Injective q ∧
      (∀ q' : Ideal B, ∀ _ : q'.IsPrime, q'.LiesOver p ↔ ∃ i, q i = q')
Tag 07QQ, a lemma

Tag 07QQ in the Stacks Project.

henselization_fibres_equiv_pi_residueFields, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/PermanenceOfProperties/DepthRegularityAndFibres.lean, line 421. References: EGA IV (18.8.12), “(ii), special case”.

Let Rh and Rsh be respectively a henselization and a strict henselization of a Noetherian local ring R. Over every prime p of R, their fibres are finite products of the residue fields at exactly the primes lying over p, and all the corresponding residue-field extensions are separable algebraic.

public theorem henselization_fibres_equiv_pi_residueFields
    (R Rh Rsh : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
    [CommRing Rsh] [IsLocalRing Rsh] [Algebra R Rsh]
    [IsHenselization R (ResidueField R) Rh]
    (κsep : Type v) [Field κsep] [Algebra (ResidueField R) κsep]
    [IsSepClosure (ResidueField R) κsep]
    [IsHenselization R κsep Rsh]
    (p : Ideal R) [p.IsPrime] :
    (∃ (t : ℕ) (q : Fin t → Ideal Rh) (hq : ∀ i, (q i).IsPrime)
        (hlo : ∀ i, (q i).LiesOver p),
      (letI : ∀ i, (q i).IsPrime := hq
       letI : ∀ i, Algebra p.ResidueField (q i).ResidueField := fun i ↦
         (Ideal.ResidueField.map p (q i) (algebraMap R Rh) (hlo i).over).toAlgebra
       Nonempty
         (TensorProduct R p.ResidueField Rh ≃ₐ[p.ResidueField]
           (∀ i, (q i).ResidueField)) ∧
       (∀ i, Algebra.IsSeparable p.ResidueField (q i).ResidueField) ∧
       (∀ i, Algebra.IsAlgebraic p.ResidueField (q i).ResidueField)) ∧
      Function.Injective q ∧
      (∀ q' : Ideal Rh, ∀ _ : q'.IsPrime, q'.LiesOver p ↔ ∃ i, q i = q')) ∧
    (∃ (s : ℕ) (r : Fin s → Ideal Rsh) (hr : ∀ i, (r i).IsPrime)
        (hlo : ∀ i, (r i).LiesOver p),
      (letI : ∀ i, (r i).IsPrime := hr
       letI : ∀ i, Algebra p.ResidueField (r i).ResidueField := fun i ↦
         (Ideal.ResidueField.map p (r i) (algebraMap R Rsh) (hlo i).over).toAlgebra
       Nonempty
         (TensorProduct R p.ResidueField Rsh ≃ₐ[p.ResidueField]
           (∀ i, (r i).ResidueField)) ∧
       (∀ i, Algebra.IsSeparable p.ResidueField (r i).ResidueField) ∧
       (∀ i, Algebra.IsAlgebraic p.ResidueField (r i).ResidueField)) ∧
      Function.Injective r ∧
      (∀ r' : Ideal Rsh, ∀ _ : r'.IsPrime, r'.LiesOver p ↔ ∃ i, r i = r'))
Sources
Leanhenselization_faithfullyFlat_and_quotient_basis · henselization_formallyEtale_and_isFormallySmooth · isNoetherianRing_iff_henselizations_and_completion_properties · isReduced_tfae_henselization_strictHenselization · nilradical_map_eq_henselization_and_strictHenselization · isNormalDomain_tfae_henselization_strictHenselization · ringKrullDim_eq_henselization_eq_strictHenselization · ringDepth_eq_henselization_eq_strictHenselization

Section15.47 Field extensions, revisited#

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

Tag 07P1, a definition

Tag 07P1 in the Stacks Project.

Declarations registered for the tag:

Tag 07P2, a lemma

Tag 07P2 in the Stacks Project.

exists_pBasis_extending, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/PBasis.lean, line 1319. The attribute's comment: “extension to p-basis”. References: EGA 0 (21.4.2), “more general”.

Stacks 07P2 (extension to p-basis). Every p-independent family {x_i} over k extends to a p-basis: there is a subset S ⊆ K containing the range of x whose inclusion S → K is a p-basis of K over k.

theorem exists_pBasis_extending
    {I : Type*} (x : I → K) (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP K p]
    (hx : PIndependent k x p) :
    ∃ S : Set K, Set.range x ⊆ S ∧ PBasis k (Subtype.val : S → K) p

exists_pBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/PBasis.lean, line 1341. The attribute's comment: “existence of p-basis”. References: EGA 0 (21.4.2).

Stacks 07P2 (existence of p-basis). There is a subset of K that is a p-basis of K over k.

theorem exists_pBasis (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP K p] :
    ∃ S : Set K, PBasis k (Subtype.val : S → K) p

pIndependent_iff_linearIndependent_differentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/PBasis.lean, line 1368. The attribute's comment: “(1)<=>(2)”. References: EGA 0 (21.2.4), “partial”; EGA 0 (21.2.5), “partial”; EGA 0 (21.4.5); EGA 0 (21.4.6), “(b) ⇔ (c)”.

Stacks 07P2 ((1)<=>(2)). For a family x : I → K, the elements {x_i} are p-independent over k if and only if the differentials {d x_i} are K-linearly independent in Ω_{K/k}.

theorem pIndependent_iff_linearIndependent_differentials
    {I : Type*} (x : I → K) (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP K p] :
    PIndependent k x p ↔
      LinearIndependent K (fun i => (KaehlerDifferential.D k K) (x i))

pBasis_iff_basis_differentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/PBasis.lean, line 1402. The attribute's comment: “(a)<=>(b)”. References: EGA 0 (21.4.5), “p-base case”; EGA 0 (21.1.7), “a)⇒c), special case”; EGA 0 (21.2.4), “special case”; EGA 0 (21.2.5), “special case”; EGA 0 (21.4.4), “more general”.

Stacks 07P2 ((a)<=>(b)). For a family x : I → K, the elements {x_i} form a p-basis of K over k if and only if the differentials {d x_i} form a K-basis of Ω_{K/k}.

theorem pBasis_iff_basis_differentials
    {I : Type*} (x : I → K) (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP K p] :
    PBasis k x p ↔
      (LinearIndependent K (fun i => (KaehlerDifferential.D k K) (x i)) ∧
        ⊤ ≤ Submodule.span K
          (Set.range (fun i => (KaehlerDifferential.D k K) (x i))))
Tag 07P3, a lemma

Tag 07P3 in the Stacks Project.

intersection_subfields_07P3, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/DirectedSubfields.lean, line 171. References: EGA 0 (21.8.1).

Let K/k be a field extension and {K_α}_{α ∈ A} a nonempty directed family of intermediate fields with intersection k. Then for every n and every K-subspace V ⊆ K^{⊕n}, V meets k^{⊕n} nontrivially iff V meets every K_α^{⊕n} nontrivially.

Here: * hinf : ⨅ α, Kα α = ⊥ encodes the condition k = ⋂_α K_α (the intermediate field ⊥ is the copy of k in K); * hdir : ∀ α α', ∃ α'', Kα α'' ≤ Kα α ⊓ Kα α' encodes downward directedness of the family; * the condition k ⊆ K_α is automatic from Kα α : IntermediateField k K.

theorem intersection_subfields_07P3 {A : Type*} [Nonempty A]
    (Kα : A → IntermediateField k K)
    (hinf : ⨅ α, Kα α = ⊥)
    (hdir : ∀ α α', ∃ α'', Kα α'' ≤ Kα α ⊓ Kα α')
    (n : ℕ) (V : Submodule K (Fin n → K)) :
    NonzeroSubset ((V : Set (Fin n → K)) ∩ coordSubset n (⊥ : IntermediateField k K)) ↔
    ∀ α, NonzeroSubset ((V : Set (Fin n → K)) ∩ coordSubset n (Kα α))
Tag 07P4, a lemma

Tag 07P4 in the Stacks Project.

iInf_ker_kaehlerDifferentialMap_eq_bot_and_frobeniusFieldRange_eq_iInf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/PBasisDifferentials.lean, line 631. References: EGA 0 (21.8.5), “k₀=K^p, L/K finite”; EGA 0 (21.8.3), “a) => c), k₀=F_p”.

Let Kα be a downward-directed family of subfields of a field K of characteristic p, each containing the p-th powers, and suppose their intersection is exactly the subfield of p-th powers. Then the kernels of the canonical maps from Ω[K/(ZMod p)] to Ω[K/(Kα α)] have trivial intersection. Moreover, after any finite extension L / K, the intersection of the composita L^p Kα is L^p.

public theorem iInf_ker_kaehlerDifferentialMap_eq_bot_and_frobeniusFieldRange_eq_iInf
    {p : ℕ} [Fact p.Prime] {K : Type u} [Field K] [CharP K p] [Algebra (ZMod p) K]
    {A : Type v} (Kα : A → IntermediateField (ZMod p) K)
    (hpow : ∀ α, (frobenius K p).fieldRange ≤ (Kα α).toSubfield)
    (hiInf : (frobenius K p).fieldRange = ⨅ α, (Kα α).toSubfield)
    (hdir : ∀ α α', ∃ α'', Kα α'' ≤ Kα α ⊓ Kα α') :
    (⨅ α, LinearMap.ker (KaehlerDifferential.map (ZMod p) (Kα α) K K)) = ⊥ ∧
      ∀ (L : Type w) [Field L] [Algebra K L] [FiniteDimensional K L],
        letI : CharP L p :=
          charP_of_injective_algebraMap (algebraMap K L).injective p
        (frobenius L p).fieldRange =
          ⨅ α, (frobenius L p).fieldRange ⊔ (Kα α).toSubfield.map (algebraMap K L)
Tag 07P5, a lemma

Tag 07P5 in the Stacks Project.

fractionFields_powerSeries_polynomial_subrings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/PBasisDifferentials.lean, line 1230. References: EGA 0 (21.8.8), “∩K_J=K^p, A_J⊂A finite”.

Let x be a p-basis of a field k of characteristic p. Inside A = k[[X₁, ..., Xₙ]][Y₁, ..., Yₘ], let AJ be obtained by taking coefficients in the subfield generated by k^p and the x i for i ∉ J, and replacing every X and Y by its p-th power. The fraction fields of the AJ form a downward-directed family whose intersection is the p-th-power subfield and each AJ ⊆ A is finite.

public theorem fractionFields_powerSeries_polynomial_subrings
    {p : ℕ} [Fact p.Prime] {k : Type u} [Field k] [CharP k p]
    [Algebra (ZMod p) k] {I : Type v} (x : I → k)
    (hx : _root_.PBasis (ZMod p) x p) (n m : ℕ) :
    let kJ : Finset I → Subfield k := fun J =>
      (frobenius k p).fieldRange ⊔ Subfield.closure (x '' {i | i ∉ J})
    let A := MvPolynomial (Fin m) (MvPowerSeries (Fin n) k)
    letI : IsDomain A := NoZeroDivisors.to_isDomain A
    letI : CharP A p :=
      charP_of_injective_algebraMap (algebraMap k A).injective p
    let K := FractionRing A
    letI : CharP K p :=
      charP_of_injective_algebraMap (IsFractionRing.injective A K) p
    let toA : (J : Finset I) →
        MvPolynomial (Fin m) (MvPowerSeries (Fin n) ↥(kJ J)) →+* A := fun J =>
      MvPolynomial.eval₂Hom
        ((MvPolynomial.C : MvPowerSeries (Fin n) k →+* A).comp
          ((MvPowerSeries.expand p (Nat.Prime.ne_zero Fact.out)).toRingHom.comp
            (MvPowerSeries.map (kJ J).subtype)))
        (fun i => MvPolynomial.X i ^ p)
    let AJ : Finset I → Subring A := fun J => RingHom.range (toA J)
    let KJ : Finset I → IntermediateField (ZMod p) K := fun J =>
      IntermediateField.adjoin (ZMod p) ((algebraMap A K) '' (AJ J : Set A))
    (∀ J, (frobenius K p).fieldRange ≤ (KJ J).toSubfield) ∧
      (frobenius K p).fieldRange = ⨅ J, (KJ J).toSubfield ∧
      (∀ J J', ∃ J'', KJ J'' ≤ KJ J ⊓ KJ J') ∧
      ∀ J, Module.Finite (AJ J) A
Sources
Lean_root_.PIndependent · _root_.PBasis · exists_pBasis_extending · exists_pBasis · pIndependent_iff_linearIndependent_differentials · pBasis_iff_basis_differentials · intersection_subfields_07P3 · iInf_ker_kaehlerDifferentialMap_eq_bot_and_frobeniusFieldRange_eq_iInf

Section15.48 The singular locus#

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

Tag 07P7, a definition

Tag 07P7 in the Stacks Project.

IsJ0, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/SingularLocus.lean, line 172. The attribute's comment: “(1)”.

Stacks 07P7 (1). A commutative ring is J-0 if its regular locus contains a nonempty open subset.

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

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

Stacks 07P7 (2). A commutative ring is J-1 if its regular locus is open.

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

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

Stacks 07P7 (3). A commutative ring is J-2 if every finite type algebra over it is J-1.

public def IsJ2 (R : Type u) [CommRing R] : Prop
Tag 07P8, a lemma

Tag 07P8 in the Stacks Project.

isJ1_iff_zeroLocus_inter_regularLocus_contains_nonempty_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/SingularLocus.lean, line 205.

Stacks 07P8. A Noetherian ring is J-1 if and only if, for every point p of its regular locus, V(p) intersected with the regular locus contains a nonempty open subset of V(p).

public theorem isJ1_iff_zeroLocus_inter_regularLocus_contains_nonempty_open
    (R : Type u) [CommRing R] [IsNoetherianRing R] :
    IsJ1 R ↔
      ∀ p : PrimeSpectrum R,
        IsRegularLocalRing (Localization.AtPrime p.asIdeal) →
          ∃ U : Set (PrimeSpectrum R), IsOpen U ∧
            (U ∩ PrimeSpectrum.zeroLocus p.asIdeal).Nonempty ∧
            U ∩ PrimeSpectrum.zeroLocus p.asIdeal ⊆
              PrimeSpectrum.zeroLocus p.asIdeal ∩
                {x | IsRegularLocalRing (Localization.AtPrime x.asIdeal)}
Tag 07P9, a lemma

Tag 07P9 in the Stacks Project.

isJ1_of_forall_quotient_isJ0, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/SingularLocus.lean, line 516.

Stacks 07P9. A Noetherian ring is J-1 if its quotient by every prime ideal is J-0.

public theorem isJ1_of_forall_quotient_isJ0 (R : Type u) [CommRing R] [IsNoetherianRing R]
    (h : ∀ p : PrimeSpectrum R, IsJ0 (R ⧸ p.asIdeal)) :
    IsJ1 R
Tag 07PA, a lemma

Tag 07PA in the Stacks Project.

isJ0_of_injective_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/SingularLocus.lean, line 613.

If an injective finite type map sends a Noetherian domain into a J-0 domain, then the source is J-0.

public theorem isJ0_of_injective_finiteType
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S]
    [IsNoetherianRing R] [Algebra R S] [Algebra.FiniteType R S]
    (hinj : Function.Injective (algebraMap R S)) (hS : IsJ0 S) :
    IsJ0 R
Tag 07PB, a lemma

Tag 07PB in the Stacks Project.

isJ0_of_finiteType_injective_of_isSeparable_fractionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/SingularLocus.lean, line 731. References: EGA IV (6.12.4.1).

Stacks 07PB. Let R → S be an injective finite type map of domains. If R is Noetherian and J-0 and the induced extension of fraction fields is separable, then S is J-0.

public theorem isJ0_of_finiteType_injective_of_isSeparable_fractionRing
    (R S : Type*) [CommRing R] [IsNoetherianRing R] [IsDomain R]
    [CommRing S] [IsDomain S] [Algebra R S] [Algebra.FiniteType R S]
    (hR : IsJ0 R) (hRS : Function.Injective (algebraMap R S))
    (hsep :
      letI : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr hRS
      letI : Algebra (FractionRing R) (FractionRing S) :=
        FractionRing.liftAlgebra R (FractionRing S)
      Algebra.IsSeparableExtension (FractionRing R) (FractionRing S)) :
    IsJ0 S
Tag 07PC, a lemma

Tag 07PC in the Stacks Project.

isJ2_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Regular/SingularLocus.lean, line 1014. References: EGA IV (6.12.4).

Stacks 07PC. For a Noetherian ring R, the following are equivalent: R is J-2; every finite type domain algebra over R is J-0; every finite algebra over R is J-1; and every finite purely inseparable extension of a residue field of R is the fraction field of a finite J-0 domain algebra over R.

public theorem isJ2_tfae (R : Type u) [CommRing R] [IsNoetherianRing R] :
    List.TFAE
      [ IsJ2 R,
        ∀ (S : Type u) [CommRing S] [Algebra R S] [Algebra.FiniteType R S] [IsDomain S],
          IsJ0 S,
        ∀ (S : Type u) [CommRing S] [Algebra R S] [Module.Finite R S],
          IsJ1 S,
        ∀ (p : PrimeSpectrum R) (L : Type u) [Field L]
          [Algebra p.asIdeal.ResidueField L] [Module.Finite p.asIdeal.ResidueField L]
          [IsPurelyInseparable p.asIdeal.ResidueField L],
          letI : Algebra R L :=
            ((algebraMap p.asIdeal.ResidueField L).comp
              (algebraMap R p.asIdeal.ResidueField)).toAlgebra
          ∃ R' : Subalgebra R L,
            Module.Finite R R' ∧ IsJ0 R' ∧ IsFractionRing R' L ]
Sources
LeanIsJ0 · IsJ1 · IsJ2 · isJ1_iff_zeroLocus_inter_regularLocus_contains_nonempty_open · isJ1_of_forall_quotient_isJ0 · isJ0_of_injective_finiteType · isJ0_of_finiteType_injective_of_isSeparable_fractionRing · isJ2_tfae

Section15.49 Regularity and derivations#

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

Tag 07PE, a lemma

Tag 07PE in the Stacks Project.

Stacks.DerivationExtension.locDeriv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Derivation/Extension.lean, line 111. The attribute's comment: “(2): the extension itself”.

The derivation of the localization L extending D along R → L.

noncomputable def locDeriv : Derivation ℤ L L

Stacks.DerivationExtension.locDeriv_extendsAlong, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Derivation/Extension.lean, line 155. The attribute's comment: “(2): the extension property of locDeriv”.

locDeriv D S L extends D along the canonical map R → L.

lemma locDeriv_extendsAlong : ExtendsAlong (algebraMap R L) D (locDeriv D S L)

Stacks.DerivationExtension.locDeriv_unique, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Derivation/Extension.lean, line 160. The attribute's comment: “(2): uniqueness of locDeriv”.

locDeriv D S L is the only derivation of L extending D along R → L.

lemma locDeriv_unique (Dloc : Derivation ℤ L L)
    (hDloc : ExtendsAlong (algebraMap R L) D Dloc) : Dloc = locDeriv D S L

Stacks.DerivationExtension.exists_derivation_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Derivation/Extension.lean, line 232. The attribute's comment: “(1)”.

A derivation D on a ring R extends, along the canonical map R → AdicCompletion I R, to a derivation of the I-adic completion of R.

theorem exists_derivation_adicCompletion
    (R : Type*) [CommRing R] (D : Derivation ℤ R R) (I : Ideal R) :
    ∃ Dcompl : Derivation ℤ (AdicCompletion I R) (AdicCompletion I R),
      ExtendsAlong (algebraMap R (AdicCompletion I R)) D Dcompl

Stacks.DerivationExtension.exists_derivation_clear_denominators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Derivation/Extension.lean, line 361. The attribute's comment: “(3)”.

Let R' be a finite type R-algebra and let g ∈ R be an element whose image in R' is a nonzerodivisor, such that the induced map f : R_g → R'_g between the localizations at the powers of g is bijective. Then for some N : ℕ the derivation g ^ N • D extends, along R → R', to a derivation of R'.

theorem exists_derivation_clear_denominators
    {R R' : Type*} [CommRing R] [CommRing R'] [Algebra R R']
    [Algebra.FiniteType R R']
    (D : Derivation ℤ R R) (g : R)
    (Rg : Type*) [CommRing Rg] [Algebra R Rg]
    [IsLocalization (Submonoid.powers g) Rg]
    (R'g : Type*) [CommRing R'g] [Algebra R' R'g]
    [IsLocalization (Submonoid.powers ((algebraMap R R') g)) R'g]
    (f : Rg →+* R'g)
    (hf_comm : f.comp (algebraMap R Rg) = (algebraMap R' R'g).comp (algebraMap R R'))
    (hf_iso : Function.Bijective f)
    (hg_nzd : (algebraMap R R') g ∈ nonZeroDivisors R') :
    ∃ (N : ℕ) (Δ : Derivation ℤ R' R'),
      ExtendsAlong (algebraMap R R') (g ^ N • D) Δ
Tag 07PF, a lemma

Tag 07PF in the Stacks Project.

isRegularRing_quotient_span_singleton_of_isUnit_derivation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Derivation/Regularity.lean, line 248.

The Jacobian criterion for hypersurfaces: if some derivation sends f to a unit modulo (f), then the quotient of a regular ring by (f) is regular.

public theorem isRegularRing_quotient_span_singleton_of_isUnit_derivation
    {R : Type*} [CommRing R] [IsRegularRing R] (f : R) (D : Derivation ℤ R R)
    (hD : IsUnit (Ideal.Quotient.mk (Ideal.span {f}) (D f))) :
    IsRegularRing (R ⧸ Ideal.span {f})
Tag 0GEE, a lemma

Tag 0GEE in the Stacks Project.

isRegularLocalRing_quotient_span_range_and_isRegular_of_isUnit_det_derivation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Derivation/Regularity.lean, line 327.

A finite family in the maximal ideal of a regular local ring is a regular sequence and has regular local quotient if its values under a family of derivations form a matrix with unit determinant.

public theorem isRegularLocalRing_quotient_span_range_and_isRegular_of_isUnit_det_derivation
    {R : Type*} [CommRing R] [IsRegularLocalRing R] {m : ℕ} (f : Fin m → R)
    (hf : ∀ i, f i ∈ IsLocalRing.maximalIdeal R) (D : Fin m → Derivation ℤ R R)
    (hD : IsUnit (Matrix.det fun i j => D i (f j))) :
    IsRegularLocalRing (R ⧸ Ideal.span (Set.range f)) ∧
      RingTheory.Sequence.IsRegular R (List.ofFn f)
Tag 07PG, a lemma

Tag 07PG in the Stacks Project.

isRegularRing_quotient_polynomial_sub_C_of_isUnit_derivation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Derivation/Regularity.lean, line 407.

If a derivation of a regular ring sends f to a unit, then the quotient of the polynomial ring by p(X) - f is regular for every integer polynomial p. In particular, this applies to p = X ^ n for every positive integer n.

public theorem isRegularRing_quotient_polynomial_sub_C_of_isUnit_derivation
    {R : Type*} [CommRing R] [IsRegularRing R] (f : R) (D : Derivation ℤ R R)
    (hD : IsUnit (D f)) (p : Polynomial ℤ) :
    IsRegularRing
      (Polynomial R ⧸ Ideal.span
        {p.map (algebraMap ℤ R) - Polynomial.C f})
Tag 07PH, a lemma

Tag 07PH in the Stacks Project.

exists_derivation_apply_ne_zero_of_not_pow_fractionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Derivation/Regularity.lean, line 821.

If a domain B of prime characteristic is of finite type over a Noetherian complete local ring, then every element of B that is not a p-th power in its fraction field is detected by an ordinary derivation of B.

public theorem exists_derivation_apply_ne_zero_of_not_pow_fractionRing
    {p : ℕ} [Fact p.Prime] {R B K : Type*}
    [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    [CommRing B] [IsDomain B] [CharP B p] [Algebra R B] [Algebra.FiniteType R B]
    [Field K] [Algebra B K] [IsFractionRing B K]
    (f : B) (hf : ¬ ∃ x : K, algebraMap B K f = x ^ p) :
    ∃ D : Derivation ℤ B B, D f ≠ 0
Tag 07PI, a lemma

Tag 07PI in the Stacks Project.

isJ0_of_isPrecomplete_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Derivation/Regularity.lean, line 1155.

Stacks 07PI. A Noetherian local domain complete for its maximal-ideal-adic topology is J-0.

public theorem isJ0_of_isPrecomplete_maximalIdeal
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [IsDomain R]
    [IsPrecomplete (IsLocalRing.maximalIdeal R) R] : IsJ0 R
Tag 07PJ, a proposition

Tag 07PJ in the Stacks Project.

isJ2_of_standard_classes_and_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Derivation/Regularity.lean, line 1408. References: EGA 0 (22.7.6); EGA IV (6.12.6), “(i)”; SGA 5 I (3.1.1), “affine case”.

Stacks 07PJ. Fields, Noetherian complete local rings, the integers, one-dimensional Noetherian local rings, one-dimensional Nagata rings, and characteristic-zero Dedekind domains are J-2; moreover, every finite type algebra over a J-2 ring is J-2.

public theorem isJ2_of_standard_classes_and_finiteType :
    (∀ (K : Type u) [Field K], IsJ2 K) ∧
    (∀ (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
      [IsPrecomplete (IsLocalRing.maximalIdeal R) R], IsJ2 R) ∧
    IsJ2 ℤ ∧
    (∀ (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R],
      ringKrullDim R = 1 → IsJ2 R) ∧
    (∀ (R : Type u) [CommRing R],
      IsNagataRing R → ringKrullDim R = 1 → IsJ2 R) ∧
    (∀ (R : Type u) [CommRing R] [IsDedekindDomain R] [CharZero R],
      IsJ2 R) ∧
    (∀ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
      [Algebra.FiniteType R S], IsJ2 R → IsJ2 S)
Sources
LeanStacks.DerivationExtension.locDeriv · Stacks.DerivationExtension.locDeriv_extendsAlong · Stacks.DerivationExtension.locDeriv_unique · Stacks.DerivationExtension.exists_derivation_adicCompletion · Stacks.DerivationExtension.exists_derivation_clear_denominators · isRegularRing_quotient_span_singleton_of_isUnit_derivation · isRegularLocalRing_quotient_span_range_and_isRegular_of_isUnit_det_derivation · isRegularRing_quotient_polynomial_sub_C_of_isUnit_derivation

Section15.50 Formal smoothness and regularity#

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

Tag 07PL, a lemma

Tag 07PL in the Stacks Project.

exists_derivation_extension_of_formallySmoothNAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Regularity.lean, line 274.

A derivation of a Noetherian local ring extends across a local homomorphism to a complete Noetherian local ring that is formally smooth for its maximal-ideal-adic topology.

public theorem exists_derivation_extension_of_formallySmoothNAdic.{u, v}
    {A : Type u} {B : Type v}
    [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    [CommRing B] [IsNoetherianRing B] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    [IsAdicComplete (IsLocalRing.maximalIdeal B) B]
    (hfs : RingHom.FormallySmoothNAdic.{max u v, u, v} f (IsLocalRing.maximalIdeal B))
    (D : Derivation ℤ A A) :
    ∃ D' : Derivation ℤ B B, ∀ a : A, D' (f a) = f (D a)
Tag 07PM, a proposition

Tag 07PM in the Stacks Project.

isRegularRingHom_flat_geometricallyRegular_specialFiber_formallySmooth_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Regularity.lean, line 1018. References: EGA 0 (19.7.1), “complete case”; EGA 0 (19.0.2), “I, complete case”; EGA IV (7.5.4), “(i)”; EGA IV (7.5.3), “(iv), special case”; SGA 1 III (1.7), “Noetherian complete case”; SGA 1 III (1.3), “special case”.

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

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

Tag 0H7U in the Stacks Project.

isRegularRingHom_flat_geometricallyRegular_specialFiber_formallySmooth_tfae_0h7u, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Regularity.lean, line 1271. References: EGA 0 (19.0.2), “I, A→A^∧ regular”; EGA 0 (19.7.1), “A → A^ regular”; EGA IV (7.5.4), “(i)”; EGA IV (7.5.3), “(iv), special case”; SGA 1 III (1.3), “special case”.

Let f : A → B be a local homomorphism of Noetherian local rings and assume that the canonical map from A to its maximal-ideal-adic completion is regular. Let k be the residue field of A and let B̄ = k ⊗[A] B be the special fibre. The following are equivalent:

  1. f is regular;
  2. f is flat and B̄ is geometrically regular over k;
  3. f is flat and k → B̄ is formally smooth for the maximal-ideal-adic topology;
  4. f is formally smooth for the maximal-ideal-adic topology on B.
public theorem isRegularRingHom_flat_geometricallyRegular_specialFiber_formallySmooth_tfae_0h7u
    {A : Type u} {B : Type v}
    [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    [CommRing B] [IsNoetherianRing B] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hA : letI : WithIdeal A := ⟨maximalIdeal A⟩
      IsRegularRingHom
        (Completion.coeRingHom : A →+* Completion A)) :
    letI : Algebra A B := f.toAlgebra
    let k := ResidueField A
    let Bbar := k ⊗[A] B
    List.TFAE [
      IsRegularRingHom f,
      Module.Flat A B ∧ Algebra.IsGeometricallyRegular k Bbar,
      Module.Flat A B ∧
        RingHom.FormallySmoothNAdic.{max u v}
          (algebraMap k Bbar) (maximalIdeal Bbar),
      RingHom.FormallySmoothNAdic.{max u v} f (maximalIdeal B)]
Sources
Leanexists_derivation_extension_of_formallySmoothNAdic · isRegularRingHom_flat_geometricallyRegular_specialFiber_formallySmooth_tfae · isRegularRingHom_flat_geometricallyRegular_specialFiber_formallySmooth_tfae_0h7u

Section15.51 G-rings#

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

Tag 07GH, a definition

Tag 07GH in the Stacks Project.

IsGRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/Defs.lean, line 37.

A commutative ring is a G-ring if it is Noetherian and, for every prime ideal p, the canonical map from its local ring at p to the completion of that local ring is regular.

public def IsGRing (R : Type u) [CommRing R] : Prop
Tag 07PN, a lemma

Tag 07PN in the Stacks Project.

isGRing_iff_quotientCompletion_isGeometricallyRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/Criteria.lean, line 135.

A Noetherian ring is a G-ring if and only if every completed localization of a prime quotient, after base change to the residue field of the smaller prime, is geometrically regular.

public theorem isGRing_iff_quotientCompletion_isGeometricallyRegular
    {R : Type u} [CommRing R] [IsNoetherianRing R] :
    IsGRing R ↔
      ∀ (p q : PrimeSpectrum R) (_hqp : q.asIdeal ≤ p.asIdeal),
        let Q := R ⧸ q.asIdeal
        let S := Localization
          (Submonoid.map (Ideal.Quotient.mk q.asIdeal) p.asIdeal.primeCompl)
        @Algebra.IsGeometricallyRegular q.asIdeal.ResidueField
          (AdicCompletion
              ((p.asIdeal.map (Ideal.Quotient.mk q.asIdeal)).map (algebraMap Q S)) S ⊗[Q]
            q.asIdeal.ResidueField)
          inferInstance inferInstance Algebra.TensorProduct.rightAlgebra
Tag 07PP, a lemma

Tag 07PP in the Stacks Project.

quasiFinite_preserves_geometricallyRegular_formalFibers_and_isGRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/Criteria.lean, line 268.

Let R → S be a finite-type map of Noetherian rings and let q' ⊆ p' be primes of S at which the map is quasi-finite at p'. Geometric regularity ascends from the corresponding formal fibre over R to that over S; it therefore ascends for every formal fibre of the local rings at the two primes. If the map is quasi-finite everywhere, it also carries the G-ring property from R to S.

public theorem quasiFinite_preserves_geometricallyRegular_formalFibers_and_isGRing
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [IsNoetherianRing R] [IsNoetherianRing S] [Algebra.FiniteType R S]
    (q' p' : Ideal S) [q'.IsPrime] [p'.IsPrime] (hq'p' : q' ≤ p')
    [Algebra.QuasiFiniteAt R p'] :
    ((let T := AdicCompletion (maximalIdeal (Localization.AtPrime (Ideal.under R p')))
          (Localization.AtPrime (Ideal.under R p')) ⊗[R] (Ideal.under R q').ResidueField
      letI : Algebra (Ideal.under R q').ResidueField T :=
        (Algebra.TensorProduct.includeRight (R := R)).toRingHom.toAlgebra
      Algebra.IsGeometricallyRegular (Ideal.under R q').ResidueField T) →
      (let T := AdicCompletion (maximalIdeal (Localization.AtPrime p'))
          (Localization.AtPrime p') ⊗[S] q'.ResidueField
      letI : Algebra q'.ResidueField T :=
        (Algebra.TensorProduct.includeRight (R := S)).toRingHom.toAlgebra
      Algebra.IsGeometricallyRegular q'.ResidueField T)) ∧
    ((∀ q : PrimeSpectrum (Localization.AtPrime (Ideal.under R p')),
        let T := AdicCompletion (maximalIdeal (Localization.AtPrime (Ideal.under R p')))
            (Localization.AtPrime (Ideal.under R p')) ⊗[Localization.AtPrime (Ideal.under R p')]
          q.asIdeal.ResidueField
        letI : Algebra q.asIdeal.ResidueField T :=
          (Algebra.TensorProduct.includeRight : q.asIdeal.ResidueField →ₐ[
            Localization.AtPrime (Ideal.under R p')] T).toRingHom.toAlgebra
        Algebra.IsGeometricallyRegular q.asIdeal.ResidueField T) →
      ∀ q : PrimeSpectrum (Localization.AtPrime p'),
        let T := AdicCompletion (maximalIdeal (Localization.AtPrime p'))
            (Localization.AtPrime p') ⊗[Localization.AtPrime p'] q.asIdeal.ResidueField
        letI : Algebra q.asIdeal.ResidueField T :=
          (Algebra.TensorProduct.includeRight :
            q.asIdeal.ResidueField →ₐ[Localization.AtPrime p'] T).toRingHom.toAlgebra
        Algebra.IsGeometricallyRegular q.asIdeal.ResidueField T) ∧
    (Algebra.QuasiFinite R S → IsGRing R → IsGRing S)
Tag 07PQ, a lemma

Tag 07PQ in the Stacks Project.

isGRing_iff_finiteFree_formalFibers_isRegularRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/Criteria.lean, line 566.

A Noetherian ring is a G-ring if and only if every formal fibre of every finite free algebra over it is a regular ring.

public theorem isGRing_iff_finiteFree_formalFibers_isRegularRing (R : Type u) [CommRing R]
    [IsNoetherianRing R] :
    IsGRing R ↔
      ∀ (S : Type (max u v)) [CommRing S] [Algebra R S] [Module.Finite R S]
          [Module.Free R S],
        ∀ (q p : Ideal S) [q.IsPrime] [p.IsPrime], q ≤ p →
          IsRegularRing
            (AdicCompletion (maximalIdeal (Localization.AtPrime p))
                (Localization.AtPrime p) ⊗[S] q.ResidueField)
Tag 07PR, a lemma

Tag 07PR in the Stacks Project.

isGeometricallyRegular_formalFiber_mvPolynomial_mvPowerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/Criteria.lean, line 1101. References: EGA 0 (22.3.4), “special case”.

If A is a polynomial ring in m variables over the formal power-series ring in n variables over a field k of prime characteristic, then the generic formal fibre of the completion of A at any prime ideal is geometrically regular over the fraction field of A.

public theorem
    isGeometricallyRegular_formalFiber_mvPolynomial_mvPowerSeries
    {p m n : ℕ} [Fact p.Prime] (k : Type u) (A : Type v) (K : Type w) [Field k] [CharP k p]
    [CommRing A] [Algebra k A]
    (_ : A ≃ₐ[k] MvPolynomial (Fin m) (MvPowerSeries (Fin n) k))
    [Field K] [Algebra A K] [IsFractionRing A K]
    (q : Ideal A) [q.IsPrime] :
    let T := AdicCompletion (maximalIdeal (Localization.AtPrime q))
        (Localization.AtPrime q) ⊗[A] K
    letI : Algebra K T :=
      (Algebra.TensorProduct.includeRight : K →ₐ[A] T).toRingHom.toAlgebra
    Algebra.IsGeometricallyRegular K T
Tag 07PS, a proposition

Tag 07PS in the Stacks Project.

isGRing_of_isPrecomplete_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/Criteria.lean, line 1375.

A Noetherian local ring complete for its maximal-ideal-adic topology is a G-ring.

public theorem isGRing_of_isPrecomplete_maximalIdeal
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    [IsPrecomplete (maximalIdeal R) R] : IsGRing R
Tag 07PT, a lemma

Tag 07PT in the Stacks Project.

isGRing_iff_isRegularRingHom_adicCompletion_at_maximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/Henselization.lean, line 181.

A Noetherian ring is a G-ring if and only if the completion map of its localization at every maximal ideal is regular.

public theorem isGRing_iff_isRegularRingHom_adicCompletion_at_maximal
    (R : Type u) [CommRing R] [IsNoetherianRing R] :
    IsGRing R ↔
      ∀ (m : Ideal R) [m.IsMaximal],
        IsRegularRingHom
          (algebraMap (Localization.AtPrime m)
            (AdicCompletion (IsLocalRing.maximalIdeal (Localization.AtPrime m))
              (Localization.AtPrime m)))
Tag 07QR, a lemma

Tag 07QR in the Stacks Project.

isGRing_henselization_and_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/Henselization.lean, line 843.

The henselization and strict henselization of a local G-ring are G-rings.

public theorem isGRing_henselization_and_strictHenselization
    (R : Type u) (Rh : Type w) (Rsh : Type x)
    [CommRing R] [IsLocalRing R]
    [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
    [CommRing Rsh] [IsLocalRing Rsh] [Algebra R Rsh]
    (κsep : Type v) [Field κsep] [Algebra (ResidueField R) κsep]
    [IsSepClosure (ResidueField R) κsep]
    [IsHenselization R (ResidueField R) Rh]
    [IsHenselization R κsep Rsh]
    (hR : IsGRing R) :
    IsGRing Rh ∧ IsGRing Rsh
Tag 07PU, a lemma

Tag 07PU in the Stacks Project.

isGeometricallyRegular_formalFiber_polynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/EssFiniteType.lean, line 390.

The formal fibre at a nonzero prime r contained in a maximal ideal q of A[X], where q lies over the maximal ideal of the Noetherian complete local domain A and r lies over zero, is geometrically regular over κ(r) when the fraction field of A has prime characteristic.

public theorem isGeometricallyRegular_formalFiber_polynomial
    (p : ℕ) (_hp : p.Prime)
    (A : Type u) [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsLocalRing A]
    [IsPrecomplete (maximalIdeal A) A] [CharP (FractionRing A) p]
    (q r : Ideal (Polynomial A)) [q.IsMaximal] [r.IsPrime]
    (hq : q.comap Polynomial.C = maximalIdeal A)
    (_hr0 : r ≠ ⊥) (_hrq : r ≤ q) (hrA : r.comap Polynomial.C = ⊥) :
    Algebra.IsGeometricallyRegular r.ResidueField
      (r.ResidueField ⊗[Polynomial A]
        AdicCompletion (maximalIdeal (Localization.AtPrime q))
          (Localization.AtPrime q))
Tag 07PV, a proposition

Tag 07PV in the Stacks Project.

isGRing_of_essFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/EssFiniteType.lean, line 657.

An algebra essentially of finite type over a G-ring is a G-ring.

public theorem isGRing_of_essFiniteType
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.EssFiniteType R S] (hR : IsGRing R) :
    IsGRing S
Tag 07PX, a proposition

Tag 07PX in the Stacks Project.

isGRing_basic_examples, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/EssFiniteType.lean, line 763. References: SGA 3 VIB (10.10), “more general”.

Fields, Noetherian complete local rings, the integers, and Dedekind domains whose fraction fields have characteristic zero are G-rings. Moreover, a finite-type algebra over any G-ring is a G-ring.

public theorem isGRing_basic_examples :
    (∀ (K : Type u) [Field K], IsGRing K) ∧
      (∀ (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
        [IsPrecomplete (IsLocalRing.maximalIdeal R) R], IsGRing R) ∧
      IsGRing ℤ ∧
      (∀ (R : Type u) [CommRing R] [IsDedekindDomain R] [CharZero (FractionRing R)],
        IsGRing R) ∧
      (∀ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
        [Algebra.FiniteType R S], IsGRing R → IsGRing S)
Tag 0A41, a lemma

Tag 0A41 in the Stacks Project.

exists_filteredColimit_henselianLocalGRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/EssFiniteType.lean, line 1077. References: EGA IV (18.6.14), “(iii)”.

A henselian local ring is a filtered colimit of henselian local G-rings with local transition maps.

public theorem exists_filteredColimit_henselianLocalGRing
    (A : Type u) [CommRing A] [HenselianLocalRing A] :
    ∃ (J : Type u) (_ : SmallCategory J) (_ : IsFiltered J)
      (F : J ⥤ CommRingCat.{u}) (c : Cocone F) (_ : IsColimit c),
      (∀ j, HenselianLocalRing (F.obj j) ∧ IsGRing (F.obj j)) ∧
        (∀ ⦃i j⦄ (f : i ⟶ j), IsLocalHom (F.map f).hom) ∧
        Nonempty (c.pt ≅ CommRingCat.of A)
Tag 0AH2, a lemma

Tag 0AH2 in the Stacks Project.

isRegularRingHom_algebraMap_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/Henselization.lean, line 214.

The canonical map from a G-ring to its completion with respect to any ideal is regular.

public theorem isRegularRingHom_algebraMap_adicCompletion
    {A : Type u} [CommRing A] (hA : IsGRing A) (I : Ideal A) :
    IsRegularRingHom (algebraMap A (AdicCompletion I A))
Tag 0AH3, a lemma

Tag 0AH3 in the Stacks Project.

isGRing_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GRing/Henselization.lean, line 574.

The henselization of a G-ring along an ideal is a G-ring.

public theorem isGRing_henselization
    {A : Type u} [CommRing A] (hA : IsGRing A) (I : Ideal A)
    (Ah : Type v) [CommRing Ah] [Algebra A Ah]
    (hh : HenselianPair Ah (I.map (algebraMap A Ah)))
    (hι : ∀ (B : Type (max u v)) (_ : CommRing B) (J : Ideal B),
      HenselianPair B J →
        ∀ f : A →+* B, I ≤ J.comap f →
          ∃! g : Ah →+* B,
            g.comp (algebraMap A Ah) = f ∧ I.map (algebraMap A Ah) ≤ J.comap g) :
    IsGRing Ah
Sources
LeanIsGRing · isGRing_iff_quotientCompletion_isGeometricallyRegular · quasiFinite_preserves_geometricallyRegular_formalFibers_and_isGRing · isGRing_iff_finiteFree_formalFibers_isRegularRing · isGeometricallyRegular_formalFiber_mvPolynomial_mvPowerSeries · isGRing_of_isPrecomplete_maximalIdeal · isGRing_iff_isRegularRingHom_adicCompletion_at_maximal · isGRing_henselization_and_strictHenselization

Section15.52 Properties of formal fibres#

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

Tag 0BIS, a lemma

Tag 0BIS in the Stacks Project.

propertyRing_iff_quotientCompletion_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/RingMapProperty/QuotientCompletion.lean, line 483.

Stacks 0BIS. A Noetherian ring has property P on all the formal fibres of its localizations at prime ideals if and only if the corresponding completed localizations of its prime quotients have property P after extension to the residue field.

public theorem propertyRing_iff_quotientCompletion_fibers
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    (P : RingMapProperty.{u, u}) :
    IsPRing P R ↔
    (∀ (p q : PrimeSpectrum R) (_hqp : q.asIdeal ≤ p.asIdeal),
      let Q := R ⧸ q.asIdeal
      let S := Localization
        (Submonoid.map (Ideal.Quotient.mk q.asIdeal) p.asIdeal.primeCompl)
      P (Algebra.TensorProduct.includeRight (R := Q)
        (A := AdicCompletion
          ((p.asIdeal.map (Ideal.Quotient.mk q.asIdeal)).map (algebraMap Q S)) S)
        (B := q.asIdeal.ResidueField)).toRingHom)
Tag 0BK8, a lemma

Tag 0BK8 in the Stacks Project.

fibersHaveProperty_iff_localizations_at_primes_and_maximals, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/RingMapProperty/FibreLocalization.lean, line 622.

A fibre property which is local for localization may be checked on all maps of localizations at primes lying over one another, or only on those obtained from maximal ideals of the target.

public theorem fibersHaveProperty_iff_localizations_at_primes_and_maximals
    (P : ∀ {k : Type u} {S : Type (max u v)} [Field k] [CommRing S], (k →+* S) → Prop)
    (hPiso : RespectsIsomorphisms P)
    (hP : IsLocalForLocalization P)
    (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
    [IsNoetherianRing B] :
    (FibersHaveProperty P A B ↔
      ∀ (q : Ideal B) [q.IsPrime],
        letI : Algebra (Localization.AtPrime (q.under A)) (Localization.AtPrime q) :=
          Localization.AtPrime.algebraOfLiesOver (q.under A) q
        FibersHaveProperty P (Localization.AtPrime (q.under A)) (Localization.AtPrime q)) ∧
    ((∀ (q : Ideal B) [q.IsPrime],
        letI : Algebra (Localization.AtPrime (q.under A)) (Localization.AtPrime q) :=
          Localization.AtPrime.algebraOfLiesOver (q.under A) q
        FibersHaveProperty P (Localization.AtPrime (q.under A)) (Localization.AtPrime q)) ↔
      ∀ (m : Ideal B) [m.IsMaximal],
        letI : Algebra (Localization.AtPrime (m.under A)) (Localization.AtPrime m) :=
          Localization.AtPrime.algebraOfLiesOver (m.under A) m
        FibersHaveProperty P (Localization.AtPrime (m.under A)) (Localization.AtPrime m))
Tag 0BIT, a lemma

Tag 0BIT in the Stacks Project.

quasiFinite_preserves_formalFiberProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/RingMapProperty/QuasiFiniteFormalFibres.lean, line 615.

Stacks 0BIT. Let R → S be a finite-type map of Noetherian rings and let q' ⊆ p' be primes of S. If the map is quasi-finite at p', then a property of field-to-Noetherian-ring maps satisfying base change along finitely generated field extensions and detection on localizations passes from the relevant formal fiber over R to that over S. Consequently it passes between the formal fibers of the two local rings, and a quasi-finite R-algebra over a P-ring is a P-ring.

public theorem quasiFinite_preserves_formalFiberProperty
    (P : RingMapProperty.{max u v w, max u v w x})
    (hbaseChange : ∀ (k K : Type (max u v w)) (A : Type (max u v w x))
      [Field k] [Field K] [CommRing A]
      [Algebra k K] [Algebra k A] [IsNoetherianRing A] [Algebra.EssFiniteType k K]
      [IsNoetherianRing (A ⊗[k] K)],
      P (algebraMap k A) →
        P (Algebra.TensorProduct.includeRight (R := k) (A := A) (B := K)).toRingHom)
    (hlocal : ∀ (k : Type (max u v w)) (A : Type (max u v w x))
      [Field k] [CommRing A] [Algebra k A]
      [IsNoetherianRing A],
      (∀ q : PrimeSpectrum A,
        P (algebraMap k (Localization.AtPrime q.asIdeal))) ↔ P (algebraMap k A))
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [IsNoetherianRing R] [IsNoetherianRing S] [Algebra.FiniteType R S]
    (q' p' : Ideal S) [q'.IsPrime] [p'.IsPrime] (_hq'p' : q' ≤ p')
    [Algebra.QuasiFiniteAt R p'] :
    (P.Holds.{u, u, max v w, x} (Algebra.TensorProduct.includeRight (R := R)
        (A := AdicCompletion (maximalIdeal (Localization.AtPrime (Ideal.under R p')))
          (Localization.AtPrime (Ideal.under R p')))
        (B := (Ideal.under R q').ResidueField)).toRingHom →
      P.Holds.{v, v, max u w, x} (Algebra.TensorProduct.includeRight (R := S)
        (A := AdicCompletion (maximalIdeal (Localization.AtPrime p'))
          (Localization.AtPrime p')) (B := q'.ResidueField)).toRingHom) ∧
    (FormalFibersHaveAt.{u, max v w, x} P
        (Localization.AtPrime (Ideal.under R p')) →
      FormalFibersHaveAt.{v, max u w, x} P (Localization.AtPrime p')) ∧
    (Algebra.QuasiFinite R S → IsPRingAt.{u, max v w, x} P R →
      IsPRingAt.{v, max u w, x} P S)
Tag 0BIU, a lemma

Tag 0BIU in the Stacks Project.

isPRing_iff_formalFibersHave_localization_maximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/Localization.lean, line 308.

For a property of ring maps satisfying ascent through regular maps and faithfully flat descent, a Noetherian ring is a P-ring exactly when the formal fibres of its localizations at maximal ideals have P.

public theorem isPRing_iff_formalFibersHave_localization_maximal
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    (P : RingMapProperty.{max u v, max u v w})
    (hC : ∀ (A B C : Type (max u v))
      [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.Flat B C],
      (∀ p : PrimeSpectrum A,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))) →
      (∀ q : PrimeSpectrum B,
        Algebra.IsGeometricallyRegular q.asIdeal.ResidueField (q.asIdeal.Fiber C)) →
      ∀ p : PrimeSpectrum A,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C)))
    (hD : ∀ (A B C : Type (max u v))
      [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.FaithfullyFlat B C],
      (∀ p : PrimeSpectrum A,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C))) →
      ∀ p : PrimeSpectrum A,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))) :
    IsPRingAt.{u, v, w} P R ↔
      ∀ (m : Ideal R) [m.IsMaximal],
        FormalFibersHaveAt.{u, v, w} P
          (Localization.AtPrime m)
Tag 0BIV, a proposition

Tag 0BIV in the Stacks Project.

isPRing_of_essFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/EssFiniteType.lean, line 249. References: EGA IV (7.4.3), “(ii)”; EGA IV (7.6.5).

Stacks 0BIV. If a property of maps from fields to Noetherian rings satisfies properties (A)--(D), then an essentially finite-type algebra over a P-ring is a P-ring.

public theorem isPRing_of_essFiniteType
    (P : RingMapProperty.{max u v, max u v})
    (hA : ∀ (k K A : Type (max u v)) [Field k] [Field K] [CommRing A]
      [Algebra k K] [Algebra k A] [IsNoetherianRing A] [Algebra.EssFiniteType k K]
      [IsNoetherianRing (A ⊗[k] K)],
      P (algebraMap k A) →
        P (Algebra.TensorProduct.includeRight (R := k) (A := A) (B := K)).toRingHom)
    (_hB : ∀ (k A : Type (max u v)) [Field k] [CommRing A] [Algebra k A]
      [IsNoetherianRing A],
      (∀ q : PrimeSpectrum A, P (algebraMap k (Localization.AtPrime q.asIdeal))) ↔
        P (algebraMap k A))
    (hC : ∀ (A B C : Type (max u v))
      [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.Flat B C],
      (∀ p : PrimeSpectrum A,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))) →
      (∀ q : PrimeSpectrum B,
        Algebra.IsGeometricallyRegular q.asIdeal.ResidueField (q.asIdeal.Fiber C)) →
      ∀ p : PrimeSpectrum A,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C)))
    (hD : ∀ (A B C : Type (max u v))
      [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.FaithfullyFlat B C],
      (∀ p : PrimeSpectrum A,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C))) →
      ∀ p : PrimeSpectrum A,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B)))
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.EssFiniteType R S]
    (hR : IsPRingAt.{u, v, v} P R) :
    IsPRingAt.{v, u, u} P S
Tag 0BK9, a lemma

Tag 0BK9 in the Stacks Project.

fibersHaveProperty_adicCompletion_of_isPRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/Localization.lean, line 566. References: EGA IV (7.4.6).

If A is a P-ring, P is local for localization, and P descends along faithfully flat maps in flat towers of Noetherian rings, then all fibres of the map from A to its completion along any ideal have property P.

public theorem fibersHaveProperty_adicCompletion_of_isPRing
    (P : RingMapProperty.{u, u})
    (hlocal : IsLocalForLocalization (fun f => P f))
    (hdescent : ∀ {R S T : Type u} [CommRing R] [CommRing S] [CommRing T]
      [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T]
      [IsNoetherianRing R] [IsNoetherianRing S] [IsNoetherianRing T]
      [Module.Flat R S] [Module.FaithfullyFlat S T],
      FibersHaveProperty (fun f => P f) R T →
        FibersHaveProperty (fun f => P f) R S)
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    (hA : IsPRing P A) (I : Ideal A) :
    FibersHaveProperty (fun f => P f) A (AdicCompletion I A)
Tag 0BKA, a lemma

Tag 0BKA in the Stacks Project.

isPRing_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/Henselization.lean, line 558. References: EGA IV (18.7.2), “Forward implication”.

A henselization of a pair over a P-ring is again a P-ring when P is local on the target, ascends along regular maps, descends along faithfully flat maps, and is preserved by separable algebraic extensions of the ground field.

public theorem isPRing_henselization :
    ∀ (P : RingMapProperty.{max u v, max u v}),
    (∀ (k R : Type (max u v)) [Field k] [CommRing R] [Algebra k R]
      [IsNoetherianRing R],
      (∀ q : PrimeSpectrum R, P (algebraMap k (Localization.AtPrime q.asIdeal))) ↔
        P (algebraMap k R)) →
    (∀ (R S T : Type (max u v))
      [CommRing R] [CommRing S] [CommRing T]
      [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T]
      [IsNoetherianRing R] [IsNoetherianRing S] [IsNoetherianRing T]
      [Module.Flat R S] [Module.Flat S T],
      (∀ p : PrimeSpectrum R,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))) →
      (∀ q : PrimeSpectrum S,
        Algebra.IsGeometricallyRegular q.asIdeal.ResidueField (q.asIdeal.Fiber T)) →
      ∀ p : PrimeSpectrum R,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber T))) →
    (∀ (R S T : Type (max u v))
      [CommRing R] [CommRing S] [CommRing T]
      [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T]
      [IsNoetherianRing R] [IsNoetherianRing S] [IsNoetherianRing T]
      [Module.Flat R S] [Module.FaithfullyFlat S T],
      (∀ p : PrimeSpectrum R,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber T))) →
      ∀ p : PrimeSpectrum R,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))) →
    (∀ (k K R : Type (max u v))
      [Field k] [Field K] [CommRing R]
      [Algebra k K] [Algebra K R] [Algebra k R] [IsScalarTower k K R]
      [IsNoetherianRing R],
      Algebra.IsAlgebraic k K → Algebra.IsSeparable k K →
        P (algebraMap k R) → P (algebraMap K R)) →
    ∀ {A : Type u} {Ah : Type v} [CommRing A] [CommRing Ah] [Algebra A Ah]
      (I : Ideal A),
      HenselianPair Ah (I.map (algebraMap A Ah)) →
      (∀ (B : Type (max u v)) (_ : CommRing B) (J : Ideal B),
        HenselianPair B J →
          ∀ f : A →+* B, I ≤ J.comap f →
            ∃! g : Ah →+* B,
              g.comp (algebraMap A Ah) = f ∧ I.map (algebraMap A Ah) ≤ J.comap g) →
      IsPRingAt.{u, v, v} P A →
      IsPRingAt.{v, u, u} P Ah
Tag 0C36, a lemma

Tag 0C36 in the Stacks Project.

isPRing_henselization_and_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/Henselization.lean, line 1209. References: EGA IV (18.7.2), “partial”.

The henselization and strict henselization of a local P-ring are P-rings when P is local on the target, ascends along regular maps, descends along faithfully flat maps, and is preserved by separable algebraic extensions of the ground field.

public theorem isPRing_henselization_and_strictHenselization
    (P : RingMapProperty.{max u (max v (max w x)), max u (max v (max w x))})
    (hB : ∀ (k R : Type (max u (max v (max w x))))
      [Field k] [CommRing R] [Algebra k R]
      [IsNoetherianRing R],
      (∀ q : PrimeSpectrum R, P (algebraMap k (Localization.AtPrime q.asIdeal))) ↔
        P (algebraMap k R))
    (hC : ∀ (R S T : Type (max u (max v (max w x))))
      [CommRing R] [CommRing S] [CommRing T]
      [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T]
      [IsNoetherianRing R] [IsNoetherianRing S] [IsNoetherianRing T]
      [Module.Flat R S] [Module.Flat S T],
      (∀ p : PrimeSpectrum R,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))) →
      (∀ q : PrimeSpectrum S,
        Algebra.IsGeometricallyRegular q.asIdeal.ResidueField (q.asIdeal.Fiber T)) →
      ∀ p : PrimeSpectrum R,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber T)))
    (hD : ∀ (R S T : Type (max u (max v (max w x))))
      [CommRing R] [CommRing S] [CommRing T]
      [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T]
      [IsNoetherianRing R] [IsNoetherianRing S] [IsNoetherianRing T]
      [Module.Flat R S] [Module.FaithfullyFlat S T],
      (∀ p : PrimeSpectrum R,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber T))) →
      ∀ p : PrimeSpectrum R,
        P.Holds (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S)))
    (hE : ∀ (k K R : Type (max u (max v (max w x))))
      [Field k] [Field K] [CommRing R]
      [Algebra k K] [Algebra K R] [Algebra k R] [IsScalarTower k K R]
      [IsNoetherianRing R],
      Algebra.IsAlgebraic k K → Algebra.IsSeparable k K →
        P (algebraMap k R) → P (algebraMap K R))
    (R : Type u) (Rh : Type w) (Rsh : Type x)
    [CommRing R] [IsLocalRing R]
    [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
    [CommRing Rsh] [IsLocalRing Rsh] [Algebra R Rsh]
    (ksep : Type v) [Field ksep] [Algebra (ResidueField R) ksep]
    [IsSepClosure (ResidueField R) ksep]
    [IsHenselization R (ResidueField R) Rh]
    [IsHenselization R ksep Rsh]
    (hR : IsPRingAt.{u, max v (max w x), max v (max w x)} P R) :
    IsPRingAt.{w, max u (max v x), max u (max v x)} P Rh ∧
      IsPRingAt.{x, max u (max v w), max u (max v w)} P Rsh
Tag 0BIW, a lemma

Tag 0BIW in the Stacks Project.

geometricReducedness_satisfies_formalFibre_properties, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/Examples/GeometricallyReduced.lean, line 387. References: EGA IV (7.5.3), “(viii) reduced”; EGA IV (7.9.7), “partial”.

Stacks 0BIW. Geometric reducedness satisfies properties (A)--(E) for formal fibres: base change by a finitely generated field extension, detection on local rings, ascent along a regular map, faithfully flat descent, and separable algebraic extension of the base field.

public theorem geometricReducedness_satisfies_formalFibre_properties :
    (∀ (k : Type u) (k' : Type v) (R : Type w) [Field k] [Field k'] [CommRing R]
      [Algebra k k'] [Algebra k R] [Algebra.EssFiniteType k k'] [IsNoetherianRing R],
      Algebra.IsGeometricallyReduced k R →
        Algebra.IsGeometricallyReduced k' (k' ⊗[k] R)) ∧
    (∀ (k : Type u) (R : Type v) [Field k] [CommRing R] [Algebra k R]
      [IsNoetherianRing R],
      (∀ (p : Ideal R) [p.IsPrime],
        Algebra.IsGeometricallyReduced k (Localization.AtPrime p)) ↔
          Algebra.IsGeometricallyReduced k R) ∧
    (∀ (A : Type u) (B : Type v) (C : Type w)
      [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.Flat B C],
      (∀ (p : Ideal A) [p.IsPrime],
        Algebra.IsGeometricallyReduced p.ResidueField (p.Fiber B)) →
      (∀ (q : Ideal B) [q.IsPrime],
        Algebra.IsGeometricallyRegular q.ResidueField (q.Fiber C)) →
      ∀ (p : Ideal A) [p.IsPrime],
        Algebra.IsGeometricallyReduced p.ResidueField (p.Fiber C)) ∧
    (∀ (A : Type u) (B : Type v) (C : Type w)
      [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.FaithfullyFlat B C],
      (∀ (p : Ideal A) [p.IsPrime],
        Algebra.IsGeometricallyReduced p.ResidueField (p.Fiber C)) →
      ∀ (p : Ideal A) [p.IsPrime],
        Algebra.IsGeometricallyReduced p.ResidueField (p.Fiber B)) ∧
    (∀ (k : Type u) (k' : Type v) (R : Type w)
      [Field k] [Field k'] [CommRing R]
      [Algebra k k'] [Algebra k R] [Algebra k' R] [IsScalarTower k k' R]
      [Algebra.IsSeparable k k'] [IsNoetherianRing R],
      Algebra.IsGeometricallyReduced k R → Algebra.IsGeometricallyReduced k' R)
Tag 0BIX, a lemma

Tag 0BIX in the Stacks Project.

geometricNormality_satisfies_formalFibre_properties, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/Examples/GeometricallyNormal.lean, line 425. References: EGA IV (7.3.10), “special case”.

Geometric normality satisfies properties (A)--(E) for formal fibres: base change by a finitely generated field extension, detection on local rings, ascent along a regular map, faithfully flat descent, and separable algebraic extension of the base field.

public theorem geometricNormality_satisfies_formalFibre_properties :
    (∀ (k : Type u) (k' : Type v) (R : Type w) [Field k] [Field k'] [CommRing R]
      [Algebra k k'] [Algebra k R] [Algebra.EssFiniteType k k'] [IsNoetherianRing R],
      Algebra.IsGeometricallyNormal k R →
        Algebra.IsGeometricallyNormal k' (k' ⊗[k] R)) ∧
    (∀ (k : Type u) (R : Type v) [Field k] [CommRing R] [Algebra k R]
      [IsNoetherianRing R],
      (∀ (p : Ideal R) [p.IsPrime],
        Algebra.IsGeometricallyNormal k (Localization.AtPrime p)) ↔
          Algebra.IsGeometricallyNormal k R) ∧
    (∀ (A : Type u) (B : Type v) (C : Type w)
      [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.Flat B C],
      (∀ (p : Ideal A) [p.IsPrime],
        Algebra.IsGeometricallyNormal p.ResidueField (p.Fiber B)) →
      (∀ (q : Ideal B) [q.IsPrime],
        Algebra.IsGeometricallyRegular q.ResidueField (q.Fiber C)) →
      ∀ (p : Ideal A) [p.IsPrime],
        Algebra.IsGeometricallyNormal p.ResidueField (p.Fiber C)) ∧
    (∀ (A : Type u) (B : Type v) (C : Type w)
      [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.FaithfullyFlat B C],
      (∀ (p : Ideal A) [p.IsPrime],
        Algebra.IsGeometricallyNormal p.ResidueField (p.Fiber C)) →
      ∀ (p : Ideal A) [p.IsPrime],
        Algebra.IsGeometricallyNormal p.ResidueField (p.Fiber B)) ∧
    (∀ (k : Type u) (k' : Type v) (R : Type w)
      [Field k] [Field k'] [CommRing R]
      [Algebra k k'] [Algebra k R] [Algebra k' R] [IsScalarTower k k' R]
      [Algebra.IsSeparable k k'] [IsNoetherianRing R],
      Algebra.IsGeometricallyNormal k R → Algebra.IsGeometricallyNormal k' R)
Tag 0BIY, a lemma

Tag 0BIY in the Stacks Project.

serreProperty_satisfies_formalFiberAxioms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/Examples/SerreCondition.lean, line 240. The attribute's comment: “The source fixes n ≥ 1, so _hn : 1 ≤ n is carried for faithfulness even though the proof does not use it — each of the five axioms holds for (Sₙ) at every n. Hence the leading underscore on that binder.”.

Stacks 0BIY. For n ≥ 1, the property that the target of a map from a field to a Noetherian ring satisfies (Sₙ) has properties (A)--(E).

public theorem serreProperty_satisfies_formalFiberAxioms
    (n : ℕ) (_hn : 1 ≤ n) :
    (∀ (k : Type u) (K : Type v) (R : Type w)
      [Field k] [Field K] [CommRing R] [Algebra k K]
      [Algebra k R] [IsNoetherianRing R] [Algebra.EssFiniteType k K],
      HasSerreCondition R n → HasSerreCondition (R ⊗[k] K) n) ∧
    (∀ (k : Type u) (R : Type v) [Field k] [CommRing R]
      [Algebra k R] [IsNoetherianRing R],
      (∀ p : PrimeSpectrum R,
        HasSerreCondition (Localization.AtPrime p.asIdeal) n) ↔
        HasSerreCondition R n) ∧
    (∀ (A : Type u) (B : Type v) (C : Type w)
      [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.Flat B C],
      (∀ p : PrimeSpectrum A, HasSerreCondition (p.asIdeal.Fiber B) n) →
      (∀ q : PrimeSpectrum B,
        Algebra.IsGeometricallyRegular q.asIdeal.ResidueField (q.asIdeal.Fiber C)) →
      ∀ p : PrimeSpectrum A, HasSerreCondition (p.asIdeal.Fiber C) n) ∧
    (∀ (A : Type u) (B : Type v) (C : Type w)
      [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.FaithfullyFlat B C],
      (∀ p : PrimeSpectrum A, HasSerreCondition (p.asIdeal.Fiber C) n) →
      ∀ p : PrimeSpectrum A, HasSerreCondition (p.asIdeal.Fiber B) n) ∧
    (∀ (k : Type u) (K : Type v) (R : Type w)
      [Field k] [Field K] [CommRing R]
      [Algebra k K] [Algebra k R] [Algebra K R] [IsScalarTower k K R]
      [IsNoetherianRing R] [Algebra.IsAlgebraic k K] [Algebra.IsSeparable k K],
      HasSerreCondition R n → HasSerreCondition R n)
Tag 0BJ9, a lemma

Tag 0BJ9 in the Stacks Project.

cohenMacaulayProperty_satisfies_formalFiberAxioms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/Examples/SerreCondition.lean, line 406. References: EGA IV (7.5.3), “(iii) Cohen-Macaulay”.

Stacks 0BJ9. The property of a map from a field to a Noetherian ring that its target is Cohen–Macaulay satisfies properties (A)--(E): it is preserved by finitely generated field extension, is local on the target, passes through a composition of flat maps when the second map is regular, descends through a faithfully flat second map, and is unchanged upon replacing the ground field by a separable algebraic extension.

public theorem cohenMacaulayProperty_satisfies_formalFiberAxioms
    (P : RingMapProperty.{u, u})
    (hP : ∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R]
      [IsNoetherianRing R], P (algebraMap k R) ↔ Module.IsCohenMacaulay R R) :
    (∀ (k K R : Type u) [Field k] [Field K] [CommRing R] [Algebra k K]
      [Algebra k R] [IsNoetherianRing R] [Algebra.EssFiniteType k K],
      P (algebraMap k R) →
        P (Algebra.TensorProduct.includeRight (R := k) (A := R) (B := K)).toRingHom) ∧
    (∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
      (∀ p : PrimeSpectrum R,
        P (algebraMap k (Localization.AtPrime p.asIdeal))) ↔ P (algebraMap k R)) ∧
    (∀ (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.Flat B C],
      (∀ p : PrimeSpectrum A,
        P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))) →
      (∀ q : PrimeSpectrum B,
        Algebra.IsGeometricallyRegular q.asIdeal.ResidueField (q.asIdeal.Fiber C)) →
      ∀ p : PrimeSpectrum A,
        P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C))) ∧
    (∀ (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.FaithfullyFlat B C],
      (∀ p : PrimeSpectrum A,
        P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C))) →
      ∀ p : PrimeSpectrum A,
        P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))) ∧
    (∀ (k K R : Type u) [Field k] [Field K] [CommRing R]
      [Algebra k K] [Algebra k R] [Algebra K R] [IsScalarTower k K R]
      [IsNoetherianRing R] [Algebra.IsAlgebraic k K] [Algebra.IsSeparable k K],
      P (algebraMap k R) → P (algebraMap K R))
Tag 0BIZ, a lemma

Tag 0BIZ in the Stacks Project.

propertyRk_after_finiteExtensions_satisfies_formalFibre_properties, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormalFibres/Examples/RegularInCodimension.lean, line 648.

For fixed n, the property that every finite extension of the ground field makes an algebra satisfy Serre's condition (R_n) satisfies properties (A)--(E) for formal fibres: base change by a finitely generated field extension, detection on local rings, ascent along a regular map, faithfully flat descent, and separable algebraic extension of the base field.

public theorem propertyRk_after_finiteExtensions_satisfies_formalFibre_properties (n : ℕ) :
    (∀ (k : Type u) (k' : Type v) (R : Type w) [Field k] [Field k'] [CommRing R]
      [Algebra k k'] [Algebra k R] [Algebra.EssFiniteType k k'] [IsNoetherianRing R],
      (∀ (K : Type u) [Field K] [Algebra k K] [FiniteDimensional k K],
        HasPropertyRk (K ⊗[k] R) n) →
      ∀ (K : Type v) [Field K] [Algebra k' K] [FiniteDimensional k' K],
        HasPropertyRk (K ⊗[k'] (k' ⊗[k] R)) n) ∧
    (∀ (k : Type u) (R : Type v) [Field k] [CommRing R] [Algebra k R]
      [IsNoetherianRing R],
      (∀ (p : Ideal R) [p.IsPrime],
        ∀ (K : Type u) [Field K] [Algebra k K] [FiniteDimensional k K],
          HasPropertyRk (K ⊗[k] Localization.AtPrime p) n) ↔
      ∀ (K : Type u) [Field K] [Algebra k K] [FiniteDimensional k K],
        HasPropertyRk (K ⊗[k] R) n) ∧
    (∀ (A : Type u) (B : Type v) (C : Type w)
      [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.Flat B C],
      (∀ (p : Ideal A) [p.IsPrime],
        ∀ (K : Type u) [Field K] [Algebra p.ResidueField K]
          [FiniteDimensional p.ResidueField K],
          HasPropertyRk (K ⊗[p.ResidueField] p.Fiber B) n) →
      (∀ (q : Ideal B) [q.IsPrime],
        Algebra.IsGeometricallyRegular q.ResidueField (q.Fiber C)) →
      ∀ (p : Ideal A) [p.IsPrime],
        ∀ (K : Type u) [Field K] [Algebra p.ResidueField K]
          [FiniteDimensional p.ResidueField K],
          HasPropertyRk (K ⊗[p.ResidueField] p.Fiber C) n) ∧
    (∀ (A : Type u) (B : Type v) (C : Type w)
      [CommRing A] [CommRing B] [CommRing C]
      [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
      [IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
      [Module.Flat A B] [Module.FaithfullyFlat B C],
      (∀ (p : Ideal A) [p.IsPrime],
        ∀ (K : Type u) [Field K] [Algebra p.ResidueField K]
          [FiniteDimensional p.ResidueField K],
          HasPropertyRk (K ⊗[p.ResidueField] p.Fiber C) n) →
      ∀ (p : Ideal A) [p.IsPrime],
        ∀ (K : Type u) [Field K] [Algebra p.ResidueField K]
          [FiniteDimensional p.ResidueField K],
          HasPropertyRk (K ⊗[p.ResidueField] p.Fiber B) n) ∧
    (∀ (k : Type u) (k' : Type v) (R : Type w)
      [Field k] [Field k'] [CommRing R]
      [Algebra k k'] [Algebra k R] [Algebra k' R] [IsScalarTower k k' R]
      [Algebra.IsSeparable k k'] [IsNoetherianRing R],
      (∀ (K : Type u) [Field K] [Algebra k K] [FiniteDimensional k K],
        HasPropertyRk (K ⊗[k] R) n) →
      ∀ (K : Type v) [Field K] [Algebra k' K] [FiniteDimensional k' K],
        HasPropertyRk (K ⊗[k'] R) n)
Sources
LeanpropertyRing_iff_quotientCompletion_fibers · fibersHaveProperty_iff_localizations_at_primes_and_maximals · quasiFinite_preserves_formalFiberProperty · isPRing_iff_formalFibersHave_localization_maximal · isPRing_of_essFiniteType · fibersHaveProperty_adicCompletion_of_isPRing · isPRing_henselization · isPRing_henselization_and_strictHenselization

Section15.53 Excellent rings#

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

Tag 07QT, a definition

Tag 07QT in the Stacks Project.

IsQuasiExcellent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Excellent/Basic.lean, line 173. The attribute's comment: “(1)”. References: EGA IV (7.8.2), “(ii), (iii)”.

A commutative ring is quasi-excellent if it is Noetherian, a G-ring, and J-2.

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

IsExcellent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Excellent/Basic.lean, line 178. The attribute's comment: “(2)”. References: EGA IV (7.8.2).

A commutative ring is excellent if it is quasi-excellent and universally catenary.

public def IsExcellent (R : Type u) [CommRing R] : Prop
Tag 07QU, a lemma

Tag 07QU in the Stacks Project.

isQuasiExcellent_and_isExcellent_of_essFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Excellent/Basic.lean, line 282. References: EGA IV (7.8.3), “more general”; EGA IV (7.8.4), “more general”.

An algebra essentially of finite type over a quasi-excellent ring is quasi-excellent, and an algebra essentially of finite type over an excellent ring is excellent.

public theorem isQuasiExcellent_and_isExcellent_of_essFiniteType
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.EssFiniteType R S] :
    (IsQuasiExcellent R → IsQuasiExcellent S) ∧
      (IsExcellent R → IsExcellent S)
Tag 07QW, a proposition

Tag 07QW in the Stacks Project.

isExcellent_of_standard_classes_and_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Excellent/Basic.lean, line 386. References: EGA IV (7.8.3), “(iii), part of (ii)”; EGA IV (7.8.6), “(i), affine case”; EGA IV (6.12.6), “special case”; SGA 3 VIB (10.10), “more general”.

Stacks 07QW. Fields, Noetherian complete local rings, the integers, and Dedekind domains whose fraction fields have characteristic zero are excellent; moreover, every finite-type algebra over an excellent ring is excellent.

public theorem isExcellent_of_standard_classes_and_finiteType :
    (∀ (K : Type u) [Field K], IsExcellent K) ∧
      (∀ (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
        [IsPrecomplete (IsLocalRing.maximalIdeal R) R], IsExcellent R) ∧
      IsExcellent ℤ ∧
      (∀ (R : Type u) [CommRing R] [IsDedekindDomain R] [CharZero (FractionRing R)],
        IsExcellent R) ∧
      (∀ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
        [Algebra.FiniteType R S], IsExcellent R → IsExcellent S)
Tag 0BJ0, a lemma

Tag 0BJ0 in the Stacks Project.

isNagataRing_iff_formalFibers_geometricallyReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Excellent/Basic.lean, line 480. References: EGA IV (7.6.4), “local case, a'')<=>b)”; EGA IV (7.7.3), “A local Noetherian”; EGA IV (7.7.4), “formal fibres clause”.

Stacks 0BJ0. A Noetherian local ring is Nagata if and only if all its formal fibres are geometrically reduced.

public theorem isNagataRing_iff_formalFibers_geometricallyReduced
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A] :
    IsNagataRing A ↔
      ∀ q : PrimeSpectrum A,
        Algebra.IsGeometricallyReduced q.asIdeal.ResidueField
          (q.asIdeal.Fiber (AdicCompletion (maximalIdeal A) A))
Tag 07QV, a lemma

Tag 07QV in the Stacks Project.

isNagataRing_of_isQuasiExcellent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Excellent/Basic.lean, line 351. References: EGA IV (7.8.3), “more general”; EGA IV (7.8.4), “(iii)”.

Stacks 07QV. A quasi-excellent commutative ring is a Nagata ring.

public theorem isNagataRing_of_isQuasiExcellent {R : Type u} [CommRing R]
    (hR : IsQuasiExcellent R) : IsNagataRing R
Tag 0C23, a lemma

Tag 0C23 in the Stacks Project.

isNormalRing_adicCompletion_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/PermanenceOfProperties.lean, line 572. References: EGA IV (7.8.3), “(v) normal ascends”.

Stacks Tag 0C23. The completion of a Noetherian normal local ring whose formal fibres are normal is a normal ring.

public theorem isNormalRing_adicCompletion_maximalIdeal
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (hA : IsNormalRing A)
    (hformal : ∀ (p : Ideal A) [p.IsPrime],
      IsNormalRing (p.Fiber (AdicCompletion (IsLocalRing.maximalIdeal A) A))) :
    IsNormalRing (AdicCompletion (IsLocalRing.maximalIdeal A) A)
Sources
LeanIsQuasiExcellent · IsExcellent · isQuasiExcellent_and_isExcellent_of_essFiniteType · isExcellent_of_standard_classes_and_finiteType · isNagataRing_iff_formalFibers_geometricallyReduced · isNagataRing_of_isQuasiExcellent · isNormalRing_adicCompletion_maximalIdeal

Section15.55 Injective abelian groups#

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

Tag 01D7, a lemma

Tag 01D7 in the Stacks Project.

AddCommGrpCat.injective_iff_divisible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Injective/Criteria.lean, line 114.

Stacks 01D7. An abelian group is an injective object in the category of abelian groups if and only if it is divisible.

Divisibility is Baer's criterion over ℤ: an injective group is Baer, and dividing x by n is extending to ℤ the map nℤ → J determined by n ↦ x. Conversely a divisible group is injective, which is Mathlib's AddCommGrpCat.injective_of_divisible.

theorem AddCommGrpCat.injective_iff_divisible (J : Type u) [AddCommGroup J] :
    Injective (C := AddCommGrpCat) (AddCommGrpCat.of J) ↔ Nonempty (DivisibleBy J ℕ)
Sources
LeanAddCommGrpCat.injective_iff_divisible

Section15.56 Injective modules#

Section 15.56 of the Stacks Project, Tag 01D8. 9 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AVD, a definition

Tag 0AVD in the Stacks Project.

Module.injective_iff_exact_linearYoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Injective/Criteria.lean, line 74.

Stacks 0AVD. An R-module J is injective if and only if its contravariant Hom functor Hom_R(-, J) is exact.

Exactness of a functor out of (ModuleCat R)ᵒᵖ is tested after composing with the forgetful functor to abelian groups, where the composite is the preadditive Yoneda functor at J, for which Mathlib already characterises injectivity.

theorem Module.injective_iff_exact_linearYoneda (R : Type u) [CommRing R]
    (J : Type v) [AddCommGroup J] [Module R J] :
    Module.Injective R J ↔
      exactFunctor _ _ ((linearYoneda R (ModuleCat.{v} R)).obj (ModuleCat.of R J))
Tag 0AUL, a lemma

Tag 0AUL in the Stacks Project.

CategoryTheory.Abelian.comparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/YonedaExtOne.lean, line 205. The attribute's comment: “the comparison itself; isCanonicalExtOneComparison_comparison is its defining properties and eq_comparison_of_isCanonical their uniqueness”.

The canonical comparison data. Its equivalence is comparisonEquiv, and its covariant and contravariant maps are Yoneda composition with Ext.mk₀ read through that equivalence.

noncomputable def comparison : ExtOneComparison (C := C)

CategoryTheory.Abelian.isCanonicalExtOneComparison_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/YonedaExtOne.lean, line 243. The attribute's comment: “the comparison has the announced properties: canonicity, representation of the two maps by pushout and pullback, naturality in both variables, additivity for Baer sums, and agreement with both connecting maps”. References: EGA 0 (12.3.2), “more general”; SGA 7 VII (3.4), “special case”.

The comparison is canonical. comparison sends a short exact sequence to its derived extension class, represents its covariant and contravariant maps by pushout and pullback of short exact sequences, is natural in both variables, takes Baer sums to sums in Ext¹, and matches the boundary maps of the two long exact Ext sequences.

theorem isCanonicalExtOneComparison_comparison :
    IsCanonicalExtOneComparison (comparison (C := C))

CategoryTheory.Abelian.eq_comparison_of_isCanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/YonedaExtOne.lean, line 282. The attribute's comment: “uniqueness of the canonical comparison”.

The canonical comparison is unique. Any comparison with the properties of IsCanonicalExtOneComparison is comparison.

theorem eq_comparison_of_isCanonical (c' : ExtOneComparison (C := C))
    (hc' : IsCanonicalExtOneComparison c') : c' = comparison
Tag 0AVE, a lemma

Tag 0AVE in the Stacks Project.

Module.injective_iff_subsingleton_ext_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Injective/Criteria.lean, line 152.

Stacks 0AVE. An R-module J is injective if and only if Ext¹_R(M, J) vanishes for every R-module M.

Mathlib's CategoryTheory.injective_iff_subsingleton_ext_one is this criterion for an object of an abelian category with an Ext theory; here it is read off for modules, the quantifier running over R-modules rather than over objects of ModuleCat R. The two agree because every object of ModuleCat.{v} R is ModuleCat.of R of its own carrier.

theorem Module.injective_iff_subsingleton_ext_one (R : Type u) [Ring R] [Small.{v} R]
    (J : Type v) [AddCommGroup J] [Module R J] :
    Module.Injective R J ↔
      ∀ (M : Type v) [AddCommGroup M] [Module R M],
        Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R J) 1)

Declarations registered for the tag:

Tag 0AVF, a lemma

Tag 0AVF in the Stacks Project.

Declarations registered for the tag:

Tag 01D9, a definition

Tag 01D9 in the Stacks Project.

CharacterModule.dualFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/CharacterModule/Duality.lean, line 55. The attribute's comment: “the contravariant functor M ↦ M^∨”.

The contravariant functor M ↦ M^∨ = Hom_ℤ(M, ℚ/ℤ) on modules over a commutative ring, acting on a linear map by precomposition (CharacterModule.dual).

noncomputable def dualFunctor (R : Type u) [CommRing R] :
    (ModuleCat.{u} R)ᵒᵖ ⥤ ModuleCat.{u} R

freeModuleCoverFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/CharacterModule/EnoughInjectives.lean, line 108. The attribute's comment: “the free module on the underlying set of a module, with its natural surjection”.

The functor sending an R-module M to the natural epimorphism F(M) → M, where F(M) is the free module on the underlying set of M. Landing in the full subcategory of the arrow category spanned by the epimorphisms retains the surjectivity of each cover.

noncomputable def freeModuleCoverFunctor (R : Type u) [CommRing R] :
    ModuleCat.{u} R ⥤ (MorphismProperty.epimorphisms (ModuleCat.{u} R)).Arrow ⊤ ⊤
Tag 01DA, a lemma

Tag 01DA in the Stacks Project.

CharacterModule.dualFunctor_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/CharacterModule/Duality.lean, line 118.

The contravariant character-dual functor on modules over a commutative ring is exact.

theorem dualFunctor_exact (R : Type u) [CommRing R] :
    exactFunctor (ModuleCat.{u} R)ᵒᵖ (ModuleCat.{u} R) (dualFunctor R)
Tag 01DB, a lemma

Tag 01DB in the Stacks Project.

CharacterModule.eval_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/CharacterModule/Duality.lean, line 140.

The canonical evaluation map from an additive commutative group into its double character module is injective.

theorem eval_injective (M : Type u) [AddCommGroup M] :
    Function.Injective (AddMonoidHom.eval : M →+ CharacterModule (CharacterModule M))
Tag 01DC, a lemma

Tag 01DC in the Stacks Project.

jModule_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/CharacterModule/EnoughInjectives.lean, line 141.

Stacks Tag 01DC, Lemma 15.56.8. For every R-module M (with R commutative), the R-module J(M) = (F(M^∨))^∨ is injective. This is characterModule_finsupp_injective for the index type M^∨.

theorem jModule_injective (R : Type*) [CommRing R] (M : Type*) [AddCommGroup M] :
    Module.Injective R (JModule R M)
Tag 01DD, a lemma

Tag 01DD in the Stacks Project.

moduleCat_hasFunctorialInjectiveEmbeddings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/CharacterModule/EnoughInjectives.lean, line 254.

Stacks Project, Tag 01DD. The canonical maps M → J(M) = (F(M^∨))^∨ form a covariant functor from R-modules to arrows of R-modules whose source projection is the identity, each of whose components is a monomorphism, and each of whose targets is an injective module.

theorem moduleCat_hasFunctorialInjectiveEmbeddings :
    IsFunctorialInjectiveEmbeddings₁ (ModuleCat.{max u v} R) (jModuleArrowFunctor R) ∧
      IsFunctorialInjectiveEmbeddings₂ (ModuleCat.{max u v} R) (jModuleArrowFunctor R) ∧
        IsFunctorialInjectiveEmbeddings₃ (ModuleCat.{max u v} R) (jModuleArrowFunctor R)
Sources
LeanModule.injective_iff_exact_linearYoneda · CategoryTheory.Abelian.comparison · CategoryTheory.Abelian.isCanonicalExtOneComparison_comparison · CategoryTheory.Abelian.eq_comparison_of_isCanonical · Module.injective_iff_subsingleton_ext_one · CategoryTheory.injective_iff_subsingleton_ext_one · ModuleCat.injective_iff_subsingleton_ext_quotient_one · ModuleCat.ext_quotient_one_subsingleton_iff

Section15.57 Derived categories of modules#

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

Tag 0915, a lemma

Tag 0915 in the Stacks Project.

isKInjective_restrictScalars_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KInjective/ChangeOfRings.lean, line 99. References: SGA 4 V (4.9), “special case”.

Stacks Tag 0915. Let f : R → S be a flat ring map of commutative rings. If I is a K-injective complex of S-modules, then its restriction of scalars res_f I is a K-injective complex of R-modules.

This is the adjoint criterion CochainComplex.isKInjective_mapHomologicalComplex (Stacks 13.31.9) applied to the extension–restriction adjunction (- ⊗_R S) ⊣ res_f (Stacks 05DQ, ModuleCat.extendRestrictScalarsAdj): the left adjoint - ⊗_R S preserves acyclicity by acyclic_extendScalarsComplex_of_flat, which is where flatness enters.

theorem isKInjective_restrictScalars_of_flat
    {R S : Type u₁} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.Flat)
    (I : CochainComplex (ModuleCat.{max v u₁} S) ℤ) (hI : I.IsKInjective) :
    ((CochainComplex.restrictScalars f).obj I).IsKInjective
Tag 0916, a lemma

Tag 0916 in the Stacks Project.

isKInjective_of_restrictScalars_of_isEpi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KInjective/ChangeOfRings.lean, line 162.

Stacks 0916. Let R → S be an epimorphism of commutative rings. If a complex of S-modules is K-injective when regarded as a complex of R-modules, then it is K-injective as a complex of S-modules.

Given an acyclic complex K of S-modules and a chain map f : K → I, restriction of scalars keeps K acyclic, so the hypothesis supplies a null-homotopy of res f. Restriction of scalars is full and faithful here, so that homotopy is the image of a null-homotopy of f itself.

theorem isKInjective_of_restrictScalars_of_isEpi [Algebra.IsEpi R S]
    (I : CochainComplex (ModuleCat.{max w u₁ u₂} S) ℤ)
    (hI : CochainComplex.IsKInjective
      (((ModuleCat.restrictScalars (algebraMap R S)).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj I :
          CochainComplex (ModuleCat.{max w u₁ u₂} R) ℤ)) :
    CochainComplex.IsKInjective I
Tag 0917, a lemma

Tag 0917 in the Stacks Project.

coextend_isKInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KInjective/ChangeOfRings.lean, line 230.

Stacks Tag 0917. If I is a K-injective complex of R-modules, then its degreewise coextension of scalars Hom_R(S, I) is a K-injective complex of S-modules.

This is the adjoint criterion CochainComplex.isKInjective_mapHomologicalComplex for the adjunction ModuleCat.restrictCoextendScalarsAdj f, whose left adjoint (-)_R preserves acyclicity by restrictScalars_acyclic.

theorem coextend_isKInjective {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S)
    (I : CochainComplex (ModuleCat.{max v u₂} R) ℤ) (hI : I.IsKInjective) :
    ((coextendComplex.{u₁, u₂, v} f).obj I).IsKInjective
Sources
LeanisKInjective_restrictScalars_of_flat · isKInjective_of_restrictScalars_of_isEpi · coextend_isKInjective

Section15.58 Computing Tor#

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

Tag 064G, an equation

Tag 064G in the Stacks Project.

CochainComplex.ComputingTor.derivedTensorProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/Computing.lean, line 517.

Stacks 064G. For every R-module M, the total left derived tensor product - ⊗ᴸ_R M : D⁻(R) ⟶ D⁻(R) exists.

public def derivedTensorProduct (M : ModuleCat.{u} R) : TotalDerivedTensor M
Tag 064H, an equation

Tag 064H in the Stacks Project.

CochainComplex.DerivedExtensionScalars.derivedExtensionScalars, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/DerivedExtensionScalars.lean, line 190. References: SGA 4½ Rapport (4.1), “special case”.

Stacks 064H. Derived extension of scalars on bounded-above derived categories. This is the dual of the bounded-below right derived functor of extension of scalars on opposite module categories, where projective modules become injective objects.

public def derivedExtensionScalars (f : R →+* A)
    [HasDerivedCategory.{wR} (ModuleCat.{max uA (max uR v)} R)]
    [HasDerivedCategory.{wA} (ModuleCat.{max uA (max uR v)} A)]
    [HasDerivedCategory (ModuleCat.{max uA (max uR v)} R)ᵒᵖ]
    [HasDerivedCategory (ModuleCat.{max uA (max uR v)} A)ᵒᵖ] :
    DerivedCategory.Minus (ModuleCat.{max uA (max uR v)} R) ⥤
      DerivedCategory.Minus (ModuleCat.{max uA (max uR v)} A)
Sources
LeanCochainComplex.ComputingTor.derivedTensorProduct · CochainComplex.DerivedExtensionScalars.derivedExtensionScalars

Section15.59 Tensor products of complexes#

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

Tag 0FNI, a lemma

Tag 0FNI in the Stacks Project.

TotalTensorComplex.cochainComplex_symmetricMonoidalCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TensorComplex/Monoidal.lean, line 115.

The category of cochain complexes of modules over a commutative ring, with tensor product given by the total complex of the degreewise tensor product, is symmetric monoidal. On the summand of bidegree (p, q), its braiding is the ordinary symmetry of tensor products multiplied by the Koszul sign (-1)^(p*q).

public theorem cochainComplex_symmetricMonoidalCategory (R : Type u) [CommRing R] :
    ∃ s : SymmetricCategory (CochainComplex (ModuleCat R) ℤ),
      ∀ (K L : CochainComplex (ModuleCat R) ℤ) (p q n : ℤ) (h : p + q = n),
        HomologicalComplex.ιTensorObj K L p q n h ≫
            (s.toBraidedCategory.braiding K L).hom.f n =
          ((p * q).negOnePow : ℤˣ) •
            ((β_ (K.X p) (L.X q)).hom ≫
              HomologicalComplex.ιTensorObj L K q p n (by simpa [add_comm] using h))
Tag 064I, a lemma

Tag 064I in the Stacks Project.

TotalTensorComplex.tensorTotal_preserves_homotopy_and_descends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TensorComplex/Monoidal.lean, line 128. References: SGA 4½ Etat 0 (1.3.3), “tensor over ModuleCat R”.

Tensoring with a fixed complex and taking the total complex preserves homotopic maps, and therefore induces an endofunctor of the homotopy category of complexes.

public theorem tensorTotal_preserves_homotopy_and_descends {R : Type u} [CommRing R]
    (P : CochainComplex (ModuleCat.{u} R) ℤ) :
    let T := (curriedTensor (ModuleCat.{u} R)).map₂CochainComplex.flip.obj P
    (∀ {L M : CochainComplex (ModuleCat.{u} R) ℤ} {f g : L ⟶ M},
      homotopic (ModuleCat.{u} R) (ComplexShape.up ℤ) f g →
        homotopic (ModuleCat.{u} R) (ComplexShape.up ℤ) (T.map f) (T.map g)) ∧
    ∃ T' : HomotopyCategory (ModuleCat.{u} R) (ComplexShape.up ℤ) ⥤
        HomotopyCategory (ModuleCat.{u} R) (ComplexShape.up ℤ),
      HomotopyCategory.quotient (ModuleCat.{u} R) (ComplexShape.up ℤ) ⋙ T' =
        T ⋙ HomotopyCategory.quotient (ModuleCat.{u} R) (ComplexShape.up ℤ)
Tag 0GWP, a lemma

Tag 0GWP in the Stacks Project.

TotalTensorComplex.homotopyCategory_symmetricMonoidalCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TensorComplex/Monoidal.lean, line 179.

The homotopy category of cochain complexes of modules over a commutative ring is symmetric monoidal under the total tensor product. Its associator and Koszul braiding are induced from the corresponding canonical constraints on complexes.

public theorem homotopyCategory_symmetricMonoidalCategory (R : Type u) [CommRing R] :
    ∃ sC : SymmetricCategory (CochainComplex (ModuleCat.{u} R) ℤ),
      (∀ (K L : CochainComplex (ModuleCat.{u} R) ℤ) (p q n : ℤ) (h : p + q = n),
        HomologicalComplex.ιTensorObj K L p q n h ≫
            (sC.toBraidedCategory.braiding K L).hom.f n =
          ((p * q).negOnePow : ℤˣ) •
            ((β_ (K.X p) (L.X q)).hom ≫
              HomologicalComplex.ιTensorObj L K q p n (by simpa [add_comm] using h))) ∧
      letI := sC
      ∃ mK : MonoidalCategory
          (HomotopyCategory (ModuleCat.{u} R) (ComplexShape.up ℤ)),
        letI := mK
        ∃ sK : SymmetricCategory
            (HomotopyCategory (ModuleCat.{u} R) (ComplexShape.up ℤ)),
          letI := sK
          Nonempty
            (HomotopyCategory.quotient (ModuleCat.{u} R) (ComplexShape.up ℤ)).Braided
Tag 064J, a lemma

Tag 064J in the Stacks Project.

TotalTensorComplex.tleft_isTriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TensorComplex/Monoidal.lean, line 260.

Tensoring on the left with a fixed complex and totalizing is an exact functor of triangulated categories on the homotopy category.

Stated for an arbitrary preadditive monoidal category whose tensor product is additive in each variable, which is the generality the statement holds in. Module categories are the case of interest, at any module universe: the instances above hold for ModuleCat.{max u v} R as well as for ModuleCat.{u} R.

public theorem tleft_isTriangulated (G : CochainComplex C ℤ) :
    ∃ e : (Tleft G).CommShift ℤ,
      @Functor.IsTriangulated _ _ _ _ _ _ (Tleft G) e _ _ _ _ _ _ _ _

TotalTensorComplex.tright_isTriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TensorComplex/Monoidal.lean, line 269.

Tensoring on the right with a fixed complex and totalizing is an exact functor of triangulated categories on the homotopy category. This is genuinely distinct from tleft_isTriangulated: the two differ by the Koszul sign in the commutativity constraint.

public theorem tright_isTriangulated (G : CochainComplex C ℤ) :
    ∃ e : (Tright G).CommShift ℤ,
      @Functor.IsTriangulated _ _ _ _ _ _ (Tright G) e _ _ _ _ _ _ _ _
Sources
LeanTotalTensorComplex.cochainComplex_symmetricMonoidalCategory · TotalTensorComplex.tensorTotal_preserves_homotopy_and_descends · TotalTensorComplex.homotopyCategory_symmetricMonoidalCategory · TotalTensorComplex.tleft_isTriangulated · TotalTensorComplex.tright_isTriangulated

Section15.60 Derived tensor product#

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

Tag 06XZ, a definition

Tag 06XZ in the Stacks Project.

CochainComplex.KFlat, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/KFlat.lean, line 49.

A cochain complex K of R-modules is K-flat if the total complex Tot(M ⊗_R K) is acyclic for every acyclic cochain complex M of R-modules. Here ⊗ is the monoidal product of cochain complexes, i.e. the total complex of the tensor product double complex with the Koszul sign convention.

def CochainComplex.KFlat (K : CochainComplex (ModuleCat.{max u v} R) ℤ) : Prop
Tag 06Y0, a lemma

Tag 06Y0 in the Stacks Project.

CochainComplex.KFlat.kFlat_tright_preserves_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KFlat/QuasiIso.lean, line 60.

Tensoring with a K-flat complex and taking the total complex preserves quasi-isomorphisms in the homotopy category.

public theorem kFlat_tright_preserves_quasiIso {R : Type u} [CommRing R]
    (K : CochainComplex (ModuleCat.{max u v} R) ℤ) (hK : K.KFlat) :
    HomotopyCategory.quasiIso (ModuleCat.{max u v} R) (ComplexShape.up ℤ) ≤
      (HomotopyCategory.quasiIso (ModuleCat.{max u v} R) (ComplexShape.up ℤ)).inverseImage
        (Tright K)
Tag 06Y1, a lemma

Tag 06Y1 in the Stacks Project.

CochainComplex.KFlat.ScalarBaseChange.kFlat_extendScalars, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KFlat/ScalarBaseChange.lean, line 693.

Stacks 06Y1. Extension of scalars along φ : R →+* R' carries a K-flat complex of R-modules to a K-flat complex of R'-modules: tensoring over R' with the base change is, after restriction of scalars, tensoring over R, and restriction of scalars reflects acyclicity.

The two rings inhabit independent universes uR and uA, as they do in the source, where they are related only by a ring map; the module universe max v uR uA is independent of both and large enough to hold the modules of either ring. CochainComplex.kFlat_baseChange in StacksFrontier.Homology.KFlat.BaseChange is the specialization of this statement to a single common universe.

public lemma kFlat_extendScalars (φ : R →+* R')
    (K : CochainComplex (ModuleCat.{max v uR uA} R) ℤ)
    (hK : CochainComplex.KFlat.{uR, max v uA} K) :
    CochainComplex.KFlat.{uA, max v uR} ((extendScalarsLarge.{v, uR, uA} φ).obj K)
Tag 0795, a lemma

Tag 0795 in the Stacks Project.

CochainComplex.KFlat.tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KFlat/Basic.lean, line 629.

(Stacks tag 0795, Lemma 15.60.4) If K and L are K-flat complexes of R-modules, then Tot(K ⊗_R L) (i.e. the monoidal tensor product K ⊗ L) is K-flat.

For acyclic M, K-flatness of K makes M ⊗ K acyclic, then K-flatness of L makes (M ⊗ K) ⊗ L acyclic, and acyclicity transfers to M ⊗ (K ⊗ L) across the associator.

theorem CochainComplex.KFlat.tensor (K L : CochainComplex (ModuleCat R) ℤ)
    (hK : K.KFlat) (hL : L.KFlat) : (K ⊗ L).KFlat
Tag 06Y2, a lemma

Tag 06Y2 in the Stacks Project.

CochainComplex.KFlat.kFlat_two_out_of_three_of_distTriang, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KFlat/Triangle.lean, line 52.

K-flatness is a two-out-of-three property in a distinguished triangle of the homotopy category.

theorem kFlat_two_out_of_three_of_distTriang
    {R : Type u} [CommRing R] {K₁ K₂ K₃ : CochainComplex (ModuleCat.{u} R) ℤ}
    (f : (HomotopyCategory.quotient (ModuleCat.{u} R) (ComplexShape.up ℤ)).obj K₁ ⟶
      (HomotopyCategory.quotient (ModuleCat.{u} R) (ComplexShape.up ℤ)).obj K₂)
    (g : (HomotopyCategory.quotient (ModuleCat.{u} R) (ComplexShape.up ℤ)).obj K₂ ⟶
      (HomotopyCategory.quotient (ModuleCat.{u} R) (ComplexShape.up ℤ)).obj K₃)
    (h : (HomotopyCategory.quotient (ModuleCat.{u} R) (ComplexShape.up ℤ)).obj K₃ ⟶
      ((HomotopyCategory.quotient (ModuleCat.{u} R) (ComplexShape.up ℤ)).obj K₁)⟦(1 : ℤ)⟧)
    (hT : Triangle.mk f g h ∈
      distTriang (HomotopyCategory (ModuleCat.{u} R) (ComplexShape.up ℤ))) :
    (K₂.KFlat → K₃.KFlat → K₁.KFlat) ∧
      (K₁.KFlat → K₃.KFlat → K₂.KFlat) ∧
      (K₁.KFlat → K₂.KFlat → K₃.KFlat)
Tag 0BYH, a lemma

Tag 0BYH in the Stacks Project.

KFlatTwoOutOfThree.kFlat_two_out_of_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KFlat/Basic.lean, line 544.

Two-out-of-three for K-flatness (Stacks Tag 0BYH, Lemma 15.60.6). Given a short exact sequence of complexes 0 → K₁ → K₂ → K₃ → 0 with every K₃^n flat, if at least two of K₁, K₂, K₃ are K-flat, then all three are.

Case analysis on the disjunction h, completing the missing third K-flatness via the corresponding directional lemma.

theorem kFlat_two_out_of_three {R : Type u} [CommRing R] (S : ShortComplex (Cx R))
    (hse : S.ShortExact) (hflat : ∀ n : ℤ, Module.Flat R (S.X₃.X n))
    (h : (CochainComplex.KFlat S.X₁ ∧ CochainComplex.KFlat S.X₂) ∨
          (CochainComplex.KFlat S.X₁ ∧ CochainComplex.KFlat S.X₃) ∨
          (CochainComplex.KFlat S.X₂ ∧ CochainComplex.KFlat S.X₃)) :
    CochainComplex.KFlat S.X₁ ∧ CochainComplex.KFlat S.X₂ ∧ CochainComplex.KFlat S.X₃
Tag 064K, a lemma

Tag 064K in the Stacks Project.

CochainComplex.KFlat.kFlat_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KFlat/Flat.lean, line 510. References: SGA 4 XVII (4.1.7), “(ii), modules over ring”.

Stacks 064K. A bounded above cochain complex of flat modules is K-flat.

public theorem kFlat_of_flat {R : Type u} [CommRing R]
    (P : CochainComplex (ModuleCat.{max u v} R) ℤ) (d : ℤ) [P.IsStrictlyLE d]
    [∀ n : ℤ, Module.Flat R (P.X n)] :
    P.KFlat
Tag 06Y3, a lemma

Tag 06Y3 in the Stacks Project.

CochainComplex.KFlat.kFlat_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KFlat/Flat.lean, line 543.

A filtered colimit of K-flat complexes of modules is K-flat.

public theorem kFlat_colimit {R : Type u} [CommRing R]
    {J : Type v} [Category.{w} J] [Small.{max u x} J] [LocallySmall.{max u x} J] [IsFiltered J]
    (K : J ⥤ CochainComplex (ModuleCat.{max u x} R) ℤ)
    (hK : ∀ j, (K.obj j).KFlat) : (colimit K).KFlat
Tag 0E8F, a lemma

Tag 0E8F in the Stacks Project.

CochainComplex.KFlat.kFlat_of_tensor_finitelyPresented_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KFlat/FinitelyPresented.lean, line 534.

Stacks 0E8F. A cochain complex whose tensor product with every finitely presented module is acyclic is K-flat.

public theorem kFlat_of_tensor_finitelyPresented_acyclic {R : Type u} [CommRing R]
    (K : CochainComplex (ModuleCat.{u} R) ℤ)
    (hK : ∀ M : ModuleCat.{u} R, Module.FinitePresentation R M →
      (K ⊗ (HomologicalComplex.single (ModuleCat.{u} R) (ComplexShape.up ℤ) 0).obj M).Acyclic) :
    K.KFlat
Tag 06Y4, a lemma

Tag 06Y4 in the Stacks Project.

CochainComplex.KFlat.exists_kFlat_resolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KFlat/Resolution.lean, line 126.

Stacks 06Y4. Every cochain complex of modules admits a termwise-surjective quasi-isomorphism from a K-flat complex with flat terms.

theorem exists_kFlat_resolution {R : Type u} [CommRing R]
    (M : CochainComplex (ModuleCat.{max u v} R) ℤ) :
    ∃ (K : CochainComplex (ModuleCat.{max u v} R) ℤ) (f : K ⟶ M),
      K.KFlat ∧
        (∀ n : ℤ, Module.Flat R (K.X n)) ∧
        QuasiIso f ∧
        ∀ n : ℤ, Function.Surjective (f.f n).hom
Tag 09PB, a remark

Tag 09PB in the Stacks Project.

CochainComplex.KFlat.property_of_coproducts_of_two_out_of_three_of_shifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KFlat/FilteredColimitShifts.lean, line 1375.

Every complex has a split filtered resolution whose graded pieces are coproducts of shifts of the ring and whose filtration yields the canonical telescope triangle. Moreover, a property of objects of D(R) that is preserved by coproducts, satisfies two-out-of-three for distinguished triangles, and holds for every shift of R, holds for every object of D(R).

theorem property_of_coproducts_of_two_out_of_three_of_shifts {R : Type u} [Ring R]
    [Small.{v} R] :
    (∀ M : CochainComplex (ModuleCat.{v} R) ℤ, Nonempty (SplitFilteredFreeResolution M)) ∧
      ∀ (T : DerivedCategory (ModuleCat.{v} R) → Prop),
        (∀ {I : Type v} (K : I → DerivedCategory (ModuleCat.{v} R)) [HasCoproduct K],
          (∀ i, T (K i)) → T (∐ K)) →
        (∀ (Δ : Triangle (DerivedCategory (ModuleCat.{v} R))),
          Δ ∈ distinguishedTriangles →
            (T Δ.obj₁ → T Δ.obj₂ → T Δ.obj₃) ∧
            (T Δ.obj₁ → T Δ.obj₃ → T Δ.obj₂) ∧
            (T Δ.obj₂ → T Δ.obj₃ → T Δ.obj₁)) →
        (∀ k : ℤ, T (((DerivedCategory.singleFunctor (ModuleCat.{v} R) 0).obj
          (ModuleCat.of R (Shrink.{v} R)))⟦k⟧)) →
        ∀ K, T K
Tag 064L, a lemma

Tag 064L in the Stacks Project.

CochainComplex.DerivedTensor.quasiIso_trightCochain_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/DerivedTensorKFlatResolution.lean, line 124.

A quasi-isomorphism between K-flat complexes remains a quasi-isomorphism after tensoring on the right with any complex. This is the companion of quasiIso_tleftCochain_map (Stacks 064L), whose fixed factor is the left one.

theorem quasiIso_trightCochain_map
    {P Q : CochainComplex (ModuleCat.{max u v} R) ℤ} (α : P ⟶ Q) [QuasiIso α]
    (hP : P.KFlat) (hQ : Q.KFlat) (L : CochainComplex (ModuleCat.{max u v} R) ℤ) :
    QuasiIso ((TrightCochain L).map α)

CochainComplex.DerivedTensor.quasiIso_tleftCochain_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/DerivedTensorLargeUniverse.lean, line 200.

A quasi-isomorphism between K-flat complexes remains a quasi-isomorphism after tensoring on the left with any complex and taking the total complex.

public theorem quasiIso_tleftCochain_map {R : Type u} [CommRing R]
    {P Q : CochainComplex (ModuleCat.{max u v} R) ℤ} (α : P ⟶ Q) [QuasiIso α]
    (hP : P.KFlat) (hQ : Q.KFlat) (L : CochainComplex (ModuleCat.{max u v} R) ℤ) :
    QuasiIso ((TleftCochain L).map α)
Tag 064M, a definition

Tag 064M in the Stacks Project.

CochainComplex.DerivedTensor.derivedTensorProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/DerivedTensorFunctorLargeUniverse.lean, line 63. References: SGA 4 XVII (4.1.7), “(i), modules over ring”.

The derived tensor product with M, computed by a K-flat resolution of a representative of M.

public noncomputable def derivedTensorProduct
    (M : DerivedCategory (ModuleCat.{max u v} R)) :
    DerivedCategory (ModuleCat.{max u v} R) ⥤ DerivedCategory (ModuleCat.{max u v} R)

CochainComplex.DerivedTensor.derivedTensorProduct_commShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/DerivedTensorFunctorLargeUniverse.lean, line 79.

The derived tensor product commutes with the shift functors.

public noncomputable instance derivedTensorProduct_commShift
    (M : DerivedCategory (ModuleCat.{max u v} R)) :
    (derivedTensorProduct M).CommShift ℤ

CochainComplex.DerivedTensor.derivedTensorProduct_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/DerivedTensorFunctorLargeUniverse.lean, line 100.

The derived tensor product is an exact functor of triangulated categories.

public noncomputable instance derivedTensorProduct_isTriangulated
    (M : DerivedCategory (ModuleCat.{max u v} R)) :
    (derivedTensorProduct M).IsTriangulated

CochainComplex.DerivedTensor.derivedTensorProduct_iso_lift_of_kFlat_resolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/DerivedTensorFunctorLargeUniverse.lean, line 207.

A K-flat resolution of any representative of M computes the derived tensor product. The comparison is a natural isomorphism, uniquely determined by its pullback to the homotopy category.

public theorem derivedTensorProduct_iso_lift_of_kFlat_resolution
    (M : DerivedCategory (ModuleCat.{max u v} R))
    (P K : CochainComplex (ModuleCat.{max u v} R) ℤ) (f : K ⟶ P) [QuasiIso f]
    (hK : K.KFlat)
    (_eP : (DerivedCategory.Qh (C := ModuleCat.{max u v} R)).obj
      ((HomotopyCategory.quotient (ModuleCat.{max u v} R) (ComplexShape.up ℤ)).obj P) ≅ M) :
    let W := HomotopyCategory.quasiIso (ModuleCat.{max u v} R) (ComplexShape.up ℤ)
    let F := Tright K ⋙ DerivedCategory.Qh
    let hF : W.IsInvertedBy F := fun _ _ g hg ↦
      Localization.inverts DerivedCategory.Qh W _
        (CochainComplex.KFlat.kFlat_tright_preserves_quasiIso K hK g hg)
    let F' := Localization.lift F hF DerivedCategory.Qh
    Nonempty (DerivedCategory.Qh ⋙ derivedTensorProduct M ≅ F) ∧
      ∀ α : DerivedCategory.Qh ⋙ derivedTensorProduct M ≅ F,
        ∃! e : derivedTensorProduct M ≅ F',
          Functor.isoWhiskerLeft DerivedCategory.Qh e =
            α ≪≫ (Localization.fac F hF DerivedCategory.Qh).symm
Tag 0BYI, a lemma

Tag 0BYI in the Stacks Project.

CochainComplex.DerivedTensor.canonicalSymmetricDerivedTensorProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/DerivedTensor.lean, line 754.

Stacks 0BYI. The canonical derived tensor product, equipped with its symmetry functorial in both complexes and represented on K-flat complexes in degrees p and q by the ordinary tensor braiding with the sign (-1) ^ (p * q).

public noncomputable def canonicalSymmetricDerivedTensorProduct
    (R : Type u) [CommRing R]
    [HasDerivedCategory (ModuleCat.{u} R)] : SymmetricDerivedTensorProduct R
Tag 0BYJ, a lemma

Tag 0BYJ in the Stacks Project.

CochainComplex.DerivedTensor.derivedTensorProduct_associator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/DerivedTensor.lean, line 1066.

Stacks 0BYJ. The derived tensor product is associative up to a canonical isomorphism, functorial in all three complexes. On K-flat representatives this is the standard associator of tensor products of complexes.

public theorem derivedTensorProduct_associator
    (R : Type u) [CommRing R] [HasDerivedCategory (ModuleCat.{u} R)] :
    let D := DerivedCategory (ModuleCat.{u} R)
    let C := CochainComplex (ModuleCat.{u} R) ℤ
    let Q := DerivedCategory.Q (C := ModuleCat.{u} R)
    let T := canonicalDerivedTensorProduct R
    ∃ associator : ∀ K L M : D,
          (T.tensor.obj ((T.tensor.obj K).obj L)).obj M ≅
            (T.tensor.obj K).obj ((T.tensor.obj L).obj M),
        (∀ {K K' L L' M M' : D} (f : K ⟶ K') (g : L ⟶ L') (h : M ⟶ M'),
          (T.tensor.map ((T.tensor.map f).app L ≫ (T.tensor.obj K').map g)).app M ≫
                (T.tensor.obj ((T.tensor.obj K').obj L')).map h ≫
                (associator K' L' M').hom =
            (associator K L M).hom ≫
              (T.tensor.map f).app ((T.tensor.obj L).obj M) ≫
              (T.tensor.obj K').map
                ((T.tensor.map g).app M ≫ (T.tensor.obj L').map h)) ∧
        ∀ (K L M : C) (hK : K.KFlat) (hL : L.KFlat) (hM : M.KFlat),
          let hKL := CochainComplex.KFlat.tensor R K L hK hL
          let hLM := CochainComplex.KFlat.tensor R L M hL hM
          (associator (Q.obj K) (Q.obj L) (Q.obj M)).hom ≫
                (T.tensor.obj (Q.obj K)).map (T.comparison L M hL hM).hom ≫
                (T.comparison K (L ⊗ M) hK hLM).hom =
            (T.tensor.map (T.comparison K L hK hL).hom).app (Q.obj M) ≫
              (T.comparison (K ⊗ L) M hKL hM).hom ≫
              Q.map (HomologicalComplex.associator K L M).hom
Tag 0G6M, a lemma

Tag 0G6M in the Stacks Project.

CochainComplex.KFlat.exists_kFlat_factorization_up_to_homotopy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/KFlat/Resolution.lean, line 310.

A morphism from a K-flat complex factors up to homotopy through another K-flat complex which maps to the target by a quasi-isomorphism. When the source has flat terms, the intermediate complex can be chosen with flat terms.

theorem exists_kFlat_factorization_up_to_homotopy
    {R : Type u} [CommRing R] {K L : CochainComplex (ModuleCat.{u} R) ℤ} (a : K ⟶ L)
    (hK : K.KFlat) :
    ∃ (N : CochainComplex (ModuleCat.{u} R) ℤ) (b : K ⟶ N) (c : N ⟶ L),
      N.KFlat ∧
        QuasiIso c ∧
        Nonempty (Homotopy a (b ≫ c)) ∧
        ((∀ n : ℤ, Module.Flat R (K.X n)) → ∀ n : ℤ, Module.Flat R (N.X n))
Sources
LeanCochainComplex.KFlat · CochainComplex.KFlat.kFlat_tright_preserves_quasiIso · CochainComplex.KFlat.ScalarBaseChange.kFlat_extendScalars · CochainComplex.KFlat.tensor · CochainComplex.KFlat.kFlat_two_out_of_three_of_distTriang · KFlatTwoOutOfThree.kFlat_two_out_of_three · CochainComplex.KFlat.kFlat_of_flat · CochainComplex.KFlat.kFlat_colimit

Section15.61 Derived change of rings#

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

Tag 06Y6, a lemma

Tag 06Y6 in the Stacks Project.

CochainComplex.DerivedTensor.canonicalDerivedTensorChangeOfRings, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/DerivedChangeOfRings.lean, line 1057.

The derived tensor product - ⊗ᴸ_R N from D(R) to D(A), with derived extension of scalars, derived tensoring over A and the change-of-rings isomorphism normalized by their counits.

public noncomputable def canonicalDerivedTensorChangeOfRings
    {R : Type uR} {A : Type uA} [CommRing R] [CommRing A] (f : R →+* A)
    (N : CochainComplex (ModuleCat.{max v uR uA} A) ℤ)
    [HasDerivedCategory.{wR} (ModuleCat.{max v uR uA} R)]
    [HasDerivedCategory.{wA} (ModuleCat.{max v uR uA} A)] :
    DerivedTensorChangeOfRings f N
Tag 0BYK, a lemma

Tag 0BYK in the Stacks Project.

CochainComplex.DerivedTensor.exists_derivedTensorNatTrans_isIso_of_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/DerivedTensorFunctoriality.lean, line 115.

A map f : L ⟶ N of complexes of A-modules induces a natural transformation 1 ⊗ᴸ f between any chosen left-derived models of the change-of-rings tensor functors - ⊗ᴸ_R L and - ⊗ᴸ_R N. The compatibility equation says that this is the transformation induced by the ordinary tensor map 1 ⊗ f. If f is a quasi-isomorphism, the induced transformation is an isomorphism of functors.

The source ring universe uR, the target ring universe uA and the module universe are mutually independent: the two rings are related by nothing but φ, and the modules of both rings have to fit in one category, so they live at max v uR uA.

public theorem exists_derivedTensorNatTrans_isIso_of_quasiIso
    {R : Type uR} {A : Type uA} [CommRing R] [CommRing A] (φ : R →+* A)
    {L N : CochainComplex (ModuleCat.{max v uR uA} A) ℤ}
    (f : L ⟶ N)
    (FL FN : DerivedCategory (ModuleCat.{max v uR uA} R) ⥤
      DerivedCategory (ModuleCat.{max v uR uA} A))
    (αL : DerivedCategory.Q ⋙ FL ⟶
      (extendScalarsLarge.{v, uR, uA} φ ⋙ tensorRightLarge.{uA, max v uR} L) ⋙
        DerivedCategory.Q)
    (αN : DerivedCategory.Q ⋙ FN ⟶
      (extendScalarsLarge.{v, uR, uA} φ ⋙ tensorRightLarge.{uA, max v uR} N) ⋙
        DerivedCategory.Q)
    [CategoryTheory.Functor.IsLeftDerivedFunctor FL αL
      (HomologicalComplex.quasiIso (ModuleCat.{max v uR uA} R) (ComplexShape.up ℤ))]
    [CategoryTheory.Functor.IsLeftDerivedFunctor FN αN
      (HomologicalComplex.quasiIso (ModuleCat.{max v uR uA} R) (ComplexShape.up ℤ))] :
    letI : MonoidalCategoryStruct (ModuleCat.{max v uR uA} A) :=
      ModuleCat.liftedModuleMonoidalStruct.{uA, max v uR}
    letI : MonoidalCategory (ModuleCat.{max v uR uA} A) :=
      ModuleCat.liftedModuleMonoidal.{uA, max v uR}
    let tensorMap :
        (extendScalarsLarge.{v, uR, uA} φ ⋙ tensorRightLarge.{uA, max v uR} L) ⋙
            DerivedCategory.Q ⟶
          (extendScalarsLarge.{v, uR, uA} φ ⋙ tensorRightLarge.{uA, max v uR} N) ⋙
            DerivedCategory.Q :=
      CategoryTheory.Functor.whiskerRight
        (CategoryTheory.Functor.whiskerLeft (extendScalarsLarge.{v, uR, uA} φ)
          ((CategoryTheory.MonoidalCategory.curriedTensor
            (ModuleCat.{max v uR uA} A)).map₂CochainComplex.flip.map f))
        DerivedCategory.Q
    ∃ t : FL ⟶ FN,
      CategoryTheory.Functor.whiskerLeft DerivedCategory.Q t ≫ αN = αL ≫ tensorMap ∧
        (HomologicalComplex.quasiIso (ModuleCat.{max v uR uA} A) (ComplexShape.up ℤ) f →
          IsIso t)
Tag 0GMT, a lemma

Tag 0GMT in the Stacks Project.

CochainComplex.DerivedExtensionScalars.derivedExtensionScalarsAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/DerivedChangeOfRingsAdjunction.lean, line 99.

Stacks 0GMT. Derived extension of scalars along a homomorphism of commutative rings is left adjoint to derived restriction of scalars. The extension functor may be any model equipped with the total-left-derived universal property, since uniqueness of left derived functors identifies it with the model computed by K-flat resolutions.

public def derivedExtensionScalarsAdjunction
    {R : Type uR} {A : Type uA} [CommRing R] [CommRing A] (f : R →+* A)
    [HasDerivedCategory.{wR} (ModuleCat.{max uR uA uM} R)]
    [HasDerivedCategory.{wA} (ModuleCat.{max uR uA uM} A)] :
    letI : (ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).IsLeftAdjoint :=
      (ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
    letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsRightAdjoint :=
      (ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isRightAdjoint
    letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsLeftAdjoint :=
      (ModuleCat.restrictCoextendScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
    ∀ (F : CategoryTheory.Functor (DerivedCategory (ModuleCat.{max uR uA uM} R))
      (DerivedCategory (ModuleCat.{max uR uA uM} A)))
    (comparison : DerivedCategory.Q ⋙ F ⟶
      (ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).mapHomologicalComplex
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    [F.IsLeftDerivedFunctor comparison
      (HomologicalComplex.quasiIso (ModuleCat.{max uR uA uM} R) (ComplexShape.up ℤ))],
    F ⊣ (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).mapDerivedCategory
Tag 08YT, a remark

Tag 08YT in the Stacks Project.

CochainComplex.DerivedChangeOfRings.derivedTensorModuleStructuresDiffer, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/ChangeOfRings.lean, line 574.

In the example R = k[x,y], A = R/(xy), and N = R/(x), the objects N_R ⊗_R^ᴸ A and N ⊗_R^ᴸ A_R of D(A) are not isomorphic. The returned data includes the two displayed K-flat resolutions and augmentations, their quasi-isomorphism certificates, and the canonical identifications with A → A and N[1] ⊕ N.

public noncomputable def derivedTensorModuleStructuresDiffer
    (k : Type u) [CommRing k] [Nontrivial k] :
    DerivedTensorComparison k
Tag 08YU, a lemma

Tag 08YU in the Stacks Project.

CochainComplex.DerivedTensor.IteratedChangeOfRings.derivedTensorProduct_doubleBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/IteratedDerivedChangeOfRings.lean, line 1174.

Canonical associativity of derived change of rings, with its signed interchange. The ordinary maps send (x ⊗ n) ⊗ k to x ⊗ (n ⊗ k) and to (-1)^(deg n * deg k) (x ⊗ k) ⊗ n, respectively. These equations and the specified counits of DerivedTensorChangeOfRings fix the derived comparisons, including for nonflat N and K.

rightFactor identifies the complex used by together with N ⊗ᴸ_B K; baseFactor identifies the second signed factor with N ⊗ᴸ_B C. The final isomorphism to extension of scalars followed by tensoring is exactly the change-of-rings projection. All comparisons are natural in the object of D(A).

public theorem derivedTensorProduct_doubleBaseChange
    {A : Type uA} {B : Type uB} {C : Type uC} [CommRing A] [CommRing B] [CommRing C]
    (f : A →+* B) (g : B →+* C)
    (N : CochainComplex (ModuleCat.{max v uA uB uC} B) ℤ)
    (K : CochainComplex (ModuleCat.{max v uA uB uC} C) ℤ) :
    let Q_A := DerivedCategory.Q (C := ModuleCat.{max v uA uB uC} A)
    let Q_B := DerivedCategory.Q (C := ModuleCat.{max v uA uB uC} B)
    let Q_C := DerivedCategory.Q (C := ModuleCat.{max v uA uB uC} C)
    let W_A := HomologicalComplex.quasiIso
      (ModuleCat.{max v uA uB uC} A) (ComplexShape.up ℤ)
    let PN := CochainComplex.KFlat.chosenResolution.{uB, max v uA uC} N
    let LK := CochainComplex.KFlat.chosenResolution.{uC, max v uA uB} K
    let AN := canonicalDerivedTensorChangeOfRings.{uA, uB, max v uA uB uC} f N
    let AP := canonicalDerivedTensorChangeOfRings.{uA, uB, max v uA uB uC} f PN.complex
    let BK := canonicalDerivedTensorChangeOfRings.{uB, uC, max v uA uB uC} g K
    let BL := canonicalDerivedTensorChangeOfRings.{uB, uC, max v uA uB uC} g LK.complex
    let AC := canonicalDerivedTensorChangeOfRings.{uA, uC, max v uA uB uC}
      (g.comp f) (BL.directTensor.obj PN.complex)
    let AL := canonicalDerivedTensorChangeOfRings.{uA, uC, max v uA uB uC}
      (g.comp f) LK.complex
    let AK := canonicalDerivedTensorChangeOfRings.{uA, uC, max v uA uB uC} (g.comp f) K
    let CP := canonicalDerivedTensorChangeOfRings.{uC, uC, max v uA uB uC}
      (RingHom.id C)
      ((extendScalarsLarge.{max v uA uB uC, uB, uC} g).obj PN.complex)
    let iterated := AN.F ⋙ BK.F
    let together := AC.F
    let signed := AK.F ⋙ CP.F
    ∃ (replaceN : AP.F ≅ AN.F) (replaceK : BL.F ≅ BK.F) (replaceAK : AL.F ≅ AK.F),
      replaceN.hom = AP.map AN PN.π ∧
      replaceK.hom = BL.map BK LK.π ∧
      replaceAK.hom = AL.map AK LK.π ∧
      ∃ (rightFactor : BK.F.obj (Q_B.obj N) ≅ Q_C.obj (BL.directTensor.obj PN.complex))
        (baseFactor : BK.B.obj (Q_B.obj N) ≅
          Q_C.obj ((extendScalarsLarge.{max v uA uB uC, uB, uC} g).obj PN.complex)),
        BL.F.map (Q_B.map PN.π) ≫ replaceK.hom.app (Q_B.obj N) ≫ rightFactor.hom =
          BL.alphaF.app PN.complex ∧
        BK.B.map (Q_B.map PN.π) ≫ baseFactor.hom = BK.alphaB.app PN.complex ∧
        ∃ (ordinaryAssociator : AP.directTensor ⋙ BL.directTensor ≅ AC.directTensor)
          (ordinaryInterchange : AP.directTensor ⋙ BL.directTensor ≅
            AL.directTensor ⋙ CP.directTensor),
          (∀ (M : CochainComplex (ModuleCat.{max v uA uB uC} A) ℤ)
              (i j k : ℤ) (x : M.X i) (n : PN.complex.X j) (l : LK.complex.X k),
            (ordinaryAssociator.hom.app M).f ((i + j) + k)
                (BL.tensorElement (AP.directTensor.obj M) (i + j) k ((i + j) + k) rfl
                  (AP.tensorElement M i j (i + j) rfl x n) l) =
              AC.tensorElement M i (j + k) ((i + j) + k) (by omega) x
                (BL.tensorElement PN.complex j k (j + k) rfl n l)) ∧
          (∀ (M : CochainComplex (ModuleCat.{max v uA uB uC} A) ℤ)
              (i j k : ℤ) (x : M.X i) (n : PN.complex.X j) (l : LK.complex.X k),
            (ordinaryInterchange.hom.app M).f ((i + j) + k)
                (BL.tensorElement (AP.directTensor.obj M) (i + j) k ((i + j) + k) rfl
                  (AP.tensorElement M i j (i + j) rfl x n) l) =
              (-1 : C) ^ (j * k).natAbs •
                CP.tensorElement (AL.directTensor.obj M) (i + k) j ((i + j) + k)
                  (by omega) (AL.tensorElement M i k (i + k) rfl x l)
                  ((1 : C) ⊗ₜ[B,g] n)) ∧
          let replaceIterated := Functor.isoWhiskerRight replaceN BL.F ≪≫
            Functor.isoWhiskerLeft AN.F replaceK
          let replaceSigned := Functor.isoWhiskerRight replaceAK CP.F
          let direct := (AP.directTensor ⋙ BL.directTensor) ⋙ Q_C
          let iteratedComparison : Q_A ⋙ iterated ⟶ direct :=
            Functor.whiskerLeft Q_A replaceIterated.inv ≫ compositeCounit.{uA, uB, uC, v} AP BL
          let togetherComparison : Q_A ⋙ together ⟶ direct :=
            AC.alphaF ≫ Functor.whiskerRight ordinaryAssociator.inv Q_C
          let signedCounit := Functor.whiskerLeft Q_A replaceSigned.inv ≫
            compositeCounit.{uA, uC, uC, max v uB} AL CP
          iterated.IsLeftDerivedFunctor iteratedComparison W_A ∧
          together.IsLeftDerivedFunctor togetherComparison W_A ∧
          ∃ (doubleBaseChange : iterated ≅ together)
            (signedComparison : iterated ≅ signed)
            (baseChangeComparison : iterated ≅ AC.B ⋙ AC.G),
            Functor.whiskerLeft Q_A doubleBaseChange.hom ≫ togetherComparison =
              iteratedComparison ∧
            (∀ e : iterated ≅ together,
              Functor.whiskerLeft Q_A e.hom ≫ togetherComparison = iteratedComparison →
                e = doubleBaseChange) ∧
            Functor.whiskerLeft Q_A signedComparison.hom ≫ signedCounit =
              iteratedComparison ≫ Functor.whiskerRight ordinaryInterchange.hom Q_C ∧
            (∀ e : iterated ≅ signed,
              Functor.whiskerLeft Q_A e.hom ≫ signedCounit =
                iteratedComparison ≫ Functor.whiskerRight ordinaryInterchange.hom Q_C →
                  e = signedComparison) ∧
            baseChangeComparison = doubleBaseChange ≪≫ AC.changeOfRings
Sources
LeanCochainComplex.DerivedTensor.canonicalDerivedTensorChangeOfRings · CochainComplex.DerivedTensor.exists_derivedTensorNatTrans_isIso_of_quasiIso · CochainComplex.DerivedExtensionScalars.derivedExtensionScalarsAdjunction · CochainComplex.DerivedChangeOfRings.derivedTensorModuleStructuresDiffer · CochainComplex.DerivedTensor.IteratedChangeOfRings.derivedTensorProduct_doubleBaseChange

Section15.62 Tor independence#

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

Tag 065Z, an equation

Tag 065Z in the Stacks Project.

RingTheory.TorIndependence.canonicalBaseChangeComparison_paste, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/BaseChangeIndependence/ComparisonPasting.lean, line 457. The attribute's comment: “the comparison of a horizontal composite of two commutative squares of rings is the composite of the two comparisons, read through the composition isomorphisms of derived extension of scalars; this is what compatibility of the comparison with localizing a square amounts to”.

The pasting law of Tag 065Z. For two commutative squares of commutative rings stacked on top of one another, the comparison of the outer square agrees with the comparison of the lower square, extended along the upper left map, followed by the comparison of the upper square — both read through the composition isomorphisms of derived extension of scalars.

Both sides are determined by the same counit equation at K-flat complexes, so the identity reduces to the underived comparison on pure tensors.

public theorem canonicalBaseChangeComparison_paste
    (f : R →+* A) (g₁ : R →+* R') (h₁ : A →+* A') (i₁ : R' →+* A')
    (g₂ : R' →+* R'') (h₂ : A' →+* A'') (i₂ : R'' →+* A'')
    (sq₁ : h₁.comp f = i₁.comp g₁) (sq₂ : h₂.comp i₁ = i₂.comp g₂)
    (X : DerivedCategory (ModuleCat.{u} A)) :
    (totalDerivedExtensionScalarsComp.{u, u} g₁ g₂).hom.app
        ((ModuleCat.restrictScalars.{u} f).mapDerivedCategory.obj X) ≫
      (canonicalBaseChangeComparison.{u, w} f (g₂.comp g₁) (h₂.comp h₁) i₂
        (comp_comp_eq_comp_comp f g₁ h₁ i₁ g₂ h₂ i₂ sq₁ sq₂)).app X =
    (totalDerivedExtensionScalars.{u, u, u} g₂).functor.map
        ((canonicalBaseChangeComparison.{u, w} f g₁ h₁ i₁ sq₁).app X) ≫
      (canonicalBaseChangeComparison.{u, w} i₁ g₂ h₂ i₂ sq₂).app
        ((totalDerivedExtensionScalars.{u, u, u} h₁).functor.obj X) ≫
      (ModuleCat.restrictScalars.{u} i₂).mapDerivedCategory.map
        ((totalDerivedExtensionScalarsComp.{u, u} h₁ h₂).hom.app X)

RingTheory.TorIndependence.canonicalBaseChangeComparison_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/BaseChangeIndependence/ComparisonPasting.lean, line 511. The attribute's comment: “the comparison is compatible with localizing a square at a prime: pasting a square with the localization square of its right-hand column composes the two comparisons”.

Tag 065Z is compatible with localizing a square at a prime. Pasting a commutative square of rings with the localization square of its right-hand column at a prime y of A' composes the two comparisons: the comparison of the square

R → A, R → R'_{y ∩ R'}, A → A'_y, R'_{y ∩ R'} → A'_y

is the comparison of the given square, extended along R' → R'_{y ∩ R'}, followed by the comparison of the localization square. This is RingTheory.TorIndependence.canonicalBaseChangeComparison_paste with the localization square as its second floor.

Note that the localization square is not a pushout square; Tag 065Z attaches a comparison to every commutative square, and that is all this uses.

public theorem canonicalBaseChangeComparison_localization
    (f : R →+* A) (g : R →+* R') (h : A →+* A') (i : R' →+* A')
    (sq : h.comp f = i.comp g) (y : Ideal A') [y.IsPrime]
    [HasDerivedCategory.{w} (ModuleCat.{u} (Localization.AtPrime (y.comap i)))]
    [HasDerivedCategory.{w} (ModuleCat.{u} (Localization.AtPrime y))]
    (X : DerivedCategory (ModuleCat.{u} A)) :
    (totalDerivedExtensionScalarsComp.{u, u} g
          (algebraMap R' (Localization.AtPrime (y.comap i)))).hom.app
        ((ModuleCat.restrictScalars.{u} f).mapDerivedCategory.obj X) ≫
      (canonicalBaseChangeComparison.{u, w} f
        ((algebraMap R' (Localization.AtPrime (y.comap i))).comp g)
        ((algebraMap A' (Localization.AtPrime y)).comp h)
        (Localization.localRingHom (y.comap i) y i rfl)
        (comp_comp_eq_comp_comp f g h i (algebraMap R' (Localization.AtPrime (y.comap i)))
          (algebraMap A' (Localization.AtPrime y))
          (Localization.localRingHom (y.comap i) y i rfl) sq
          (comp_algebraMap_eq_localRingHom_comp i y))).app X =
    (totalDerivedExtensionScalars.{u, u, u}
          (algebraMap R' (Localization.AtPrime (y.comap i)))).functor.map
        ((canonicalBaseChangeComparison.{u, w} f g h i sq).app X) ≫
      (canonicalBaseChangeComparison.{u, w} i
          (algebraMap R' (Localization.AtPrime (y.comap i)))
          (algebraMap A' (Localization.AtPrime y))
          (Localization.localRingHom (y.comap i) y i rfl)
          (comp_algebraMap_eq_localRingHom_comp i y)).app
        ((totalDerivedExtensionScalars.{u, u, u} h).functor.obj X) ≫
      (ModuleCat.restrictScalars.{u}
            (Localization.localRingHom (y.comap i) y i rfl)).mapDerivedCategory.map
        ((totalDerivedExtensionScalarsComp.{u, u} h
          (algebraMap A' (Localization.AtPrime y))).hom.app X)

RingTheory.TorIndependence.derivedBaseChangeComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/Independence.lean, line 1049.

Let R → A, R → R', A → A', and R' → A' be a commutative square of commutative rings. There is a natural comparison K ⊗ᴸ_R R' ⟶ K ⊗ᴸ_A A' in D(R').

The first component of the result is the underived comparison, normalized on pure tensors. The second is its canonical lift between any chosen models of the two total left-derived functors; the displayed factorization records canonicity as well as functoriality in K.

public noncomputable def derivedBaseChangeComparison
    {R : Type uR} {A : Type uA} {R' : Type uRp} {A' : Type uAp}
    [CommRing R] [CommRing A] [CommRing R'] [CommRing A']
    [HasDerivedCategory (ModuleCat.{max v uR uA uRp uAp} R)]
    [HasDerivedCategory (ModuleCat.{max v uR uA uRp uAp} A)]
    [HasDerivedCategory (ModuleCat.{max v uR uA uRp uAp} R')]
    [HasDerivedCategory (ModuleCat.{max v uR uA uRp uAp} A')]
    (f : R →+* A) (g : R →+* R') (h : A →+* A') (i : R' →+* A')
    (sq : h.comp f = i.comp g) :
    let Res_f := ModuleCat.restrictScalars.{max v uR uA uRp uAp} f
    let Res_i := ModuleCat.restrictScalars.{max v uR uA uRp uAp} i
    let Ext_g := ModuleCat.extendScalars.{uR, uRp, max v uR uA uRp uAp} g
    let Ext_h := ModuleCat.extendScalars.{uA, uAp, max v uR uA uRp uAp} h
    letI : (ModuleCat.restrictScalars.{max v uR uA uRp uAp} f).IsLeftAdjoint :=
      (ModuleCat.restrictCoextendScalarsAdj.{max v uR uA uRp uAp, uR, uA} f).isLeftAdjoint
    letI : (ModuleCat.restrictScalars.{max v uR uA uRp uAp} f).IsRightAdjoint :=
      (ModuleCat.extendRestrictScalarsAdj.{max v uR uA uRp uAp, uR, uA} f).isRightAdjoint
    letI : (ModuleCat.restrictScalars.{max v uR uA uRp uAp} i).IsLeftAdjoint :=
      (ModuleCat.restrictCoextendScalarsAdj.{max v uR uA uRp uAp, uRp, uAp} i).isLeftAdjoint
    letI : (ModuleCat.restrictScalars.{max v uR uA uRp uAp} i).IsRightAdjoint :=
      (ModuleCat.extendRestrictScalarsAdj.{max v uR uA uRp uAp, uRp, uAp} i).isRightAdjoint
    let F_R := Res_f ⋙ Ext_g
    let F_A := Ext_h ⋙ Res_i
    let U_g := Ext_g.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
      DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} R')
    let U_h := Ext_h.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
      DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} A')
    ∀ (L_g : DerivedCategory (ModuleCat.{max v uR uA uRp uAp} R) ⥤
          DerivedCategory (ModuleCat.{max v uR uA uRp uAp} R'))
      (L_h : DerivedCategory (ModuleCat.{max v uR uA uRp uAp} A) ⥤
          DerivedCategory (ModuleCat.{max v uR uA uRp uAp} A'))
      (alpha_g : DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} R) ⋙ L_g ⟶ U_g)
      (alpha_h : DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} A) ⋙ L_h ⟶ U_h),
      [L_g.IsLeftDerivedFunctor alpha_g
        (HomologicalComplex.quasiIso (ModuleCat.{max v uR uA uRp uAp} R) (ComplexShape.up ℤ))] →
      [L_h.IsLeftDerivedFunctor alpha_h
        (HomologicalComplex.quasiIso (ModuleCat.{max v uR uA uRp uAp} A) (ComplexShape.up ℤ))] →
      let DRes_f := Res_f.mapDerivedCategory
      let DRes_i := Res_i.mapDerivedCategory
      let beta_R :
          DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} A) ⋙ (DRes_f ⋙ L_g) ⟶
            F_R.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} R') :=
        (Functor.associator _ _ _).inv ≫
          Functor.whiskerRight Res_f.mapDerivedCategoryFactors.hom L_g ≫
          (Functor.associator _ _ _).hom ≫
          Functor.whiskerLeft (Res_f.mapHomologicalComplex (ComplexShape.up ℤ)) alpha_g ≫
          (Functor.associator _ _ _).inv ≫
          Functor.whiskerRight
            (Functor.mapHomologicalComplexCompIso (Iso.refl F_R)
              (ComplexShape.up ℤ)).hom
            (DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} R'))
      let beta_A :
          DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} A) ⋙ (L_h ⋙ DRes_i) ⟶
            F_A.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} R') :=
        (Functor.associator _ _ _).inv ≫
          Functor.whiskerRight alpha_h DRes_i ≫
          (Functor.associator _ _ _).hom ≫
          Functor.whiskerLeft (Ext_h.mapHomologicalComplex (ComplexShape.up ℤ))
            Res_i.mapDerivedCategoryFactors.hom ≫
          (Functor.associator _ _ _).inv ≫
          Functor.whiskerRight
            (Functor.mapHomologicalComplexCompIso (Iso.refl F_A)
              (ComplexShape.up ℤ)).hom
            (DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} R'))
      Σ' (tau0 : F_R ⟶ F_A),
        {tau : DRes_f ⋙ L_g ⟶ L_h ⋙ DRes_i //
          (∀ (M : ModuleCat.{max v uR uA uRp uAp} A) (r' : R') (m : M),
            tau0.app M (r' ⊗ₜ[R,g] m) = (i r') ⊗ₜ[A,h] m) ∧
          Functor.whiskerLeft (DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} A)) tau ≫
            beta_A =
            beta_R ≫ Functor.whiskerRight
                (NatTrans.mapHomologicalComplex tau0 (ComplexShape.up ℤ))
                (DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} R'))}
Tag 0660, a definition

Tag 0660 in the Stacks Project.

RingTheory.TorIndependence.TorIndependent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/Independence.lean, line 94. References: SGA 6 III (1.5), “affine case”.

Two R-algebras are Tor independent over R when their positive-degree Tor modules over R vanish.

public def TorIndependent (R : Type uR) (A : Type uA) (B : Type uB)
    [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] : Prop
Tag 0661, a lemma

Tag 0661 in the Stacks Project.

RingTheory.TorIndependence.derivedBaseChangeComparison_isIso_of_torIndependent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/IndependenceBaseChange.lean, line 768.

Stacks 0661. If A and R' are Tor independent over R, then the canonical comparison from derived base change over R to derived base change over A is an isomorphism, for every pushout square with upper-right corner A'.

public theorem derivedBaseChangeComparison_isIso_of_torIndependent
    {R : Type uR} {A : Type uA} {R' : Type uRp} {A' : Type uAp}
    [CommRing R] [CommRing A] [CommRing R'] [CommRing A']
    [Algebra R A] [Algebra R R'] [Algebra R A'] [Algebra A A'] [Algebra R' A']
    [IsScalarTower R A A'] [IsScalarTower R R' A'] [Algebra.IsPushout R A R' A']
    [HasDerivedCategory (ModuleCat.{max v uR uA uRp uAp} R)]
    [HasDerivedCategory (ModuleCat.{max v uR uA uRp uAp} A)]
    [HasDerivedCategory (ModuleCat.{max v uR uA uRp uAp} R')]
    [HasDerivedCategory (ModuleCat.{max v uR uA uRp uAp} A')]
    (hTor : TorIndependent R A R') :
    let f : R →+* A := algebraMap R A
    let g : R →+* R' := algebraMap R R'
    let h : A →+* A' := algebraMap A A'
    let i : R' →+* A' := algebraMap R' A'
    let sq : h.comp f = i.comp g := by
      exact (IsScalarTower.algebraMap_eq R A A').symm.trans
        (IsScalarTower.algebraMap_eq R R' A')
    let Ext_g := ModuleCat.extendScalars.{uR, uRp, max v uR uA uRp uAp} g
    let Ext_h := ModuleCat.extendScalars.{uA, uAp, max v uR uA uRp uAp} h
    letI : Ext_g.IsLeftAdjoint :=
      (ModuleCat.extendRestrictScalarsAdj.{max v uR uA uRp uAp, uR, uRp}
        g).isLeftAdjoint
    letI : Ext_h.IsLeftAdjoint :=
      (ModuleCat.extendRestrictScalarsAdj.{max v uR uA uRp uAp, uA, uAp}
        h).isLeftAdjoint
    let U_g := Ext_g.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
      DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} R')
    let U_h := Ext_h.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
      DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} A')
    ∀ (L_g : DerivedCategory (ModuleCat.{max v uR uA uRp uAp} R) ⥤
          DerivedCategory (ModuleCat.{max v uR uA uRp uAp} R'))
      (L_h : DerivedCategory (ModuleCat.{max v uR uA uRp uAp} A) ⥤
          DerivedCategory (ModuleCat.{max v uR uA uRp uAp} A'))
      (alpha_g : DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} R) ⋙ L_g ⟶ U_g)
      (alpha_h : DerivedCategory.Q (C := ModuleCat.{max v uR uA uRp uAp} A) ⋙ L_h ⟶ U_h),
      [L_g.IsLeftDerivedFunctor alpha_g
        (HomologicalComplex.quasiIso (ModuleCat.{max v uR uA uRp uAp} R)
          (ComplexShape.up ℤ))] →
      [L_h.IsLeftDerivedFunctor alpha_h
        (HomologicalComplex.quasiIso (ModuleCat.{max v uR uA uRp uAp} A)
          (ComplexShape.up ℤ))] →
      let comparison := derivedBaseChangeComparison f g h i sq
        L_g L_h alpha_g alpha_h
      IsIso comparison.2.1
Tag 08HW, a lemma

Tag 08HW in the Stacks Project.

RingTheory.TorIndependence.isIso_torExtensionMap_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/Independence.lean, line 352.

Stacks 08HW. If R' is flat over R, A' is flat over A ⊗[R] R', and B' is flat over R' ⊗[R] B, the canonical scalar-extended change-of-rings map on ordinary Tor is an isomorphism. The diagram is lifted to the maximum of its six independent universes so that Mathlib's categorical Tor and extension-of-scalars constructions apply.

public theorem isIso_torExtensionMap_of_flat
    (R : Type uR) (R' : Type uS) (A : Type uA) (B : Type uB)
    (A' : Type uC) (B' : Type uD)
    [CommRing R] [CommRing R'] [CommRing A] [CommRing B] [CommRing A'] [CommRing B']
    [Algebra R R'] [Algebra R A] [Algebra R B] [Algebra R A'] [Algebra R B']
    [Algebra R' A'] [Algebra R' B'] [IsScalarTower R R' A'] [IsScalarTower R R' B']
    (fA : A →ₐ[R] A') (fB : B →ₐ[R] B')
    (hR' : RingHom.Flat (algebraMap R R'))
    (hA' : RingHom.Flat (Algebra.TensorProduct.lift fA
      (IsScalarTower.toAlgHom R R' A') (fun _ _ ↦ Commute.all _ _)).toRingHom)
    (hB' : RingHom.Flat (Algebra.TensorProduct.lift
      (IsScalarTower.toAlgHom R R' B') fB (fun _ _ ↦ Commute.all _ _)).toRingHom)
    (i : ℕ) :
    IsIso (TorChangeOfRings.extensionMap TorChangeOfRings.canonicalSystem_nonempty
      (ULift.{max uR uS uA uB uC uD} R) (ULift.{max uR uS uA uB uC uD} R')
      (ULift.{max uR uS uA uB uC uD} A) (ULift.{max uR uS uA uB uC uD} B)
      (ULift.{max uR uS uA uB uC uD} A') (ULift.{max uR uS uA uB uC uD} B')
      i fA.ulift fB.ulift)
Tag 0FXF, a lemma

Tag 0FXF in the Stacks Project.

RingTheory.TorIndependence.torIndependent_tensorProduct_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/Independence.lean, line 566.

Stacks 0FXF. Tor independence of two algebras is preserved by extension of scalars along a flat map of commutative rings.

public theorem torIndependent_tensorProduct_of_flat
    (R : Type uR) (R' : Type uS) (A : Type uA) (B : Type uB)
    [CommRing R] [CommRing R'] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] [Algebra R R']
    (h : TorIndependent R A B)
    (hR' : RingHom.Flat (algebraMap R R')) :
    let _ : Algebra R' (A ⊗[R] R') := Algebra.TensorProduct.rightAlgebra
    let _ : Algebra R' (B ⊗[R] R') := Algebra.TensorProduct.rightAlgebra
    TorIndependent R' (A ⊗[R] R') (B ⊗[R] R')
Tag 0DJD, a lemma

Tag 0DJD in the Stacks Project.

RingTheory.TorIndependence.derivedBaseChangeHomologyIso_of_flat, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/FlatBaseChangeHomology.lean, line 200.

Stacks 0DJD. Under the flatness hypotheses of Tag 08HW, the cohomology of (M ⊗ᴸ_A A') ⊗ᴸ_{R'} B' is canonically and naturally isomorphic, as a module over A' ⊗[R'] B', to the extension of scalars of the cohomology of M ⊗ᴸ_R B along A ⊗[R] B → A' ⊗[R'] B'.

public def derivedBaseChangeHomologyIso_of_flat
    (R R' A B A' B' : Type u)
    [CommRing R] [CommRing R'] [CommRing A] [CommRing B] [CommRing A'] [CommRing B']
    [Algebra R R'] [Algebra R A] [Algebra R B] [Algebra R A'] [Algebra R B']
    [Algebra R' A'] [Algebra R' B'] [IsScalarTower R R' A'] [IsScalarTower R R' B']
    (fA : A →ₐ[R] A') (fB : B →ₐ[R] B')
    (hR' : RingHom.Flat (algebraMap R R'))
    (hA' : RingHom.Flat (Algebra.TensorProduct.lift fA
      (IsScalarTower.toAlgHom R R' A') (fun _ _ ↦ Commute.all _ _)).toRingHom)
    (hB' : RingHom.Flat (Algebra.TensorProduct.lift
      (IsScalarTower.toAlgHom R R' B') fB (fun _ _ ↦ Commute.all _ _)).toRingHom)
    (i : ℤ) :
    let C := A ⊗[R] B
    let C' := A' ⊗[R'] B'
    let extAA' := (totalDerivedExtensionScalars.{u, u, u} fA.toRingHom).functor
    let extAC := (totalDerivedExtensionScalars.{u, u, u}
      (Algebra.TensorProduct.includeLeftRingHom : A →+* C)).functor
    let extA'C' := (totalDerivedExtensionScalars.{u, u, u}
      (Algebra.TensorProduct.includeLeftRingHom : A' →+* C')).functor
    let g : C →+* C' :=
      TorChangeOfRings.tensorProductMap R R' A B A' B' fA fB
    extAA' ⋙ extA'C' ⋙ DerivedCategory.homologyFunctor (ModuleCat.{u} C') i ≅
      extAC ⋙ DerivedCategory.homologyFunctor (ModuleCat.{u} C) i ⋙
        ModuleCat.extendScalars g
Tag 08HX, a lemma

Tag 08HX in the Stacks Project.

RingTheory.TorIndependence.torIndependent_localizations_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/Independence.lean, line 706.

Stacks 08HX. For R-algebras A and B, the following are equivalent:

  1. A and B are Tor independent over R;
  2. A_p and B_q are Tor independent over R_r whenever p and q lie over r;
  3. every positive-degree Tor module of A and B vanishes after localization at every prime of A ⊗[R] B.
public theorem torIndependent_localizations_tfae
    (R A B : Type u) [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] :
    List.TFAE [
      TorIndependent R A B,
      (∀ (r : PrimeSpectrum R) (p : PrimeSpectrum A) (q : PrimeSpectrum B)
        (hp : r.asIdeal = p.asIdeal.comap (algebraMap R A))
        (hq : r.asIdeal = q.asIdeal.comap (algebraMap R B)),
        letI : p.asIdeal.LiesOver r.asIdeal := ⟨hp⟩
        letI : q.asIdeal.LiesOver r.asIdeal := ⟨hq⟩
        letI : Algebra (Localization.AtPrime r.asIdeal)
            (Localization.AtPrime p.asIdeal) :=
          Localization.AtPrime.algebraOfLiesOver r.asIdeal p.asIdeal
        letI : Algebra (Localization.AtPrime r.asIdeal)
            (Localization.AtPrime q.asIdeal) :=
          Localization.AtPrime.algebraOfLiesOver r.asIdeal q.asIdeal
        TorIndependent (Localization.AtPrime r.asIdeal)
          (Localization.AtPrime p.asIdeal) (Localization.AtPrime q.asIdeal)),
      (∀ (i : ℕ), 0 < i → ∀ s : PrimeSpectrum (A ⊗[R] B),
        letI := TorChangeOfRings.moduleStructure
          TorChangeOfRings.canonicalSystem_nonempty R A B i
        Subsingleton
          (LocalizedModule s.asIdeal.primeCompl (TorChangeOfRings.torObj R i A B)))]
Sources
LeanRingTheory.TorIndependence.canonicalBaseChangeComparison_paste · RingTheory.TorIndependence.canonicalBaseChangeComparison_localization · RingTheory.TorIndependence.derivedBaseChangeComparison · RingTheory.TorIndependence.TorIndependent · RingTheory.TorIndependence.derivedBaseChangeComparison_isIso_of_torIndependent · RingTheory.TorIndependence.isIso_torExtensionMap_of_flat · RingTheory.TorIndependence.torIndependent_tensorProduct_of_flat · RingTheory.TorIndependence.derivedBaseChangeHomologyIso_of_flat

Section15.63 Spectral sequences for Tor#

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

Tag 061Z, an example

Tag 061Z in the Stacks Project.

CochainComplex.Tor.exists_spectral_sequences_tor_homology_and_terms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/Tor.lean, line 1258. References: EGA III (6.3.2), “Q• = module M, K bdd”; EGA III (7.6.4), “(i) spectral sequence”.

Let K be a bounded-below chain complex of R-modules and let M be an R-module. There is a bounded-below free resolution P of M, and the two filtrations of K ⊗[R] P give spectral sequences abutting to its homology.

The first has second page Torⱼᴿ(Hᵢ(K), M) and differential of bidegree (1, -2). The second has first page Torⱼᴿ(Kᵢ, M); under the displayed identifications, its first differential is the map on Tor induced by Kᵢ ⟶ Kᵢ₋₁.

public theorem exists_spectral_sequences_tor_homology_and_terms
    (R : Type u) [CommRing R]
    (K : CochainComplex (ModuleCat.{v} R) ℤ)
    (hK : ∃ a : ℤ, ∀ i : ℤ, a < i → IsZero (K.X i))
    (M : ModuleCat.{w} R) :
    let K' := ((ModuleCat.uliftFunctor.{max u w, v} R).mapHomologicalComplex
      (ComplexShape.up ℤ)).obj K
    let M' := (ModuleCat.uliftFunctor.{max u v, w} R).obj M
    ∃ (P : CochainComplex (ModuleCat.{max u v w} R) ℤ),
      ∃ (ε : P ⟶ (HomologicalComplex.single (ModuleCat.{max u v w} R)
        (ComplexShape.up ℤ) 0).obj M')
        (_ : QuasiIso ε),
      (∀ i : ℤ, Module.Free R (P.X i)) ∧
      (∀ i : ℤ, 0 < i → IsZero (P.X i)) ∧
      Nonempty (P.homology 0 ≅ M') ∧
      (∀ i : ℤ, i ≠ 0 → IsZero (P.homology i)) ∧
      ∃ (E : FirstTorSpectralSequence (ModuleCat.{max u v w} R))
        (E' : SecondTorSpectralSequence (ModuleCat.{max u v w} R))
        (_e₂ : ∀ i j : ℤ, (E.page 2).X (i, j) ≅ TorInDegree.{u, max v w} R j (K'.homology (-i)) M')
        (e₁ : ∀ i j : ℤ, (E'.page 1).X (i, j) ≅ TorInDegree.{u, max v w} R j (K'.X (-i)) M'),
        let T := HomologicalComplex.mapBifunctor K' P (moduleTensorBifunctor.{u, max v w} R)
          (ComplexShape.up ℤ)
        ∃ (F F' : HomologicalFiltration T)
          (S : TorFiltrationData E F false)
          (S' : TorFiltrationData E' F' true),
          F.step = tensorFiltrationSteps.{u, max v w} R K' P false ∧
          F'.step = tensorFiltrationSteps.{u, max v w} R K' P true ∧
          (∀ n, ∃ a b : ℤ, a ≤ b ∧ F.step a n = ⊥ ∧ F.step b n = ⊤) ∧
          (∀ n, ∃ a b : ℤ, a ≤ b ∧ F'.step a n = ⊥ ∧ F'.step b n = ⊤) ∧
          S.Converges ∧ S'.Converges ∧
          ∀ i j : ℤ,
            (e₁ i j).inv ≫ (E'.page 1).d (i, j) (i - 1, j) ≫ (e₁ (i - 1) j).hom =
              torInDegreeMap.{u, max v w} R j (K'.d (-i) (-(i - 1))) M'
Tag 068F, an example

Tag 068F in the Stacks Project.

CochainComplex.Tor.ChangeOfRingsSpectralSequence.exists_tor_change_of_rings_spectral_sequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/ChangeOfRingsSpectralSequence.lean, line 452. References: EGA III (6.9.3), “special case”; EGA III (6.9.3.2), “special case”; EGA III (6.9.3.3), “special case”; SGA 7 VIII (2.1), “special case”.

Stacks 068F. Let R → S be a homomorphism of commutative rings, M an R-module and N an S-module. There is a free resolution P^• of M over R such that the homology of P^• ⊗_R S, with its natural S-module structure, computes Tor_*^R(M, S), and there is a spectral sequence 

Tor_n^S(Tor_m^R(M, S), N) ⟹ Tor_{n+m}^R(M, N).
The second-page identification is displayed, and the last clause records the abutment; the two Nonempty clauses before it record that the homology of the two base-changed complexes is Tor_*^R(M, S) and Tor_*^R(M, N) after restricting scalars along R → S.

public theorem exists_tor_change_of_rings_spectral_sequence
    (R S : Type u) [CommRing R] [CommRing S] (f : R →+* S)
    (M : ModuleCat.{max u v} R) (N : ModuleCat.{max u v} S) :
    ∃ (P : CochainComplex (ModuleCat.{max u v} R) ℤ),
      ∃ (ε : P ⟶ (HomologicalComplex.single (ModuleCat.{max u v} R)
        (ComplexShape.up ℤ) 0).obj M)
        (_ : QuasiIso ε),
      (∀ i : ℤ, Module.Free R (P.X i)) ∧
      (∀ i : ℤ, 0 < i → IsZero (P.X i)) ∧
      Nonempty (P.homology 0 ≅ M) ∧
      (∀ i : ℤ, i ≠ 0 → IsZero (P.homology i)) ∧
      (∀ i : ℤ, Nonempty
        ((ModuleCat.restrictScalars f).obj ((baseChangeComplex f P).homology (-i)) ≅
          TorInDegree.{u, v} R i M
            ((ModuleCat.restrictScalars f).obj (ModuleCat.of S (ULift.{v} S))))) ∧
      (∀ n : ℤ, Nonempty
        ((ModuleCat.restrictScalars f).obj
            ((baseChangeTensorComplex f P N).homology (-n)) ≅
          TorInDegree.{u, v} R n M ((ModuleCat.restrictScalars f).obj N))) ∧
      ∃ (E : FirstTorSpectralSequence (ModuleCat.{max u v} S))
        (_e₂ : ∀ i j : ℤ, (E.page 2).X (i, j) ≅
          TorInDegree.{u, v} S j ((baseChangeComplex f P).homology (-i)) N),
        HomologicalSpectralSequenceAbutsTo E
          (fun n ↦ (baseChangeTensorComplex f P N).homology (-n))
Tag 0620, an example

Tag 0620 in the Stacks Project.

RingTheory.TorBaseChange.exists_tor_base_change_spectral_sequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/BaseChangeSpectralSequence.lean, line 715. References: EGA III (6.9.8), “(6.9.8.1)”.

If A → B and the B-modules M and N are flat over A, then for B' = B ⊗[A] A', M' = M ⊗[B] B', and N' = N ⊗[B] B', there is a homological spectral sequence Torᴬᵢ(Torᴮⱼ(M, N), A') ⇒ Torᴮʳᵢ₊ⱼ(M', N').

Both sides are viewed as A-modules in order to state the spectral sequence in one abelian category.

public theorem exists_tor_base_change_spectral_sequence
    (A B A' : Type u) [CommRing A] [CommRing B] [CommRing A']
    [Algebra A B] [Algebra A A'] (M N : ModuleCat.{max u v} B)
    [Module.Flat A B]
    [Module.Flat A ((ModuleCat.restrictScalars (algebraMap A B)).obj M)]
    [Module.Flat A ((ModuleCat.restrictScalars (algebraMap A B)).obj N)] :
    ∃ (E : CochainComplex.Tor.FirstTorSpectralSequence (ModuleCat.{max u v} A))
      (_e₂ : ∀ i j : ℤ,
        (E.page 2).X (i, j) ≅
          @CochainComplex.Tor.TorInDegree.{u, v} A _ j
            (restrictScalars A B
              (@CochainComplex.Tor.TorInDegree.{u, v} B _ i M N))
            (restrictScalars A A' (@regularModule.{u, v} A' _))),
      CochainComplex.Tor.HomologicalSpectralSequenceAbutsTo E
        (fun n ↦
          (ModuleCat.restrictScalars
            (algebraMap A (BaseChangedAlgebra A B A'))).obj
            (@CochainComplex.Tor.TorInDegree.{u, v} (BaseChangedAlgebra A B A') _ n
              (@baseChange.{u, v} A B A' _ _ _ _ _ M)
              (@baseChange.{u, v} A B A' _ _ _ _ _ N)))
Tag 0662, an example

Tag 0662 in the Stacks Project.

CochainComplex.DerivedTensorSpectralSequence.exists_derived_tensor_spectral_sequences, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/DerivedTensor.lean, line 1317.

Stacks 0662. For two bounded-above objects K, L of the derived category of a commutative ring R there are two convergent spectral sequences 'E_2^{p,q} = H^p(K ⊗^L H^q(L)) and ''E_2^{p,q} = H^p(H^q(K) ⊗^L L), both abutting to H^{p+q}(K ⊗^L L).

They are the spectral sequences of the two canonical filtrations of the total tensor complex P^• ⊗ Q^• of bounded-above complexes of projectives representing K and L; the abutment isomorphism is the one induced by those representatives and the canonical K-flat comparison of the derived tensor product, and the derived second-page isomorphisms factor through the filtered-complex second-page isomorphisms.

public theorem exists_derived_tensor_spectral_sequences
    (R : Type u) [CommRing R]
    (K L : DerivedCategory.Minus (ModuleCat.{u} R)) :
    ∃ (P Q : CochainComplex (ModuleCat.{u} R) ℤ) (bP bQ : ℤ),
      P.IsStrictlyLE bP ∧ (∀ i : ℤ, Projective (P.X i)) ∧
      Q.IsStrictlyLE bQ ∧ (∀ i : ℤ, Projective (Q.X i)) ∧
      ∃ (hPflat : P.KFlat) (hQflat : Q.KFlat)
        (eK : K.1 ≅ DerivedCategory.Q.obj P)
        (eL : L.1 ≅ DerivedCategory.Q.obj Q)
        (E : AssociatedFiltrationSpectralSequence ((tensorLeft P).obj Q)
            (firstDegreeFiltration P Q bP bQ))
        (E' : AssociatedFiltrationSpectralSequence ((tensorLeft P).obj Q)
            (secondDegreeFiltration P Q bP bQ))
        (firstFilteredE₂Iso : ∀ p q : ℤ,
          filteredPageObject ((tensorLeft P).obj Q) (firstDegreeFiltration P Q bP bQ)
              2 p q ≅
          ((tensorLeft P).obj ((single (ModuleCat.{u} R) (ComplexShape.up ℤ) 0).obj
            (Q.homology q))).homology p)
        (secondFilteredE₂Iso : ∀ p q : ℤ,
          filteredPageObject ((tensorLeft P).obj Q) (secondDegreeFiltration P Q bP bQ)
              2 p q ≅
          ((tensorLeft ((single (ModuleCat.{u} R) (ComplexShape.up ℤ) 0).obj
            (P.homology q))).obj Q).homology p)
        (firstE₂Iso : ∀ p q : ℤ, (E.spectralSequence.page 2).X (p, q) ≅
          ((tensorLeft P).obj ((single (ModuleCat.{u} R) (ComplexShape.up ℤ) 0).obj
            (Q.homology q))).homology p)
        (secondE₂Iso : ∀ p q : ℤ, (E'.spectralSequence.page 2).X (p, q) ≅
          ((tensorLeft ((single (ModuleCat.{u} R) (ComplexShape.up ℤ) 0).obj
            (P.homology q))).obj Q).homology p)
        (abutmentIso : ∀ n : ℤ, ((tensorLeft P).obj Q).homology n ≅
          (DerivedCategory.homologyFunctor (ModuleCat.{u} R) n).obj
            (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj
              K.1).obj L.1))
        (firstOrdinaryToDerivedE₂Iso : ∀ p q : ℤ,
          ((tensorLeft P).obj ((single (ModuleCat.{u} R) (ComplexShape.up ℤ) 0).obj
            (Q.homology q))).homology p ≅
          (DerivedCategory.homologyFunctor (ModuleCat.{u} R) p).obj
            (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj K.1).obj
              ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
                ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) q).obj L.1))))
        (secondOrdinaryToDerivedE₂Iso : ∀ p q : ℤ,
          ((tensorLeft ((single (ModuleCat.{u} R) (ComplexShape.up ℤ) 0).obj
            (P.homology q))).obj Q).homology p ≅
          (DerivedCategory.homologyFunctor (ModuleCat.{u} R) p).obj
            (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj
              ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
                ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) q).obj K.1))).obj L.1))
        (firstDerivedE₂Iso : ∀ p q : ℤ, (E.spectralSequence.page 2).X (p, q) ≅
          (DerivedCategory.homologyFunctor (ModuleCat.{u} R) p).obj
            (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj K.1).obj
              ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
                ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) q).obj L.1))))
        (secondDerivedE₂Iso : ∀ p q : ℤ, (E'.spectralSequence.page 2).X (p, q) ≅
          (DerivedCategory.homologyFunctor (ModuleCat.{u} R) p).obj
            (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj
              ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
                ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) q).obj K.1))).obj L.1)),
        (∀ p q : ℤ, (firstE₂Iso p q).hom =
          (E.pageIso 2 p q (by omega)).hom ≫ (firstFilteredE₂Iso p q).hom) ∧
        (∀ p q : ℤ, (secondE₂Iso p q).hom =
          (E'.pageIso 2 p q (by omega)).hom ≫ (secondFilteredE₂Iso p q).hom) ∧
        (∀ p q : ℤ, (firstDerivedE₂Iso p q).hom =
          (firstE₂Iso p q).hom ≫ (firstOrdinaryToDerivedE₂Iso p q).hom) ∧
        (∀ p q : ℤ, (secondDerivedE₂Iso p q).hom =
          (secondE₂Iso p q).hom ≫ (secondOrdinaryToDerivedE₂Iso p q).hom) ∧
        (∀ n : ℤ,
          (abutmentIso n).symm =
            (DerivedCategory.homologyFunctor (ModuleCat.{u} R) n).mapIso
              (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor
                  R).mapIso eK).app L.1 ≪≫
                ((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj
                  (DerivedCategory.Q.obj P)).mapIso eL ≪≫
                (CochainComplex.DerivedTensor.canonicalDerivedTensorProduct R).comparison P Q
                  hPflat hQflat) ≪≫
              (DerivedCategory.homologyFunctorFactors (ModuleCat.{u} R) n).app
                ((tensorLeft P).obj Q))
Sources
LeanCochainComplex.Tor.exists_spectral_sequences_tor_homology_and_terms · CochainComplex.Tor.ChangeOfRingsSpectralSequence.exists_tor_change_of_rings_spectral_sequence · RingTheory.TorBaseChange.exists_tor_base_change_spectral_sequence · CochainComplex.DerivedTensorSpectralSequence.exists_derived_tensor_spectral_sequences

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.