10.85 Projective modules over a… to 10.104 Cohen-Macaulay rings

Section10.85 Projective modules over a local ring#

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

Tag 0590, a lemma

Tag 0590 in the Stacks Project.

Module.forall_free_of_projective_iff_forall_free_of_projective_of_countable_span, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/CountablyGenerated.lean, line 167. The attribute's comment: “The equivalence, with countable generation written as a countable spanning set.”.

Let R be a ring. Every projective R-module is free if and only if every projective R-module admitting a countable generating set is free.

public theorem Module.forall_free_of_projective_iff_forall_free_of_projective_of_countable_span
    (R : Type u) [Ring R] :
    (∀ (M : Type v) [AddCommGroup M] [Module R M], Module.Projective R M → Module.Free R M) ↔
      ∀ (M : Type v) [AddCommGroup M] [Module R M], Module.Projective R M →
        (∃ s : Set M, s.Countable ∧ Submodule.span R s = ⊤) → Module.Free R M
Tag 0591, a lemma

Tag 0591 in the Stacks Project.

countablyGenerated_propertyP_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Kaplansky.lean, line 375.

Stacks Tag 0591 / Lemma 10.85.2: a countably generated module satisfying property (P) is free.

theorem countablyGenerated_propertyP_free
    (hcg : CountablyGenerated R M) (hP : PropertyP R M) :
    Module.Free R M
Tag 0592, a lemma

Tag 0592 in the Stacks Project.

projective_local_free_summand, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Kaplansky.lean, line 512.

Stacks Tag 0592, Lemma 10.85.3. Any element of a projective module over a (commutative) local ring is contained in a free direct summand. Concretely, for every x in a projective module P over a local ring R, there is a submodule N of P with x ∈ N, with N free as an R-module, and with N a direct summand of P (witnessed by a complementary submodule N', IsCompl N N').

theorem projective_local_free_summand {R : Type*} [CommRing R] [IsLocalRing R]
    {P : Type*} [AddCommGroup P] [Module R P] [Module.Projective R P] (x : P) :
    ∃ N : Submodule R P, x ∈ N ∧ Module.Free R N ∧ ∃ N' : Submodule R P, IsCompl N N'
Tag 0593, a theorem

Tag 0593 in the Stacks Project.

Module.free_of_projective_of_isLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Kaplansky.lean, line 621. The attribute's comment: “Projective modules over local rings are free, with no finiteness hypothesis.”. References: SGA 3 VIA (2.1.3).

Stacks 0593 (Kaplansky). If P is a projective module over a commutative local ring R, then P is free. No finiteness hypothesis on P is needed.

public theorem Module.free_of_projective_of_isLocalRing {R : Type u} {P : Type v} [CommRing R]
    [AddCommGroup P] [Module R P] [IsLocalRing R] [Module.Projective R P] : Module.Free R P
Sources
LeanModule.forall_free_of_projective_iff_forall_free_of_projective_of_countable_span · countablyGenerated_propertyP_free · projective_local_free_summand · Module.free_of_projective_of_isLocalRing

Section10.86 Mittag-Leffler systems#

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

Tag 0595, a definition

Tag 0595 in the Stacks Project.

MittagLeffler.IsMittagLefflerSet, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/InverseSystem.lean, line 71. References: EGA 0 (13.1.2), “inverse systems of sets”; EGA 0 (13.1.3); EGA III (4.1.7); SGA 4½ Rapport (4.11).

A directed inverse system of sets (F_i, φ_{ji}) is Mittag-Leffler if for every index i, there exists some j ≥ i such that for all k ≥ j, the image of F_k in F_i (via the transition map) equals the image of F_j in F_i.

def IsMittagLefflerSet {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {F : ι → Type*}
    (φ : ⦃i j : ι⦄ → i ≤ j → F j → F i) [InverseSystem φ] : Prop

MittagLeffler.IsMittagLefflerModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/InverseSystem.lean, line 81. References: EGA 0 (13.1.2), “modules over a ring”; EGA III (4.1.7); SGA 4½ Rapport (4.11).

A directed inverse system of R-modules (M_i, φ_{ji}) is Mittag-Leffler if the underlying directed inverse system of sets is Mittag-Leffler.

def IsMittagLefflerModule {R : Type*} [Ring R] {ι : Type*} [Preorder ι]
    [IsDirected ι (· ≤ ·)] {M : ι → Type*} [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)]
    (φ : ⦃i j : ι⦄ → i ≤ j → M j →ₗ[R] M i)
    [InverseSystem (fun _ _ h => (φ h : M _ → M _))] : Prop
Tag 0597, a lemma

Tag 0597 in the Stacks Project.

DirInvSystem.nonempty_limit_of_isMittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/InverseSystem.lean, line 289. References: SGA 4 I (App.Lemma3), “more general”.

Let (A_i, φ_{ji}) be a directed inverse system of sets over a directed set I. If I is countable, the system is Mittag-Leffler, and each A_i is nonempty, then the limit lim A_i is nonempty.

theorem DirInvSystem.nonempty_limit_of_isMittagLeffler
    [Countable I] [Nonempty I] [IsDirected I (· ≤ ·)]
    {A : I → Type*} (S : DirInvSystem A)
    (hML : S.IsMittagLeffler) (hne : ∀ i, Nonempty (A i)) :
    S.limit.Nonempty
Tag 0598, a lemma

Tag 0598 in the Stacks Project.

invLimit_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/InverseSystem.lean, line 721. References: EGA 0 (13.2.2); EGA III (4.1.7.21), “more general”.

Let I be a countable directed set and let 0 → A →[f] B →[g] C → 0 be an exact sequence of directed inverse systems of abelian groups over I. If the system (A, φ) is Mittag-Leffler, then the induced sequence of inverse limits 0 → lim A →[lim f] lim B →[lim g] lim C → 0 is exact:

  1. lim f is injective;
  2. range (lim f) = ker (lim g);
  3. lim g is surjective.

Left-exactness (parts 1 and 2) holds for any exact sequence of inverse systems; the Mittag-Leffler hypothesis and countability are used for part 3, the surjectivity of lim g.

theorem invLimit_exact
    {I : Type*} [Preorder I] [IsDirected I (· ≤ ·)] [Nonempty I] [Countable I]
    {A : I → Type*} [∀ i, AddCommGroup (A i)]
    {φ : ⦃i j : I⦄ → i ≤ j → (A j →+ A i)}
    (hφ : InverseSystem (fun _ _ h => (φ h : _ → _)))
    {B : I → Type*} [∀ i, AddCommGroup (B i)]
    {ψ : ⦃i j : I⦄ → i ≤ j → (B j →+ B i)}
    (hψ : InverseSystem (fun _ _ h => (ψ h : _ → _)))
    {C : I → Type*} [∀ i, AddCommGroup (C i)]
    {χ : ⦃i j : I⦄ → i ≤ j → (C j →+ C i)}
    (hχ : InverseSystem (fun _ _ h => (χ h : _ → _)))
    {f : ⦃i : I⦄ → (A i →+ B i)} {g : ⦃i : I⦄ → (B i →+ C i)}
    (hexact : IsExactSeq (φ := φ) (ψ := ψ) (χ := χ) f g)
    (hML : IsMittagLefflerSystem A φ) :
    Function.Injective (addInvLimit.map A φ B ψ f hexact.hf_mor) ∧
      (addInvLimit.map A φ B ψ f hexact.hf_mor).range =
        (addInvLimit.map B ψ C χ g hexact.hg_mor).ker ∧
      Function.Surjective (addInvLimit.map B ψ C χ g hexact.hg_mor)
Sources
LeanMittagLeffler.IsMittagLefflerSet · MittagLeffler.IsMittagLefflerModule · DirInvSystem.nonempty_limit_of_isMittagLeffler · invLimit_exact

Section10.87 Inverse systems#

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

Tag 03CA, a lemma

Tag 03CA in the Stacks Project.

CategoryTheory.ShortComplex.shortExact_map_lim_of_isMittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/ShortComplex/InverseLimit.lean, line 252. References: EGA 0 (13.2.2), “ℕ-indexed systems”; EGA III (4.1.7.21), “more general”.

Stacks 03CA. Let R be a ring and let S be a short complex of towers of R-modules, that is of functors ℕᵒᵖ ⥤ ModuleCat R, which is short exact at every index: for each i the sequence 0 → S.X₁ i → S.X₂ i → S.X₃ i → 0 is short exact. If the tower S.X₁ satisfies the Mittag-Leffler condition, that is for every i there is a c ≥ i with Im(S.X₁ c → S.X₁ i) = Im(S.X₁ j → S.X₁ i) for all j ≥ c, then the sequence of inverse limits 0 → lim S.X₁ → lim S.X₂ → lim S.X₃ → 0 is short exact.

public theorem shortExact_map_lim_of_isMittagLeffler {R : Type u} [Ring R]
    (S : ShortComplex (ℕᵒᵖ ⥤ ModuleCat.{v} R))
    (hS : ∀ n : ℕᵒᵖ, (S.map ((evaluation ℕᵒᵖ (ModuleCat.{v} R)).obj n)).ShortExact)
    (hML : (S.X₁ ⋙ forget (ModuleCat.{v} R)).IsMittagLeffler) :
    (S.map (lim : (ℕᵒᵖ ⥤ ModuleCat.{v} R) ⥤ ModuleCat.{v} R)).ShortExact
Sources
LeanCategoryTheory.ShortComplex.shortExact_map_lim_of_isMittagLeffler

Section10.88 Mittag-Leffler modules#

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

Tag 059A, a definition

Tag 059A in the Stacks Project.

CategoryTheory.Functor.IsMittagLefflerSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Defs.lean, line 128.

Stacks 059A. A diagram F : J ⥤ ModuleCat R of R-modules, thought of as a directed system (M i, f i j), is a Mittag-Leffler system if every M i is an R-module of finite presentation and if for every R-module N the inverse system of dual modules (Hom_R(M i, N), Hom_R(f i j, N)), that is F.op ⋙ yoneda.obj N, satisfies the Mittag-Leffler condition.

public def IsMittagLefflerSystem {R : Type u} [Ring R] {J : Type w} [Category.{w'} J]
    (F : J ⥤ ModuleCat.{v} R) : Prop
Tag 059B, a definition

Tag 059B in the Stacks Project.

LinearMap.Dominates, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Dominates.lean, line 136. The attribute's comment: “Domination is spelled out as containment of the kernels of the two maps tensored with the identity of the test module.”.

Stacks 059B. Let f : M → N and g : M → M' be maps of R-modules with common source. We say g dominates f if for every R-module Q we have Ker(f ⊗_R id_Q) ⊆ Ker(g ⊗_R id_Q) as submodules of M ⊗_R Q.

public def Dominates {R : Type u} [CommSemiring R] {M : Type v} {N : Type w} {M' : Type w'}
    [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid M']
    [Module R M'] (g : M →ₗ[R] M') (f : M →ₗ[R] N) : Prop
Tag 059C, a lemma

Tag 059C in the Stacks Project.

LinearMap.dominates_iff_forall_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Dominates.lean, line 451. The attribute's comment: “Domination is the project's LinearMap.Dominates; the containment of kernels is the containment of the kernels of the maps tensored with the identity of the test module.”.

Stacks 059C. Let f : M → N and g : M → M' be maps of R-modules. Then g dominates f, that is Ker(f ⊗_R id_Q) ⊆ Ker(g ⊗_R id_Q) for every R-module Q, if and only if Ker(f ⊗_R id_Q) ⊆ Ker(g ⊗_R id_Q) for every finitely presented R-module Q.

public theorem LinearMap.dominates_iff_forall_finitePresentation {R : Type u} [CommRing R]
    [Small.{v} R] {M : Type v} {N : Type w} {M' : Type w'} [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] [AddCommGroup M'] [Module R M'] (g : M →ₗ[R] M')
    (f : M →ₗ[R] N) :
    g.Dominates f ↔
      ∀ (Q : Type v) [AddCommGroup Q] [Module R Q] [Module.FinitePresentation R Q],
        LinearMap.ker (f.rTensor Q) ≤ LinearMap.ker (g.rTensor Q)
Tag 0AUM, a lemma

Tag 0AUM in the Stacks Project.

dominates_iff_pushoutInl_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Dominates.lean, line 621.

Let f : M → N and g : M → M' be maps of R-modules, and form the pushout square f' : M' → N', g' : N → N'. Then g dominates f if and only if f' is universally injective.

theorem dominates_iff_pushoutInl_universallyInjective
    {M N M' : Type u} [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] [AddCommGroup M'] [Module R M']
    (f : M →ₗ[R] N) (g : M →ₗ[R] M') :
    Dominates.{u, u, u, u, u} f g ↔ UniversallyInjective (pushoutInl f g)
Tag 059D, a lemma

Tag 059D in the Stacks Project.

LinearMap.forall_ker_rTensor_le_iff_exists_eq_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Factorization.lean, line 296. The attribute's comment: “Domination is spelled out as containment of the kernels of the tensored maps.”.

Stacks 059D. Let f : M → N and g : M → M' be maps of R-modules and suppose that Coker(f) = N ⧸ Im(f) is of finite presentation. Then g dominates f, that is Ker(f ⊗ id_Q) ⊆ Ker(g ⊗ id_Q) for every R-module Q, if and only if g factors through f, that is g = h ∘ f for some module map h : N → M'.

public theorem LinearMap.forall_ker_rTensor_le_iff_exists_eq_comp {R : Type u} [CommRing R]
    [Small.{v} R] {M N M' : Type v} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] N) (g : M →ₗ[R] M')
    [Module.FinitePresentation R (N ⧸ LinearMap.range f)] :
    (∀ (Q : Type v) [AddCommGroup Q] [Module R Q],
        LinearMap.ker (f.rTensor Q) ≤ LinearMap.ker (g.rTensor Q)) ↔
      ∃ h : N →ₗ[R] M', g = h ∘ₗ f
Tag 059E, a proposition

Tag 059E in the Stacks Project.

CategoryTheory.Functor.tfae_isMittagLefflerSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Criteria.lean, line 519. The attribute's comment: “Domination is spelled out as containment of the kernels of the tensored maps; condition (4) is 059A's IsMittagLefflerSystem.”.

Stacks 059E. Let R be a commutative ring, let F : J ⥤ ModuleCat R be a directed system (M i, f i j) of finitely presented R-modules over a nonempty directed preorder J, and let c be a colimit cocone on F, so that M = c.pt is colim_{i ∈ J} M i with canonical maps f i : M i → M. The following are equivalent:

  1. for every finitely presented R-module P and every map f : P → M there are a finitely presented R-module Q and a map g : P → Q which dominate each other, that is Ker(f ⊗ id_T) = Ker(g ⊗ id_T) for every R-module T;
  2. for each i there is a j ≥ i such that f i j dominates f i, that is Ker(f i ⊗ id_T) ⊆ Ker(f i j ⊗ id_T) for every R-module T;
  3. for each i there is a j ≥ i such that f i j factors through f i k for every k ≥ i;
  4. F is a Mittag-Leffler system: the inverse system (Hom_R(M i, T), Hom_R(f i j, T)) is Mittag-Leffler for every R-module T;
  5. that inverse system is Mittag-Leffler for the single module T = ∏_{s ∈ J} M s.
public theorem tfae_isMittagLefflerSystem {R : Type u} [CommRing R] [Small.{w} R] {J : Type w}
    [Preorder J] [IsDirectedOrder J] [Nonempty J] (F : J ⥤ ModuleCat.{w} R)
    [∀ i, Module.FinitePresentation R (F.obj i)] {c : Cocone F} (hc : IsColimit c) :
    List.TFAE
      [∀ (P : ModuleCat.{w} R) [Module.FinitePresentation R P] (f : P ⟶ c.pt),
          ∃ (Q : ModuleCat.{w} R) (_ : Module.FinitePresentation R Q) (g : P ⟶ Q),
            ∀ T : ModuleCat.{w} R,
              LinearMap.ker (f.hom.rTensor T) = LinearMap.ker (g.hom.rTensor T),
        ∀ i : J, ∃ (j : J) (u : i ⟶ j), ∀ T : ModuleCat.{w} R,
          LinearMap.ker ((c.ι.app i).hom.rTensor T) ≤ LinearMap.ker ((F.map u).hom.rTensor T),
        ∀ i : J, ∃ (j : J) (u : i ⟶ j), ∀ (k : J) (v : i ⟶ k),
          ∃ h : F.obj k ⟶ F.obj j, F.map u = F.map v ≫ h,
        F.IsMittagLefflerSystem,
        (F.op ⋙ yoneda.obj (ModuleCat.of R (∀ s : J, F.obj s))).IsMittagLeffler]
Tag 059F, a definition

Tag 059F in the Stacks Project.

IsMittagLeffler, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Defs.lean, line 218.

(Stacks 10.88.7, tag 059F.) An R-module M is Mittag-Leffler if for every finitely presented R-module P and every R-linear map f : P → M, there exists a finitely presented R-module Q and an R-linear map g : P → Q such that f and g dominate each other.

This is condition (1) of Stacks Proposition 10.88.6 (tag 059E), which is equivalent to the other four conditions in that proposition. We choose this condition because it is intrinsic to M and does not depend on any auxiliary choice of a directed system writing M as a colimit of finitely presented modules.

The universe parameters uP, uQ, uN are independent of uR, uM, so "for every finitely presented R-module P", "there exists ... Q", and "for every test module N" each range over their own arbitrary universe, matching the Stacks quantifications.

def IsMittagLeffler (R : Type uR) [CommRing R] (M : Type uM)
    [AddCommGroup M] [Module R M] : Prop
Tag 059G, a remark

Tag 059G in the Stacks Project.

CategoryTheory.Functor.isMittagLefflerSystem_iff_isMittagLeffler_dual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Dual.lean, line 249. The attribute's comment: “The content is the reduction of criterion (4) of 059E to the single test module R, stated for finitely generated projective members and an arbitrary index category, and as an iff; the passage to the colimit is 059E and the system comes from 058G. See the module docstring.”.

Stacks 059G. Let R be a commutative ring and let F : J ⥤ ModuleCat R be a diagram (M i, f i j) of finitely generated projective R-modules. Then F is a Mittag-Leffler system — that is, the inverse system of duals (Hom_R(M i, N), Hom_R(f i j, N)) is Mittag-Leffler for every R-module N, and the M i are of finite presentation — if and only if the single inverse system of R-duals (Hom_R(M i, R), Hom_R(f i j, R)) is Mittag-Leffler.

Combined with criterion (4) of Proposition 059E, this says that for a flat module M written by Lazard's theorem (Theorem 058G) as the colimit of a directed system of finite free modules M = colim M i, it is enough for (Hom_R(M i, R), Hom_R(f i j, R)) to be Mittag-Leffler for M to be a Mittag-Leffler module.

public theorem isMittagLefflerSystem_iff_isMittagLeffler_dual {R : Type u} [CommRing R]
    [Small.{v} R] {J : Type w} [Category.{w'} J] (F : J ⥤ ModuleCat.{v} R)
    [∀ i, Module.Finite R (F.obj i)] [∀ i, Module.Projective R (F.obj i)] :
    F.IsMittagLefflerSystem ↔
      (F.op ⋙ yoneda.obj (ModuleCat.of R (Shrink.{v} R))).IsMittagLeffler
Tag 05CN, a lemma

Tag 05CN in the Stacks Project.

Module.mittagLeffler_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/TensorProduct.lean, line 358. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E.”.

Stacks 05CN. If R is a ring and M, N are Mittag-Leffler modules over R, then M ⊗_R N is a Mittag-Leffler module. The Mittag-Leffler condition is spelled out in the intrinsic form 059E (1): every map f from a finitely presented module into the module in question dominates and is dominated by a map g into a finitely presented module, domination meaning containment of the kernels of the maps · ⊗ id_T.

public theorem Module.mittagLeffler_tensorProduct {R : Type u} [CommRing R] [Small.{v} R]
    {M N : Type v} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    (hM : ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (T : Type v) [AddCommGroup T]
          [Module R T], LinearMap.ker (f.rTensor T) = LinearMap.ker (g.rTensor T))
    (hN : ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] N), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (T : Type v) [AddCommGroup T]
          [Module R T], LinearMap.ker (f.rTensor T) = LinearMap.ker (g.rTensor T)) :
    ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] M ⊗[R] N), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (T : Type v) [AddCommGroup T]
          [Module R T], LinearMap.ker (f.rTensor T) = LinearMap.ker (g.rTensor T)
Tag 05CP, a lemma

Tag 05CP in the Stacks Project.

Module.mittagLeffler_iff_forall_finite_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Criteria.lean, line 748. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E; domination as equality of the kernels of the tensored maps.”.

Stacks 05CP. Let R be a ring and M an R-module. Then M is Mittag-Leffler if and only if for every finite free R-module F and every module map f : F → M there are a finitely presented R-module Q and a module map g : F → Q such that f and g dominate each other, that is Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N. Being Mittag-Leffler is spelled out in the intrinsic form 059E (1): the same condition with F ranging over all finitely presented modules.

public theorem Module.mittagLeffler_iff_forall_finite_free {R : Type u} [CommRing R] [Small.{v} R]
    {M : Type v} [AddCommGroup M] [Module R M] :
    (∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
        (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
          (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
            [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) ↔
      ∀ (F : Type v) [AddCommGroup F] [Module R F] [Module.Free R F] [Module.Finite R F]
        (f : F →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
          (_ : Module.FinitePresentation R Q) (g : F →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
            [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)
Tag 05CQ, a lemma

Tag 05CQ in the Stacks Project.

Module.mittagLeffler_trans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/RestrictScalars.lean, line 286. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E.”.

Stacks 05CQ. Let R → S be a ring map with S finitely presented as an R-module (for instance a finite and finitely presented ring map) and let M be an S-module. If M is Mittag-Leffler over S then M is Mittag-Leffler over R. The Mittag-Leffler condition is spelled out in the intrinsic form 059E (1): every map f from a finitely presented module into M dominates and is dominated by a map g into a finitely presented module, domination meaning containment of the kernels of the maps · ⊗ id_N.

public theorem Module.mittagLeffler_trans {R : Type u} {S : Type w} {M : Type v} [CommRing R]
    [CommRing S] [Algebra R S] [Small.{v} R] [Module.FinitePresentation R S] [AddCommGroup M]
    [Module R M] [Module S M] [IsScalarTower R S M]
    (hM : ∀ (P : Type v) [AddCommGroup P] [Module S P] [Module.FinitePresentation S P]
      (f : P →ₗ[S] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module S Q)
        (_ : Module.FinitePresentation S Q) (g : P →ₗ[S] Q), ∀ (N : Type v) [AddCommGroup N]
          [Module S N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) :
    ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
          [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)
Tag 05CR, a lemma

Tag 05CR in the Stacks Project.

Module.mittagLeffler_restrictScalars_iff_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Quotient.lean, line 295. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E; S = R/I with I finitely generated is spelled abstractly as a surjective algebraMap R S with S finitely presented as an R-module.”.

Stacks 05CR. Let R be a ring and let S = R/I for a finitely generated ideal I, presented here as an R-algebra with surjective structure map which is finitely presented as an R-module. Let M be an S-module. Then M is a Mittag-Leffler module over R if and only if M is a Mittag-Leffler module over S. The Mittag-Leffler condition is spelled out in the intrinsic form 059E (1): every map f from a finitely presented module into M dominates and is dominated by a map g into a finitely presented module, domination meaning equality of the kernels of the maps · ⊗ id_N.

public theorem Module.mittagLeffler_restrictScalars_iff_of_surjective {R : Type u} {S : Type w}
    {M : Type v} [CommRing R] [CommRing S] [Algebra R S] [Small.{v} R]
    [Module.FinitePresentation R S] [AddCommGroup M] [Module R M] [Module S M]
    [IsScalarTower R S M] (hRS : Function.Surjective (algebraMap R S)) :
    (∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
          [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) ↔
      ∀ (P : Type v) [AddCommGroup P] [Module S P] [Module.FinitePresentation S P]
        (f : P →ₗ[S] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module S Q)
          (_ : Module.FinitePresentation S Q) (g : P →ₗ[S] Q), ∀ (N : Type v) [AddCommGroup N]
            [Module S N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)
Sources
LeanCategoryTheory.Functor.IsMittagLefflerSystem · LinearMap.Dominates · LinearMap.dominates_iff_forall_finitePresentation · dominates_iff_pushoutInl_universallyInjective · LinearMap.forall_ker_rTensor_le_iff_exists_eq_comp · CategoryTheory.Functor.tfae_isMittagLefflerSystem · IsMittagLeffler · CategoryTheory.Functor.isMittagLefflerSystem_iff_isMittagLeffler_dual

Section10.89 Interchanging direct products with tensor#

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

Tag 059I, an example

Tag 059I in the Stacks Project.

comparisonMap_not_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Basic.lean, line 519. The attribute's comment: “(1)”.

Statement 1 (the comparison map need not be injective). With Q_n = Z/(n+1)Z, the canonical map c : Q ⊗_Z (∏_n Z/(n+1)Z) → ∏_n (Q ⊗_Z Z/(n+1)Z) is not injective.

theorem comparisonMap_not_injective :
    ¬ Function.Injective (tensorPiComparison (fun n : ℕ => ZMod (n + 1)))

comparisonMap_not_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Basic.lean, line 598. The attribute's comment: “(2)”.

Statement 2 (the comparison map need not be surjective). With Q_n = Z and the identification Q ⊗_Z Z ≅ Q, the canonical map c : Q ⊗_Z (∏_n Z) → ∏_n Q is not surjective.

theorem comparisonMap_not_surjective :
    ¬ Function.Surjective comparisonMapQ
Tag 059J, a proposition

Tag 059J in the Stacks Project.

Module.Finite.tfae_piRightHom_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Finiteness/TensorProductPi.lean, line 330.

Stacks 059J. Let R be a commutative ring and M an R-module. The following are equivalent: (1) M is finitely generated; (2) for every family Q of R-modules the canonical map M ⊗[R] (∀ α, Q α) → ∀ α, M ⊗[R] Q α is surjective; (3) for every R-module Q and every set A the canonical map M ⊗[R] Q^A → (M ⊗[R] Q)^A is surjective; (4) for every set A the canonical map M ⊗[R] R^A → M^A is surjective.

public theorem Module.Finite.tfae_piRightHom_surjective (R : Type u) [CommRing R] (M : Type v)
    [AddCommGroup M] [Module R M] :
    List.TFAE
      [Module.Finite R M,
        ∀ (A : Type v) (Q : A → Type v) [∀ α, AddCommGroup (Q α)] [∀ α, Module R (Q α)],
          Function.Surjective (TensorProduct.piRightHom R R M Q),
        ∀ (A : Type v) (Q : Type v) [AddCommGroup Q] [Module R Q],
          Function.Surjective (TensorProduct.piRightHom R R M fun _ : A ↦ Q),
        ∀ A : Type v, Function.Surjective (TensorProduct.piScalarRightHom R R M A)]
Tag 059K, a proposition

Tag 059K in the Stacks Project.

Module.FinitePresentation.tfae_piRightHom_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/FinitePresentation/TensorProductPi.lean, line 444. The attribute's comment: “Test data in the universe of M, as in 059J; hence Small.{v} R. See the module docstring.”.

Stacks 059K. Let R be a commutative ring and M an R-module. The following are equivalent: (1) M is finitely presented; (2) for every family Q of R-modules the canonical map M ⊗[R] (∀ α, Q α) → ∀ α, M ⊗[R] Q α is bijective; (3) for every R-module Q and every set A the canonical map M ⊗[R] Q^A → (M ⊗[R] Q)^A is bijective; (4) for every set A the canonical map M ⊗[R] R^A → M^A is bijective.

public theorem Module.FinitePresentation.tfae_piRightHom_bijective (R : Type u) [CommRing R]
    [Small.{v} R] (M : Type v) [AddCommGroup M] [Module R M] :
    List.TFAE
      [Module.FinitePresentation R M,
        ∀ (A : Type v) (Q : A → Type v) [∀ α, AddCommGroup (Q α)] [∀ α, Module R (Q α)],
          Function.Bijective (TensorProduct.piRightHom R R M Q),
        ∀ (A : Type v) (Q : Type v) [AddCommGroup Q] [Module R Q],
          Function.Bijective (TensorProduct.piRightHom R R M fun _ : A ↦ Q),
        ∀ A : Type v, Function.Bijective (TensorProduct.piScalarRightHom R R M A)]
Tag 059L, a lemma

Tag 059L in the Stacks Project.

LinearMap.exists_finitePresentation_factorization_of_rTensor_apply_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/FinitePresentation/Factorization.lean, line 336. The attribute's comment: “The kernel conditions are elementwise, x being a single element; f factors through f' by the pinned equation f = g ∘ₗ f'.”.

Stacks 059L. Let R be a commutative ring, P a finitely presented R-module, f : P → M a map of R-modules and Q an R-module, and let x ∈ P ⊗ Q be killed by f ⊗ id_Q. Then there are a finitely presented R-module P' and maps f' : P → P', g : P' → M with f = g ∘ f' such that x is killed by f' ⊗ id_Q.

public theorem LinearMap.exists_finitePresentation_factorization_of_rTensor_apply_eq_zero
    {R : Type u} [CommRing R] [Small.{v} R] {P M : Type v} {Q : Type w} [AddCommGroup P]
    [Module R P] [AddCommGroup M] [Module R M] [AddCommGroup Q] [Module R Q]
    [Module.FinitePresentation R P] (f : P →ₗ[R] M) {x : P ⊗[R] Q}
    (hx : f.rTensor Q x = 0) :
    ∃ (P' : Type v) (_ : AddCommGroup P') (_ : Module R P')
      (_ : Module.FinitePresentation R P') (f' : P →ₗ[R] P') (g : P' →ₗ[R] M),
      f = g ∘ₗ f' ∧ f'.rTensor Q x = 0
Tag 059M, a proposition

Tag 059M in the Stacks Project.

Module.mittagLeffler_iff_piRightHom_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/TensorProductPi.lean, line 336. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E; test data in the universe of M, as in 059J and 059K, whence Small.{v} R. See the module docstring.”.

Stacks 059M. Let R be a commutative ring and M an R-module. Then M is Mittag-Leffler — every map f : P → M from a finitely presented R-module dominates and is dominated by a map g : P → Q into a finitely presented R-module, that is Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N, which is condition (1) of Proposition 059E — if and only if for every family (Q α) of R-modules the canonical map M ⊗[R] (∀ α, Q α) → ∀ α, M ⊗[R] Q α is injective.

public theorem Module.mittagLeffler_iff_piRightHom_injective (R : Type u) [CommRing R]
    [Small.{v} R] (M : Type v) [AddCommGroup M] [Module R M] :
    (∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
        (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
          (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
            [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) ↔
      ∀ (A : Type v) (Q : A → Type v) [∀ α, AddCommGroup (Q α)] [∀ α, Module R (Q α)],
        Function.Injective (TensorProduct.piRightHom R R M Q)
Tag 0AS6, a lemma

Tag 0AS6 in the Stacks Project.

Submodule.exists_fg_isLeast_mem_range_rTensor_subtype_of_mittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Flat.lean, line 283. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059M and 05CQ; x ∈ N ⊗_R M is membership in the range of N.subtype.rTensor M, and smallest is IsLeast. Test data in the universe of M and F, whence Small.{v} R. See the module docstring.”.

Let R be a commutative ring, let M be a flat Mittag-Leffler R-module, let F be an R-module and let x ∈ F ⊗[R] M. Then among the submodules N ⊆ F with x ∈ N ⊗[R] M — that is, with x in the range of N ⊗[R] M → F ⊗[R] M — there is a smallest one, and it is a finite R-module.

Being Mittag-Leffler is spelled out inline as condition (1) of Proposition 059E: every map f : P → M from a finitely presented R-module dominates and is dominated by a map g : P → Q into a finitely presented R-module, that is Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N.

public theorem Submodule.exists_fg_isLeast_mem_range_rTensor_subtype_of_mittagLeffler
    {R : Type u} [CommRing R] [Small.{v} R] {M : Type v} [AddCommGroup M] [Module R M]
    [Module.Flat R M]
    (hML : ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
          [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N))
    {F : Type v} [AddCommGroup F] [Module R F] (x : F ⊗[R] M) :
    ∃ F' : Submodule R F, F'.FG ∧
      IsLeast {N : Submodule R F | x ∈ LinearMap.range (N.subtype.rTensor M)} F'
Tag 059N, a lemma

Tag 059N in the Stacks Project.

Function.Exact.mittagLeffler_M₁_and_mittagLeffler_M₂_of_forall_rTensor_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/ShortExact.lean, line 311. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059M and 05CQ; universal exactness is h, h₂ and injectivity of f₁ ⊗ id_T for every T, as in 058K (1). The two items are the two conjuncts.”.

Let 0 → M₁ →[f₁] M₂ →[f₂] M₃ → 0 be a universally exact sequence of R-modules, that is, a short exact sequence for which f₁ ⊗ id_T : M₁ ⊗ T → M₂ ⊗ T is injective for every R-module T. Then (1) if M₂ is Mittag-Leffler, so is M₁, and (2) if M₁ and M₃ are Mittag-Leffler, so is M₂. Being Mittag-Leffler is spelled out in the intrinsic form 059E (1): every map f : P → M from a finitely presented module dominates and is dominated by a map g : P → Q into a finitely presented module, domination meaning Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N.

public theorem Function.Exact.mittagLeffler_M₁_and_mittagLeffler_M₂_of_forall_rTensor_injective
    {R : Type u} [CommRing R] [Small.{v} R] {M₁ M₂ M₃ : Type v} [AddCommGroup M₁] [Module R M₁]
    [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] {f₁ : M₁ →ₗ[R] M₂}
    {f₂ : M₂ →ₗ[R] M₃} (h : Function.Exact f₁ f₂) (h₂ : Function.Surjective f₂)
    (hf₁ : ∀ (T : Type v) [AddCommGroup T] [Module R T], Function.Injective (f₁.rTensor T)) :
    ((∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
          (f : P →ₗ[R] M₂), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
            (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
              [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) →
        ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
          (f : P →ₗ[R] M₁), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
            (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
              [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) ∧
      ((∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
            (f : P →ₗ[R] M₁), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
              (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
                [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) →
        (∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
            (f : P →ₗ[R] M₃), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
              (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
                [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) →
        ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
          (f : P →ₗ[R] M₂), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
            (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
              [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N))
Tag 0EGI, a lemma

Tag 0EGI in the Stacks Project.

Module.mittagLeffler_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/ShortExact.lean, line 552. The attribute's comment: “The exact sequence M₁ → M₂ → M₃ → 0 with M₁ finitely generated is stated as a surjection with finitely generated kernel, as in Module.finitePresentation_of_surjective; Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059M, 05CQ and 0AS6, with test data in the universe of M, whence Small.{v} R. See the module docstring.”.

Let R be a commutative ring, let M be a Mittag-Leffler R-module — every map f : P → M from a finitely presented R-module dominates and is dominated by a map g : P → Q into a finitely presented R-module, that is Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N, which is condition (1) of Proposition 059E — and let l : M → M' be a surjective R-linear map whose kernel is finitely generated. Then M' is Mittag-Leffler.

public theorem Module.mittagLeffler_of_surjective {R : Type u} [CommRing R] [Small.{v} R]
    {M : Type v} [AddCommGroup M] [Module R M] {M' : Type v} [AddCommGroup M'] [Module R M']
    (hML : ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
          [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N))
    (l : M →ₗ[R] M') (hl : Function.Surjective l) (hl' : (LinearMap.ker l).FG) :
    ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] M'), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
          [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)
Tag 0AS7, a lemma

Tag 0AS7 in the Stacks Project.

ModuleCat.mittagLeffler_pt_of_forall_mittagLeffler_of_forall_rTensor_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Colimit.lean, line 393. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059M and 059N; the directed system is a functor with a colimit cocone, as in 059E and 059W; universal injectivity of f i j is injectivity of (F.map u).hom.rTensor T for every T, as in 058K (1). See the module docstring.”.

Stacks 0AS7. Let R be a commutative ring, let F : J ⥤ ModuleCat R be a directed system (M i, f i j) of R-modules over a nonempty directed preorder J, and let c be a colimit cocone on F, so that M = c.pt is colim_{i ∈ J} M i. Assume every transition map is universally injective, that is f i j ⊗ id_T is injective for every R-module T, and that every M i is Mittag-Leffler. Then M is Mittag-Leffler. Being Mittag-Leffler is spelled out in the intrinsic form 059E (1): every map f : P → M from a finitely presented module dominates and is dominated by a map g : P → Q into a finitely presented module, domination meaning Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N.

public theorem ModuleCat.mittagLeffler_pt_of_forall_mittagLeffler_of_forall_rTensor_injective
    {R : Type u} [CommRing R] [Small.{v} R] {J : Type w} [Preorder J] [IsDirectedOrder J]
    [Nonempty J] {F : J ⥤ ModuleCat.{v} R}
    (hinj : ∀ ⦃i j : J⦄ (u : i ⟶ j) (T : Type v) [AddCommGroup T] [Module R T],
      Function.Injective ((F.map u).hom.rTensor T))
    (hML : ∀ i : J, ∀ (P : Type v) [AddCommGroup P] [Module R P]
        [Module.FinitePresentation R P] (f : P →ₗ[R] F.obj i),
      ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q) (_ : Module.FinitePresentation R Q)
        (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N] [Module R N],
          LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N))
    {c : Cocone F} (hc : IsColimit c) :
    ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
        (f : P →ₗ[R] c.pt),
      ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q) (_ : Module.FinitePresentation R Q)
        (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N] [Module R N],
          LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)
Tag 059P, a lemma

Tag 059P in the Stacks Project.

Module.mittagLeffler_directSum_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/DirectSum.lean, line 338. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059M, 059N and 05CQ; the module is Mathlib's DirectSum, as in Module.Flat.directSum_iff. No smallness of R is assumed, neither direction using it. See the module docstring.”.

Stacks 059P. Let R be a commutative ring and (M i) a family of R-modules indexed by a type ι. Then the direct sum ⨁ i, M i is Mittag-Leffler if and only if each M i is. Being Mittag-Leffler is spelled out in the intrinsic form 059E (1): every map f : P → M from a finitely presented module dominates and is dominated by a map g : P → Q into a finitely presented module, domination meaning Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N.

public theorem Module.mittagLeffler_directSum_iff (R : Type u) [CommRing R] {ι : Type v}
    (M : ι → Type v) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)] :
    (∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
        (f : P →ₗ[R] (⨁ i, M i)), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
          (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
            [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) ↔
      ∀ i, ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
        (f : P →ₗ[R] M i), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
          (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
            [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)
Tag 05CT, a lemma

Tag 05CT in the Stacks Project.

Module.mittagLeffler_trans_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/RestrictScalars.lean, line 506. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059M, 059N, 059P and 05CQ; flatness is Module.Flat S M. S and M share the universe of the test data, whence the single Small.{v} R. See the module docstring.”.

Stacks 05CT. Let R → S be a ring map and let M be an S-module. If S is Mittag-Leffler as an R-module, and M is flat and Mittag-Leffler as an S-module, then M is Mittag-Leffler as an R-module. Being Mittag-Leffler is spelled out in the intrinsic form 059E (1): every map f : P → M from a finitely presented module dominates and is dominated by a map g : P → Q into a finitely presented module, domination meaning Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every test module N.

public theorem Module.mittagLeffler_trans_of_flat {R : Type u} {S M : Type v} [CommRing R]
    [CommRing S] [Algebra R S] [Small.{v} R] [AddCommGroup M] [Module R M] [Module S M]
    [IsScalarTower R S M] [Module.Flat S M]
    (hS : ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] S), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
          [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N))
    (hM : ∀ (P : Type v) [AddCommGroup P] [Module S P] [Module.FinitePresentation S P]
      (f : P →ₗ[S] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module S Q)
        (_ : Module.FinitePresentation S Q) (g : P →ₗ[S] Q), ∀ (N : Type v) [AddCommGroup N]
          [Module S N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) :
    ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
          [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)
Sources
LeancomparisonMap_not_injective · comparisonMap_not_surjective · Module.Finite.tfae_piRightHom_surjective · Module.FinitePresentation.tfae_piRightHom_bijective · LinearMap.exists_finitePresentation_factorization_of_rTensor_apply_eq_zero · Module.mittagLeffler_iff_piRightHom_injective · Submodule.exists_fg_isLeast_mem_range_rTensor_subtype_of_mittagLeffler · Function.Exact.mittagLeffler_M₁_and_mittagLeffler_M₂_of_forall_rTensor_injective

Section10.90 Coherent rings#

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

Tag 05CV, a definition

Tag 05CV in the Stacks Project.

Module.IsCoherent, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Coherent/Basic.lean, line 71. The attribute's comment: “coherent module”. References: SGA 6 I (3.1), “special case”; SGA 6 IV (2.1), “special case”.

An R-module M is coherent if it is finitely generated and every finitely generated submodule of M is finitely presented over R.

class Module.IsCoherent (R : Type*) (M : Type*) [Ring R] [AddCommGroup M] [Module R M] :
    Prop

IsCoherentRing, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Coherent/Basic.lean, line 82. The attribute's comment: “coherent ring”. References: EGA 0 (5.3.7), “special case”.

A ring R is a coherent ring if it is coherent as a module over itself.

class IsCoherentRing (R : Type*) [Ring R] : Prop
Tag 0EWV, an example

Tag 0EWV in the Stacks Project.

IsBezout.instIsCoherentRing, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Coherent/Bezout.lean, line 134. The attribute's comment: “Stated for a Bézout domain: the source's proof of the valuation ring case uses only that finitely generated ideals are principal and that the ring is a domain. The valuation ring case is instance search through ValuationRing.instIsBezout.”.

A Bézout domain is a coherent ring: a finitely generated ideal is principal (IsBezout.isPrincipal_of_FG), hence free since the ring is a domain, hence finitely presented. The source states this for a valuation ring, which is a local Bézout domain (ValuationRing.iff_local_bezout_domain); locality is not used.

public instance IsBezout.instIsCoherentRing (A : Type*) [CommRing A] [IsDomain A] [IsBezout A] :
    IsCoherentRing A
Tag 05CW, a lemma

Tag 05CW in the Stacks Project.

isCoherent_of_fg_submodule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Coherent/Basic.lean, line 106. The attribute's comment: “(1)”. References: EGA 0 (5.3.2), “submodule clause, ring”; EGA 0 (5.3.4), “special case”.

A finitely generated submodule of a coherent module is coherent.

theorem isCoherent_of_fg_submodule
    {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [Module.IsCoherent R M]
    (N : Submodule R M) (hN : N.FG) :
    Module.IsCoherent R N

finite_ker_and_coherent_range_coker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Coherent/Basic.lean, line 158. The attribute's comment: “(2)”. References: EGA 0 (5.3.4), “special case”; SGA 6 I (3.3), “special case”; SGA 6 I (3.4), “partial”.

If φ : N → M with N finite and M coherent, then the kernel of φ is finite, the range of φ is coherent, and the cokernel M ⧸ range φ is coherent.

theorem finite_ker_and_coherent_range_coker
    {R N M : Type*} [Ring R] [AddCommGroup N] [Module R N]
    [AddCommGroup M] [Module R M] [Module.Finite R N] [Module.IsCoherent R M]
    (φ : N →ₗ[R] M) :
    Module.Finite R (LinearMap.ker φ) ∧
      Module.IsCoherent R (LinearMap.range φ) ∧
      Module.IsCoherent R (M ⧸ LinearMap.range φ)

coherent_ker_and_coker_of_coherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Coherent/Basic.lean, line 180. The attribute's comment: “(3)”. References: EGA 0 (5.3.4), “special case”; SGA 6 I (3.3), “special case”; SGA 6 I (3.4), “partial”; SGA 6 IV (2.4), “partial”.

If φ : N → M is a homomorphism of coherent modules, then its kernel and cokernel are coherent.

theorem coherent_ker_and_coker_of_coherent
    {R N M : Type*} [Ring R] [AddCommGroup N] [Module R N]
    [AddCommGroup M] [Module R M] [Module.IsCoherent R N] [Module.IsCoherent R M]
    (φ : N →ₗ[R] M) :
    Module.IsCoherent R (LinearMap.ker φ) ∧
      Module.IsCoherent R (M ⧸ LinearMap.range φ)

isCoherent_two_out_of_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Coherent/Basic.lean, line 244. The attribute's comment: “(4)”. References: SGA 6 I (3.3), “special case”; SGA 6 I (3.4), “special case”.

Two-out-of-three for coherence in a short exact sequence 0 → M₁ → M₂ → M₃ → 0, where i is injective, p is surjective and range i = ker p: any two of M₁, M₂, M₃ coherent imply the third is coherent.

theorem isCoherent_two_out_of_three
    {R M₁ M₂ M₃ : Type*} [Ring R]
    [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂]
    [AddCommGroup M₃] [Module R M₃]
    (i : M₁ →ₗ[R] M₂) (p : M₂ →ₗ[R] M₃)
    (hi : Function.Injective i) (hp : Function.Surjective p)
    (hexact : LinearMap.range i = LinearMap.ker p) :
    (Module.IsCoherent R M₁ → Module.IsCoherent R M₂ → Module.IsCoherent R M₃) ∧
    (Module.IsCoherent R M₁ → Module.IsCoherent R M₃ → Module.IsCoherent R M₂) ∧
    (Module.IsCoherent R M₂ → Module.IsCoherent R M₃ → Module.IsCoherent R M₁)
Tag 05CX, a lemma

Tag 05CX in the Stacks Project.

coherent_iff_finitePresentation_of_coherentRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Coherent/Basic.lean, line 326. References: SGA 6 I (3.5), “a) (i)⇔(ii)”.

If R is a coherent ring, then an R-module M is coherent if and only if it is finitely presented.

theorem coherent_iff_finitePresentation_of_coherentRing
    (hR : Module.IsCoherent R R)
    (M : Type*) [AddCommGroup M] [Module R M] :
    Module.IsCoherent R M ↔ Module.FinitePresentation R M
Tag 05CY, a lemma

Tag 05CY in the Stacks Project.

isCoherentRing_of_isNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Coherent/Basic.lean, line 343. References: SGA 6 I (3.6), “special case”.

Every left Noetherian ring is a coherent ring.

theorem isCoherentRing_of_isNoetherianRing (R : Type*) [Ring R] [IsNoetherianRing R] :
    IsCoherentRing R
Tag 05CZ, a proposition

Tag 05CZ in the Stacks Project.

IsCoherentRing.tfae_flat_pi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Coherent/Flat.lean, line 139. The attribute's comment: “Test data in the universe of R. See the module docstring.”.

Stacks 05CZ (Chase's theorem). Let R be a commutative ring. The following are equivalent: (1) R is coherent; (2) any product of flat R-modules is flat; (3) for every set A the module R^A is flat.

theorem IsCoherentRing.tfae_flat_pi (R : Type u) [CommRing R] :
    List.TFAE
      [IsCoherentRing R,
        ∀ (A : Type u) (Q : A → Type u) [∀ α, AddCommGroup (Q α)] [∀ α, Module R (Q α)],
          (∀ α, Module.Flat R (Q α)) → Module.Flat R (∀ α, Q α),
        ∀ A : Type u, Module.Flat R (A → R)]
Sources
LeanModule.IsCoherent · IsCoherentRing · IsBezout.instIsCoherentRing · isCoherent_of_fg_submodule · finite_ker_and_coherent_range_coker · coherent_ker_and_coker_of_coherent · isCoherent_two_out_of_three · coherent_iff_finitePresentation_of_coherentRing

Section10.91 Examples and non-examples of Mittag-Leffler modules#

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

Tag 059R, an example

Tag 059R in the Stacks Project.

Module.mittagLeffler_iff_finitePresentation_and_mittagLeffler_of_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Basic.lean, line 336. The attribute's comment: “Items (1) and (3) together, over one module and with the two hypotheses as antecedents; the forms to cite are the two halves. Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059M, 059N and 059P. Test data in the universe of M, whence Small.{v} R. See the module docstring.”.

Stacks 059R. Let R be a commutative ring and M an R-module. Then (1) if M is finitely generated, M is Mittag-Leffler if and only if M is finitely presented — in particular every finitely presented module is Mittag-Leffler — and (2) if M is projective, in particular if M is free, then M is Mittag-Leffler. Being Mittag-Leffler is spelled out in the intrinsic form 059E (1): every map f : P → M from a finitely presented module dominates and is dominated by a map g : P → Q into a finitely presented module, domination meaning Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N.

This is the example as the source states it, over one module. The two items are independent of each other and each is stated separately, over its own hypothesis alone, as Module.mittagLeffler_iff_finitePresentation and Module.mittagLeffler_of_projective.

public theorem Module.mittagLeffler_iff_finitePresentation_and_mittagLeffler_of_projective
    (R : Type u) [CommRing R] [Small.{v} R] (M : Type v) [AddCommGroup M] [Module R M] :
    (Module.Finite R M →
        ((∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
            (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
              (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
                [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) ↔
          Module.FinitePresentation R M)) ∧
      (Module.Projective R M →
        ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
          (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
            (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
              [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N))

Module.mittagLeffler_iff_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Basic.lean, line 360. The attribute's comment: “Item (1), with the finite generation an instance hypothesis; finitely presented implies Mittag-Leffler is the direction ←, via instFiniteOfFinitePresentation.”.

Stacks 059R, item (1). Let R be a commutative ring and M a finitely generated R-module. Then M is Mittag-Leffler if and only if M is finitely presented; in particular every finitely presented module is Mittag-Leffler, finite presentation implying finite generation. Being Mittag-Leffler is spelled out in the intrinsic form 059E (1): every map f : P → M from a finitely presented module dominates and is dominated by a map g : P → Q into a finitely presented module, domination meaning Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N.

public theorem Module.mittagLeffler_iff_finitePresentation (R : Type u) [CommRing R] [Small.{v} R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    (∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
        (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
          (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
            [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) ↔
      Module.FinitePresentation R M

Module.mittagLeffler_of_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Basic.lean, line 376. The attribute's comment: “Items (2) and (3), with the projectivity an instance hypothesis; item (2), a free module, is this statement via Module.Projective.of_free.”.

Stacks 059R, items (2) and (3). Let R be a commutative ring and M a projective R-module, in particular a free one, Module.Projective.of_free being an instance. Then M is Mittag-Leffler, spelled out in the intrinsic form 059E (1): every map f : P → M from a finitely presented module dominates and is dominated by a map g : P → Q into a finitely presented module, domination meaning Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N.

public theorem Module.mittagLeffler_of_projective (R : Type u) [CommRing R] [Small.{v} R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Projective R M] :
    ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
        (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
          (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
            [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)
Tag 059S, a lemma

Tag 059S in the Stacks Project.

Module.mittagLeffler_iff_exists_isLeast_mem_range_rTensor_subtype, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Flat.lean, line 631. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059M and 0AS6; finite free is Module.Free and Module.Finite, x ∈ F' ⊗_R M is membership in the range of F'.subtype.rTensor M, and smallest is IsLeast. Test data in the universe of M, whence Small.{v} R. See the module docstring.”.

Let R be a commutative ring and let M be a flat R-module. Then M is Mittag-Leffler if and only if for every finite free R-module F and every x ∈ F ⊗[R] M there is a smallest submodule F' of F with x ∈ F' ⊗[R] M — that is, with x in the range of F' ⊗[R] M → F ⊗[R] M.

Being Mittag-Leffler is spelled out inline as condition (1) of Proposition 059E: every map f : P → M from a finitely presented R-module dominates and is dominated by a map g : P → Q into a finitely presented R-module, that is Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N. This is Definition 059F, IsMittagLeffler, by isMittagLeffler_def_iff.

public theorem Module.mittagLeffler_iff_exists_isLeast_mem_range_rTensor_subtype (R : Type u)
    [CommRing R] [Small.{v} R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Flat R M] :
    (∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
        (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
          (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
            [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) ↔
      ∀ (F : Type v) [AddCommGroup F] [Module R F] [Module.Free R F] [Module.Finite R F]
        (x : F ⊗[R] M), ∃ F' : Submodule R F,
          IsLeast {N : Submodule R F | x ∈ LinearMap.range (N.subtype.rTensor M)} F'
Tag 05D0, a lemma

Tag 05D0 in the Stacks Project.

Module.flat_and_mittagLeffler_pi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Pi.lean, line 162. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059M, 059S and 0AS6; R^A is the Pi module A → R, as in item (3) of 05CZ, and the two conclusions are one conjunction, as in the source. Test data in the universe of R and A. See the module docstring.”.

Let R be a Noetherian ring and A a set. Then M = R^A, the R-module of functions A → R, is a flat and Mittag-Leffler R-module.

Being Mittag-Leffler is spelled out inline as condition (1) of Proposition 059E: every map f : P → M from a finitely presented R-module dominates and is dominated by a map g : P → Q into a finitely presented R-module, that is Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N.

theorem Module.flat_and_mittagLeffler_pi (R : Type u) [CommRing R] [IsNoetherianRing R]
    (A : Type u) :
    Module.Flat R (A → R) ∧
      ∀ (P : Type u) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
        (f : P →ₗ[R] (A → R)), ∃ (Q : Type u) (_ : AddCommGroup Q) (_ : Module R Q)
          (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type u) [AddCommGroup N]
            [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)
Tag 059T, a lemma

Tag 059T in the Stacks Project.

Module.flat_and_mittagLeffler_mvPowerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/MvPowerSeries.lean, line 127. The attribute's comment: “The source's 0 < n is dropped as unused: at n = 0 the module is free of rank one, hence flat and Mittag-Leffler. Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 05D0, 059M, 059S and 0AS6; R[[t_1, …, t_n]] is MvPowerSeries (Fin n) R, the product over the monomials with its coefficientwise R-module structure, and the two conclusions are one conjunction, as in the source. Test data in the universe of R. See the module docstring.”.

Let R be a Noetherian ring and let n : ℕ. Then the power series module M = R[[t_1, …, t_n]], regarded as an R-module, is flat and Mittag-Leffler.

Being Mittag-Leffler is spelled out inline as condition (1) of Proposition 059E: every map f : P → M from a finitely presented R-module dominates and is dominated by a map g : P → Q into a finitely presented R-module, that is Ker(f ⊗ id_N) = Ker(g ⊗ id_N) for every R-module N.

theorem Module.flat_and_mittagLeffler_mvPowerSeries (R : Type u) [CommRing R]
    [IsNoetherianRing R] (n : ℕ) :
    Module.Flat R (MvPowerSeries (Fin n) R) ∧
      ∀ (P : Type u) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
        (f : P →ₗ[R] MvPowerSeries (Fin n) R), ∃ (Q : Type u) (_ : AddCommGroup Q)
          (_ : Module R Q) (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q),
            ∀ (N : Type u) [AddCommGroup N] [Module R N],
              LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)
Sources
LeanModule.mittagLeffler_iff_finitePresentation_and_mittagLeffler_of_projective · Module.mittagLeffler_iff_finitePresentation · Module.mittagLeffler_of_projective · Module.mittagLeffler_iff_exists_isLeast_mem_range_rTensor_subtype · Module.flat_and_mittagLeffler_pi · Module.flat_and_mittagLeffler_mvPowerSeries

Section10.92 Countably generated Mittag-Leffler modules#

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

Tag 059W, a lemma

Tag 059W in the Stacks Project.

ModuleCat.exists_countable_directedOn_isColimit_whisker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/DirectLimit/Countable.lean, line 564. The attribute's comment: “Mittag-Leffler as 059E (3); finite presentation of the members is unused”.

Stacks 059W. Let R be a ring, w-small relative to the universe of the modules below, let F : J ⥤ ModuleCat R be a directed system of R-modules over a nonempty directed preorder J, and let c be a colimit cocone on F, so that M = c.pt is colim_{i ∈ J} M i. Assume that for every i there is a j ≥ i such that the transition map M i → M j factors through M i → M k for every k ≥ i — condition (3) of Stacks 059E, which for a system of finitely presented modules says exactly that M is Mittag-Leffler — and that M is spanned by a countable set. Then there is a nonempty countable directed subset J' ⊆ J such that M, with the canonical maps M i → M for i ∈ J', is a colimit of the restricted system: M = colim_{i ∈ J'} M i.

public theorem ModuleCat.exists_countable_directedOn_isColimit_whisker
    {R : Type u} [Ring R] [Small.{w} R] {J : Type v} [Preorder J] [IsDirectedOrder J] [Nonempty J]
    {F : J ⥤ ModuleCat.{w} R}
    (hfac : ∀ i : J, ∃ (j : J) (u : i ⟶ j), ∀ (k : J) (v : i ⟶ k),
      ∃ h : F.obj k ⟶ F.obj j, F.map u = F.map v ≫ h)
    {c : Cocone F} (hc : IsColimit c)
    (hcg : ∃ t : Set c.pt, t.Countable ∧ Submodule.span R t = ⊤) :
    ∃ s : Set J, s.Nonempty ∧ s.Countable ∧ DirectedOn (· ≤ ·) s ∧
      Nonempty (IsColimit (c.whisker (Set.mono_coe s).functor))
Tag 05D2, a lemma

Tag 05D2 in the Stacks Project.

Module.exists_end_factorization_finitePresentation_of_countable_span_of_mittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Endomorphism.lean, line 607. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059M, 059N, 059P, 059R, 05CQ, 059X and 05D6; countable generation as a countable spanning set, as in 0590. Test data in the universe of M, whence Small.{v} R; the source's P keeps its own universe. Factoring through a finitely presented module is the equation α = v ∘ₗ u, as in Module.Flat.exists_factorization_of_finitePresentation. See the module docstring.”.

Let R be a commutative ring and let M be an R-module which is countably generated — it admits a countable spanning set — and Mittag-Leffler, the latter in the intrinsic form 059E (1): every map f : P → M from a finitely presented module dominates and is dominated by a map g : P → Q into a finitely presented module, domination meaning Ker (f ⊗ id_T) = Ker (g ⊗ id_T) for every R-module T. Then for every R-module map f : P → M with P finitely generated there is an endomorphism α : M → M such that (1) α factors through a finitely presented R-module, that is α = v ∘ₗ u for some u : M → Q and v : Q → M with Q finitely presented, and (2) α ∘ f = f.

public theorem Module.exists_end_factorization_finitePresentation_of_countable_span_of_mittagLeffler
    (R : Type u) [CommRing R] [Small.{v} R] (M : Type v) [AddCommGroup M] [Module R M]
    (hcg : ∃ s : Set M, s.Countable ∧ Submodule.span R s = ⊤)
    (hML : ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (T : Type v) [AddCommGroup T]
          [Module R T], LinearMap.ker (f.rTensor T) = LinearMap.ker (g.rTensor T))
    {P : Type w} [AddCommGroup P] [Module R P] [Module.Finite R P] (f : P →ₗ[R] M) :
    ∃ α : M →ₗ[R] M,
      (∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q) (_ : Module.FinitePresentation R Q)
        (u : M →ₗ[R] Q) (v : Q →ₗ[R] M), α = v ∘ₗ u) ∧ α ∘ₗ f = f
Sources
LeanModuleCat.exists_countable_directedOn_isColimit_whisker · Module.exists_end_factorization_finitePresentation_of_countable_span_of_mittagLeffler

Section10.93 Characterizing projective modules#

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

Tag 059X, a lemma

Tag 059X in the Stacks Project.

Module.Flat.projective_of_isMittagLeffler_of_countablyGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Projective.lean, line 439. The attribute's comment: “Mittag-Leffler is IsMittagLeffler (059F) and countable generation is Module.CountablyGenerated (from Tag 0GVD), both cited by name; the companion statements write them out inline, isMittagLeffler_def_iff identifying the two forms. Test data in the universe of M, whence Small.{v} R. See the module docstring.”.

Stacks 059X. A flat, Mittag-Leffler, countably generated module over a commutative ring is projective. The Mittag-Leffler condition is IsMittagLeffler (Definition 059F), with its finitely presented modules and test modules taken in the universe of M; countable generation is Module.CountablyGenerated, the existence of a countable spanning set.

public theorem Module.Flat.projective_of_isMittagLeffler_of_countablyGenerated
    (R : Type u) [CommRing R] [Small.{v} R] (M : Type v) [AddCommGroup M] [Module R M]
    [Module.Flat R M] (hML : IsMittagLeffler.{u, v, v, v, v} R M)
    (hcg : Module.CountablyGenerated R M) :
    Module.Projective R M
Tag 059Z, a theorem

Tag 059Z in the Stacks Project.

Module.projective_iff_flat_and_mittagLeffler_and_exists_sSupIndep_countable_span, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/ProjectiveCharacterization.lean, line 233. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059M, 059N, 059P, 059R, 05CQ, 05D6 and 059X; the direct sum decomposition internally, as an independent set of submodules of M with supremum ⊤, as in 058W and 058Y, with countable generation as a countable spanning set, as in 0590. Test data in the universe of M, whence Small.{v} R. See the module docstring.”.

Let R be a commutative ring and M an R-module. Then M is projective if and only if (1) M is flat, (2) M is Mittag-Leffler, and (3) M is a direct sum of countably generated R-modules. Being Mittag-Leffler is spelled out in the intrinsic form 059E (1): every map f : P → M from a finitely presented module dominates and is dominated by a map g : P → Q into a finitely presented module, domination meaning Ker(f ⊗ id_T) = Ker(g ⊗ id_T) for every R-module T. Being a direct sum of countably generated modules is spelled internally, as in 058W and 058Y: an independent set of submodules of M with supremum ⊤, each spanned by a countable set.

public theorem Module.projective_iff_flat_and_mittagLeffler_and_exists_sSupIndep_countable_span
    (R : Type u) [CommRing R] [Small.{v} R] (M : Type v) [AddCommGroup M] [Module R M] :
    Module.Projective R M ↔
      Module.Flat R M ∧
        (∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
            (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
              (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (T : Type v) [AddCommGroup T]
                [Module R T], LinearMap.ker (f.rTensor T) = LinearMap.ker (g.rTensor T)) ∧
        (∃ S : Set (Submodule R M), sSupIndep S ∧ sSup S = ⊤ ∧
          ∀ N ∈ S, ∃ t : Set M, t.Countable ∧ Submodule.span R t = N)
Tag 05A0, a lemma

Tag 05A0 in the Stacks Project.

Module.projective_of_forall_rTensor_injective_of_exists_sSupIndep_countable_span, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/CountablyGenerated.lean, line 390. The attribute's comment: “Universal injectivity of f is injectivity of f ⊗ id_T for every T, as in 058K (1) and 059N; Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059N, 059X and 059Z; the direct sum decomposition internally, as an independent set of submodules of M with supremum ⊤, as in 058W and 058Y, with countable generation as a countable spanning set, as in 0590. Test data in the universe of M and N, whence Small.{v} R. See the module docstring.”.

Let f : M → N be a universally injective map of R-modules, that is, one for which f ⊗ id_T is injective for every R-module T. Suppose M is a direct sum of countably generated R-modules and suppose N is flat and Mittag-Leffler. Then M is projective. Being a direct sum of countably generated modules is spelled internally, as in 058W and 058Y: an independent set of submodules of M with supremum ⊤, each spanned by a countable set. Being Mittag-Leffler is spelled out in the intrinsic form 059E (1): every map g : P → N from a finitely presented module dominates and is dominated by a map h : P → Q into a finitely presented module, domination meaning Ker(g ⊗ id_T) = Ker(h ⊗ id_T) for every R-module T.

public theorem Module.projective_of_forall_rTensor_injective_of_exists_sSupIndep_countable_span
    (R : Type u) [CommRing R] [Small.{v} R] (M : Type v) [AddCommGroup M] [Module R M]
    (N : Type v) [AddCommGroup N] [Module R N] [Module.Flat R N] (f : M →ₗ[R] N)
    (hf : ∀ (T : Type v) [AddCommGroup T] [Module R T], Function.Injective (f.rTensor T))
    (hM : ∃ S : Set (Submodule R M), sSupIndep S ∧ sSup S = ⊤ ∧
      ∀ K ∈ S, ∃ t : Set M, t.Countable ∧ Submodule.span R t = K)
    (hML : ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (g : P →ₗ[R] N), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (h : P →ₗ[R] Q), ∀ (T : Type v) [AddCommGroup T]
          [Module R T], LinearMap.ker (g.rTensor T) = LinearMap.ker (h.rTensor T)) :
    Module.Projective R M
Tag 05A1, a lemma

Tag 05A1 in the Stacks Project.

Module.projective_of_forall_rTensor_injective_mvPowerSeries_of_exists_sSupIndep_countable_span, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Projective/CountablyGenerated.lean, line 549. The attribute's comment: “R[[t_1, …, t_n]] is MvPowerSeries (Fin n) R with its coefficientwise R-module structure, as in 059T; universal injectivity of f is injectivity of f ⊗ id_T for every T, as in 058K (1), 059N and 05A0; the direct sum decomposition internally, as an independent set of submodules of M with supremum ⊤ each spanned by a countable set, as in 058W, 058Y and 05A0. n and f are parameters rather than existentially bound, the conclusion mentioning neither, and no positivity of n is assumed, as none is in the source. See the module docstring.”.

Let R be a Noetherian ring and let M be an R-module. Suppose M is a direct sum of countably generated R-modules, and suppose there is a universally injective map f : M → R[[t_1, …, t_n]] for some n, that is, one for which f ⊗ id_T is injective for every R-module T. Then M is projective. Being a direct sum of countably generated modules is spelled internally, as in 058W, 058Y and 05A0: an independent set of submodules of M with supremum ⊤, each spanned by a countable set.

public theorem
    Module.projective_of_forall_rTensor_injective_mvPowerSeries_of_exists_sSupIndep_countable_span
    (R : Type u) [CommRing R] [IsNoetherianRing R] (M : Type u) [AddCommGroup M] [Module R M]
    (n : ℕ) (f : M →ₗ[R] MvPowerSeries (Fin n) R)
    (hf : ∀ (T : Type u) [AddCommGroup T] [Module R T], Function.Injective (f.rTensor T))
    (hM : ∃ S : Set (Submodule R M), sSupIndep S ∧ sSup S = ⊤ ∧
      ∀ K ∈ S, ∃ t : Set M, t.Countable ∧ Submodule.span R t = K) :
    Module.Projective R M
Sources
LeanModule.Flat.projective_of_isMittagLeffler_of_countablyGenerated · Module.projective_iff_flat_and_mittagLeffler_and_exists_sSupIndep_countable_span · Module.projective_of_forall_rTensor_injective_of_exists_sSupIndep_countable_span · Module.projective_of_forall_rTensor_injective_mvPowerSeries_of_exists_sSupIndep_countable_span

Section10.94 Ascending properties of modules#

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

Tag 05A3, a lemma

Tag 05A3 in the Stacks Project.

Module.baseChange_flat_and_mittagLeffler_and_exists_sSupIndep_countable_span_and_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/BaseChange.lean, line 85. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E and "direct sum of countably generated modules" as an independent set of countably spanned submodules with supremum ⊤, as in 059M, 05A5 and 058W. The source's M ⊗_R S is written S ⊗[R] M.”.

Base change along a ring map R → S preserves flatness, the Mittag-Leffler condition, being a direct sum of countably generated modules, and projectivity.

theorem baseChange_flat_and_mittagLeffler_and_exists_sSupIndep_countable_span_and_projective
    [Small.{v} R] :
    (Module.Flat R M → Module.Flat S (S ⊗[R] M)) ∧
    ((∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (N : Type v) [AddCommGroup N]
          [Module R N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) →
      ∀ (P : Type v) [AddCommGroup P] [Module S P] [Module.FinitePresentation S P]
      (f : P →ₗ[S] S ⊗[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module S Q)
        (_ : Module.FinitePresentation S Q) (g : P →ₗ[S] Q), ∀ (N : Type v) [AddCommGroup N]
          [Module S N], LinearMap.ker (f.rTensor N) = LinearMap.ker (g.rTensor N)) ∧
    ((∃ 𝒮 : Set (Submodule R M), sSupIndep 𝒮 ∧ sSup 𝒮 = ⊤ ∧
        ∀ N ∈ 𝒮, ∃ t : Set M, t.Countable ∧ Submodule.span R t = N) →
      ∃ 𝒮 : Set (Submodule S (S ⊗[R] M)), sSupIndep 𝒮 ∧ sSup 𝒮 = ⊤ ∧
        ∀ N ∈ 𝒮, ∃ t : Set (S ⊗[R] M), t.Countable ∧ Submodule.span S t = N) ∧
    (Module.Projective R M → Module.Projective S (S ⊗[R] M))
Sources
LeanModule.baseChange_flat_and_mittagLeffler_and_exists_sSupIndep_countable_span_and_projective

Section10.95 Descending properties of modules#

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

Tag 05A5, a lemma

Tag 05A5 in the Stacks Project.

Module.mittagLeffler_of_mittagLeffler_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Descent.lean, line 501. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 05A3, 05CN and 05CQ. The base change is written S ⊗[R] M, Mathlib's order, the source writing M ⊗_R S.”. References: SGA 3 VIB (11.8.2).

Stacks 05A5. Let R → S be a faithfully flat ring map and let M be an R-module. If the S-module S ⊗_R M is Mittag-Leffler, then M is Mittag-Leffler. The Mittag-Leffler condition is spelled out in the intrinsic form 059E (1): every map f from a finitely presented module into the module in question dominates and is dominated by a map g into a finitely presented module, domination meaning equality of the kernels of the maps · ⊗ id_T.

public theorem Module.mittagLeffler_of_mittagLeffler_tensorProduct {R : Type u} [CommRing R]
    [Small.{v} R] {S : Type v} [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S]
    {M : Type v} [AddCommGroup M] [Module R M]
    (hM : ∀ (P : Type v) [AddCommGroup P] [Module S P] [Module.FinitePresentation S P]
      (f : P →ₗ[S] S ⊗[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module S Q)
        (_ : Module.FinitePresentation S Q) (g : P →ₗ[S] Q), ∀ (T : Type v) [AddCommGroup T]
          [Module S T], LinearMap.ker (f.rTensor T) = LinearMap.ker (g.rTensor T)) :
    ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (T : Type v) [AddCommGroup T]
          [Module R T], LinearMap.ker (f.rTensor T) = LinearMap.ker (g.rTensor T)
Tag 0GVD, a lemma

Tag 0GVD in the Stacks Project.

countablyGenerated_of_faithfullyFlat_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Descent.lean, line 275.

Stacks 0GVD. Let R → S be a faithfully flat ring map and let M be an R-module. If the base change S ⊗[R] M is countably generated as an S-module, then M is countably generated as an R-module.

theorem countablyGenerated_of_faithfullyFlat_baseChange
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S]
    (M : Type*) [AddCommGroup M] [Module R M]
    (h : Module.CountablyGenerated S (S ⊗[R] M)) :
    Module.CountablyGenerated R M
Tag 05A6, a lemma

Tag 05A6 in the Stacks Project.

Module.countablyGenerated_and_projective_of_faithfullyFlat_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/CountablyGeneratedProjective.lean, line 272. The attribute's comment: “Countable generation is Module.CountablyGenerated, the predicate introduced with 0GVD. The base change is written S ⊗[R] M, Mathlib's order, the source writing M ⊗_R S.”. References: SGA 3 VIB (11.8.2), “countably generated case”; SGA 3 VIB (11.8.2), “countably generated case”; SGA 3 VIB (11.8.1), “(ii), special case”.

Stacks 05A6. Let R → S be a faithfully flat ring map and let M be an R-module. If the S-module S ⊗_R M is countably generated and projective, then M is countably generated and projective.

public theorem countablyGenerated_and_projective_of_faithfullyFlat_baseChange {R : Type*}
    [CommRing R] {S : Type*} [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S] {M : Type*}
    [AddCommGroup M] [Module R M] [Module.Projective S (S ⊗[R] M)]
    (hM : Module.CountablyGenerated S (S ⊗[R] M)) :
    Module.CountablyGenerated R M ∧ Module.Projective R M
Tag 05A7, a lemma

Tag 05A7 in the Stacks Project.

exists_countablyGenerated_submodule_le_baseChange_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/CountablyGenerated.lean, line 77.

Stacks Tag 05A7, Lemma 10.95.4. Let R → S be a ring map, M an R-module, and Q a countably generated S-submodule of S ⊗[R] M. Then there exists a countably generated R-submodule P of M such that Q ⊆ Im(S ⊗[R] P → S ⊗[R] M), where the map is induced by the inclusion P ↪ M.

theorem exists_countablyGenerated_submodule_le_baseChange_range
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    {M : Type*} [AddCommGroup M] [Module R M]
    (Q : Submodule S (S ⊗[R] M)) (hQ : Q.IsCountablyGenerated) :
    ∃ P : Submodule R M, P.IsCountablyGenerated ∧
      Q ≤ LinearMap.range (LinearMap.baseChange S P.subtype)
Tag 05A8, a lemma

Tag 05A8 in the Stacks Project.

exists_countablyGenerated_baseChange_eq_iSup_of_internal_directSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/CountablyGenerated.lean, line 167.

Stacks Tag 05A8 / Lemma 10.95.5. If M ⊗_R S decomposes as an internal direct sum of countably generated S-submodules Q_i, then any countably generated R-submodule N of M is contained in a countably generated R-submodule N' whose image Im(N' ⊗_R S → M ⊗_R S) = N'.baseChange S equals the partial direct sum ⨁_{i ∈ I'} Q_i over some subset I' ⊆ I.

theorem exists_countablyGenerated_baseChange_eq_iSup_of_internal_directSum
    (Q : I → Submodule S (TensorProduct R S M))
    (hQ : DirectSum.IsInternal Q)
    (hQcg : ∀ i, (Q i).IsCountablyGenerated)
    (N : Submodule R M) (hN : N.IsCountablyGenerated) :
    ∃ (N' : Submodule R M) (I' : Set I),
      N'.IsCountablyGenerated ∧ N ≤ N' ∧
      N'.baseChange S = ⨆ i : I', Q i
Tag 05A9, a theorem

Tag 05A9 in the Stacks Project.

Module.Projective.of_projective_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Projective.lean, line 579. The attribute's comment: “The source's M ⊗_R S is written S ⊗[R] M, Mathlib's order for a base change and the one used by Module.Flat.of_flat_tensorProduct. The finite case is 058S and the countably generated case is 05A6; neither hypothesis appears here.”. References: SGA 3 VIB (11.8.2); SGA 3 VIB (11.8.1), “(ii)”.

Stacks 05A9. Let R → S be a faithfully flat ring map and let M be an R-module. If the S-module S ⊗_R M is projective, then M is projective. This is the projective analogue of Module.Flat.of_flat_tensorProduct, and it assumes no finiteness of M.

public theorem Projective.of_projective_tensorProduct {R : Type*} [CommRing R] {M : Type*}
    [AddCommGroup M] [Module R M] (S : Type*) [CommRing S] [Algebra R S]
    [Module.FaithfullyFlat R S] [Module.Projective S (S ⊗[R] M)] :
    Module.Projective R M
Sources
LeanModule.mittagLeffler_of_mittagLeffler_tensorProduct · countablyGenerated_of_faithfullyFlat_baseChange · Module.countablyGenerated_and_projective_of_faithfullyFlat_baseChange · exists_countablyGenerated_submodule_le_baseChange_range · exists_countablyGenerated_baseChange_eq_iSup_of_internal_directSum · Module.Projective.of_projective_tensorProduct

Section10.96 Completion#

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

Tag 0315, a lemma

Tag 0315 in the Stacks Project.

AdicCompletion.map_shortExact_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/ShortExact.lean, line 472. The attribute's comment: “(3)”.

Stacks 0315 (3). If 0 → K → P → M → 0 is a short exact sequence of R-modules and M is flat over R, then its I-adic completion is again short exact.

public theorem map_shortExact_of_flat {R : Type u} [CommRing R]
    (I : Ideal R) {K : Type v} {P : Type w} {M : Type t} [AddCommGroup K] [Module R K]
    [AddCommGroup P] [Module R P] [AddCommGroup M] [Module R M] [Module.Flat R M]
    {f : K →ₗ[R] P} {g : P →ₗ[R] M} (hf : Function.Injective f)
    (hfg : Function.Exact f g) (hg : Function.Surjective g) :
    Function.Injective (map I f) ∧ Function.Exact (map I f) (map I g) ∧
      Function.Surjective (map I g)

Declarations registered for the tag:

Tag 0317, a definition

Tag 0317 in the Stacks Project.

Declarations registered for the tag:

Tag 0BNG, a lemma

Tag 0BNG in the Stacks Project.

AdicCompletion.map_shortExact_and_isAdicComplete_of_pow_smul_top_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/ShortExact.lean, line 903. The attribute's comment: “The third term is written Q^∧, and the conjunct IsAdicComplete I Q identifies it with the source's Q. No Noetherian or finiteness hypothesis, unlike map_injective and map_exact.”.

Stacks 0BNG. Let R be a ring, let I ⊆ R be an ideal and let 0 → M → N → Q → 0 be a short exact sequence of R-modules such that Q is annihilated by the power I ^ c of I. Then I-adic completion produces a short exact sequence 0 → M^∧ → N^∧ → Q^∧ → 0, and Q is I-adically complete, so that this third term is Q itself as in the source's 0 → M^∧ → N^∧ → Q → 0.

public theorem map_shortExact_and_isAdicComplete_of_pow_smul_top_eq_bot
    {R : Type*} [CommRing R] (I : Ideal R) {M : Type*} [AddCommGroup M] [Module R M]
    {N : Type*} [AddCommGroup N] [Module R N] {Q : Type*} [AddCommGroup Q] [Module R Q]
    {f : M →ₗ[R] N} {g : N →ₗ[R] Q} (hf : Function.Injective f)
    (hfg : Function.Exact f g) (hg : Function.Surjective g)
    {c : ℕ} (hQ : I ^ c • (⊤ : Submodule R Q) = ⊥) :
    Function.Injective (map I f) ∧ Function.Exact (map I f) (map I g) ∧
      Function.Surjective (map I g) ∧ IsAdicComplete I Q
Tag 0318, a lemma

Tag 0318 in the Stacks Project.

AdicCompletion.isAdicComplete_iff_pow_smul_top_eq_ker_eval, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Criteria.lean, line 338. The attribute's comment: “The criterion of Lenstra and de Smit; no hypothesis on I or R.”.

Stacks 0318. Let R be a ring, let I ⊆ R be an ideal and let M be an R-module. Write Kₙ = Ker(M^∧ → M/IⁿM) for the kernel of the n-th projection out of the I-adic completion M^∧ of M. Then M^∧ is I-adically complete if and only if Kₙ = IⁿM^∧ for all n ≥ 1.

public theorem isAdicComplete_iff_pow_smul_top_eq_ker_eval
    {R : Type*} [CommRing R] (I : Ideal R) (M : Type*) [AddCommGroup M] [Module R M] :
    IsAdicComplete I (AdicCompletion I M) ↔
      ∀ n : ℕ, 1 ≤ n →
        I ^ n • (⊤ : Submodule R (AdicCompletion I M)) = (eval I M n).ker
Tag 05GI, a lemma

Tag 05GI in the Stacks Project.

AdicCompletion.isUnit_of_isUnit_evalOneₐ_and_isUnit_one_add_and_le_jacobson_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Units.lean, line 277. The attribute's comment: “All four parts, for an arbitrary ideal of an arbitrary commutative ring.”.

Stacks 05GI. Let R be a ring, let I ⊆ R be an ideal, and let R^∧ = lim R/Iⁿ. Then (1) any element of R^∧ which maps to a unit of R/I is a unit, (2) any element of 1 + I maps to an invertible element of R^∧, (3) any element of 1 + IR^∧ is invertible in R^∧, and (4) the ideals IR^∧ and Ker(R^∧ → R/I) are contained in the Jacobson radical of R^∧.

public theorem isUnit_of_isUnit_evalOneₐ_and_isUnit_one_add_and_le_jacobson_bot
    {R : Type*} [CommRing R] (I : Ideal R) :
    (∀ x : AdicCompletion I R, IsUnit (evalOneₐ I x) → IsUnit x) ∧
      (∀ a ∈ I, IsUnit (algebraMap R (AdicCompletion I R) (1 + a))) ∧
      (∀ x ∈ I.map (algebraMap R (AdicCompletion I R)), IsUnit (1 + x)) ∧
      I.map (algebraMap R (AdicCompletion I R)) ≤ (⊥ : Ideal (AdicCompletion I R)).jacobson ∧
      RingHom.ker (evalOneₐ I).toRingHom ≤ (⊥ : Ideal (AdicCompletion I R)).jacobson
Tag 090S, a lemma

Tag 090S in the Stacks Project.

adicCompletion_of_surjective_of_forall_span_singleton_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Basic.lean, line 281.

If I is generated by the finite family f_1, …, f_r, indexed here by Fin r, and the canonical map M → limₙ M/f_i^n M is surjective for each i, then the canonical map M → limₙ M/I^n M is surjective.

theorem adicCompletion_of_surjective_of_forall_span_singleton_surjective
    {A : Type*} [CommRing A] (M : Type*) [AddCommGroup M] [Module A M]
    {r : ℕ} (f : Fin r → A)
    (hf : ∀ i, Function.Surjective (AdicCompletion.of (Ideal.span {f i}) M))
    (I : Ideal A) (hI : I = Ideal.span (Set.range f)) :
    Function.Surjective (AdicCompletion.of I M)
Tag 090T, a lemma

Tag 090T in the Stacks Project.

isAdicComplete_of_le_of_fg_of_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Basic.lean, line 349. References: EGA 0 (7.2.3), “special case”; EGA 0 (7.2.4), “Case M = A”.

Let A be a (commutative, unital) ring, and let I ⊆ J ⊆ A be ideals. If M is J-adically complete and I is a finitely generated ideal, then M is I-adically complete.

theorem isAdicComplete_of_le_of_fg_of_isAdicComplete
    {A : Type*} [CommRing A] {I J : Ideal A} (hIJ : I ≤ J)
    {M : Type*} [AddCommGroup M] [Module A M]
    (hM : IsAdicComplete J M) (hI : I.FG) :
    IsAdicComplete I M
Tag 0319, a lemma

Tag 0319 in the Stacks Project.

agreement_of_completions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Basic.lean, line 586.

Under the hypotheses I^c ⊆ J and J^d ⊆ I (with c, d > 0), for every R-module M there is a canonical R-linear isomorphism between the I-adic and J-adic completions of M, compatible with the canonical maps from M.

theorem agreement_of_completions
    {R : Type*} [CommRing R] (I J : Ideal R)
    {c d : ℕ} (hc : 0 < c) (hd : 0 < d)
    (hIJ : I ^ c ≤ J) (hJI : J ^ d ≤ I)
    (M : Type*) [AddCommGroup M] [Module R M] :
    ∃ e : AdicCompletion I M ≃ₗ[R] AdicCompletion J M,
      e.toLinearMap.comp (AdicCompletion.of I M) = AdicCompletion.of J M

completeness_preserved, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Basic.lean, line 604. The attribute's comment: “in particular”.

Under the hypotheses I^c ⊆ J and J^d ⊆ I (with c, d > 0), an R-module M is I-adically complete if and only if it is J-adically complete.

theorem completeness_preserved
    {R : Type*} [CommRing R] (I J : Ideal R)
    {c d : ℕ} (hc : 0 < c) (hd : 0 < d)
    (hIJ : I ^ c ≤ J) (hJI : J ^ d ≤ I)
    (M : Type*) [AddCommGroup M] [Module R M] :
    IsAdicComplete I M ↔ IsAdicComplete J M
Tag 031A, a lemma

Tag 031A in the Stacks Project.

main_theorem_031a, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Basic.lean, line 653.

For an \(I\)-adically complete module \(M\) and a submodule \(K\), the equality \(K = \bigcap_n (K + I^n M)\) holds if and only if the quotient \(M/K\) is \(I\)-adically complete.

theorem main_theorem_031a {R : Type*} [CommRing R] (I : Ideal R) (M : Type*)
    [AddCommGroup M] [Module R M] [IsAdicComplete I M] (K : Submodule R M) :
    (K = ⨅ n : ℕ, (K ⊔ (I ^ n • ⊤ : Submodule R M))) ↔ IsAdicComplete I (M ⧸ K)
Tag 031B, a lemma

Tag 031B in the Stacks Project.

isAdicComplete_of_iInf_smul_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Basic.lean, line 750.

A finite module M over an I-adically complete ring R is itself I-adically complete as soon as ⋂ₙ IⁿM = 0.

theorem isAdicComplete_of_iInf_smul_eq_bot
    {R : Type*} [CommRing R] (I : Ideal R)
    {M : Type*} [AddCommGroup M] [Module R M]
    [IsAdicComplete I R] [Module.Finite R M]
    (h : ⨅ n : ℕ, (I ^ n • (⊤ : Submodule R M)) = ⊥) :
    IsAdicComplete I M
Tag 031D, a lemma

Tag 031D in the Stacks Project.

Module.Finite.of_iInf_pow_smul_top_eq_bot_of_finite_quotient_smul_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Finiteness.lean, line 206.

Let R be a ring, let I ⊆ R be an ideal and let M be an R-module. Assume that R is I-adically precomplete, that ⋂_{n ≥ 1} IⁿM = 0, and that M/IM is a finite R/I-module. Then M is a finite R-module. Here IⁿM is I ^ n • (⊤ : Submodule R M), so the second hypothesis is ⨅ n, I ^ n • ⊤ = ⊥, and M/IM is M ⧸ I • ⊤ with its canonical R ⧸ I-module structure.

public theorem Module.Finite.of_iInf_pow_smul_top_eq_bot_of_finite_quotient_smul_top
    {R : Type*} [CommRing R] (I : Ideal R) {M : Type*} [AddCommGroup M] [Module R M]
    [IsPrecomplete I R] (hsep : ⨅ n : ℕ, I ^ n • (⊤ : Submodule R M) = ⊥)
    (hfin : Module.Finite (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M))) :
    Module.Finite R M
Sources
LeanAdicCompletion.map_shortExact_of_flat · AdicCompletion.map_surjective_of_mkQ_comp_surjective · AdicCompletion.map_surjective · AdicCompletion.ofTensorProduct_surjective_of_finite · AdicCompletion.of_bijective_iff · AdicCompletion.map_shortExact_and_isAdicComplete_of_pow_smul_top_eq_bot · AdicCompletion.isAdicComplete_iff_pow_smul_top_eq_ker_eval · AdicCompletion.isUnit_of_isUnit_evalOneₐ_and_isUnit_one_add_and_le_jacobson_bot

Section10.97 Completion for Noetherian rings#

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

Tag 00MA, a lemma

Tag 00MA in the Stacks Project.

Declarations registered for the tag:

Tag 00MB, a lemma

Tag 00MB in the Stacks Project.

adicCompletion_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Flat/LimitExactness.lean, line 108. The attribute's comment: “(2)”. References: EGA 0 (7.3.1), “special case”; EGA 0 (7.3.3); SGA 3 VIIB (5.5.2), “partial”.

For a Noetherian ring \(R\), every short exact sequence \(0 \to M' \to M \to M'' \to 0\) of \(R\)-modules with \(M\) finitely generated completes to a short exact sequence \(0 \to (M')^\wedge \to M^\wedge \to (M'')^\wedge \to 0\).

theorem adicCompletion_shortExact {R : Type u} [CommRing R] [IsNoetherianRing R] (I : Ideal R)
    {M' M M'' : Type u} [AddCommGroup M'] [Module R M'] [AddCommGroup M] [Module R M]
    [Module.Finite R M] [AddCommGroup M''] [Module R M'']
    {f : M' →ₗ[R] M} {g : M →ₗ[R] M''} (hf : Function.Injective f) (hfg : Function.Exact f g)
    (hg : Function.Surjective g) :
    Function.Injective (AdicCompletion.map I f) ∧
    Function.Surjective (AdicCompletion.map I g) ∧
    Function.Exact (AdicCompletion.map I f) (AdicCompletion.map I g)

Declarations registered for the tag:

Tag 00MC, a lemma

Tag 00MC in the Stacks Project.

AdicCompletion.faithfullyFlat_of_le_ringJacobson, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Flat/LimitExactness.lean, line 64. The attribute's comment: “Stated as the class Module.FaithfullyFlat R (AdicCompletion I R), the shape of the flatness half AdicCompletion.flat_of_isNoetherian; the in particular is the case I = 𝔪. See the module docstring.”. References: EGA 0 (7.3.5), “(a) => (b)”; SGA 1 IV (3.2), “if direction”; SGA 1 IV (3.1), “flatness, I ⊆ rad”; SGA 1 IV (3.1), “flatness, I ⊆ rad”; SGA 3 VIIB (5.5.2), “partial”.

Let I be an ideal of a Noetherian ring R and let R^∧ be the I-adic completion of R. If I is contained in the Jacobson radical of R, then the ring map R → R^∧ is faithfully flat. In particular, if (R, 𝔪) is a Noetherian local ring, then the completion lim_n R/𝔪ⁿ is faithfully flat over R.

public theorem AdicCompletion.faithfullyFlat_of_le_ringJacobson {R : Type*} [CommRing R]
    [IsNoetherianRing R] (I : Ideal R) (hI : I ≤ Ring.jacobson R) :
    Module.FaithfullyFlat R (AdicCompletion I R)
Tag 031C, a lemma

Tag 031C in the Stacks Project.

AdicCompletion.instIsAdicComplete, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Noetherian.lean, line 155. The attribute's comment: “Adic completeness, as an instance over a Noetherian ring; the general form is AdicCompletion.isAdicComplete. The other two assertions specialise from Lemma 05GG along IsNoetherian.noetherian I : I.FG: IⁿM^∧ = (IⁿM)^∧ is AdicCompletion.pow_smul_top_eq_ker_eval composed with AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_eval, and M^∧/IⁿM^∧ = M/IⁿM is AdicCompletion.quotPowSMulTopEquiv.”.

Stacks 031C, adic completeness. Let R be a Noetherian ring, I an ideal of R and M an R-module. Then the I-adic completion M^∧ of M is I-adically complete. This is the Noetherian form of AdicCompletion.isAdicComplete, stated as an instance: over a Noetherian ring the finite generation of I that the proof needs is automatic, so no side condition has to be supplied.

public instance instIsAdicComplete {R : Type*} [CommRing R] [IsNoetherianRing R] (I : Ideal R)
    (M : Type*) [AddCommGroup M] [Module R M] :
    IsAdicComplete I (AdicCompletion I M)
Tag 05GH, a lemma

Tag 05GH in the Stacks Project.

completion_noetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/NoetherianRing/CompleteNoetherian.lean, line 334. References: EGA 0 (7.3.1), “more general”; EGA 0 (7.6.11), “more general”; EGA 0 (7.6.18), “partial”; EGA I (10.6.4), “special case”; EGA I (10.8.6), “special case”; EGA IV (8.11.4), “partial”; SGA 3 VIIB (5.5.2), “Noetherianity of ”; SGA 3 X (4.0), “partial”.

Let I be an ideal of a commutative ring R with R / I Noetherian and I finitely generated. Then the I-adic completion R^∧ = AdicCompletion I R is a Noetherian ring, and it is complete with respect to I R^∧ = I.map (algebraMap R (AdicCompletion I R)).

theorem completion_noetherian
    (R : Type*) [CommRing R] (I : Ideal R)
    (h1 : IsNoetherianRing (R ⧸ I)) (h2 : I.FG) :
    IsNoetherianRing (AdicCompletion I R) ∧
    IsAdicComplete (I.map (algebraMap R (AdicCompletion I R))) (AdicCompletion I R)
Tag 0316, a lemma

Tag 0316 in the Stacks Project.

AdicCompletion.isNoetherianRing, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/NoetherianRing/PowerSeriesSurjection.lean, line 236. The attribute's comment: “Stated as an instance for IsNoetherianRing (AdicCompletion I R), Mathlib's spelling of the completion R^∧ = lim_n R/Iⁿ. See the module docstring.”.

Stacks 0316. Let R be a Noetherian ring and let I be an ideal of R. The completion R^∧ = lim_n R/Iⁿ of R with respect to I is Noetherian.

public instance AdicCompletion.isNoetherianRing {R : Type*} [CommRing R] [IsNoetherianRing R]
    (I : Ideal R) : IsNoetherianRing (AdicCompletion I R)
Tag 0394, a lemma

Tag 0394 in the Stacks Project.

AdicCompletion.nonempty_algEquiv_map_and_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/FiniteAlgebra.lean, line 257. The attribute's comment: “Stated without the source's finite generation of n, which no step needs; the m-adic completion of S appears as a completion along the ideal mS of S in the first conjunct and along m in the second. See the module docstring.”. References: SGA 1 I (2.1), “(i) => (iii)”.

Let R → S be a local homomorphism of local rings (R, m) and (S, n) with m finitely generated, and assume that the fibre S/mS is a finite R-module, i.e. dim_{κ(m)} S/mS < ∞. Then the completion S^∧ = lim S/nᵏ is, as an S-algebra, the m-adic completion lim S/mᵏS of S, and the latter is a finite module over R^∧ = lim R/mᵏ.

public theorem AdicCompletion.nonempty_algEquiv_map_and_finite
    {R S : Type*} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] (hm : (maximalIdeal R).FG)
    [Module.Finite R (S ⧸ (maximalIdeal R).map (algebraMap R S))] :
    Nonempty (AdicCompletion (maximalIdeal S) S ≃ₐ[S]
        AdicCompletion ((maximalIdeal R).map (algebraMap R S)) S) ∧
      Module.Finite (AdicCompletion (maximalIdeal R) R) (AdicCompletion (maximalIdeal R) S)
Tag 07N9, a lemma

Tag 07N9 in the Stacks Project.

AdicCompletion.nonempty_algEquiv_pi_primesOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/FiniteAlgebra.lean, line 980. The attribute's comment: “The source's middle term (S_p)^∧ is Mathlib's AdicCompletion.ofTensorProductEquivOfFiniteNoetherian over Rₚ; the two outer terms are identified here. See the module docstring.”.

Let R be a Noetherian ring, S a finite R-algebra and p a prime of R. Let Rₚ be the local ring of R at p and, for each of the (finitely many) primes q of S lying over p, let S_q be the local ring of S at q. Then the base change of S along the completion Rₚ^∧ of Rₚ at its maximal ideal is, as an S-algebra, the product of the completions S_q^∧ of the S_q at their maximal ideals: Rₚ^∧ ⊗[R] S = S_{q₁}^∧ × ⋯ × S_{q_m}^∧.

public theorem AdicCompletion.nonempty_algEquiv_pi_primesOver
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [IsNoetherianRing R]
    [Module.Finite R S] (p : Ideal R) [p.IsPrime]
    (Rp : Type*) [CommRing Rp] [Algebra R Rp] [IsLocalization.AtPrime Rp p] [IsLocalRing Rp]
    (Sq : p.primesOver S → Type*) [∀ q, CommRing (Sq q)] [∀ q, Algebra S (Sq q)]
    [∀ q, IsLocalization.AtPrime (Sq q) q.1] [∀ q, IsLocalRing (Sq q)] :
    Nonempty (S ⊗[R] AdicCompletion (maximalIdeal Rp) Rp ≃ₐ[S]
      ∀ q, AdicCompletion (maximalIdeal (Sq q)) (Sq q))
Tag 05D3, a lemma

Tag 05D3 in the Stacks Project.

AdicCompletion.map_splitExact_of_projective_quotient_smul_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/ShortExact.lean, line 570. References: EGA 0 (7.3.1), “special case”.

Stacks 05D3. Let R be a ring, let I ⊆ R be an ideal and let 0 → K → P → M → 0 be a short exact sequence of R-modules, given by f : K →ₗ[R] P injective, g : P →ₗ[R] M surjective and Function.Exact f g. If M is flat over R and M/IM is a projective R ⧸ I-module, then the sequence of I-adic completions 0 → K^∧ → P^∧ → M^∧ → 0 is split exact: map I f is injective, map I f and map I g are exact, and map I g has an R^∧-linear right inverse.

public theorem map_splitExact_of_projective_quotient_smul_top {R : Type u} [CommRing R]
    (I : Ideal R) {K : Type v} {P : Type w} {M : Type t} [AddCommGroup K] [Module R K]
    [AddCommGroup P] [Module R P] [AddCommGroup M] [Module R M] [Module.Flat R M]
    {f : K →ₗ[R] P} {g : P →ₗ[R] M} (hf : Function.Injective f) (hfg : Function.Exact f g)
    (hg : Function.Surjective g)
    (hM : Module.Projective (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M))) :
    Function.Injective (map I f) ∧ Function.Exact (map I f) (map I g) ∧
      ∃ s : AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I P,
        map I g ∘ₗ s = LinearMap.id
Tag 0DYC, a lemma

Tag 0DYC in the Stacks Project.

IsAdicComplete.of_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/Quotient.lean, line 277. The attribute's comment: “The hypothesis on A/I is stated along the ideal J of the base ring A, Mathlib's normal form via IsAdicComplete.map_algebraMap_iff. See the module docstring.”.

Let A be a Noetherian ring and let I, J be ideals of A. If A is I-adically complete and A/I is J-adically complete, then A is J-adically complete.

public theorem IsAdicComplete.of_quotient {A : Type*} [CommRing A] [IsNoetherianRing A]
    (I J : Ideal A) [IsAdicComplete I A] (hJ : IsAdicComplete J (A ⧸ I)) :
    IsAdicComplete J A
Sources
LeanAdicCompletion.map_injective · AdicCompletion.map_surjective · AdicCompletion.map_exact · AdicCompletion.ofTensorProduct_bijective_of_finite_of_isNoetherian · adicCompletion_shortExact · AdicCompletion.flat_of_isNoetherian · AdicCompletion.faithfullyFlat_of_le_ringJacobson · AdicCompletion.instIsAdicComplete

Section10.98 Taking limits of modules#

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

Tag 0G1Q, a lemma

Tag 0G1Q in the Stacks Project.

invLimit_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/InverseLimit.lean, line 647.

Stacks 0G1Q. For a finitely generated ideal I of a commutative ring A and an inverse system (M_n) of A-modules with I^n M_n = 0 for all n, the inverse limit M = lim_n M_n is I-adically complete: it is a direct summand of its own completion, which is I-adically complete because I is finitely generated.

theorem invLimit_isAdicComplete (hI : I.FG)
    (hM : ∀ n, I ^ n • (⊤ : Submodule A (M n)) = ⊥) :
    IsAdicComplete I (invLimit M t)
Tag 09B8, a lemma

Tag 09B8 in the Stacks Project.

Stacks.AdicCompletion.InverseLimit.InverseSystem.quotientEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/InverseLimit.lean, line 505. The attribute's comment: “(1)”.

Identification of the quotients: the map M / Iⁿ M → M n induced by the limit projection p n is an isomorphism of A-modules.

noncomputable def quotientEquiv (hI : I.FG) (n : ℕ) :
    (S.limit ⧸ (I ^ n • (⊤ : Submodule A S.limit))) ≃ₗ[A] S.M n

Stacks.AdicCompletion.InverseLimit.InverseSystem.isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/InverseLimit.lean, line 540. The attribute's comment: “(2)”.

The limit M = lim_n M n is I-adically complete: the canonical map M → lim_k M / Iᵏ M is an isomorphism.

theorem isAdicComplete (hI : I.FG) : IsAdicComplete I S.limit
Tag 0EKC, a lemma

Tag 0EKC in the Stacks Project.

Ideal.IsHomogeneous.exists_finite_graded_forall_ker_eq_pow_smul_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/InverseLimit.lean, line 1402.

Stacks 0EKC. Let A = ⨁_{i ≥ 0} 𝒜 i be a graded ring, let I ⊆ 𝒜₊ = ⨁_{i > 0} 𝒜 i be a homogeneous ideal, and let (Nₙ) be an inverse system of finite graded A-modules whose transition maps t n : N_{n+1} → Nₙ are graded and exhibit Nₙ = N_{n+1}/Iⁿ N_{n+1}. Then there is a finite graded A-module M and a compatible system of graded surjections f n : M → Nₙ with ker (f n) = Iⁿ M, i.e. Nₙ = M/Iⁿ M as graded modules for all n.

The source assumes A Noetherian; the argument uses only that each Nₙ is a finite A-module, so that hypothesis is omitted.

public theorem exists_finite_graded_forall_ker_eq_pow_smul_top
    {A : Type u} {σ : Type*} [CommRing A]
    [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜]
    {I : Ideal A} (hIhom : I.IsHomogeneous 𝒜)
    (hI : I ≤ (HomogeneousIdeal.irrelevant 𝒜).toIdeal)
    {N : ℕ → Type v} [∀ n, AddCommGroup (N n)] [∀ n, Module A (N n)]
    [∀ n, Module.Finite A (N n)]
    (𝒩 : ∀ n, ℤ → AddSubgroup (N n)) [∀ n, DirectSum.Decomposition (𝒩 n)]
    (h𝒩 : ∀ (n i : ℕ) (d : ℤ) (a : A) (x : N n), a ∈ 𝒜 i → x ∈ 𝒩 n d → a • x ∈ 𝒩 n (i + d))
    (t : ∀ n, N (n + 1) →ₗ[A] N n)
    (ht : ∀ (n : ℕ) (d : ℤ) (x : N (n + 1)), x ∈ 𝒩 (n + 1) d → t n x ∈ 𝒩 n d)
    (htsurj : ∀ n, Function.Surjective (t n))
    (htker : ∀ n, LinearMap.ker (t n) = I ^ n • (⊤ : Submodule A (N (n + 1)))) :
    ∃ (M : Type v) (_ : AddCommGroup M) (_ : Module A M) (ℳ : ℤ → AddSubgroup M)
        (_ : DirectSum.Decomposition ℳ) (f : ∀ n, M →ₗ[A] N n),
      Module.Finite A M ∧
      (∀ (i : ℕ) (d : ℤ) (a : A) (x : M), a ∈ 𝒜 i → x ∈ ℳ d → a • x ∈ ℳ (i + d)) ∧
      (∀ (n : ℕ) (d : ℤ) (x : M), x ∈ ℳ d → f n x ∈ 𝒩 n d) ∧
      (∀ n, Function.Surjective (f n)) ∧
      (∀ n, LinearMap.ker (f n) = I ^ n • (⊤ : Submodule A M)) ∧
      (∀ n, (t n).comp (f (n + 1)) = f n)
Tag 0EKD, a lemma

Tag 0EKD in the Stacks Project.

GradedCompletionData.main_theorem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Completion.lean, line 991.

Stacks tag 0EKD (Lemma 10.98.4): if the induced map φ : M ⊗_A A' → lim_n Gₙ is an isomorphism, then for every d ∈ ℤ the induced map φ^(d) : M_d → lim_n G_{n,d} is an isomorphism.

Bijectivity of φ^(d) splits into injectivity and surjectivity, each reduced through limGdIncl to baseChange_degree_injective and baseChange_degree_surjective.

theorem main_theorem (D : GradedCompletionData)
    (hφ : Function.Bijective D.φ) (d : ℤ) :
    Function.Bijective (D.phiD d)
Sources
LeaninvLimit_isAdicComplete · Stacks.AdicCompletion.InverseLimit.InverseSystem.quotientEquiv · Stacks.AdicCompletion.InverseLimit.InverseSystem.isAdicComplete · Ideal.IsHomogeneous.exists_finite_graded_forall_ker_eq_pow_smul_top · GradedCompletionData.main_theorem

Section10.99 Criteria for flatness#

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

Tag 00ME, a lemma

Tag 00ME in the Stacks Project.

Module.Flat.injective_and_flat_quotient_range_of_injective_mapQ_maximalIdeal_of_isNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriteria/FibreCriteria.lean, line 206. The attribute's comment: “N/𝔪N is N ⧸ 𝔪 • (⊤ : Submodule R N) and ū the canonical Submodule.mapQ of u. The cokernel M/u(N) is M ⧸ LinearMap.range u, and the two conclusions are conjoined; see the module docstring. The non-Noetherian generalization is 046Y.”. References: EGA III (4.6.7.1).

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

Here N/𝔪N is N ⧸ 𝔪 • ⊤ and ū is the canonical Submodule.mapQ, which sends the class of x to the class of u x; see the module docstring.

theorem
    Module.Flat.injective_and_flat_quotient_range_of_injective_mapQ_maximalIdeal_of_isNoetherianRing
    {R S N M : Type*} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] [IsNoetherianRing S]
    [AddCommGroup M] [Module R M] [Module.Flat R M]
    [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] [Module.Finite S N]
    (u : N →ₗ[R] M)
    (hu : Function.Injective (Submodule.mapQ (maximalIdeal R • (⊤ : Submodule R N))
      (maximalIdeal R • (⊤ : Submodule R M)) u
      (Submodule.smul_top_le_comap_smul_top (maximalIdeal R) u))) :
    Function.Injective u ∧ Module.Flat R (M ⧸ LinearMap.range u)
Tag 00MF, a lemma

Tag 00MF in the Stacks Project.

Module.Flat.mem_nonZeroDivisors_and_flat_quotient_span_singleton_of_mem_nonZeroDivisors_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriteria/FibreCriteria.lean, line 327. The attribute's comment: “"Nonzerodivisor" is nonZeroDivisors at the level of rings, as in the source: 𝔪S is Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) and S/fS is S ⧸ Ideal.span {f}. The two conclusions are conjoined, in the order of the sibling lemmas 00ME and 046Z rather than the source's. IsNoetherianRing R is redundant (faithful flatness descends the ascending chain condition) but is part of the tag's hypotheses; see the module docstring.”. References: SGA 3 V (7.2).

Stacks 00MF. Let R → S be a flat and local ring homomorphism of Noetherian local rings, let 𝔪 be the maximal ideal of R, and let f ∈ S be a nonzerodivisor in S/𝔪S. Then f is a nonzerodivisor in S and S/fS is flat over R.

Here S/𝔪S is the ring quotient S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R), the image of f in it is pinned as Ideal.Quotient.mk, and S/fS is S ⧸ Ideal.span {f} with its canonical R-algebra structure; see the module docstring.

theorem
    mem_nonZeroDivisors_and_flat_quotient_span_singleton_of_mem_nonZeroDivisors_maximalIdeal
    {R S : Type*} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] [IsNoetherianRing R] [IsNoetherianRing S] [Module.Flat R S]
    {f : S}
    (hf : Ideal.Quotient.mk (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R)) f ∈
      nonZeroDivisors (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) :
    f ∈ nonZeroDivisors S ∧ Module.Flat R (S ⧸ Ideal.span {f})
Tag 00MG, a lemma

Tag 00MG in the Stacks Project.

Module.Flat.isRegular_and_flat_quotient_ofList_take_of_isRegular_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriteria/FibreCriteria.lean, line 532. The attribute's comment: “"Regular sequence" is RingTheory.Sequence.IsRegular, which is Definition 00LF verbatim, nonvanishing clause included, and the sequence is a List S. The fibre is S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) and S/(f₁, …, f_i) is S ⧸ Ideal.ofList (fs.take i), quantified over all i : ℕ since List.take saturates. IsNoetherianRing R and IsLocalHom (algebraMap R S) are both redundant here but are part of the tag's hypotheses; see the module docstring.”. References: EGA 0 (15.1.16), “c) => a), M = B”; EGA IV (11.3.8), “(c) ⇒ (a), special case”.

Stacks 00MG. Let R → S be a flat and local ring homomorphism of Noetherian local rings, let 𝔪 be the maximal ideal of R, and let f₁, …, f_c be elements of S whose images form a regular sequence in S/𝔪S. Then f₁, …, f_c is a regular sequence in S and each of the quotients S/(f₁, …, f_i) is flat over R.

Here S/𝔪S is the ring quotient S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R), the images are pinned as Ideal.Quotient.mk, and S/(f₁, …, f_i) is S ⧸ Ideal.ofList (fs.take i) with its canonical R-algebra structure; see the module docstring.

theorem Module.Flat.isRegular_and_flat_quotient_ofList_take_of_isRegular_maximalIdeal
    {R S : Type*} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] [IsNoetherianRing R] [IsNoetherianRing S] [Module.Flat R S]
    {fs : List S}
    (hfs : RingTheory.Sequence.IsRegular
      (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))
      (fs.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))))) :
    RingTheory.Sequence.IsRegular S fs ∧
      ∀ i, Module.Flat R (S ⧸ Ideal.ofList (fs.take i))
Tag 00MH, a lemma

Tag 00MH in the Stacks Project.

Module.Flat.free_and_flat_of_free_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriteria/FibreCriteria.lean, line 688. The attribute's comment: “"Nonzero" is Nontrivial M. The fibre ring is S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) and M/𝔪M is M ⧸ 𝔪S • (⊤ : Submodule S M), whose S/𝔪S-module structure is Module.instQuotientIdealSubmoduleHSMulTop. The two conclusions are conjoined, in the source's order: M is free over S, S is flat over R. IsNoetherianRing R is unused but is part of the tag's hypotheses; see the module docstring.”. References: EGA 0 (10.1.3), “special case”.

Stacks 00MH. Let R → S be a local homomorphism of Noetherian local rings, let 𝔪 be the maximal ideal of R, and let M be a nonzero finite S-module. If M/𝔪M is a free S/𝔪S-module and M is flat over R, then M is free over S and S is flat over R.

Here S/𝔪S is the ring quotient S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) and M/𝔪M is the quotient M ⧸ 𝔪S • (⊤ : Submodule S M) with its canonical S/𝔪S-module structure; see the module docstring.

theorem free_and_flat_of_free_maximalIdeal
    {R S M : Type*} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] [IsNoetherianRing R] [IsNoetherianRing S]
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Module.Finite S M]
    [Nontrivial M] [Module.Flat R M]
    (hM : Module.Free (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))
      (M ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) • (⊤ : Submodule S M))) :
    Module.Free S M ∧ Module.Flat R S
Tag 00MI, a lemma

Tag 00MI in the Stacks Project.

Module.Flat.exactAt_and_flat_cokernel_of_exactAt_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriteria/FibreCriteria.lean, line 844. The attribute's comment: “The complex is a ChainComplex (ModuleCat S) ℕ vanishing above e, as in 00N0, so that ExactAt e is the leading 0 →; exactness is assumed and concluded at every positive index, which above e is automatic. F_i/𝔪F_i is the base change (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) ⊗[S] F_i of ModuleCat.extendScalars, applied to C as a complex, and Coker(F_1 → F_0) is cokernel (C.d 1 0). IsNoetherianRing R is unused but is part of the tag's hypotheses; see the module docstring.”.

Stacks 00MI. Let R → S be a local homomorphism of Noetherian local rings, let 𝔪 be the maximal ideal of R, and let 0 → F_e → F_{e-1} → ⋯ → F_0 be a finite complex of finite S-modules, presented as a chain complex C of S-modules with C.X i = 0 for i > e. Assume that every F_i is flat over R and that the reduced complex 0 → F_e/𝔪F_e → ⋯ → F_0/𝔪F_0 is exact. Then 0 → F_e → ⋯ → F_0 is exact, and Coker(F_1 → F_0) is flat over R.

Reduction modulo 𝔪 is base change along S → S/𝔪S, Coker(F_1 → F_0) is the categorical cokernel, and flatness over R is flatness after restricting scalars along algebraMap R S; see the module docstring.

theorem Module.Flat.exactAt_and_flat_cokernel_of_exactAt_maximalIdeal
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
    [Algebra R S] [IsLocalHom (algebraMap R S)] [IsNoetherianRing R] [IsNoetherianRing S]
    (C : ChainComplex (ModuleCat.{max w v} S) ℕ) [∀ i, Module.Finite S (C.X i)] (e : ℕ)
    (hC : ∀ i, e < i → IsZero (C.X i))
    (hflat : ∀ i, Module.Flat R ((ModuleCat.restrictScalars (algebraMap R S)).obj (C.X i)))
    (hexact : ∀ i, 0 < i →
      (((ModuleCat.extendScalars
          (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (maximalIdeal R)))).mapHomologicalComplex
        (ComplexShape.down ℕ)).obj C).ExactAt i) :
    (∀ i, 0 < i → C.ExactAt i) ∧
      Module.Flat R ((ModuleCat.restrictScalars (algebraMap R S)).obj (cokernel (C.d 1 0)))
Tag 00MJ, a lemma

Tag 00MJ in the Stacks Project.

IsLocalRing.isZero_Tor'_one_of_isFiniteLength, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriteria/TorAndNilpotentDescent.lean, line 397.

Stacks 00MJ. Let R be a local ring with residue field κ and let M be an R-module. If Tor₁(κ, M) = 0, then Tor₁(N, M) = 0 for every R-module N of finite length. Here Tor₁(N, M) is ((Tor' (ModuleCat R) 1).obj N).obj M, the first left derived functor of - ⊗ M evaluated at N.

theorem isZero_Tor'_one_of_isFiniteLength {R : Type u} [CommRing R] [IsLocalRing R]
    (M : ModuleCat.{u} R)
    (hM : IsZero (((Tor' (ModuleCat.{u} R) 1).obj (ModuleCat.of R (ResidueField R))).obj M))
    (N : ModuleCat.{u} R) (hN : IsFiniteLength R N) :
    IsZero (((Tor' (ModuleCat.{u} R) 1).obj N).obj M)
Tag 00MK, a lemma

Tag 00MK in the Stacks Project.

Module.Flat.of_isZero_Tor'_one_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriterion.lean, line 170. The attribute's comment: “Tor₁^R(κ, M) is Tor', the left derived functor of - ⊗_R M evaluated at κ; forming it in ModuleCat R puts M in the universe of R.”. References: EGA 0 (10.1.3), “(d)⇒(c), case (ii)”; EGA 0 (10.2.2), “Tor₁^A(M, special case”; EGA IV (11.3.12), “b⇒a, special case”; SGA 1 IV (4.3), “case (b): (iv) ⇒ (iii)”; SGA 1 IV (5.6), “(ii)⇒(i), special case”.

Stacks 00MK (local criterion for flatness). Let R → S be a local homomorphism of Noetherian local rings, let κ be the residue field of R and let M be a finite S-module. If Tor₁^R(κ, M) = 0, then M is flat over R. Here Tor₁^R(κ, M) is ((Tor' (ModuleCat R) 1).obj κ).obj M, the first left derived functor of - ⊗_R M at κ.

theorem of_isZero_Tor'_one_residueField {R : Type u} (S : Type v) (M : Type u) [CommRing R]
    [CommRing S] [IsLocalRing R] [IsLocalRing S] [IsNoetherianRing R] [IsNoetherianRing S]
    [Algebra R S] [IsLocalHom (algebraMap R S)] [AddCommGroup M] [Module R M] [Module S M]
    [IsScalarTower R S M] [Module.Finite S M]
    (hTor : IsZero (((Tor' (ModuleCat.{u} R) 1).obj
      (ModuleCat.of R (ResidueField R))).obj (ModuleCat.of R M))) :
    Module.Flat R M
Tag 051C, a lemma

Tag 051C in the Stacks Project.

tor1_vanishes_of_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/TorCriterion/NilpotentIdeal.lean, line 220. The attribute's comment: “(2)”. References: SGA 1 IV (5.3), “=> (iii)”; SGA 1 IV (5.2), “(ii) ⇒ (i), special case”; SGA 3 VIB (12.7), “partial”.

If M/IM is flat over R/I and Tor₁^R(R/I, M) = 0, then Tor₁^R(N, M) = 0 for every R-module N annihilated by Iᵐ for some m.

theorem tor1_vanishes_of_annihilated
    (H1 : Module.Flat (R ⧸ I) (M ⧸ (I • (⊤ : Submodule R M))))
    (H2 : Tor1Vanishes R (R ⧸ I) M)
    (N : Type u) [AddCommGroup N] [Module R N]
    (m : ℕ) (hN : (I ^ m) • (⊤ : Submodule R N) = ⊥) :
    Tor1Vanishes R N M

flat_quotient_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/TorCriterion/NilpotentIdeal.lean, line 263. The attribute's comment: “(1)”. References: EGA 0 (10.2.1), “(b) ⇒ (d)”; EGA 0 (10.2.2), “b ⇒ d”; SGA 1 IV (5.5), “more general”; SGA 1 IV (5.6), “(ii)⇒(iv)”; SGA 3 VIB (12.7), “more general”.

If M/IM is flat over R/I and Tor₁^R(R/I, M) = 0, then for every n ≥ 1 the R/Iⁿ-module M/IⁿM is flat over R/Iⁿ.

theorem flat_quotient_pow
    (H1 : Module.Flat (R ⧸ I) (M ⧸ (I • (⊤ : Submodule R M))))
    (H2 : Tor1Vanishes R (R ⧸ I) M) :
    ∀ n : ℕ, 1 ≤ n →
      Module.Flat (R ⧸ I ^ n) (M ⧸ ((I ^ n) • (⊤ : Submodule R M)))

flat_of_nilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/TorCriterion/NilpotentIdeal.lean, line 281. The attribute's comment: “in particular”. References: EGA 0 (10.2.1), “(b)⇒(a), 𝔍 nilpotent”; EGA 0 (10.1.3), “(i)”; EGA 0 (10.2.2), “special case”; EGA IV (11.2.5), “special case”; EGA IV (11.3.12), “b⇒a when J is nilpotent”; SGA 1 IV (5.5), “(ii) => (i)”; SGA 1 IV (5.6), “(ii)⇒(i), special case”.

If M/IM is flat over R/I, Tor₁^R(R/I, M) = 0 and I is nilpotent, then M is flat over R.

theorem flat_of_nilpotent
    (H1 : Module.Flat (R ⧸ I) (M ⧸ (I • (⊤ : Submodule R M))))
    (H2 : Tor1Vanishes R (R ⧸ I) M)
    (hI : ∃ n : ℕ, 1 ≤ n ∧ I ^ n = ⊥) :
    Module.Flat R M
Tag 0AS8, a lemma

Tag 0AS8 in the Stacks Project.

Module.flat_quotient_pow_succ_of_flat_quotient_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/AdicFiltration.lean, line 204. The attribute's comment: “Both parts: part (1) is the case k = 1. The injectivity of M ⊗_R I^n/I^{n + 1} → I^nM/I^{n + 1}M is stated as exactness of M ⊗_R I^{n + 1} → M ⊗_R I^n → M/I^{n + 1}M, an equivalent form; see the module docstring.”.

Let R be a ring, I ⊆ R an ideal and M an R-module. If M/IM is flat over R/I and the multiplication map M ⊗_R I^n/I^{n+1} → I^nM/I^{n+1}M is injective for n = 1, …, k, then M/I^{k+1}M is flat over R/I^{k+1}.

The injectivity of M ⊗_R I^n/I^{n+1} → I^nM/I^{n+1}M is spelled as the exactness of M ⊗_R I^{n+1} → M ⊗_R I^n → M/I^{n+1}M, the first map being lTensor M of the inclusion I^{n+1} ⊆ I^n and the second m ⊗ x ↦ x • m followed by the quotient map; see the module docstring for why this is the same condition.

public theorem flat_quotient_pow_succ_of_flat_quotient_of_exact {R : Type u} [CommRing R]
    (I : Ideal R) (M : Type v) [AddCommGroup M] [Module R M] (k : ℕ)
    (hflat : Module.Flat (R ⧸ I) (M ⧸ (I • (⊤ : Submodule R M))))
    (hexact : ∀ n, 1 ≤ n → n ≤ k →
      Function.Exact
        ((Submodule.inclusion (Ideal.pow_le_pow_right n.le_succ : I ^ (n + 1) ≤ I ^ n)).lTensor M)
        ((I ^ (n + 1) • (⊤ : Submodule R M)).mkQ ∘ₗ
          (TensorProduct.rid R M).toLinearMap ∘ₗ (I ^ n).subtype.lTensor M)) :
    Module.Flat (R ⧸ I ^ (k + 1)) (M ⧸ (I ^ (k + 1) • (⊤ : Submodule R M)))
Tag 00ML, a lemma

Tag 00ML in the Stacks Project.

Module.Flat.of_rTensor_subtype_injective_of_flat_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriterionVariant/Criterion.lean, line 80. The attribute's comment: “The hypothesis Tor_1^R(M, R/I) = 0 is stated in the form Remark 00M6 identifies it with, the injectivity of I ⊗_R M → R ⊗_R M; this is the form the source's own second proof of the lemma assumes, and unlike Tor_1 it puts R and M in no common universe. See the module docstring.”. References: EGA IV (11.3.12), “partial”; SGA 1 IV (5.6), “(ii)⇒(i), special case”.

Stacks 00ML (variant of the local criterion for flatness). Let R → S be a local homomorphism of Noetherian local rings, let I ≠ R be an ideal of R and let M be a finite S-module. If Tor₁^R(M, R/I) = 0 and M/IM is flat over R/I, then M is flat over R. Here the Tor hypothesis appears in the form of Remark 00M6, as the injectivity of I ⊗_R M → R ⊗_R M, and M/IM is M ⧸ I • ⊤ with its canonical R ⧸ I-module structure.

public theorem of_rTensor_subtype_injective_of_flat_quotient {R : Type u} (S : Type v) (M : Type w)
    [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [IsNoetherianRing R]
    [IsNoetherianRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [AddCommGroup M] [Module R M]
    [Module S M] [IsScalarTower R S M] [Module.Finite S M] (I : Ideal R) (hI : I ≠ ⊤)
    (hTor : Function.Injective (I.subtype.rTensor M))
    (hflat : Module.Flat (R ⧸ I) (M ⧸ (I • (⊤ : Submodule R M)))) : Module.Flat R M
Tag 0523, a lemma

Tag 0523 in the Stacks Project.

Module.Flat.of_flat_quotient_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/AdicFiltration.lean, line 419. The attribute's comment: “Both statements: the second is the case where S is local, q is its maximal ideal and the localization is taken to be M itself. M/IⁿM is M ⧸ (I ^ n • ⊤ : Submodule R M) and M_q is given by IsLocalizedModule.AtPrime q f; see the module docstring.”. References: EGA 0 (10.2.1), “d ⇒ a”.

Let R → S be a ring map with R and S Noetherian, let I ⊆ R be an ideal and let M be a finite S-module. If M/IⁿM is flat over R/Iⁿ for every n ≥ 1, then for every prime q of S containing IS the localization M_q is flat over R.

The localization is taken abstractly: Mq is any S-module with a map f : M →ₗ[S] Mq exhibiting it as the localization of M at q. Taking S local with maximal ideal q, Mq = M and f = LinearMap.id shows that M is flat over R when IS is contained in the maximal ideal of a local S.

public theorem of_flat_quotient_pow {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [IsNoetherianRing R] [IsNoetherianRing S] (I : Ideal R)
    (M : Type*) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.Finite S M]
    (hflat : ∀ n : ℕ,
      Module.Flat (R ⧸ I ^ (n + 1)) (M ⧸ (I ^ (n + 1) • (⊤ : Submodule R M))))
    (q : Ideal S) [q.IsPrime] (hq : I.map (algebraMap R S) ≤ q)
    (Mq : Type*) [AddCommGroup Mq] [Module R Mq] [Module S Mq] [IsScalarTower R S Mq]
    (f : M →ₗ[S] Mq) [IsLocalizedModule.AtPrime q f] :
    Module.Flat R Mq
Tag 00MM, a lemma

Tag 00MM in the Stacks Project.

Stacks.TorOneBaseChange.tor_baseChange_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/TorOneBaseChange.lean, line 696. The attribute's comment: “Proved for the resolution model Tor1 S = H₁(P ⊗ᴿ S); the map is the explicit phi, not identified with the canonical derived base-change natural transformation.”.

Stacks Tag 00MM (Lemma 10.99.12).

Let R → R' → R'' be ring maps and let M be an R-module with a chosen projective resolution P over R. If the R'-module M ⊗ᴿ R' is flat over R', then the natural base-change map

Φ : R'' ⊗_{R'} Tor₁ᴿ(M, R') → Tor₁ᴿ(M, R'')

(equivalently Tor₁ᴿ(M, R') ⊗_{R'} R'' → Tor₁ᴿ(M, R'')), characterized by phi_apply_mk, is surjective. Here Tor₁ᴿ is the resolution model H₁(P ⊗ᴿ -); Φ is not identified with the canonical base-change natural transformation on derived functors (see the caveat on exists_baseChange_eq_phi).

The reduction to cycles_baseChange_surjective runs as follows. Tor1 R'' = K''/B'' is a quotient of K'' = cycles R'' d₁, so by surjectivity of the quotient map Submodule.Quotient.mk it suffices to hit every class ⟦c⟧ with c ∈ K''. By the crux cycles_baseChange_surjective, c = cyclesBC z for some z ∈ R'' ⊗_{R'} K', where cyclesBC = AlgebraTensorModule.lift (cyclesMap d₁). Pushing z through lTensor R'' (mkQ : K' → Tor1 R') gives an element of R'' ⊗_{R'} Tor1 R', and the square phi ∘ (id ⊗ mkQ) = mkQ'' ∘ cyclesBC commutes on generators r'' ⊗ k by phi_apply_mk (both sides are ⟦cmpBil r'' k⟧). Hence phi (lTensor mkQ z) = mkQ''(cyclesBC z) = ⟦c⟧, proving surjectivity.

theorem tor_baseChange_surjective
    (M : ModuleCat.{u} R) (P : ProjectiveResolution M)
    -- flatness hypothesis: `M ⊗ᴿ R'`, as an `R'`-module, is flat over `R'`.
    -- We use `R' ⊗ᴿ M`, the standard Mathlib orientation with `R'` on the left,
    -- which is canonically `R'`-isomorphic to `M ⊗ᴿ R'`.
    (hflat : Module.Flat R' (R' ⊗[R] (M : Type u))) :
    Function.Surjective
      (phi (R := R) (R' := R') (R'' := R'')
        (P.complex.d 2 1).hom (P.complex.d 1 0).hom)
Tag 00MN, a lemma

Tag 00MN in the Stacks Project.

TorSurjective.surjective_on_tor_one_trivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/BaseChangeSurjectivity.lean, line 1041. The attribute's comment: “Epi holds between the genuine Tor objects for N = R'/IR', but the comparison map is naturalMap conjugated by Classical.choice isomorphisms, so it is not identified with the canonical derived base-change natural transformation.”.

The Stacks lemma (tag [0BPB]). With N = R'/I' and M' = M ⊗_R R', the natural map Tor_1^R(R'/I', M) → Tor_1^{R'}(R'/I', M') (constructed via the Stacks data S: the pushed-forward R-free resolution, the genuine R'-resolution D differing only by an added free summand in degree 2, and the comparison chain map φ that is the identity in degrees 0, 1) is surjective, i.e. an epimorphism of abelian groups.

Equivalently, the map naturalMap f S (R'/I') induced on degree-1 homology is an epimorphism (see surjective_on_tor_one_trivial').

Scope of what is proved. torNaturalMap is naturalMap conjugated by Classical.choice of the Nonempty correctness isomorphisms naturalMap_src_iso / naturalMap_tgt_iso. Since Epi is invariant under pre- and post-composition with isomorphisms, the epimorphism conclusion between the genuine Tor objects torOneRestrict and torOneExtend is real, and the module N = quotIdeal f I = R'/IR' is exactly the module Stacks 00MN is stated for. What is not established is that torNaturalMap is the canonical base-change natural transformation on derived functors: because the two isomorphisms are extracted by choice, the map is not canonically determined. Pinning that down requires turning naturalMap_src_iso / naturalMap_tgt_iso into defs and identifying the composite with a NatTrans built independently of this construction.

theorem surjective_on_tor_one_trivial (I : Ideal R) (M : ModuleCat R)
    (F : ProjectiveResolution M) (S : StacksData f F) :
    Epi (torNaturalMap f S (quotIdeal f I))
Tag 00MO, a lemma

Tag 00MO in the Stacks Project.

Module.Flat.of_flat_quotient_of_tor_one_map_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriterionVariant/BaseChangeSquare.lean, line 680. The attribute's comment: “Tor₁ is spelled through Remark 00M6 as Ker(I ⊗_R M → R ⊗_R M), and the hypothesis that Tor_1^R(M, R/I) → Tor_1^{R'}(M', R'/I') is zero as the vanishing on that kernel of the canonical map I ⊗_R M → I' ⊗_{R'} M'. M' and S' are abstract (IsBaseChange, IsLocalization). The unused hypotheses R Noetherian, S local Noetherian, R → S local and S → S' local are dropped; see the module docstring.”. References: EGA IV (11.2.5), “case b), local rings”; EGA IV (11.3.12), “partial”.

Stacks 00MO. Let S ← R → R' → S', S → S' be a commutative square of ring maps with R, R', S' local, R' and S' Noetherian and R → R', R' → S' local, let I ⊆ R be a proper ideal, let M be a finite S-module and let f : M → M' be the base change of M to an S'-module. Assume S' is a localization of S ⊗_R R'. If M/IM is flat over R/I and the canonical map Tor_1^R(M, R/I) → Tor_1^{R'}(M', R'/I') is zero, then M' is flat over R'.

By Remark 00M6 the source Tor_1^R(M, R/I) is Ker(I ⊗_R M → R ⊗_R M) and the target is a submodule of I' ⊗_{R'} M' for I' = IR', so the last hypothesis is that the canonical map I ⊗_R M → I' ⊗_{R'} M', the unique R-linear map with a ⊗ x ↦ a ⊗ f x, vanishes on that kernel; see the module docstring.

public theorem of_flat_quotient_of_tor_one_map_eq_zero {R R' S S' M M' : Type*} [CommRing R]
    [CommRing R'] [CommRing S] [CommRing S'] [IsLocalRing R] [IsLocalRing R'] [IsNoetherianRing R']
    [IsLocalRing S'] [IsNoetherianRing S'] [Algebra R S] [Algebra R R'] [Algebra S S']
    [Algebra R' S'] [IsLocalHom (algebraMap R R')] [IsLocalHom (algebraMap R' S')]
    [Algebra (S ⊗[R] R') S'] [IsScalarTower S (S ⊗[R] R') S']
    (hR' :
      (algebraMap (S ⊗[R] R') S').comp
          (Algebra.TensorProduct.includeRight : R' →ₐ[R] S ⊗[R] R').toRingHom =
        algebraMap R' S')
    (T : Submonoid (S ⊗[R] R')) [IsLocalization T S'] [AddCommGroup M] [Module R M] [Module S M]
    [IsScalarTower R S M] [Module.Finite S M] [AddCommGroup M'] [Module R M'] [Module S M']
    [Module R' M'] [Module S' M'] [IsScalarTower R S M'] [IsScalarTower R R' M']
    [IsScalarTower S S' M'] [IsScalarTower R' S' M'] (I : Ideal R) (hI : I ≠ ⊤) (f : M →ₗ[S] M')
    (hf : IsBaseChange S' f) (hflat : Module.Flat (R ⧸ I) (M ⧸ (I • (⊤ : Submodule R M))))
    (htor :
      LinearMap.ker (I.subtype.rTensor M) ≤
        LinearMap.ker
          (TensorProduct.lift
            (((TensorProduct.mk R' ↥(I.map (algebraMap R R')) M').restrictScalars₁₂ R R).compl₁₂
              ((Algebra.linearMap R R').restrict (p := I) (q :=
                (I.map (algebraMap R R')).restrictScalars R) fun _ hx => Ideal.mem_map_of_mem _ hx)
              (f.restrictScalars R)))) :
    Module.Flat R' M'
Tag 00MP, a lemma

Tag 00MP in the Stacks Project.

Module.flat_and_flat_of_flat_quotient_maximalIdeal_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FibrewiseCriterion.lean, line 751. The attribute's comment: “The composite R → S' is not assumed: the two scalar towers on M already pin the R-action to the restriction along R → S → S'. 𝔪M is written as 𝔪S • ⊤ over S, so that the quotient carries the S/𝔪S-structure; see the module docstring.”. References: EGA IV (11.3.10), “special case”; EGA IV (11.3.10.1), “(a) ⇒ (b)”; SGA 1 I (5.9), “partial”; SGA 1 IV (5.9), “(ii) ⇒ (i)”; SGA 3 VIB (1.3.0), “special case”; SGA 3 VIB (12.7), “special case”; SGA 3 VIB (2.5), “flatness clause”; SGA 3 X (3.5), “Flat case”.

Critère de platitude par fibres, Noetherian local case. Let R → S → S' be local homomorphisms of Noetherian local rings, let 𝔪 ⊆ R be the maximal ideal of R, and let M be an S'-module whose S- and R-module structures come from the two ring maps. If M is finite over S', nonzero, M/𝔪M is flat over S/𝔪S and M is flat over R, then S is flat over R and M is flat over S.

public theorem Module.flat_and_flat_of_flat_quotient_maximalIdeal_of_flat
    {R S S' M : Type*} [CommRing R] [CommRing S] [CommRing S']
    [IsLocalRing R] [IsLocalRing S] [IsLocalRing S']
    [IsNoetherianRing R] [IsNoetherianRing S] [IsNoetherianRing S']
    [Algebra R S] [Algebra S S']
    [IsLocalHom (algebraMap R S)] [IsLocalHom (algebraMap S S')]
    [AddCommGroup M] [Module R M] [Module S M] [Module S' M]
    [IsScalarTower R S M] [IsScalarTower S S' M]
    [Module.Finite S' M] [Nontrivial M]
    [Module.Flat (S ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S))
      (M ⧸ ((IsLocalRing.maximalIdeal R).map (algebraMap R S) • (⊤ : Submodule S M)))]
    [Module.Flat R M] :
    Module.Flat R S ∧ Module.Flat S M
Tag 0H7N, a lemma

Tag 0H7N in the Stacks Project.

Module.flat_and_faithfullyFlat_of_flat_away_of_flat_quotSMulTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriteria/TorAndNilpotentDescent.lean, line 670. The attribute's comment: “The two forms of the lemma are the two components of the conjunction: they share the hypotheses on f. M_f is an arbitrary localization away from f (IsLocalization.Away, IsLocalizedModule) rather than the model, M/fM is QuotSMulTop f M over A ⧸ Ideal.span {f}, and f a nonzerodivisor on A and on M is IsSMulRegular A f and IsSMulRegular M f.”.

Stacks 0H7N. Let A be a ring, let M be an A-module and let f ∈ A be a nonzerodivisor on A and on M. If M_f is a flat A_f-module and M/fM is a flat A/fA-module, then M is a flat A-module; the same with "flat" replaced by "faithfully flat".

Here A_f is any localization Aₜ of A away from f and M_f is any localization Mₜ of M at the powers of f, while M/fM is QuotSMulTop f M as a module over A ⧸ Ideal.span {f}.

theorem flat_and_faithfullyFlat_of_flat_away_of_flat_quotSMulTop
    {A : Type*} [CommRing A] {M : Type*} [AddCommGroup M] [Module A M] (f : A)
    (Aₜ : Type*) [CommRing Aₜ] [Algebra A Aₜ] [IsLocalization.Away f Aₜ]
    (Mₜ : Type*) [AddCommGroup Mₜ] [Module A Mₜ] [Module Aₜ Mₜ] [IsScalarTower A Aₜ Mₜ]
    (g : M →ₗ[A] Mₜ) [IsLocalizedModule (Submonoid.powers f) g]
    (hA : IsSMulRegular A f) (hM : IsSMulRegular M f) :
    (Flat Aₜ Mₜ → Flat (A ⧸ Ideal.span {f}) (QuotSMulTop f M) → Flat A M) ∧
      (FaithfullyFlat Aₜ Mₜ → FaithfullyFlat (A ⧸ Ideal.span {f}) (QuotSMulTop f M) →
        FaithfullyFlat A M)
Tag 0H7P, a lemma

Tag 0H7P in the Stacks Project.

Module.flat_and_faithfullyFlat_of_isLocalized_away_of_isZero_Tor', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/TorCriterion/AwayGenerators.lean, line 766. The attribute's comment: “Both statements: .1 is the flat one and .2 the faithfully flat one ("same with flat replaced by faithfully flat"), sharing the generating family and the Tor hypotheses. The two arguments of Tor_n^A are in the order used by the source's own proof (through 051C), namely Tor_n^A(A/I, M); the two orders agree by the symmetry of Tor (00M3). The generators are a family indexed by a finite type, and the source's r ≥ 1 is dropped. See the module docstring.”.

Let A be a ring, let M be an A-module, and let I be the ideal generated by a finite family of elements f i of A, with r the number of generators. Assume Tor_n^A(A/I, M) = 0 for 1 ≤ n ≤ r + 1. If each localization M_{f i} is flat over A_{f i} and M/IM is flat over A/I, then M is flat over A; and the same with "flat" replaced by "faithfully flat" throughout.

Here Tor_n^A(A/I, M) is ((Tor' (ModuleCat A) n).obj (A ⧸ I)).obj M, the n-th left derived functor of - ⊗_A M evaluated at A ⧸ I, and M/IM is M ⧸ I • ⊤ with its canonical A ⧸ I-module structure. The localizations are given abstractly, by IsLocalization.Away (f i) (Af i) and IsLocalizedModule.Away (f i) (g i).

public theorem flat_and_faithfullyFlat_of_isLocalized_away_of_isZero_Tor'
    (hI : Ideal.span (Set.range f) = I)
    (hTor : ∀ n : ℕ, 1 ≤ n → n ≤ Nat.card ι + 1 →
      IsZero (((Tor' (ModuleCat.{u} A) n).obj (ModuleCat.of A (A ⧸ I))).obj
        (ModuleCat.of A M))) :
    ((∀ i, Module.Flat (Af i) (Mf i)) →
        Module.Flat (A ⧸ I) (M ⧸ (I • (⊤ : Submodule A M))) →
        Module.Flat A M) ∧
      ((∀ i, Module.FaithfullyFlat (Af i) (Mf i)) →
        Module.FaithfullyFlat (A ⧸ I) (M ⧸ (I • (⊤ : Submodule A M))) →
        Module.FaithfullyFlat A M)
Sources
LeanModule.Flat.injective_and_flat_quotient_range_of_injective_mapQ_maximalIdeal_of_isNoetherianRing · Module.Flat.mem_nonZeroDivisors_and_flat_quotient_span_singleton_of_mem_nonZeroDivisors_maximalIdeal · Module.Flat.isRegular_and_flat_quotient_ofList_take_of_isRegular_maximalIdeal · Module.Flat.free_and_flat_of_free_maximalIdeal · Module.Flat.exactAt_and_flat_cokernel_of_exactAt_maximalIdeal · IsLocalRing.isZero_Tor'_one_of_isFiniteLength · Module.Flat.of_isZero_Tor'_one_residueField · tor1_vanishes_of_annihilated

Section10.100 Base change and flatness#

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

Tag 00MQ, a lemma

Tag 00MQ in the Stacks Project.

Module.Flat.baseChange_and_of_flat_baseChange_of_isPushout_of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/BaseChange.lean, line 267. The attribute's comment: “Parts (1) and (2). Of the source's eight locality assumptions only IsLocalRing S, IsLocalRing S' and IsLocalHom (algebraMap S S') are used, by part (2) alone, and they are bound inside the second conjunct together with Module.Flat R R', so that part (1) is stated for an arbitrary commutative square; the rest are dropped. "S' is a localization of S ⊗_R R'" is IsLocalization W S' over an abstract pushout Algebra.IsPushout R S R' T, as in the siblings 00P4 and 00RJ, and M' = S' ⊗_S M is IsBaseChange S' f, as in 00MO. Parts (3) and (4) are the instance M := S, M' := S' and are not separate declarations. See the module docstring.”.

Stacks 00MQ, parts (1) and (2). Let S ← R → R' be ring maps, let T be the pushout S ⊗_R R', let S' be a localization of T at a submonoid W, and let f : M →ₗ[S] M' realize M' as the base change S' ⊗_S M of an S-module M. Then (1) if M is flat over R then M' is flat over R', and (2) if moreover S and S' are local with S → S' a local homomorphism, then M' flat over R' and R → R' flat imply M flat over R.

Part (1) holds for an arbitrary such square: the source's local rings and local homomorphisms are used only in part (2), and only for S, S' and S → S', so they are bound inside the second conjunct instead of in the signature.

Parts (3) and (4) of the source, that S flat over R implies S' flat over R' and that R' → S' and R → R' flat imply S flat over R, are the instance M := S, M' := S', f := Algebra.linearMap S S'; see the module docstring.

public theorem baseChange_and_of_flat_baseChange_of_isPushout_of_isLocalization
    (R : Type*) {S R' T S' M M' : Type*}
    [CommRing R] [CommRing S] [CommRing R'] [CommRing T] [CommRing S']
    [Algebra R S] [Algebra R R'] [Algebra R T] [Algebra S T] [Algebra R' T]
    [IsScalarTower R S T] [IsScalarTower R R' T] [Algebra.IsPushout R S R' T]
    [Algebra S S'] [Algebra R' S'] [Algebra T S']
    [IsScalarTower S T S'] [IsScalarTower R' T S']
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [AddCommGroup M'] [Module S M'] [Module R' M'] [Module S' M']
    [IsScalarTower S S' M'] [IsScalarTower R' S' M']
    (W : Submonoid T) [IsLocalization W S'] (f : M →ₗ[S] M') (hf : IsBaseChange S' f) :
    (Module.Flat R M → Module.Flat R' M') ∧
      (∀ [IsLocalRing S] [IsLocalRing S'] [IsLocalHom (algebraMap S S')],
        Module.Flat R' M' → Module.Flat R R' → Module.Flat R M)
Tag 0GEB, a lemma

Tag 0GEB in the Stacks Project.

Module.Flat.baseChange_of_map_maximalIdeal_eq_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalBaseChange.lean, line 254. The attribute's comment: “The commutative square is presented by the two scalar towers into S', M ⊗_S S' by IsBaseChange S' f as in the sibling 00MO, and 𝔪_R R' by Ideal.map (algebraMap R R') (IsLocalRing.maximalIdeal R). The source's unused hypotheses S local, R → S local and S → S' local are dropped, and R → R' local is implied by hm. See the module docstring.”.

Stacks 0GEB. Let S ← R → R', S → S', R' → S' be a commutative diagram of local rings and local homomorphisms, let M be a finite S-module and let f : M → M' realize M' as the base change M ⊗_S S'. Assume the horizontal arrows R → R' and S → S' are flat, that M is flat over R, that 𝔪_R R' = 𝔪_{R'} and that R' and S' are Noetherian. Then M' is flat over R'.

public theorem baseChange_of_map_maximalIdeal_eq_maximalIdeal
    {R S R' S' M M' : Type*} [CommRing R] [CommRing S] [CommRing R'] [CommRing S']
    [IsLocalRing R] [IsLocalRing R'] [IsLocalRing S']
    [IsNoetherianRing R'] [IsNoetherianRing S']
    [Algebra R S] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S']
    [IsScalarTower R S S'] [IsScalarTower R R' S']
    [IsLocalHom (algebraMap R' S')]
    [Module.Flat R R'] [Module.Flat S S']
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.Finite S M] [Module.Flat R M]
    [AddCommGroup M'] [Module S M'] [Module R' M'] [Module S' M']
    [IsScalarTower S S' M'] [IsScalarTower R' S' M']
    (hm : (IsLocalRing.maximalIdeal R).map (algebraMap R R') = IsLocalRing.maximalIdeal R')
    (f : M →ₗ[S] M') (hf : IsBaseChange S' f) :
    Module.Flat R' M'
Sources
LeanModule.Flat.baseChange_and_of_flat_baseChange_of_isPushout_of_isLocalization · Module.Flat.baseChange_of_map_maximalIdeal_eq_maximalIdeal

Section10.101 Flatness criteria over Artinian rings#

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

Tag 051F, a lemma

Tag 051F in the Stacks Project.

Module.Flat.linearIndependent_and_span_eq_top_mkQ_comp_iff_of_isNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Nilpotent.lean, line 282. The attribute's comment: “Stated for an arbitrary nilpotent ideal I of an arbitrary commutative ring, the source's local ring being the case I = IsLocalRing.maximalIdeal R; M/IM is M ⧸ I • ⊤ over R ⧸ I with reduction map Submodule.mkQ, and forms a basis is LinearIndependent … ∧ Submodule.span … = ⊤. See the module docstring.”. References: SGA 3 VIIA (7.4.3), “special case”; SGA 3 VIII (6.2), “flat clause”.

Let R be a commutative ring, let I ⊆ R be a nilpotent ideal and let M be a flat R-module. A family x : ι → M, indexed by an arbitrary type, is an R-basis of M if and only if the family of its reductions is an R/I-basis of M/IM. "Is a basis" is read as LinearIndependent … ∧ Submodule.span … = ⊤, the hypotheses of Module.Basis.mk.

theorem linearIndependent_and_span_eq_top_mkQ_comp_iff_of_isNilpotent {R : Type*}
    [CommRing R] {M : Type*} [AddCommGroup M] [Module R M] [Module.Flat R M] (I : Ideal R)
    (hI : IsNilpotent I) {ι : Type*} (x : ι → M) :
    (LinearIndependent (R ⧸ I) ((I • (⊤ : Submodule R M)).mkQ ∘ x) ∧
        Submodule.span (R ⧸ I) (Set.range ((I • (⊤ : Submodule R M)).mkQ ∘ x)) = ⊤) ↔
      (LinearIndependent R x ∧ Submodule.span R (Set.range x) = ⊤)
Tag 051G, a lemma

Tag 051G in the Stacks Project.

Module.tfae_flat_free_projective_of_isNilpotent_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/NilpotentIdeal.lean, line 386. The attribute's comment: “The equivalence is a List.TFAE in the source's order (flat, free, projective); nilpotence of the maximal ideal is IsNilpotent (IsLocalRing.maximalIdeal R).”. References: EGA 0 (10.1.3), “case (i)”; EGA 0 (10.1.3), “case (i)”; EGA III (7.3.5), “commutative case”; EGA IV (11.3.12), “special case”; EGA IV (2.2.17), “special case”; SGA 1 IV (4.3), “(i),(ii),(iii)”; SGA 3 VIA (2.1.3), “special case”; SGA 3 VIB (6.2.2), “more general”; SGA 3 VIIA (8.4), “partial”; SGA 3 VIIB (0.2.2), “special case”; SGA 3 VIIB (0.3.7), “local Artinian rings”; SGA 3 VIIB (1.2.1), “special case”; SGA 3 VIII (6.2), “more general”.

Stacks 051G: let (R, 𝔪) be a local ring whose maximal ideal is nilpotent — an Artinian local ring, for instance — and let M be an R-module. Then M is flat over R if and only if M is a free R-module if and only if M is a projective R-module. No finiteness hypothesis on M is needed; compare Module.free_of_flat_of_isLocalRing, which assumes Module.Finite R M over an arbitrary local ring, and Module.Flat.projective_of_finitePresentation. The proof is the source's: a family of elements of M whose reductions form a basis of M/𝔪M over R/𝔪 is a basis of M over R, by Lemma 051F.

public theorem tfae_flat_free_projective_of_isNilpotent_maximalIdeal {R : Type*} [CommRing R]
    [IsLocalRing R] {M : Type*} [AddCommGroup M] [Module R M]
    (hR : IsNilpotent (IsLocalRing.maximalIdeal R)) :
    List.TFAE [Module.Flat R M, Module.Free R M, Module.Projective R M]
Tag 051H, a lemma

Tag 051H in the Stacks Project.

Stacks.FreeOfNilpotentIdeal.free_of_nilpotent_of_basis_mod_of_tor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Free/OfNilpotentIdeal/Freeness.lean, line 511.

Theorem (Stacks Project, Tag 051H; Lemma 10.101.3).

Let R be a ring, I ⊆ R an ideal, M an R-module, A a set, and x : A → M a family of elements of M. Assume:

  1. I is nilpotent;
  2. the family of reductions (reduction I (x α))_{α} forms a basis of the R/I-module M/IM, witnessed by a basis b with b α = reduction I (x α);
  3. Tor₁^R(R/I, M) = 0, expressed as injectivity of the multiplication map torMul I : I ⊗_R M → M.

Then x is a basis of M as an R-module: it is linearly independent and spans M.

theorem free_of_nilpotent_of_basis_mod_of_tor
    {A : Type*} (x : A → M) (I : Ideal R)
    (hI : IsNilpotent I)
    (b : Module.Basis A (R ⧸ I) (M ⧸ smul (M := M) I))
    (hb : ∀ α, b α = reduction I (x α))
    (hTor : Function.Injective (torMul (M := M) I)) :
    LinearIndependent R x ∧ ⊤ ≤ Submodule.span R (Set.range x)
Tag 051I, a lemma

Tag 051I in the Stacks Project.

flat_quot_idealTwo_smul_top_of_flat_quot_and_flat_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriteria/SquareZeroCriterion.lean, line 487.

Stacks Tag 051I, Lemma 10.101.4. Wires the square-zero local criterion (flat_of_sq_zero_local_criterion) to the two base-change inputs (hquot_from_h1, htor_from_base_change), using that the image of I in R ⧸ I₂ is square-zero (image_I_sq_eq_bot).

theorem flat_quot_idealTwo_smul_top_of_flat_quot_and_flat_baseChange
    {R R' : Type*} [CommRing R] [CommRing R'] [Algebra R R']
    {M : Type*} [AddCommGroup M] [Module R M]
    (I : Ideal R)
    (h1 : Module.Flat (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M)))
    (h2 : Module.Flat R' (R' ⊗[R] M)) :
    Module.Flat (R ⧸ idealTwo I R')
      (M ⧸ (idealTwo I R') • (⊤ : Submodule R M))
Tag 051J, a lemma

Tag 051J in the Stacks Project.

Module.Flat.of_flat_quotient_of_flat_tensorProduct_of_isNilpotent_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalCriteria/TorAndNilpotentDescent.lean, line 889. The attribute's comment: “The ring map is algebraMap R R'; M/IM is M ⧸ I • ⊤ with its canonical R ⧸ I-action and the base change is R' ⊗[R] M, acted on by R' through the left factor. See the module docstring.”. References: EGA IV (11.4.1), “special case”; EGA IV (11.4.9), “sufficiency (flat case)”.

Stacks 051J: the local criterion for flatness along an injective ring map. Let φ : R → R' be a map of commutative rings, I ⊆ R a nilpotent ideal and M an R-module. If φ = algebraMap R R' is injective, M/IM is flat over R ⧸ I and the base change R' ⊗[R] M is flat over R', then M is flat over R. Compare Module.Flat.of_flat_tensorProduct, which descends flatness along a faithfully flat ring map with no nilpotent ideal in sight, and Module.Flat.of_flat_baseChange_of_injective (Stacks 051L), the case where R is Artinian and I is its Jacobson radical, so that flatness of the reduction is automatic. The proof is the source's: the tower I₁ = I, I_{n+1} = φ⁻¹(φ(I_n) ^ 2 R') reaches 0 because I is nilpotent and φ is injective, and each step preserves flatness of the reduction by the square-zero criterion (Stacks 051I).

public theorem of_flat_quotient_of_flat_tensorProduct_of_isNilpotent_of_injective
    {R R' : Type*} [CommRing R] [CommRing R'] [Algebra R R']
    {M : Type*} [AddCommGroup M] [Module R M] (I : Ideal R)
    (hI : IsNilpotent I) (hφ : Function.Injective (algebraMap R R'))
    (hMI : Module.Flat (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M)))
    (hM' : Module.Flat R' (R' ⊗[R] M)) :
    Module.Flat R M
Tag 051K, a lemma

Tag 051K in the Stacks Project.

Module.Flat.iff_flat_quotient_and_isZero_Tor'_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Nilpotent.lean, line 315. The attribute's comment: “The source's Artinian local R is weakened to R local with nilpotent maximal ideal, the hypothesis of 051G; Tor_1^R(R/I, M) is Tor', which derives the first variable, as in 00MJ and 00M5. See the module docstring.”. References: EGA 0 (10.1.3), “(i): c ⇔ d, c ⇔ d”; EGA 0 (10.2.1), “a ⇒ b, a ⇔ b”; EGA IV (11.2.5), “special case”; SGA 1 IV (5.5), “(i)⇔(ii), special case”.

The local criterion for flatness over a local ring with nilpotent maximal ideal (an Artinian local ring, for instance). Let R be such a ring, let M be an R-module and let I ⊆ R be a proper ideal. Then M is flat over R if and only if M/IM is flat over R/I and Tor₁^R(R/I, M) = 0. Here Tor₁^R(R/I, M) is ((Tor' (ModuleCat R) 1).obj (ModuleCat.of R (R ⧸ I))).obj (ModuleCat.of R M), the first left derived functor of - ⊗ M evaluated at R ⧸ I.

theorem iff_flat_quotient_and_isZero_Tor'_one {R : Type u} [CommRing R] [IsLocalRing R]
    (M : Type u) [AddCommGroup M] [Module R M] (I : Ideal R)
    (hR : IsNilpotent (IsLocalRing.maximalIdeal R)) (hI : I ≠ ⊤) :
    Module.Flat R M ↔
      Module.Flat (R ⧸ I) (M ⧸ (I • ⊤ : Submodule R M)) ∧
        IsZero (((Tor' (ModuleCat.{u} R) 1).obj (ModuleCat.of R (R ⧸ I))).obj
          (ModuleCat.of R M))
Tag 051L, a lemma

Tag 051L in the Stacks Project.

Module.Flat.of_flat_baseChange_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/BaseChange.lean, line 487. The attribute's comment: “The source's M ⊗_R S is an arbitrary base change f : M →ₗ[R] N with IsBaseChange S f, which specialises to it by TensorProduct.isBaseChange; injectivity of the ring map is injectivity of algebraMap R S. See the module docstring.”.

Stacks 051L: flatness descends along an injective ring map whose source is Artinian. Let R → S be a map of commutative rings with R Artinian and algebraMap R S injective, let M be an R-module and let f : M →ₗ[R] N exhibit N as the base change of M to S, for instance N = S ⊗[R] M with f = TensorProduct.mk R S M 1. If N is flat over S, then M is flat over R. Compare Module.Flat.of_flat_tensorProduct, where R → S is faithfully flat instead.

public theorem of_flat_baseChange_of_injective {R : Type*} [CommRing R] [IsArtinianRing R]
    (S : Type*) [CommRing S] [Algebra R S] {M : Type*} [AddCommGroup M] [Module R M]
    (N : Type*) [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N]
    [Module.Flat S N] {f : M →ₗ[R] N} (hf : IsBaseChange S f)
    (hRS : Function.Injective (algebraMap R S)) :
    Module.Flat R M
Tag 06A5, a lemma

Tag 06A5 in the Stacks Project.

Module.flat_and_flat_localization_of_flat_quotient_of_isNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FibrewiseCriterion.lean, line 503. The attribute's comment: “The auxiliary ring S' of the source's triangle is dropped: M is taken to be an S-module over R → S, which is equivalent and does not mention S'. IM is written as IS • ⊤ over S, and S_q is an abstract localization at q; see the module docstring.”. References: EGA IV (11.3.11), “(a) ⇒ (b), special case”; SGA 1 IV (5.9), “(ii) ⇒ (i), special case”; SGA 3 VIB (1.3.0), “special case”; SGA 3 VIB (12.7), “more general”; SGA 3 VIB (2.5), “flatness clause”.

Critère de platitude par fibres, nilpotent case. Let R → S be a map of commutative rings, let M be an S-module whose R-module structure comes from R → S, and let I ⊆ R be a nilpotent ideal. If M/IM is flat over S/IS and M is flat over R, then M is flat over S, and S_q is flat over R for every prime q ⊆ S with M ⊗_S κ(q) nonzero.

public theorem Module.flat_and_flat_localization_of_flat_quotient_of_isNilpotent
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    {M : Type*} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    (I : Ideal R) (hI : IsNilpotent I)
    [Module.Flat (S ⧸ I.map (algebraMap R S))
      (M ⧸ (I.map (algebraMap R S) • (⊤ : Submodule S M)))]
    [Module.Flat R M] :
    Module.Flat S M ∧
      ∀ (q : Ideal S) [q.IsPrime] (Sq : Type*) [CommRing Sq] [Algebra S Sq]
        [IsLocalization.AtPrime Sq q] [Algebra R Sq] [IsScalarTower R S Sq],
        Nontrivial (M ⊗[S] q.ResidueField) → Module.Flat R Sq
Sources
LeanModule.Flat.linearIndependent_and_span_eq_top_mkQ_comp_iff_of_isNilpotent · Module.tfae_flat_free_projective_of_isNilpotent_maximalIdeal · Stacks.FreeOfNilpotentIdeal.free_of_nilpotent_of_basis_mod_of_tor · flat_quot_idealTwo_smul_top_of_flat_quot_and_flat_baseChange · Module.Flat.of_flat_quotient_of_flat_tensorProduct_of_isNilpotent_of_injective · Module.Flat.iff_flat_quotient_and_isZero_Tor'_one · Module.Flat.of_flat_baseChange_of_injective · Module.flat_and_flat_localization_of_flat_quotient_of_isNilpotent

Section10.102 What makes a complex exact?#

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

Tag 00MS, a situation

Tag 00MS in the Stacks Project.

BoundedFreeComplex, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/FiniteFreeComplex/BoundedFreeComplex.lean, line 35. References: SGA 4½ Rapport (4.11).

A complex 0 → R^{n_e} → R^{n_{e-1}} → ⋯ → R^{n_0} of finite free R-modules, as in Stacks Situation 10.102.1 (tag 00MS). The ranks are given by n : ℕ → ℕ with n i = 0 for i > e, and the differential R^{n_{i+1}} → R^{n_i} by the matrix φ i : Matrix (Fin (n i)) (Fin (n (i + 1))) R.

structure BoundedFreeComplex (R : Type*) [CommRing R]
Tag 00MT, a lemma

Tag 00MT in the Stacks Project.

exists_splitOff_elementaryComplex_of_hasInvertibleCoeff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/FiniteFreeComplex/SplitOffElementary.lean, line 801.

Let R be a ring and C a complex of finite free R-modules C_j = R^{n_j}. If the differential φ_i has an invertible matrix coefficient, then n_i ≥ 1, n_{i-1} ≥ 1, and there is a complex of finite free R-modules C' with the ranks decremented at degrees i and i-1 (and unchanged elsewhere) together with an isomorphism of complexes C ≅ C' ⊕ T^{(i)}, where T^{(i)} is the elementary identity complex of elementaryComplex.

theorem exists_splitOff_elementaryComplex_of_hasInvertibleCoeff {R : Type*} [CommRing R]
    (C : FreeComplex R) (i : ℤ) (h : HasInvertibleCoeff C i) :
    1 ≤ C.n i ∧ 1 ≤ C.n (i - 1) ∧
    ∃ C' : FreeComplex R,
      (∀ j, C'.n j = if j = i then C.n i - 1 else if j = i - 1 then C.n (i - 1) - 1 else C.n j) ∧
      Nonempty (C.toComplex ≅ C'.toComplex ⊞ (elementaryComplex R i).toComplex)
Tag 00MY, a lemma

Tag 00MY in the Stacks Project.

exists_trivial_iso_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/FiniteFreeComplex/TrivialIsoOfExact.lean, line 802.

Let R be a Noetherian local ring whose maximal ideal m is an associated prime of R, i.e. R has depth 0. Then every complex of finite free R-modules 0 → R^{n_e} → ⋯ → R^{n_0} which is exact at R^{n_e}, …, R^{n_1} is isomorphic to a complex of the same length and ranks all of whose differentials are partial permutation matrices, that is, to a direct sum of trivial complexes.

theorem exists_trivial_iso_of_exact
    [IsNoetherianRing R] [IsLocalRing R]
    (hdepth : (IsLocalRing.maximalIdeal R) ∈ associatedPrimes R R)
    (C : BoundedFreeComplex R) (hC : C.Exact) :
    ∃ D : BoundedFreeComplex R, ∃ _ : C.Iso D,
      D.e = C.e ∧ (∀ i, D.n i = C.n i) ∧ D.IsTrivial
Tag 00MU, a lemma

Tag 00MU in the Stacks Project.

LinearMap.exists_trivialDecomposition_of_injective_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Artinian/FreeComplex.lean, line 501.

An exact complex of finite free modules over an Artinian local ring is a direct sum of trivial complexes. Let R be an Artinian local ring and let 0 → R^{n_{e+1}} →[φ e] R^{n_e} → ⋯ → R^{n_1} →[φ 0] R^{n_0} be a complex of finite free R-modules which is exact at R^{n_{e+1}}, …, R^{n_1}. Then there are multiplicities c j and R-linear bijections g i : R^{n_i} ≃ R^{c_i} × R^{c_{i+1}} in the degrees i ≤ e + 1, with c (e + 2) = 0, carrying each differential φ i to (x, y) ↦ (0, x); that is, the complex is isomorphic to the direct sum of c_j copies, for each 0 ≤ j ≤ e + 1, of the trivial complex with the identity map of R in degrees j and j - 1.

public theorem LinearMap.exists_trivialDecomposition_of_injective_of_exact
    {R : Type*} [CommRing R] [IsArtinianRing R] [IsLocalRing R] (e : ℕ) (n : ℕ → ℕ)
    (φ : ∀ i, (Fin (n (i + 1)) → R) →ₗ[R] (Fin (n i) → R))
    (hφ : ∀ k < e, φ k ∘ₗ φ (k + 1) = 0)
    (htop : Function.Injective (φ e))
    (hex : ∀ k < e, Function.Exact (φ (k + 1)) (φ k)) :
    ∃ (c : ℕ → ℕ) (g : ∀ i, (Fin (n i) → R) →ₗ[R] ((Fin (c i) → R) × (Fin (c (i + 1)) → R))),
      c (e + 2) = 0 ∧ (∀ i ≤ e + 1, Function.Bijective (g i)) ∧
        (∀ i ≤ e, g i ∘ₗ φ i = LinearMap.inr R _ _ ∘ₗ LinearMap.fst R _ _ ∘ₗ g (i + 1))
Tag 00MV, a definition

Tag 00MV in the Stacks Project.

Stacks.DeterminantalRank.exteriorRank, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/DeterminantalRank/ExteriorRank.lean, line 103. The attribute's comment: “(1)”.

The rank of φ = mulVecLin A: the largest r ≤ min m n such that the r-th exterior power ⋀^r φ is nonzero. Since ⋀^r φ = 0 for r > min m n, and ⋀^0 φ = id ≠ 0 for nontrivial R, this is the largest r with ⋀^r φ ≠ 0.

noncomputable def exteriorRank (A : Matrix (Fin n) (Fin m) R) : ℕ

Stacks.DeterminantalRank.detIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/DeterminantalRank/ExteriorRank.lean, line 109. The attribute's comment: “(2)”.

The determinantal ideal I(φ): the ideal generated by the rank × rank minors of A. When rank = 0 the only minor is the empty minor det (A.submatrix _ _) = 1, so I(φ) = R.

noncomputable def detIdeal (A : Matrix (Fin n) (Fin m) R) : Ideal R
Tag 00MW, a lemma

Tag 00MW in the Stacks Project.

StacksComplex.rank_eq_rIndex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/DeterminantalRank/SumOfTrivials.lean, line 478. The attribute's comment: “(1)”.

If the complex is isomorphic to a direct sum of trivial complexes, then for 1 ≤ i ≤ e the rank of φ_i (which is d (i-1), or equivalently d k with k = i-1 ranging over 0 ≤ k ≤ e-1) equals r_i = ∑_{l=i}^e (-1)^{l-i} n_l.

theorem rank_eq_rIndex (C : Complex R e) (hC : IsoToSumOfTrivials C)
    (k : ℕ) (hk : k < e) :
    (rank (C.d k) : ℤ) = rIndex C (k + 1)

StacksComplex.rank_add_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/DeterminantalRank/SumOfTrivials.lean, line 489. The attribute's comment: “(2)”.

If the complex is isomorphic to a direct sum of trivial complexes, then for 1 ≤ i ≤ e-1, rank(φ_{i+1}) + rank(φ_i) = n_i. In the indexing d j = φ_{j+1}, with k = i-1 ranging over 0 ≤ k ≤ e-2, this reads rank (d (k+1)) + rank (d k) = n (k+1).

theorem rank_add_rank (C : Complex R e) (hC : IsoToSumOfTrivials C)
    (k : ℕ) (hk : k + 1 < e) :
    rank (C.d (k + 1)) + rank (C.d k) = C.n (k + 1)

StacksComplex.minorIdeal_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/DeterminantalRank/SumOfTrivials.lean, line 527. The attribute's comment: “(3)”.

If the complex is isomorphic to a direct sum of trivial complexes, then for 1 ≤ i ≤ e, the ideal I(φ_i) is the unit ideal R. In the indexing d k = φ_{k+1} with 0 ≤ k ≤ e-1, this is I(d k) = ⊤.

theorem minorIdeal_eq_top (C : Complex R e) (hC : IsoToSumOfTrivials C)
    (k : ℕ) :
    minorIdeal (C.d k) = ⊤
Tag 00MZ, a lemma

Tag 00MZ in the Stacks Project.

tag_00MZ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/FiniteFreeComplex/ReductionModNonzerodivisor.lean, line 65.

Let R be a commutative local ring with maximal ideal m, and let φ : R^{n (•+1)} → R^{n •} be a complex of finite free modules ending at position e (so n (e+1) = 0). If the complex is exact at positions 1, ..., e and x ∈ m is a nonzerodivisor of R, then the reduced complex φ mod x is exact at positions 2, ..., e.

theorem tag_00MZ (R : Type*) [CommRing R] [IsLocalRing R]
    (e : ℕ) (n : ℕ → ℕ)
    (φ : (i : ℕ) → Matrix (Fin (n i)) (Fin (n (i + 1))) R)
    (hcomplex : IsMatrixComplex n φ)
    (x : R)
    (hxnzd : ∀ r : R, x * r = 0 → r = 0)
    (hexact : ∀ i, i < e → ExactAtSucc n φ i) :
    ∀ i, 1 ≤ i → i < e → ExactAtSucc n (reduceMat x n φ) i
Tag 00N0, a lemma

Tag 00N0 in the Stacks Project.

Module.one_le_depth_homology_of_forall_le_depth_of_isGreatest_not_exactAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/Acyclicity.lean, line 205.

Acyclicity lemma. Let R be a Noetherian local ring and let 0 → M_e → M_{e-1} → ⋯ → M_0 be a complex of finite R-modules, presented as a chain complex C of R-modules with C.X j = 0 for j > e. Assume depth(M_i) ≥ i for i ≤ e. If i is the largest index at which C fails to be exact and i > 0, then Ker(M_i → M_{i-1})/Im(M_{i+1} → M_i) has depth at least 1.

public theorem Module.one_le_depth_homology_of_forall_le_depth_of_isGreatest_not_exactAt
    {R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (C : ChainComplex (ModuleCat.{v} R) ℕ) [∀ j, Module.Finite R (C.X j)] (e : ℕ)
    (hC : ∀ j, e < j → IsZero (C.X j))
    (hdepth : ∀ j ≤ e, (j : ℕ∞) ≤ Module.depth R (IsLocalRing.maximalIdeal R) (C.X j))
    {i : ℕ} (hi : IsGreatest {j : ℕ | ¬ C.ExactAt j} i) (hi0 : 0 < i) :
    1 ≤ Module.depth R (IsLocalRing.maximalIdeal R) (C.homology i)
Tag 00N1, a proposition

Tag 00N1 in the Stacks Project.

LinearMap.injective_and_exact_iff_forall_rank_eq_and_le_depth_minors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/ExactnessCriterion/Converse.lean, line 699.

Buchsbaum–Eisenbud exactness criterion. A complex 0 → R^{n_{e+1}} →[φ e] R^{n_e} → ⋯ → R^{n_1} →[φ 0] R^{n_0} of finite free modules over a local Noetherian ring is exact at R^{n_{e+1}}, …, R^{n_1} if and only if, for every k ≤ e, the rank of φ k — the largest r with ⋀^r (φ k) ≠ 0 — is the alternating sum n_{k+1} - n_{k+2} + ⋯ ± n_{e+1}, and the ideal generated by the r × r minors of the matrix of φ k has depth at least k + 1, that is, it is R or contains a regular sequence of length k + 1.

public theorem LinearMap.injective_and_exact_iff_forall_rank_eq_and_le_depth_minors
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (e : ℕ) (n : ℕ → ℕ)
    (φ : ∀ i, (Fin (n (i + 1)) → R) →ₗ[R] (Fin (n i) → R))
    (hφ : ∀ k < e, φ k ∘ₗ φ (k + 1) = 0) :
    (Function.Injective (φ e) ∧ ∀ k < e, Function.Exact (φ (k + 1)) (φ k)) ↔
      ∀ k ≤ e, ∃ r : ℕ,
        (r : ℤ) = ∑ t ∈ Finset.range (e + 1 - k), (-1) ^ t * (n (k + 1 + t) : ℤ) ∧
        IsGreatest {j : ℕ | exteriorPower.map j (φ k) ≠ 0} r ∧
        ((k + 1 : ℕ) : ℕ∞) ≤ Module.depth R (Ideal.span {x : R |
          ∃ (ρ : Fin r → Fin (n k)) (γ : Fin r → Fin (n (k + 1))),
            ((LinearMap.toMatrix' (φ k)).submatrix ρ γ).det = x}) R
Sources
LeanBoundedFreeComplex · exists_splitOff_elementaryComplex_of_hasInvertibleCoeff · exists_trivial_iso_of_exact · LinearMap.exists_trivialDecomposition_of_injective_of_exact · Stacks.DeterminantalRank.exteriorRank · Stacks.DeterminantalRank.detIdeal · StacksComplex.rank_eq_rIndex · StacksComplex.rank_add_rank

Section10.103 Cohen-Macaulay modules#

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

Tag 00N3, a definition

Tag 00N3 in the Stacks Project.

Module.IsCohenMacaulayAtMaximalIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Defs.lean, line 171. The attribute's comment: “Stated without the Noetherian and finiteness hypotheses, as in tags 00LI, 00NF and 0AAH; the equation is oriented depth_𝔪(M) = dim Supp(M), the spelling of Cohen–Macaulayness already used by tags 00LK, 00NF, 0AAG, 0AAH and 0C6G. The name records that the depth is taken at the maximal ideal, Module.IsCohenMacaulay being Definition 0AAH for a not necessarily local ring. See the module docstring.”. References: EGA 0 (16.5.1), “CM module def”; EGA IV (7.5.3).

Cohen–Macaulay module over a local ring. A module M over a local ring (R, 𝔪) is Cohen–Macaulay if the dimension of its support equals its depth, dim(Supp(M)) = depth_𝔪(M), the equality being read in WithBot ℕ∞ where Module.supportDim lives.

public def Module.IsCohenMacaulayAtMaximalIdeal (R : Type*) [CommRing R] [IsLocalRing R]
    (M : Type*) [AddCommGroup M] [Module R M] : Prop

Declarations registered for the tag:

Tag 00N4, a lemma

Tag 00N4 in the Stacks Project.

isCohenMacaulayModule_quotient_of_isGoodElement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Module/GoodElement.lean, line 258.

(Stacks 00N4, Lemma 10.103.2.) Let R be a Noetherian local ring with maximal ideal m, let M be a Cohen-Macaulay finite R-module, and let f_1, ..., f_d ∈ m (here d = f.length) be an M-regular sequence with d = dim(Supp(M)). Assume d ≥ 1 and let g ∈ m be good with respect to (M, f_1, ..., f_d). Then: (a) g is a nonzerodivisor on M; (b) M/gM is Cohen-Macaulay, the images of f_1, ..., f_{d-1} form an (M/gM)-regular sequence, and this sequence is maximal, equivalently dim(Supp(M/gM)) = depth(M/gM) = d - 1.

theorem isCohenMacaulayModule_quotient_of_isGoodElement {R : Type*} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] {M : Type*}
    [AddCommGroup M] [Module R M] [Module.Finite R M] (hCM : IsCohenMacaulayModule R M)
    (f : List R) (hf : RingTheory.Sequence.IsRegular M f)
    (hfm : ∀ x ∈ f, x ∈ IsLocalRing.maximalIdeal R)
    (hd : (f.length : WithBot ℕ∞) = Module.supportDim R M) (hd1 : 1 ≤ f.length) (g : R)
    (hg : g ∈ IsLocalRing.maximalIdeal R) (hgood : IsGoodElement M f g) :
    -- (a) g is a nonzerodivisor on M
    IsSMulRegular M g ∧
      -- (b) M/gM is Cohen-Macaulay
      IsCohenMacaulayModule R (M ⧸ (Ideal.span {g}) • (⊤ : Submodule R M)) ∧
      -- the images of f_1, ..., f_{d-1} form an (M/gM)-regular sequence
      RingTheory.Sequence.IsRegular (M ⧸ (Ideal.span {g}) • (⊤ : Submodule R M))
        (f.take (f.length - 1)) ∧
      -- maximality: dim(Supp(M/gM)) = depth(M/gM) = d - 1 (the depth equality is the
      -- Cohen-Macaulay conclusion above; here we record the common value is d - 1)
      Module.supportDim R (M ⧸ (Ideal.span {g}) • (⊤ : Submodule R M)) =
        ((f.length - 1 : ℕ) : WithBot ℕ∞)
Tag 00N5, a lemma

Tag 00N5 in the Stacks Project.

isSMulRegular_and_isCohenMacaulayModule_quotSMulTop_of_supportDim_drop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Module/RegularSequenceExtension.lean, line 544. References: EGA 0 (16.5.5), “b) ⇒ a), last part”.

Stacks 00N5. Let M be a Cohen-Macaulay module over a Noetherian local ring R, of support dimension e ≥ 1, and let g ∈ m be such that dim (Supp M ∩ V(g)) = dim (Supp M) - 1, i.e. dim (Supp (M/gM)) = e - 1. Then

  • (a) g is a nonzerodivisor on M, and
  • (b) M/gM is Cohen-Macaulay, of depth one less than the depth of M.

The hypothesis 1 ≤ e is the Stacks hypothesis that the dimension actually drops: e - 1 is truncated subtraction in ℕ, and for e = 0 the displayed condition of the source has no solutions.

theorem isSMulRegular_and_isCohenMacaulayModule_quotSMulTop_of_supportDim_drop
    (hCM : IsCohenMacaulayModule R M)
    (e : ℕ) (he : Module.supportDim R M = ((e : ℕ∞) : WithBot ℕ∞)) (hpos : 1 ≤ e)
    {g : R} (hg : g ∈ maximalIdeal R)
    (hdrop : Module.supportDim R (QuotSMulTop g M) = (((e - 1 : ℕ) : ℕ∞) : WithBot ℕ∞)) :
    IsSMulRegular M g ∧ IsCohenMacaulayModule R (QuotSMulTop g M) ∧
      Module.depthSup R (maximalIdeal R) (QuotSMulTop g M) + 1
        = Module.depthSup R (maximalIdeal R) M
Tag 00N6, a proposition

Tag 00N6 in the Stacks Project.

cohenMacaulay_regularSequence_extend, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Module/RegularSequenceExtension.lean, line 365. References: EGA 0 (16.5.6), “b) ⇒ a)”; EGA 0 (16.5.5), “b) ⇒ a)”; EGA 0 (16.5.7), “CM: sop ⇒ max reg seq”; SGA 2 III (2.6), “CM local, dim condition”.

Stacks Tag 00N6 (Proposition 10.103.4). Let R be a Noetherian local ring with maximal ideal m, and let M be a finite, nonzero, Cohen-Macaulay R-module with dim(Supp(M)) = d. If g_1, ..., g_c ∈ m (here gs, with gs.length = c and c ≤ d) satisfy dim(Supp(M/(g_1,...,g_c)M)) = d - c, then: 1. gs is an M-regular sequence, and 2. gs extends to a maximal M-regular sequence of length d (= depth M): there is a list gs' of elements of m with (gs ++ gs').length = d such that gs ++ gs' is a maximal M-regular sequence.

The hypothesis dim(Supp(M)) = d with d : ℕ already forces M ≠ 0 (since dim(Supp(0)) = ⊥); this is recorded by [Nontrivial M]. The hypothesis hcd : c ≤ d ensures the truncated subtraction (d - c : ℕ) agrees with the intended integer d - c, which is forced to be nonnegative by the mathematical hypothesis on dimensions.

theorem cohenMacaulay_regularSequence_extend
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M]
    (d c : ℕ) (hcd : c ≤ d) (hd : Module.supportDim R M = (d : WithBot ℕ∞))
    (hCM : IsCohenMacaulay R M)
    (gs : List R) (hgs_len : gs.length = c)
    (hgs_mem : ∀ g ∈ gs, g ∈ maximalIdeal R)
    (hdim : Module.supportDim R (M ⧸ (Ideal.ofList gs • (⊤ : Submodule R M)))
      = ((d - c : ℕ) : WithBot ℕ∞)) :
    IsRegular M gs ∧
    ∃ gs' : List R, (∀ g ∈ gs', g ∈ maximalIdeal R) ∧
      (gs ++ gs').length = d ∧
      IsMaximalRegularSequence R M (gs ++ gs')
Tag 0C6G, a lemma

Tag 0C6G in the Stacks Project.

Module.depth_eq_supportDim_iff_quotSMulTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Dimension.lean, line 172. The attribute's comment: “Cohen-Macaulayness is written out as the equation depth_𝔪(N) = dim Supp(N) that Definition 00N3 is, rather than as the predicate, so that each side is verbatim the hypothesis of Stacks 0BUS; the two differ by unfolding a definition. It is not spelled as the existence of an M-regular sequence of length dim Supp(M), which needs Stacks 090R(2) to be the same condition.”.

Stacks 0C6G. Let R be a Noetherian local ring with maximal ideal 𝔪, let M be a finite R-module and let x ∈ 𝔪 be a nonzerodivisor on M. Then M is Cohen-Macaulay if and only if M/xM is, Cohen-Macaulayness of a module N being the equality depth_𝔪(N) = dim Supp(N) — the definiens of Module.IsCohenMacaulayAtMaximalIdeal R N (Definition 00N3), written out so that each side is what Stacks 0BUS assumes.

public theorem depth_eq_supportDim_iff_quotSMulTop {R : Type*} [CommRing R] [IsNoetherianRing R]
    [IsLocalRing R] {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] {x : R}
    (hx : x ∈ IsLocalRing.maximalIdeal R) (hreg : IsSMulRegular M x) :
    (depth R (IsLocalRing.maximalIdeal R) M : WithBot ℕ∞) = supportDim R M ↔
      (depth R (IsLocalRing.maximalIdeal R) (QuotSMulTop x M) : WithBot ℕ∞) =
        supportDim R (QuotSMulTop x M)

isCohenMacaulayModule_iff_isCohenMacaulayModule_quotSMulTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Module/RegularSequenceExtension.lean, line 577.

Stacks 0C6G. Let R be a Noetherian local ring, M a finite R-module and x ∈ m a nonzerodivisor on M. Then M is Cohen-Macaulay if and only if M/xM is.

Both the depth and the dimension of the support drop by exactly one along x: the first by Stacks 090R (depth_quotient_succ_of_isSMulRegular) and the second by Stacks 0B52 (Module.supportDim_quotSMulTop_succ_eq_supportDim).

theorem isCohenMacaulayModule_iff_isCohenMacaulayModule_quotSMulTop
    {x : R} (hx : x ∈ maximalIdeal R) (hreg : IsSMulRegular M x) :
    IsCohenMacaulayModule R M ↔ IsCohenMacaulayModule R (QuotSMulTop x M)
Tag 0AAD, a lemma

Tag 0AAD in the Stacks Project.

isCohenMacaulay_iff_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Module/RegularSequenceExtension.lean, line 866. References: EGA 0 (16.5.3), “surjective ρ”; EGA IV (5.7.10), “special case”.

Stacks 10.103.6 (tag 0AAD). Let φ : R →+* S be a surjective homomorphism of Noetherian local rings, and let N be a finite S-module. Then N is Cohen-Macaulay as an S-module if and only if N is Cohen-Macaulay as an R-module, where the R-module structure on N is obtained by restriction of scalars along φ (Module.compHom N φ).

Here Noetherianity of R is encoded by IsNoetherianRing R (and S is then automatically Noetherian as a quotient, but we also assume it for convenience).

theorem isCohenMacaulay_iff_of_surjective
    (R S : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [CommRing S] [IsLocalRing S] [IsNoetherianRing S]
    (φ : R →+* S) (hφ : Function.Surjective φ)
    (N : Type*) [AddCommGroup N] [Module S N] [Module.Finite S N] :
    IsCohenMacaulayPropForm S N ↔
      (letI : Module R N := Module.compHom N φ; IsCohenMacaulayPropForm R N)

isCohenMacaulay_iff_of_surjective', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Module/RegularSequenceExtension.lean, line 889. References: EGA 0 (16.5.3), “surjective ρ”.

Stacks 10.103.6 (tag 0AAD). Let φ : R →+* S be a surjective homomorphism of Noetherian local rings, and let N be a finite S-module. Then N is Cohen-Macaulay as an S-module if and only if N is Cohen-Macaulay as an R-module, where the R-module structure on N is obtained by restriction of scalars along φ (Module.compHom N φ).

Here Noetherianity of R is encoded by IsNoetherianRing R (and S is then automatically Noetherian as a quotient, but we also assume it for convenience).

theorem isCohenMacaulay_iff_of_surjective'
    (R S : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [CommRing S] [IsLocalRing S] [IsNoetherianRing S]
    (φ : R →+* S) (hφ : Function.Surjective φ)
    (N : Type*) [AddCommGroup N] [Module S N] [Module.Finite S N] :
    IsCohenMacaulayModule S N ↔
      (letI : Algebra R S := φ.toAlgebra
       letI : Module R N := Module.compHom N φ
       haveI : IsScalarTower R S N := ⟨fun r s n => mul_smul (φ r) s n⟩
       haveI : Module.Finite R S := Module.Finite.of_surjective (Algebra.linearMap R S) hφ
       haveI : Module.Finite R N := Module.Finite.trans S N
       IsCohenMacaulayModule R N)
Tag 0BUS, a lemma

Tag 0BUS in the Stacks Project.

Module.ringKrullDim_quotient_eq_supportDim_and_minimal_support_of_mem_associatedPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Dimension.lean, line 385. The attribute's comment: “Cohen-Macaulayness is spelled out as depth_𝔪(M) = dim Supp(M), the definition Stacks 00N8 unfolds to, there being no predicate for it in this library yet.”. References: EGA 0 (16.5.4); EGA IV (15.4.1), “local form”; EGA IV (7.2.1.1), “more general”.

Stacks 0BUS. Let R be a Noetherian local ring and let M be a finite Cohen-Macaulay R-module, that is, one whose depth along the maximal ideal equals the dimension of its support. If 𝔭 is an associated prime of M, then dim(R/𝔭) = dim Supp(M) and 𝔭 is a minimal point of Supp(M).

In particular M has no embedded associated primes: since Ass(M) ⊆ Supp(M), a prime minimal in Supp(M) is minimal in Ass(M).

public theorem ringKrullDim_quotient_eq_supportDim_and_minimal_support_of_mem_associatedPrimes
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {M : Type*} [AddCommGroup M]
    [Module R M] [Module.Finite R M]
    (hCM : (depth R (IsLocalRing.maximalIdeal R) M : WithBot ℕ∞) = supportDim R M)
    {p : PrimeSpectrum R} (hp : p.asIdeal ∈ associatedPrimes R M) :
    ringKrullDim (R ⧸ p.asIdeal) = supportDim R M ∧ Minimal (· ∈ support R M) p

coheight_eq_supportDim_of_mem_associatedPrimes_of_isCohenMacaulayModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Module/RegularSequenceExtension.lean, line 614. References: EGA 0 (16.5.4); EGA IV (7.2.1.1), “more general”.

Stacks 0BUS (EGA Ch. 0, Proposition 16.5.4). Let M be a finite Cohen-Macaulay module over a Noetherian local ring R and let p ∈ Ass(M). Then dim (R/p) = dim (Supp M), and p is a minimal prime of the support of M. In particular M has no embedded associated primes.

Here dim (R/p) is Order.coheight p in PrimeSpectrum R, and minimality of p in the support is spelled out as: no prime of Supp M is strictly below p.

The dimension equality holds because dim (Supp M) = depth M ≤ dim (R/p) (Stacks 0AUJ, the Cohen-Macaulay form of which is supportDim_le_coheight_of_isCohenMacaulayModule) while dim (R/p) ≤ dim (Supp M) since Supp M is closed under specialization and contains p. Minimality then follows: a prime q ∈ Supp M with q < p would give dim (R/p) + 1 ≤ dim (R/q) ≤ dim (Supp M) = dim (R/p).

theorem coheight_eq_supportDim_of_mem_associatedPrimes_of_isCohenMacaulayModule
    (hCM : IsCohenMacaulayModule R M) {p : Ideal R} (hp : p ∈ associatedPrimes R M) :
    (Order.coheight (⟨p, hp.1⟩ : PrimeSpectrum R) : WithBot ℕ∞) = Module.supportDim R M ∧
      ∀ q ∈ Module.support R M, q ≤ (⟨p, hp.1⟩ : PrimeSpectrum R) →
        q = (⟨p, hp.1⟩ : PrimeSpectrum R)
Tag 00NF, a definition

Tag 00NF in the Stacks Project.

Module.IsMaximalCohenMacaulay, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Defs.lean, line 110. The attribute's comment: “Stated without the Noetherian and finiteness hypotheses; see the module docstring.”. References: EGA IV (7.5.3).

Maximal Cohen–Macaulay module. A module M over a local ring (R, 𝔪) is maximal Cohen–Macaulay if its depth along 𝔪 equals the Krull dimension of R, depth_𝔪(M) = dim(R), which is the largest value the depth of an R-module can take. The source states this for R Noetherian and M finite; neither hypothesis is needed to state the condition, so both are left to the lemmas.

public def Module.IsMaximalCohenMacaulay (R : Type*) [CommRing R] [IsLocalRing R] (M : Type*)
    [AddCommGroup M] [Module R M] : Prop

IsMaximalCohenMacaulayModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Module/RegularSequenceExtension.lean, line 655.

Stacks 00NF. A finite module M over a Noetherian local ring R is maximal Cohen-Macaulay if depth M = dim R, i.e. if its depth is as large as it can possibly be.

def IsMaximalCohenMacaulayModule (R : Type*) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] : Prop
Tag 0AAE, a lemma

Tag 0AAE in the Stacks Project.

Module.IsMaximalCohenMacaulay.length_eq_ringKrullDim_of_support_eq_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Dimension.lean, line 746. The attribute's comment: “The source's M Cohen-Macaulay with Spec(R) = Supp(M) is the conjunction of Module.IsMaximalCohenMacaulay R M (Definition 00NF, i.e. depth_𝔪(M) = dim R) and Module.support R M = Set.univ, the two being equivalent to it as the source itself remarks; a maximal chain of primes is a RelSeries for the covering relation ⋖ on PrimeSpectrum R whose head is minimal and whose last is maximal. See the module docstring.”. References: EGA IV (15.4.1), “special case”.

Maximal chains of primes in a local ring with a Cohen–Macaulay module of full support. Let R be a Noetherian local ring and let M be a finite R-module which is Cohen–Macaulay with Supp(M) = Spec(R), that is depth_𝔪(M) = dim(R) and Supp(M) = Spec(R). Then every maximal chain of primes of R — one whose steps are covering pairs 𝔭_i ⋖ 𝔭_{i + 1}, starting at a minimal prime and ending at a maximal ideal — has length dim(R).

public theorem Module.IsMaximalCohenMacaulay.length_eq_ringKrullDim_of_support_eq_univ
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {M : Type*} [AddCommGroup M]
    [Module R M] [Module.Finite R M] (hM : Module.IsMaximalCohenMacaulay R M)
    (hsupp : Module.support R M = Set.univ)
    (s : RelSeries {(p, q) : PrimeSpectrum R × PrimeSpectrum R | p ⋖ q})
    (hmin : IsMin s.head) (hmax : IsMax s.last) :
    (s.length : WithBot ℕ∞) = ringKrullDim R
Tag 0AAF, a lemma

Tag 0AAF in the Stacks Project.

Module.IsMaximalCohenMacaulay.ringKrullDim_eq_height_add_ringKrullDim_quotient_of_support_eq_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Dimension.lean, line 1173. The attribute's comment: “The source's M Cohen-Macaulay with Spec(R) = Supp(M) is the conjunction of Module.IsMaximalCohenMacaulay R M (Definition 00NF, i.e. depth_𝔪(M) = dim R) and Module.support R M = Set.univ, the two being equivalent to it as the source itself remarks; dim(R_𝔭) is written 𝔭.height. See the module docstring.”. References: EGA 0 (16.5.11); EGA 0 (16.5.10), “(ii), Supp M = Spec A”; EGA IV (15.4.1), “special case”.

The dimension formula in a local ring with a Cohen–Macaulay module of full support. Let R be a Noetherian local ring and let M be a finite R-module which is Cohen–Macaulay with Supp(M) = Spec(R), that is depth_𝔪(M) = dim(R) and Supp(M) = Spec(R). Then every prime 𝔭 of R satisfies dim(R) = dim(R_𝔭) + dim(R/𝔭), the dimension of the localisation R_𝔭 being written as the height of 𝔭.

public theorem ringKrullDim_eq_height_add_ringKrullDim_quotient_of_support_eq_univ
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {M : Type*} [AddCommGroup M]
    [Module R M] [Module.Finite R M] (hM : Module.IsMaximalCohenMacaulay R M)
    (hsupp : Module.support R M = Set.univ) (p : Ideal R) [p.IsPrime] :
    ringKrullDim R = p.height + ringKrullDim (R ⧸ p)
Tag 0AAG, a lemma

Tag 0AAG in the Stacks Project.

Module.depth_eq_supportDim_of_isLocalizedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Localization.lean, line 288. The attribute's comment: “Cohen–Macaulayness is spelled out as depth_𝔪(N) = dim Supp(N), the equation Definition 00N3 unfolds to, there being no predicate for it in this library yet; the localization is presented by IsLocalization.AtPrime and IsLocalizedModule; and 𝔭 is required to lie in Supp(M), spelled Nontrivial Mₚ, without which the conclusion is false for the source's own conventions. See the module docstring.”. References: EGA 0 (16.5.10); EGA 0 (16.5.13), “forward direction”.

Cohen–Macaulayness localizes. Let (R, 𝔪) be a Noetherian local ring and M a finite R-module which is Cohen–Macaulay, i.e. depth_𝔪(M) = dim Supp(M) (Definition 00N3). Let 𝔭 ⊆ R be a prime in the support of M, presented by a localization Rₚ of R at 𝔭 and a localization f : M →ₗ[R] Mₚ of M at 𝔭. Then M_𝔭 is Cohen–Macaulay over R_𝔭, that is depth_{𝔭R_𝔭}(M_𝔭) = dim Supp(M_𝔭). Both equations are read in WithBot ℕ∞, where Module.supportDim lives.

public theorem depth_eq_supportDim_of_isLocalizedModule {R : Type*} [CommRing R]
    [IsNoetherianRing R] [IsLocalRing R] (M : Type*) [AddCommGroup M] [Module R M]
    [Module.Finite R M]
    (hM : (depth R (IsLocalRing.maximalIdeal R) M : WithBot ℕ∞) = supportDim R M)
    (p : Ideal R) [p.IsPrime] (Rₚ : Type*) [CommRing Rₚ] [Algebra R Rₚ]
    [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] (Mₚ : Type*) [AddCommGroup Mₚ] [Nontrivial Mₚ]
    [Module R Mₚ] [Module Rₚ Mₚ] [IsScalarTower R Rₚ Mₚ] (f : M →ₗ[R] Mₚ)
    [IsLocalizedModule p.primeCompl f] :
    (depth Rₚ (IsLocalRing.maximalIdeal Rₚ) Mₚ : WithBot ℕ∞) = supportDim Rₚ Mₚ
Tag 0AAH, a definition

Tag 0AAH in the Stacks Project.

Module.IsCohenMacaulay, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Defs.lean, line 136. The attribute's comment: “The condition is imposed at the primes of Supp(M) rather than at all primes of R, the literal reading being vacuous for the source's own conventions on the zero module; Cohen–Macaulayness at a prime is spelled out as the equation depth_{𝔭R_𝔭}(M_𝔭) = dim Supp(M_𝔭) of Definition 00N3, there being no predicate for it in this library; the localisations are the canonical models; and the Noetherian and finiteness hypotheses are dropped, as in tags 00LI and 00NF. See the module docstring.”. References: EGA 0 (16.5.13); EGA IV (5.7.1), “special case”; EGA IV (7.5.3).

Cohen–Macaulay module. An R-module M is Cohen–Macaulay if for every prime 𝔭 in the support of M the localisation M_𝔭 is a Cohen–Macaulay module over the local ring R_𝔭, that is depth_{𝔭R_𝔭}(M_𝔭) = dim Supp(M_𝔭), the equation being read in WithBot ℕ∞.

public def IsCohenMacaulay (R : Type*) [CommRing R] (M : Type*) [AddCommGroup M]
    [Module R M] : Prop

IsLocallyCohenMacaulayModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Module/RegularSequenceExtension.lean, line 695. The attribute's comment: “Quantified over Supp M. The source's literal all-primes wording is inconsistent when M_p = 0, since the zero module is not Cohen-Macaulay here; this is a source erratum, and the definition captures 0AAH in full.”. References: EGA 0 (16.5.13).

Stacks 0AAH. Let R be a Noetherian ring, not necessarily local, and let M be a finite R-module. Then M is Cohen-Macaulay if M_p is a Cohen-Macaulay R_p-module for every prime p in the support of M. The name records that this is a condition imposed at the points of Spec R; the Stacks project calls it simply "Cohen-Macaulay", which in this repository is already the name of the local notion IsCohenMacaulayModule.

Erratum in the source. Stacks 0AAH literally reads "for all primes p of R". Taken literally that wording is mathematically inconsistent, because at a prime p ∉ Supp M the localization M_p is the zero module, and the zero module is not Cohen-Macaulay: with

IsCohenMacaulayModule R M ↔ depthSup R 𝔪 M = (krullDim (Module.support R M) : WithBot ℕ∞),

the right-hand side is ⊥ for the zero module (its support is empty) while the left-hand side is a coercion from ℕ∞ and so is never ⊥. A literal all-primes reading would therefore be satisfied by no module except those of full support, which is plainly not the notion 0AAH intends.

This definition quantifies over Module.support R M deliberately, which is the intended content of 0AAH. The restriction is a correction of the source's wording, not a narrowing of the formalization: the class of modules defined here is exactly the class 0AAH describes.

def IsLocallyCohenMacaulayModule (R : Type*) [CommRing R] [IsNoetherianRing R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] : Prop
Tag 0AAI, a lemma

Tag 0AAI in the Stacks Project.

Module.IsCohenMacaulay.mvPolynomial_of_isBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/MvPolynomial.lean, line 1484. The attribute's comment: “The base change M ⊗_R R[x_1, …, x_n] is presented abstractly, as an S-module N with an R-linear f : M →ₗ[R] N satisfying IsBaseChange S f for S = MvPolynomial σ R, as in tag 0AAG and in Mathlib's RingTheory.Sequence.IsWeaklyRegular.of_flat_of_isBaseChange; the variables are indexed by an arbitrary finite type rather than by Fin n; and the finiteness of M, which the source keeps inside Definition 0AAH, is assumed explicitly. See the module docstring.”. References: EGA IV (6.3.6); EGA IV (6.11.9), “more general”.

Cohen–Macaulayness ascends along a polynomial extension. Let R be a Noetherian ring, let M be a finite Cohen–Macaulay R-module, and let N, together with an R-linear map f : M →ₗ[R] N, be the base change of M to the polynomial ring S = MvPolynomial σ R in finitely many variables. Then N is a Cohen–Macaulay S-module.

public theorem IsCohenMacaulay.mvPolynomial_of_isBaseChange {R : Type*} [CommRing R]
    [IsNoetherianRing R] {σ : Type*} [Finite σ] {M : Type*} [AddCommGroup M] [Module R M]
    [Module.Finite R M] {N : Type*} [AddCommGroup N] [Module R N] [Module (MvPolynomial σ R) N]
    [IsScalarTower R (MvPolynomial σ R) N] {f : M →ₗ[R] N} (hf : IsBaseChange (MvPolynomial σ R) f)
    (hM : IsCohenMacaulay R M) : IsCohenMacaulay (MvPolynomial σ R) N
Sources
LeanModule.IsCohenMacaulayAtMaximalIdeal · IsCohenMacaulayModule · isCohenMacaulayModule_quotient_of_isGoodElement · isSMulRegular_and_isCohenMacaulayModule_quotSMulTop_of_supportDim_drop · cohenMacaulay_regularSequence_extend · Module.depth_eq_supportDim_iff_quotSMulTop · isCohenMacaulayModule_iff_isCohenMacaulayModule_quotSMulTop · isCohenMacaulay_iff_of_surjective

Section10.104 Cohen-Macaulay rings#

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

Tag 00N8, a definition

Tag 00N8 in the Stacks Project.

IsCohenMacaulayLocalRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Defs.lean, line 201. References: EGA 0 (16.5.13), “local ring”; EGA 0 (16.5.1); EGA IV (5.7.1); EGA IV (7.5.3).

A Noetherian local ring R is called Cohen–Macaulay if it is Cohen–Macaulay as a module over itself.

def IsCohenMacaulayLocalRing (R : Type*) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] :
    Prop
Tag 02JN, a lemma

Tag 02JN in the Stacks Project.

Module.IsMaximalCohenMacaulay.isRegular_iff_ringKrullDim_add_length_eq_ringKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/RegularSequence/DimensionCriterion.lean, line 567. The attribute's comment: “R Cohen–Macaulay is Module.IsMaximalCohenMacaulay R R (Definition 00NF at M = R, equal to Definition 00N8 by Module.supportDim_self_eq_ringKrullDim); the source's dim(R/(x₁, …, x_i)) = dim(R) - i is stated additively, as in ringKrullDim_add_length_eq_ringKrullDim_of_isRegular; the extension is an append, and the local ring structures on the quotients are existentially bound. See the module docstring.”. References: EGA 0 (16.5.6), “M = R (CM local ring)”; EGA 0 (16.5.5), “M = R; a) ⇔ b)”; EGA 0 (16.5.7), “case M = R”; EGA 0 (16.5.9), “special case”; SGA 2 III (2.6), “M = R, CM local”.

Regular sequences in a Cohen–Macaulay local ring are those cutting out the right dimension. Let (R, 𝔪) be a Noetherian local Cohen–Macaulay ring and let xs = x₁, …, x_c be a list of elements of 𝔪. Then xs is a regular sequence if and only if dim(R/(x₁, …, x_c)) + c = dim(R), and in that case xs extends by elements of 𝔪 to a regular sequence of length dim(R) and each R/(x₁, …, x_i) is a Cohen–Macaulay local ring of dimension dim(R) - i. The source's subtraction is moved to the other side of the equations, Krull dimensions being valued in WithBot ℕ∞; see the module docstring.

public theorem Module.IsMaximalCohenMacaulay.isRegular_iff_ringKrullDim_add_length_eq_ringKrullDim
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (hR : Module.IsMaximalCohenMacaulay R R) (xs : List R)
    (hxs : ∀ x ∈ xs, x ∈ maximalIdeal R) :
    (RingTheory.Sequence.IsRegular R xs ↔
        ringKrullDim (R ⧸ Ideal.ofList xs) + xs.length = ringKrullDim R) ∧
      (RingTheory.Sequence.IsRegular R xs →
        (∃ ys : List R, (∀ y ∈ ys, y ∈ maximalIdeal R) ∧
            RingTheory.Sequence.IsRegular R (xs ++ ys) ∧
            ((xs ++ ys).length : WithBot ℕ∞) = ringKrullDim R) ∧
        ∀ i ≤ xs.length, ∃ _ : IsLocalRing (R ⧸ Ideal.ofList (xs.take i)),
          Module.IsMaximalCohenMacaulay (R ⧸ Ideal.ofList (xs.take i))
              (R ⧸ Ideal.ofList (xs.take i)) ∧
            ringKrullDim (R ⧸ Ideal.ofList (xs.take i)) + i = ringKrullDim R)
Tag 00N9, a lemma

Tag 00N9 in the Stacks Project.

Module.IsMaximalCohenMacaulay.length_eq_ringKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Dimension.lean, line 897. The attribute's comment: “Cohen-Macaulayness of the Noetherian local ring R is the predicate Module.IsMaximalCohenMacaulay R R (Definition 00N8, i.e. depth_𝔪(R) = dim R); a maximal chain of primes is a RelSeries for the covering relation ⋖ on PrimeSpectrum R whose head is minimal and whose last is maximal; the source's name d for dim R is dropped. See the module docstring.”. References: EGA IV (15.4.1), “special case”.

Maximal chains of primes in a Cohen–Macaulay local ring. Let R be a Noetherian local Cohen–Macaulay ring, that is depth_𝔪(R) = dim(R). Then every maximal chain of primes of R — one whose steps are covering pairs 𝔭_i ⋖ 𝔭_{i + 1}, starting at a minimal prime and ending at the maximal ideal — has length dim(R).

public theorem Module.IsMaximalCohenMacaulay.length_eq_ringKrullDim
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (hR : Module.IsMaximalCohenMacaulay R R)
    (s : RelSeries {(p, q) : PrimeSpectrum R × PrimeSpectrum R | p ⋖ q})
    (hmin : IsMin s.head) (hmax : IsMax s.last) :
    (s.length : WithBot ℕ∞) = ringKrullDim R
Tag 00NA, a lemma

Tag 00NA in the Stacks Project.

Module.IsMaximalCohenMacaulay.ringKrullDim_eq_height_add_ringKrullDim_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Dimension.lean, line 1321. The attribute's comment: “Cohen-Macaulayness of R is the hypothesis Module.IsMaximalCohenMacaulay R R, i.e. depth_𝔪(R) = dim R (Definition 00N8); dim(R_𝔭) is written 𝔭.height; the source's name d for dim R is dropped.”. References: EGA 0 (16.5.11), “case M = R”; EGA 0 (16.5.10), “(ii) for M = A”; EGA IV (15.4.1), “special case”.

The dimension formula in a Cohen–Macaulay local ring. If R is a Noetherian local Cohen–Macaulay ring, that is depth_𝔪(R) = dim R, then every prime 𝔭 of R satisfies dim R = dim R_𝔭 + dim R/𝔭, the dimension of the localisation R_𝔭 being written as the height of 𝔭.

public theorem Module.IsMaximalCohenMacaulay.ringKrullDim_eq_height_add_ringKrullDim_quotient
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (hR : Module.IsMaximalCohenMacaulay R R) (p : Ideal R) [p.IsPrime] :
    ringKrullDim R = p.height + ringKrullDim (R ⧸ p)
Tag 00NB, a lemma

Tag 00NB in the Stacks Project.

Module.IsMaximalCohenMacaulay.of_isLocalization_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Localization.lean, line 439. The attribute's comment: “Cohen-Macaulayness of a Noetherian local ring is the predicate Module.IsMaximalCohenMacaulay S S, i.e. depth_{𝔪_S}(S) = dim S (Definition 00N8); the localization is an abstract IsLocalization.AtPrime. See the module docstring.”. References: EGA 0 (16.5.10), “(i) for M = A”; EGA 0 (16.5.13), “partial”; EGA IV (6.11.5), “special case”.

Cohen–Macaulayness localizes at a prime. If R is a Noetherian local Cohen–Macaulay ring, that is depth_𝔪(R) = dim R, then for every prime 𝔭 of R the local ring R_𝔭 is Cohen–Macaulay: depth_{𝔭R_𝔭}(R_𝔭) = dim R_𝔭. The localization is any R-algebra Rₚ with IsLocalization.AtPrime Rₚ p.

public theorem Module.IsMaximalCohenMacaulay.of_isLocalization_atPrime {R : Type*} [CommRing R]
    [IsNoetherianRing R] [IsLocalRing R] (hR : Module.IsMaximalCohenMacaulay R R) (p : Ideal R)
    [p.IsPrime] (Rₚ : Type*) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p]
    [IsLocalRing Rₚ] : Module.IsMaximalCohenMacaulay Rₚ Rₚ
Tag 00NC, a definition

Tag 00NC in the Stacks Project.

IsCohenMacaulayRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Defs.lean, line 243. References: EGA 0 (16.5.13); EGA IV (7.5.3).

A Noetherian ring R is Cohen–Macaulay if every localisation R_𝔭 at a prime ideal 𝔭 is a Cohen–Macaulay local ring.

def IsCohenMacaulayRing (R : Type*) [CommRing R] [IsNoetherianRing R] : Prop
Tag 00ND, a lemma

Tag 00ND in the Stacks Project.

Module.IsMaximalCohenMacaulay.of_isLocalization_atPrime_mvPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/MvPolynomial.lean, line 1575. The attribute's comment: “Cohen-Macaulayness of a Noetherian local ring is Module.IsMaximalCohenMacaulay S S (Definition 00N8); that of a Noetherian ring (Definition 00NC) is spelled out as a condition on its localizations at primes, the hypothesis at the concrete Localization.AtPrime and the conclusion at an abstract IsLocalization.AtPrime; R[x_1, …, x_n] is MvPolynomial σ R for finite σ. See the module docstring.”. References: EGA IV (6.3.6); EGA IV (6.11.9).

A polynomial algebra over a Noetherian Cohen–Macaulay ring is Cohen–Macaulay. Let R be a Noetherian ring all of whose local rings R_𝔭 are Cohen–Macaulay, and let σ be finite. Then for every prime 𝔮 of R[x_i : i ∈ σ], every localization S of R[x_i : i ∈ σ] at 𝔮 is a Cohen–Macaulay local ring.

public theorem Module.IsMaximalCohenMacaulay.of_isLocalization_atPrime_mvPolynomial {R : Type*}
    [CommRing R] [IsNoetherianRing R]
    (hR :
      ∀ (p : Ideal R) [p.IsPrime],
        Module.IsMaximalCohenMacaulay (Localization.AtPrime p) (Localization.AtPrime p))
    {σ : Type*} [Finite σ] (q : Ideal (MvPolynomial σ R)) [q.IsPrime] (S : Type*) [CommRing S]
    [Algebra (MvPolynomial σ R) S] [IsLocalization.AtPrime S q] [IsLocalRing S] :
    Module.IsMaximalCohenMacaulay S S
Tag 00NE, a lemma

Tag 00NE in the Stacks Project.

Module.IsMaximalCohenMacaulay.depth_lt_depth_or_isMaximalCohenMacaulay_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/Syzygy.lean, line 338. The attribute's comment: “Cohen-Macaulayness of the Noetherian local ring R is Module.IsMaximalCohenMacaulay R R, i.e. depth_𝔪(R) = dim R (Definition 00N8); R^{⊕n} is an arbitrary finite free module F; the alternative M = 0 is the hypothesis [Nontrivial M]; and depth(K) = depth(M) = d is maximal Cohen-Macaulayness of K and of M. See the module docstring.”.

Depth of a syzygy module over a Cohen–Macaulay local ring. Let (R, 𝔪) be a Noetherian local Cohen–Macaulay ring, that is depth_𝔪(R) = dim R, let F be a finite free R-module and let 0 → K → F → M → 0 be a short exact sequence of R-modules, given by f : K →ₗ[R] F injective, g : F →ₗ[R] M surjective and Function.Exact f g, with M nonzero. Then either depth_𝔪(M) < depth_𝔪(K), or depth_𝔪(K) = depth_𝔪(M) = dim R, i.e. both K and M are maximal Cohen–Macaulay.

The source states the third alternative as depth(K) = depth(M) = d and the middle term as R^{⊕n}, and lists M = 0 as a first alternative in place of the hypothesis [Nontrivial M].

public theorem IsMaximalCohenMacaulay.depth_lt_depth_or_isMaximalCohenMacaulay_of_exact
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (hR : IsMaximalCohenMacaulay R R) {K F M : Type*} [AddCommGroup K] [Module R K]
    [AddCommGroup F] [Module R F] [Module.Free R F] [Module.Finite R F] [AddCommGroup M]
    [Module R M] [Nontrivial M] {f : K →ₗ[R] F} {g : F →ₗ[R] M} (h : Function.Exact f g)
    (hf : Function.Injective f) (hg : Function.Surjective g) :
    depth R (maximalIdeal R) M < depth R (maximalIdeal R) K ∨
      (IsMaximalCohenMacaulay R K ∧ IsMaximalCohenMacaulay R M)
Tag 00NG, a lemma

Tag 00NG in the Stacks Project.

Module.IsMaximalCohenMacaulay.exists_composableArrows_exact_free_and_isMaximalCohenMacaulay_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/FreeComplex.lean, line 479. The attribute's comment: “Cohen-Macaulayness of the Noetherian local ring R is Module.IsMaximalCohenMacaulay R R, i.e. depth_𝔪(R) = dim R (Definition 00N8); the complex is a ComposableArrows (ModuleCat R) (d - e + 1) whose rightmost object is M, its interior exactness being Exact and the outer two conditions Mono and Epi as in ShortComplex.ShortExact. See the module docstring.”.

Finite free complexes with a maximal Cohen–Macaulay kernel. Let (R, 𝔪) be a Noetherian local Cohen–Macaulay ring, that is depth_𝔪(R) = dim R, of dimension d, and let M be a finite R-module of depth e. Then there is an exact complex

0 → K → F_{d-e-1} → ⋯ → F₀ → M → 0

of R-modules with the d - e modules Fᵢ finite free and K maximal Cohen–Macaulay. The complex is a ComposableArrows (ModuleCat R) (d - e + 1) with rightmost object M, whose exactness at the interior objects Fᵢ is S.Exact and whose outer two exactness conditions are Mono (S.map' 0 1) and Epi (S.map' (d - e) (d - e + 1)); the module K is its leftmost object S.left.

public theorem exists_composableArrows_exact_free_and_isMaximalCohenMacaulay_left {R : Type u}
    [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (hR : Module.IsMaximalCohenMacaulay R R)
    (M : ModuleCat.{u} R) [Module.Finite R M] {d e : ℕ} (hd : ringKrullDim R = d)
    (he : Module.depth R (maximalIdeal R) M = e) :
    ∃ S : ComposableArrows (ModuleCat.{u} R) (d - e + 1),
      S.right = M ∧ S.Exact ∧ Mono (S.map' 0 1) ∧ Epi (S.map' (d - e) (d - e + 1)) ∧
        (∀ i, Module.Finite R (S.obj i)) ∧
        (∀ (i : ℕ) (hi : i < d - e), Module.Free R (S.obj' (i + 1))) ∧
        Module.IsMaximalCohenMacaulay R S.left
Tag 06LC, a lemma

Tag 06LC in the Stacks Project.

exists_isRegular_map_length_eq_ringKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/RegularSequence/LocalRingMap.lean, line 639.

The main theorem (Stacks Tag 06LC). Reduce to the engine lemma at d the finite value of ringKrullDim B.

theorem exists_isRegular_map_length_eq_ringKrullDim {A B : Type*} [CommRing A] [CommRing B]
  [IsLocalRing A] [IsLocalRing B]
    [IsNoetherianRing B] (hCM : IsCohenMacaulayLocalRing B) (φ : A →+* B)
    (h : IsLocalRing.maximalIdeal B = (Ideal.map φ (IsLocalRing.maximalIdeal A)).radical) :
    ∃ f : List A,
      (f.length : WithBot ℕ∞) = ringKrullDim B ∧ RingTheory.Sequence.IsRegular B (f.map φ)
Sources
LeanIsCohenMacaulayLocalRing · Module.IsMaximalCohenMacaulay.isRegular_iff_ringKrullDim_add_length_eq_ringKrullDim · Module.IsMaximalCohenMacaulay.length_eq_ringKrullDim · Module.IsMaximalCohenMacaulay.ringKrullDim_eq_height_add_ringKrullDim_quotient · Module.IsMaximalCohenMacaulay.of_isLocalization_atPrime · IsCohenMacaulayRing · Module.IsMaximalCohenMacaulay.of_isLocalization_atPrime_mvPolynomial · Module.IsMaximalCohenMacaulay.depth_lt_depth_or_isMaximalCohenMacaulay_of_exact

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.