10.64 Symbolic powers to 10.84 Transfinite dévissage of…

Section10.64 Symbolic powers#

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

Tag 0313, a definition

Tag 0313 in the Stacks Project.

Ideal.symbolicPower, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/SymbolicPower.lean, line 49. References: EGA IV (11.4.7).

The nth symbolic power p ^ (n) of a prime ideal p of a commutative semiring R: the kernel of R → R_p / p ^ n R_p, realized as the contraction to R of the ideal p ^ n R_p of the localization R_p.

public def symbolicPower {R : Type*} [CommSemiring R] (p : Ideal R) [p.IsPrime] (n : ℕ) :
    Ideal R
Tag 0314, a lemma

Tag 0314 in the Stacks Project.

ass_quotient_symbolicPower', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/SymbolicPower/AssociatedPrimes.lean, line 166.

For a Noetherian ring R, a prime ideal p, and n > 0, the set of associated primes of R / p^{(n)} is exactly {p}.

theorem ass_quotient_symbolicPower' {R : Type*} [CommRing R] [IsNoetherianRing R]
    (p : Ideal R) [p.IsPrime] (n : ℕ) (hn : 0 < n) :
    Stacks.AssociatedPrimes.assPrimes R (R ⧸ symbolicPower' p n) = {p}
Tag 0BC0, a lemma

Tag 0BC0 in the Stacks Project.

symbolicPower_map_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/SymbolicPower.lean, line 697.

For a flat ring map R → S and a prime p ⊆ R whose extension q = p S is prime, p^{(n)} S = q^{(n)}.

theorem symbolicPower_map_of_flat {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S)
    (hφ : φ.Flat) (p : Ideal R) [p.IsPrime] (hq : (p.map φ).IsPrime) (n : ℕ) :
    (symbolicPower' p n).map φ = symbolicPower' (p.map φ) n
Sources
LeanIdeal.symbolicPower · ass_quotient_symbolicPower' · symbolicPower_map_of_flat

Section10.65 Relative assassin#

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

Tag 05GB, a lemma

Tag 05GB in the Stacks Project.

Module.relativeAssassin_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/RelativeAssassin.lean, line 842.

Let R → S be a ring map, let N be an S-module, and let A, A', A_fin, A'_fin, B, B_fin be the six sets of primes of S attached to this data: with 𝔭 = R ∩ 𝔮, the primes 𝔮 associated to N ⊗_R κ(𝔭) over S, those in the image of the primes associated to N ⊗_R κ(𝔭) over the fibre ring S ⊗_R κ(𝔭), those associated to N / 𝔭N, those associated to N / 𝔭'N for some prime 𝔭' of R, those associated to N ⊗_R M for some R-module M, and those associated to N ⊗_R M for some finite R-module M. Then (1) A = A'; (2) A_fin ⊆ A, B_fin ⊆ B, A_fin ⊆ A'_fin ⊆ B_fin and A ⊆ B; (3) if S is Noetherian then A = A_fin and B = B_fin; (4) if N is flat over R then A = A_fin = A'_fin and B = B_fin; (5) if R is Noetherian and N is flat over R then all six sets are equal.

public theorem relativeAssassin_comparison (R : Type u) (S : Type v) [CommRing R] [CommRing S]
    [Algebra R S] (N : Type w) [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    {A A' Afin A'fin B Bfin : Set (PrimeSpectrum S)}
    (hA : A = {q | q.asIdeal ∈
      associatedPrimes S (N ⊗[R] (PrimeSpectrum.comap (algebraMap R S) q).asIdeal.ResidueField)})
    (hA' : A' = {q | ∃ Q : PrimeSpectrum
        (S ⊗[R] (PrimeSpectrum.comap (algebraMap R S) q).asIdeal.ResidueField),
        Q.asIdeal ∈ associatedPrimes
          (S ⊗[R] (PrimeSpectrum.comap (algebraMap R S) q).asIdeal.ResidueField)
          ((S ⊗[R] (PrimeSpectrum.comap (algebraMap R S) q).asIdeal.ResidueField) ⊗[S] N) ∧
        PrimeSpectrum.comap (algebraMap S
          (S ⊗[R] (PrimeSpectrum.comap (algebraMap R S) q).asIdeal.ResidueField)) Q = q})
    (hAfin : Afin = {q | q.asIdeal ∈ associatedPrimes S
      (N ⧸ ((PrimeSpectrum.comap (algebraMap R S) q).asIdeal.map (algebraMap R S) •
        (⊤ : Submodule S N)))})
    (hA'fin : A'fin = {q | ∃ p : PrimeSpectrum R, q.asIdeal ∈ associatedPrimes S
      (N ⧸ (p.asIdeal.map (algebraMap R S) • (⊤ : Submodule S N)))})
    (hB : B = {q | ∃ (M : Type (max u v)) (_ : AddCommGroup M) (_ : Module R M),
      q.asIdeal ∈ associatedPrimes S (N ⊗[R] M)})
    (hBfin : Bfin = {q | ∃ (M : Type (max u v)) (_ : AddCommGroup M) (_ : Module R M)
      (_ : Module.Finite R M), q.asIdeal ∈ associatedPrimes S (N ⊗[R] M)}) :
    A = A' ∧
    (Afin ⊆ A ∧ Bfin ⊆ B ∧ Afin ⊆ A'fin ∧ A'fin ⊆ Bfin ∧ A ⊆ B) ∧
    (IsNoetherianRing S → A = Afin ∧ B = Bfin) ∧
    (Module.Flat R N → A = Afin ∧ Afin = A'fin ∧ B = Bfin) ∧
    (IsNoetherianRing R → Module.Flat R N →
      A = A' ∧ A' = Afin ∧ Afin = A'fin ∧ A'fin = Bfin ∧ Bfin = B)
Tag 05GC, a definition

Tag 05GC in the Stacks Project.

Module.relativeAssassin, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/RelativeAssassin/Defs.lean, line 100.

The relative assassin Ass_{S/R}(N) of an S-module N over a ring map R → S: the set of primes 𝔮 of S which, with 𝔭 = R ∩ 𝔮 the contraction of 𝔮 to R, are associated primes over S of the fibre module N ⊗_R κ(𝔭), that is, are the annihilator of some element of it. This is the set A of Module.relativeAssassin_comparison.

public def relativeAssassin : Set (PrimeSpectrum S)
Tag 0312, a lemma

Tag 0312 in the Stacks Project.

associatedPrimes.tensorProduct_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/FlatBaseChange.lean, line 495.

Let R → S be a ring map, let M be an R-module and let N be an S-module which is flat as an R-module. Then Ass_S(N ⊗_R M) ⊇ ⋃_{𝔭 ∈ Ass_R(M)} Ass_S(N / 𝔭N), and if R is Noetherian this inclusion is an equality. Here Ass is the set of primes that are the annihilator of an element, written out as such, and the index set of the equality is associatedPrimes R M.

public theorem associatedPrimes.tensorProduct_of_flat {R S M N : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module S N] [Module R N]
    [IsScalarTower R S N] [Module.Flat R N] :
    (⋃ p ∈ {p : Ideal R | p.IsPrime ∧ ∃ m : M, (⊥ : Submodule R M).colon {m} = p},
        {q : Ideal S | q.IsPrime ∧
          ∃ w : N ⧸ (p.map (algebraMap R S) • (⊤ : Submodule S N)),
            (⊥ : Submodule S (N ⧸ (p.map (algebraMap R S) • (⊤ : Submodule S N)))).colon {w} =
              q}) ⊆
      {q : Ideal S | q.IsPrime ∧ ∃ w : N ⊗[R] M, (⊥ : Submodule S (N ⊗[R] M)).colon {w} = q} ∧
    (IsNoetherianRing R →
      {q : Ideal S | q.IsPrime ∧ ∃ w : N ⊗[R] M, (⊥ : Submodule S (N ⊗[R] M)).colon {w} = q} =
        ⋃ p ∈ associatedPrimes R M,
          {q : Ideal S | q.IsPrime ∧
            ∃ w : N ⧸ (p.map (algebraMap R S) • (⊤ : Submodule S N)),
              (⊥ : Submodule S (N ⧸ (p.map (algebraMap R S) • (⊤ : Submodule S N)))).colon {w} =
                q})
Tag 05C1, a lemma

Tag 05C1 in the Stacks Project.

Stacks.AssociatedPrimes.Localization.associatedPrimes_chain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Localization.lean, line 311.

Stacks 05C1, combined (abstract). Under flatness, via the canonical map Spec(S ⊗_R K) → Spec(S), we have Ass_S(N) = Ass_S(N ⊗_R K) = Ass_{S ⊗_R K}(N ⊗_R K), where the last equality is read as the preimage identity along Ideal.comap (algebraMap S (S ⊗_R K)). All localization data are explicit hypotheses.

theorem associatedPrimes_chain [Module.Flat R N] (μN : N →ₗ[R] NK) (μNₛ : N →ₗ[S] NK)
    (hSK : IsLocalization (Algebra.algebraMapSubmonoid S (nonZeroDivisors R)) SK)
    (hμN : IsLocalizedModule (nonZeroDivisors R) μN)
    (hμNₛ : IsLocalizedModule (Algebra.algebraMapSubmonoid S (nonZeroDivisors R)) μNₛ)
    (hμ : ∀ n, μNₛ n = μN n) :
    associatedPrimes S N = associatedPrimes S NK ∧
      (Ideal.comap (algebraMap S SK)) ⁻¹' (associatedPrimes S NK)
        = associatedPrimes SK NK
Tag 05C2, a lemma

Tag 05C2 in the Stacks Project.

associatedPrimes.tensorProduct_of_flat_fiberRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/FlatTensorProduct.lean, line 420. References: EGA IV (3.3.1), “affine case”; EGA IV (3.3.6), “affine case, X = S”.

Stacks Tag 05C2. Let R → S be a ring map, let M be an R-module and let N be an S-module which is flat as an R-module. Viewing Spec(S ⊗_R κ(𝔭)) as a subset of Spec(S) (Tag 00E6), we have Ass_S(N ⊗_R M) ⊇ ⋃_{𝔭 ∈ Ass_R(M)} Ass_{S ⊗_R κ(𝔭)}(N ⊗_R κ(𝔭)), and this inclusion is an equality if R is Noetherian. Here Ass_R(M) is the source's set of associated primes of Tag 00LA, the primes that are the annihilator of an element of M; over a Noetherian ring it agrees with Mathlib's associatedPrimes, which is how the second assertion spells it.

public theorem associatedPrimes.tensorProduct_of_flat_fiberRing {R S M N : Type*} [CommRing R]
    [CommRing S] [Algebra R S] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module S N]
    [Module R N] [IsScalarTower R S N] [Module.Flat R N] :
    (⋃ p ∈ {p : PrimeSpectrum R | ∃ m : M, (⊥ : Submodule R M).colon {m} = p.asIdeal},
        PrimeSpectrum.comap (algebraMap S (S ⊗[R] p.asIdeal.ResidueField)) ''
          {Q | Q.asIdeal ∈ associatedPrimes (S ⊗[R] p.asIdeal.ResidueField)
            ((S ⊗[R] p.asIdeal.ResidueField) ⊗[S] N)}) ⊆
      {q : PrimeSpectrum S | q.asIdeal ∈ associatedPrimes S (N ⊗[R] M)} ∧
    (IsNoetherianRing R →
      {q : PrimeSpectrum S | q.asIdeal ∈ associatedPrimes S (N ⊗[R] M)} =
        ⋃ p ∈ {p : PrimeSpectrum R | p.asIdeal ∈ associatedPrimes R M},
          PrimeSpectrum.comap (algebraMap S (S ⊗[R] p.asIdeal.ResidueField)) ''
            {Q | Q.asIdeal ∈ associatedPrimes (S ⊗[R] p.asIdeal.ResidueField)
              ((S ⊗[R] p.asIdeal.ResidueField) ⊗[S] N)})
Sources
LeanModule.relativeAssassin_comparison · Module.relativeAssassin · associatedPrimes.tensorProduct_of_flat · Stacks.AssociatedPrimes.Localization.associatedPrimes_chain · associatedPrimes.tensorProduct_of_flat_fiberRing

Section10.66 Weakly associated primes#

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

Tag 0547, a definition

Tag 0547 in the Stacks Project.

IsWeaklyAssociatedPrime, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Defs.lean, line 81. The attribute's comment: “predicate”.

A prime ideal I of R is weakly associated to the R-module M if I is minimal among the prime ideals containing the annihilator (R ∙ m).annihilator of some element m ∈ M.

def IsWeaklyAssociatedPrime (I : Ideal R) : Prop

weaklyAssociatedPrimes, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Defs.lean, line 86. The attribute's comment: “set”.

The set of weakly associated primes of M (over R).

def weaklyAssociatedPrimes : Set (Ideal R)
Tag 0566, a lemma

Tag 0566 in the Stacks Project.

weaklyAssociated_iff_localization_and_exists_radical_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Defs.lean, line 247.

For a prime p of R, the following are equivalent:

  1. p is weakly associated to M;
  2. p R_p is weakly associated to M_p;
  3. there exists t ∈ M_p with √(Ann_{R_p}(t)) = p R_p.
theorem weaklyAssociated_iff_localization_and_exists_radical_eq
    (p : Ideal R) [p.IsPrime] :
    (WeaklyAssociated p M ↔
      WeaklyAssociated (IsLocalRing.maximalIdeal (Localization.AtPrime p))
        (LocalizedModule.AtPrime p M))
    ∧ (WeaklyAssociated (IsLocalRing.maximalIdeal (Localization.AtPrime p))
        (LocalizedModule.AtPrime p M) ↔
      ∃ t : LocalizedModule.AtPrime p M,
        (annihilatorOfElem_semiring (R := Localization.AtPrime p) t).radical
          = IsLocalRing.maximalIdeal (Localization.AtPrime p))
Tag 0EMA, a lemma

Tag 0EMA in the Stacks Project.

weakAss_eq_minimalPrimes0EMA, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Defs.lean, line 505.

For a reduced commutative ring R, the weakly associated primes of R are exactly the minimal primes of R.

theorem weakAss_eq_minimalPrimes0EMA [IsReduced R] :
    weaklyAssociatedPrimes R R = minimalPrimes R
Tag 0548, a lemma

Tag 0548 in the Stacks Project.

Module.weaklyAssociatedPrimes_subset_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/WeaklyAssociated.lean, line 680.

Stacks 0548, first inclusion. Let R be a ring and let f : M →ₗ[R] M' be an injective map of R-modules. Then WeakAss(M) ⊆ WeakAss(M'), where WeakAss(N) is the set of primes of R minimal over the annihilator of an element of N.

public theorem Module.weaklyAssociatedPrimes_subset_of_injective
    {R : Type*} [CommSemiring R] {M M' : Type*}
    [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M']
    {f : M →ₗ[R] M'} (hf : Function.Injective f) :
    {p : Ideal R | ∃ m : M, p ∈ (R ∙ m).annihilator.minimalPrimes} ⊆
      {p : Ideal R | ∃ m : M', p ∈ (R ∙ m).annihilator.minimalPrimes}

Module.weaklyAssociatedPrimes_subset_union_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/WeaklyAssociated.lean, line 695.

Stacks 0548, second inclusion. Let R be a ring and let 0 → M → M' → M'' be an exact sequence of R-modules, i.e. f : M →ₗ[R] M' is injective with image the kernel of g : M' →ₗ[R] M''. Then WeakAss(M') ⊆ WeakAss(M) ∪ WeakAss(M''), where WeakAss(N) is the set of primes of R minimal over the annihilator of an element of N.

public theorem Module.weaklyAssociatedPrimes_subset_union_of_exact
    {R : Type*} [CommSemiring R] {M M' M'' : Type*}
    [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M']
    [AddCommMonoid M''] [Module R M''] {f : M →ₗ[R] M'} {g : M' →ₗ[R] M''}
    (hf : Function.Injective f) (hfg : Function.Exact f g) :
    {p : Ideal R | ∃ m : M', p ∈ (R ∙ m).annihilator.minimalPrimes} ⊆
      {p : Ideal R | ∃ m : M, p ∈ (R ∙ m).annihilator.minimalPrimes} ∪
        {p : Ideal R | ∃ m : M'', p ∈ (R ∙ m).annihilator.minimalPrimes}
Tag 0588, a lemma

Tag 0588 in the Stacks Project.

weakAss_empty_iff_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Basic.lean, line 30.

Stacks Tag 0588 (Lemma 10.66.5): an R-module M is the zero module if and only if it has no weakly associated primes.

theorem weakAss_empty_iff_zero {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M]
    [Module R M] :
    (∀ m : M, m = 0) ↔ weaklyAssociatedPrimes R M = ∅
Tag 0589, a lemma

Tag 0589 in the Stacks Project.

StacksProblem.ass_subset_weakAss_subset_supp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Defs.lean, line 313. References: SGA 2 III (1.2), “(ii) ⇒ (i)”.

Stacks tag 0589 (Lemma 10.66.6): Ass(M) ⊆ WeakAss(M) ⊆ Supp(M).

theorem ass_subset_weakAss_subset_supp (R : Type*) [CommRing R] (M : Type*)
    [AddCommGroup M] [Module R M] :
    Ass R M ⊆ WeakAss R M ∧ WeakAss R M ⊆ Supp R M
Tag 05C3, a lemma

Tag 05C3 in the Stacks Project.

iUnion_weaklyAssociatedPrimes_eq_zeroDivisorsOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Defs.lean, line 293.

Let R be a commutative ring and M an R-module. The union of the weakly associated primes of M is the set of zerodivisors on M.

theorem iUnion_weaklyAssociatedPrimes_eq_zeroDivisorsOn
    (R : Type*) [CommRing R] (M : Type*) [AddCommGroup M] [Module R M] :
    (⋃ q ∈ weaklyAssociatedPrimes05C3 R M, (q : Set R)) = zeroDivisorsOn05C3 R M
Tag 05C4, a lemma

Tag 05C4 in the Stacks Project.

Module.exists_mem_minimalPrimes_annihilator_span_singleton_of_minimal_mem_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/WeaklyAssociated.lean, line 466.

Stacks 05C4. Let R be a ring and M an R-module. Any prime 𝔭 which is minimal among the elements of the support of M is weakly associated to M, i.e. 𝔭 is minimal over the annihilator of some element of M.

public theorem Module.exists_mem_minimalPrimes_annihilator_span_singleton_of_minimal_mem_support
    {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M] {p : PrimeSpectrum R}
    (hp : Minimal (· ∈ Module.support R M) p) :
    ∃ m : M, p.asIdeal ∈ (R ∙ m).annihilator.minimalPrimes
Tag 058A, a lemma

Tag 058A in the Stacks Project.

isAssociatedPrime_tfae_of_fg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/WeaklyAssociated.lean, line 312.

Stacks 058A. Let R be a ring, M an R-module and p a finitely generated ideal of R. Then p ∈ Ass(M), i.e. p is prime and is the annihilator of an element of M, iff p is an associated prime of M in Mathlib's sense (the radical of the annihilator of an element), iff p ∈ WeakAss(M), i.e. p is minimal among the primes containing the annihilator of an element of M.

public theorem isAssociatedPrime_tfae_of_fg {R : Type*} [CommSemiring R] {M : Type*}
    [AddCommMonoid M] [Module R M] {p : Ideal R} (hp : p.FG) :
    List.TFAE [(p.IsPrime ∧ ∃ m : M, p = (R ∙ m).annihilator),
      IsAssociatedPrime p M,
      ∃ m : M, p ∈ (R ∙ m).annihilator.minimalPrimes]

associatedPrimes_eq_setOf_exists_mem_minimalPrimes_annihilator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/WeaklyAssociated.lean, line 323.

Stacks 058A, the Noetherian case. Let R be a Noetherian ring and M an R-module. Then Ass(M) = WeakAss(M): a prime of R is the radical of the annihilator of an element of M if and only if it is minimal among the primes containing the annihilator of an element of M.

public theorem associatedPrimes_eq_setOf_exists_mem_minimalPrimes_annihilator {R : Type*}
    [CommSemiring R] [IsNoetherianRing R] {M : Type*} [AddCommMonoid M] [Module R M] :
    associatedPrimes R M =
      {p : Ideal R | ∃ m : M, p ∈ (R ∙ m).annihilator.minimalPrimes}
Tag 05C6, a lemma

Tag 05C6 in the Stacks Project.

weakAss_subset_image_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Basic.lean, line 79. References: EGA IV (3.1.10.1), “Lifting inclusion”.

Stacks tag 05C6 (Lemma 10.66.11): for a ring map φ : R → S and an S-module M regarded as an R-module by restriction of scalars along φ, every prime of R weakly associated to M is the contraction along φ of a prime of S weakly associated to M.

theorem weakAss_subset_image_comap
    {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S)
    {M : Type*} [AddCommGroup M] [Module S M] :
    letI : Module R M := Module.compHom M φ
    weaklyAssociatedPrimes R M ⊆ (Ideal.comap φ) '' (weaklyAssociatedPrimes S M)
Tag 05E1, a lemma

Tag 05E1 in the Stacks Project.

weakAss_eq_comap_image_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Functoriality.lean, line 262.

For a finite ring map φ : R → S and an S-module M, the weakly associated primes of M over R are exactly the contractions along f = Spec(φ) of the weakly associated primes of M over S, i.e. WeakAss_R(M) = f(WeakAss_S(M)) as subsets of Spec(R).

theorem weakAss_eq_comap_image_of_finite (hfin : Module.Finite R S) :
    {p : Ideal R | IsWeaklyAssociatedPrime R M p}
      = (Ideal.comap (algebraMap R S)) '' {q : Ideal S | IsWeaklyAssociatedPrime S M q}
Tag 05C8, a lemma

Tag 05C8 in the Stacks Project.

weaklyAssociatedPrimes_comap_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Defs.lean, line 342. References: EGA IV (3.1.10.1), “Quotient maps A → A/I”.

For a commutative ring R, an ideal I, and an R/I-module M (viewed as an R-module by restriction of scalars), the canonical injection π* = Ideal.comap (R → R/I) carries the weakly associated primes computed over R/I onto those computed over R.

theorem weaklyAssociatedPrimes_comap_quotient :
    Ideal.comap (Ideal.Quotient.mk I) '' weaklyAssociatedPrimes (R ⧸ I) M
      = weaklyAssociatedPrimes R M
Tag 05C9, a lemma

Tag 05C9 in the Stacks Project.

weakAss_localizedModule_eq_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Defs.lean, line 436. The attribute's comment: “(1)”.

WeakAss_R(S⁻¹M) = ι(WeakAss_{S⁻¹R}(S⁻¹M)): the R-module weakly associated primes of S⁻¹M are the image under ι of the S⁻¹R-module weakly associated primes of S⁻¹M.

theorem weakAss_localizedModule_eq_image :
    weakAss R (LocalizedModule S M) =
      localizationComap S '' (weakAss (Localization S) (LocalizedModule S M))

weakAss_inter_image_eq_weakAss_localizedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Defs.lean, line 466. The attribute's comment: “(2)”.

{ p ∈ WeakAss_R(M) | p ∈ ι(Spec(S⁻¹R)) } = WeakAss_R(S⁻¹M): the primes weakly associated to M and lying in the image of ι (i.e. disjoint from S) are exactly the primes weakly associated to S⁻¹M.

theorem weakAss_inter_image_eq_weakAss_localizedModule :
    {p ∈ weakAss R M | p ∈ Set.range (localizationComap S)} =
      weakAss R (LocalizedModule S M)
Tag 05CA, a lemma

Tag 05CA in the Stacks Project.

Module.weaklyAssociatedPrimes_eq_of_isSMulRegular_of_isLocalizedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Localization.lean, line 172.

Stacks 05CA. Let R be a ring, M an R-module and S ⊆ R a multiplicative subset such that every s ∈ S is a nonzerodivisor on M. Then M and its localization S⁻¹M have the same weakly associated primes: WeakAss(M) = WeakAss(S⁻¹M), where WeakAss(N) is the set of primes of R minimal over the annihilator of an element of N.

public theorem Module.weaklyAssociatedPrimes_eq_of_isSMulRegular_of_isLocalizedModule
    {R : Type*} [CommSemiring R] {M M' : Type*}
    [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M']
    (S : Submonoid R) (f : M →ₗ[R] M') [IsLocalizedModule S f]
    (hS : ∀ s ∈ S, IsSMulRegular M s) :
    {p : Ideal R | ∃ m : M, p ∈ (R ∙ m).annihilator.minimalPrimes} =
      {p : Ideal R | ∃ m : M', p ∈ (R ∙ m).annihilator.minimalPrimes}
Tag 05CB, a lemma

Tag 05CB in the Stacks Project.

Module.injective_pi_localization_weaklyAssociatedPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Separation.lean, line 197.

Stacks 05CB. Let R be a ring and M an R-module. The canonical map M → ∏_{𝔭 ∈ WeakAss(M)} M_𝔭 from M to the product of its localizations at the weakly associated primes of M — the primes minimal over the annihilator of an element of M — is injective.

public theorem Module.injective_pi_localization_weaklyAssociatedPrimes
    {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
    {Mₚ : {p : PrimeSpectrum R // ∃ m : M, p.asIdeal ∈ (R ∙ m).annihilator.minimalPrimes} → Type*}
    [∀ p, AddCommMonoid (Mₚ p)] [∀ p, Module R (Mₚ p)] (f : ∀ p, M →ₗ[R] Mₚ p)
    [∀ p, IsLocalizedModule.AtPrime p.1.asIdeal (f p)] :
    Function.Injective (LinearMap.pi f)
Tag 05CC, a lemma

Tag 05CC in the Stacks Project.

Stacks.WeaklyAssociatedPrimes.BaseChange.weakAss_eq_of_flat_domain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/Localization.lean, line 341.

Stacks tag 05CC (Lemma 10.66.18): let R → S be a ring map and N an S-module that is flat over the domain R (with Module R N compatible with the S-action via IsScalarTower R S N). Identifying S ⊗_R K with A = Localization T_S, N ⊗_R K with M = LocalizedModule T_S N, and Spec(S ⊗_R K) with its image in Spec(S) under PrimeSpectrum.comap (algebraMap S A), the weakly associated primes of N over S are exactly the images of the weakly associated primes of N ⊗_R K over S ⊗_R K: a prime q of S is weakly associated to N if and only if there is a prime q' of A that is weakly associated to M and whose contraction along S → A equals q.

theorem weakAss_eq_of_flat_domain
    [Module.Flat R N] (q : PrimeSpectrum S) :
    IsWeaklyAssociatedPrime S N q.asIdeal ↔
      ∃ q' : PrimeSpectrum (Localization (baseChangeSubmonoid R S)),
        IsWeaklyAssociatedPrime (Localization (baseChangeSubmonoid R S))
          (LocalizedModule (baseChangeSubmonoid R S) N) q'.asIdeal ∧
        PrimeSpectrum.comap (algebraMap S (Localization (baseChangeSubmonoid R S))) q' = q
Tag 0CUB, a lemma

Tag 0CUB in the Stacks Project.

IsWeaklyAssociatedPrime.comap_tensorProduct_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/WeaklyAssociatedFieldExtension.lean, line 499.

Stacks 0CUB. Let K / k be a field extension, R a k-algebra and M an R-module. If a prime 𝔮 ⊂ R ⊗[k] K is weakly associated to M ⊗[k] K, here written as the base change (R ⊗[k] K) ⊗[R] M, then the prime 𝔭 = 𝔮 ∩ R it lies over is weakly associated to M.

theorem IsWeaklyAssociatedPrime.comap_tensorProduct_field {k K R M : Type*} [Field k]
    [Field K] [Algebra k K] [CommRing R] [Algebra k R] [AddCommGroup M] [Module R M]
    {q : Ideal (R ⊗[k] K)} (hq : IsWeaklyAssociatedPrime (R ⊗[k] K) ((R ⊗[k] K) ⊗[R] M) q) :
    IsWeaklyAssociatedPrime R M (q.comap (algebraMap R (R ⊗[k] K)))
Sources
LeanIsWeaklyAssociatedPrime · weaklyAssociatedPrimes · weaklyAssociated_iff_localization_and_exists_radical_eq · weakAss_eq_minimalPrimes0EMA · Module.weaklyAssociatedPrimes_subset_of_injective · Module.weaklyAssociatedPrimes_subset_union_of_exact · weakAss_empty_iff_zero · StacksProblem.ass_subset_weakAss_subset_supp

Section10.67 Embedded primes#

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

Tag 02M5, a definition

Tag 02M5 in the Stacks Project.

IsEmbeddedAssociatedPrime, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Embedded.lean, line 899.

Definition 1 (Embedded associated prime). A prime 𝔭 is an embedded associated prime of M if it is an associated prime of M that is not minimal among the associated primes of M, i.e. there is an associated prime 𝔮 of M with 𝔮 ⊊ 𝔭.

def IsEmbeddedAssociatedPrime
    (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M] (𝔭 : Ideal R) : Prop
Tag 02M6, a lemma

Tag 02M6 in the Stacks Project.

Module.exists_isGreatest_isNowhereDense_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Embedded.lean, line 421.

Let R be a Noetherian ring and M a finite R-module. The set of R-submodules K ⊆ M whose support is nowhere dense in Supp(M) has a largest element K, and the quotient M' = M / K satisfies: (1) Supp(M) = Supp(M'); (2) every associated prime of M' is minimal among the associated primes of M', that is, M' has no embedded associated primes; (3) for every f ∈ R lying in all embedded associated primes of M, the localization of M → M' at the powers of f is bijective, so M_f ≅ M'_f.

public theorem exists_isGreatest_isNowhereDense_support :
    ∃ K : Submodule R M,
      IsGreatest {K : Submodule R M |
          IsNowhereDense (Subtype.val ⁻¹' support R ↥K : Set ↥(support R M))} K ∧
        support R (M ⧸ K) = support R M ∧
        (∀ p ∈ associatedPrimes R (M ⧸ K), Minimal (· ∈ associatedPrimes R (M ⧸ K)) p) ∧
        ∀ f : R, (∀ p ∈ associatedPrimes R M, ¬ Minimal (· ∈ associatedPrimes R M) p → f ∈ p) →
          Function.Bijective (LocalizedModule.map (Submonoid.powers f) K.mkQ)
Tag 02M7, a lemma

Tag 02M7 in the Stacks Project.

Module.isGreatest_isNowhereDense_support_localized', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Embedded.lean, line 859.

Let R be a Noetherian ring, M a finite R-module, and let K ⊆ M be the largest R-submodule whose support is nowhere dense in Supp(M), as produced by Module.exists_isGreatest_isNowhereDense_support. Let Rₚ be the localization of R at a submonoid p and g : M →ₗ[R] Mₚ the localization of M at p. Then the localized submodule Kₚ ⊆ Mₚ is the largest Rₚ-submodule of Mₚ whose support is nowhere dense in Supp(Mₚ). Since (M ⧸ K)ₚ = Mₚ ⧸ Kₚ, this says that removing the embedded associated primes commutes with localization: (M')ₚ = (Mₚ)'.

public theorem isGreatest_isNowhereDense_support_localized' (p : Submonoid R)
    [IsLocalization p Rₚ] (g : M →ₗ[R] Mₚ) [IsLocalizedModule p g] {K : Submodule R M}
    (hK : IsGreatest {K : Submodule R M |
        IsNowhereDense (Subtype.val ⁻¹' support R ↥K : Set ↥(support R M))} K) :
    IsGreatest {L : Submodule Rₚ Mₚ |
        IsNowhereDense (Subtype.val ⁻¹' support Rₚ ↥L : Set ↥(support Rₚ Mₚ))}
      (K.localized' Rₚ p g)
Tag 02M8, a lemma

Tag 02M8 in the Stacks Project.

hasNoEmbeddedAssociatedPrimes_quotient_annihilator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Embedded.lean, line 980.

Theorem (Stacks Tag 02M8). Let R be a Noetherian commutative ring and M a finite R-module having no embedded associated primes. Let I be the annihilator of M. Then R ⧸ I, viewed as a module over itself, has no embedded associated primes (i.e. the ring R ⧸ I has no embedded primes, in the sense of HasNoEmbeddedAssociatedPrimes).

theorem hasNoEmbeddedAssociatedPrimes_quotient_annihilator
    (R M : Type*) [CommRing R] [IsNoetherianRing R]
    [AddCommGroup M] [Module R M] [Module.Finite R M]
    (hM : HasNoEmbeddedAssociatedPrimes R M) :
    HasNoEmbeddedAssociatedPrimes (R ⧸ Module.annihilator R M) (R ⧸ Module.annihilator R M)
Sources
LeanIsEmbeddedAssociatedPrime · Module.exists_isGreatest_isNowhereDense_support · Module.isGreatest_isNowhereDense_support_localized' · hasNoEmbeddedAssociatedPrimes_quotient_annihilator

Section10.68 Regular sequences#

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

Tag 00LF, a definition

Tag 00LF in the Stacks Project.

Declarations registered for the tag:

Tag 00LG, an example

Tag 00LG in the Stacks Project.

regularSequence_xyz_one_sub_x, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/Regular/Basic.lean, line 281. The attribute's comment: “(1)”.

The sequence x, y(1-x), z(1-x) is a regular sequence on k[x, y, z].

theorem regularSequence_xyz_one_sub_x (k : Type) [Field k] :
    RingTheory.Sequence.IsRegular (mvPolyRingFin3 k)
      ([X 0, X 1 * (1 - X 0), X 2 * (1 - X 0)] : List (mvPolyRingFin3 k))

not_regularSequence_permuted_xyz_one_sub_x, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/Regular/Basic.lean, line 295. The attribute's comment: “(2)”.

The sequence y(1-x), z(1-x), x is not a regular sequence on k[x, y, z].

theorem not_regularSequence_permuted_xyz_one_sub_x (k : Type) [Field k] :
    ¬ RingTheory.Sequence.IsRegular (mvPolyRingFin3 k)
      ([X 1 * (1 - X 0), X 2 * (1 - X 0), X 0] : List (mvPolyRingFin3 k))
Tag 00LJ, a lemma

Tag 00LJ in the Stacks Project.

Declarations registered for the tag:

Tag 00LM, a lemma

Tag 00LM in the Stacks Project.

RingTheory.Sequence.isRegular_map_algebraMap_iff_of_faithfullyFlat_of_isBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/BaseChange.lean, line 155. References: EGA 0 (15.1.14), “converse (ff case)”; EGA 0 (15.2.5), “affine, faithfully flat”; EGA 0 (15.1.13), “special case”; SGA 3 VIIB (5.5.2), “special case”.

Let R be a commutative ring, M an R-module, S a faithfully flat R-algebra and f : M →ₗ[R] N a base change of M to S. Then a sequence rs in R is M-regular if and only if its image in S is N-regular.

public theorem isRegular_map_algebraMap_iff_of_faithfullyFlat_of_isBaseChange
    {f : M →ₗ[R] N} (hf : IsBaseChange S f) (rs : List R) :
    IsRegular N (rs.map (algebraMap R S)) ↔ IsRegular M rs
Tag 061L, a lemma

Tag 061L in the Stacks Project.

regular_sequence_localize_away_of_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/Regular/Basic.lean, line 580. References: EGA 0 (15.2.4), “special case”.

Regularity of a sequence over the localization at a prime spreads out to a localization away from some element not in the prime.

theorem regular_sequence_localize_away_of_atPrime
    {R : Type*} [CommRing R] [IsNoetherianRing R]
    {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M]
    (p : Ideal R) [p.IsPrime] (xs : List R)
    (hp : IsRegular (LocalizedModule p.primeCompl M)
      (xs.map (algebraMap R (Localization.AtPrime p)))) :
    ∃ g ∈ p.primeCompl,
      IsRegular (LocalizedModule (Submonoid.powers g) M)
        (xs.map (algebraMap R (Localization.Away g)))
Tag 065K, a lemma

Tag 065K in the Stacks Project.

Stacks.RingTheory.Sequence.isRegular_append_of_isRegular_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/Regular/Append.lean, line 50.

Let f be a regular sequence in A generating the ideal I, and let g be a list of elements of A whose images in A ⧸ I form a regular sequence. Then f ++ g is a regular sequence in A.

theorem isRegular_append_of_isRegular_quotient {A : Type*} [CommRing A] {I : Ideal A}
    {f g : List A} (hf : IsRegular A f) (hI : Ideal.ofList f = I)
    (hg : IsRegular (A ⧸ I) (g.map (Ideal.Quotient.mk I))) : IsRegular A (f ++ g)
Tag 0F1T, a lemma

Tag 0F1T in the Stacks Project.

isRegular_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/Regular/Basic.lean, line 670.

Given a short exact sequence 0 → M₁ →[α] M₂ →[β] M₃ → 0 of R-modules, if a sequence rs of elements of R is both M₁-regular and M₃-regular, then it is M₂-regular.

theorem isRegular_of_shortExact {R : Type*} [CommRing R]
    {M₁ M₂ M₃ : Type*} [AddCommGroup M₁] [Module R M₁]
    [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃]
    (α : M₁ →ₗ[R] M₂) (β : M₂ →ₗ[R] M₃)
    (hα : Function.Injective α) (hβ : Function.Surjective β)
    (hexact : LinearMap.range α = LinearMap.ker β)
    (rs : List R)
    (h1 : IsRegular M₁ rs) (h3 : IsRegular M₃ rs) :
    IsRegular M₂ rs
Tag 07DV, a lemma

Tag 07DV in the Stacks Project.

RingTheory.Sequence.isRegular_zipWith_pow_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/Powers.lean, line 302. References: EGA 0 (15.1.20), “first assertion”.

Stacks 07DV. Let R be a commutative ring, let M be an R-module, let rs = [f₁, …, f_r] be a list of elements of R and let es = [e₁, …, e_r] be a list of positive integers of the same length. Then f₁ ^ e₁, …, f_r ^ e_r is an M-regular sequence if and only if f₁, …, f_r is an M-regular sequence.

public theorem RingTheory.Sequence.isRegular_zipWith_pow_iff {R : Type*} [CommRing R]
    (M : Type*) [AddCommGroup M] [Module R M] {rs : List R} {es : List ℕ}
    (hlen : rs.length = es.length) (hes : ∀ e ∈ es, 0 < e) :
    IsRegular M (rs.zipWith (· ^ ·) es) ↔ IsRegular M rs
Tag 07DW, a lemma

Tag 07DW in the Stacks Project.

tfae_isRegular_perm_sublist_polySeq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/Regular/Permutation.lean, line 721.

Stacks Tag 07DW (Lemma 10.68.10). For fs = [f_1, …, f_r] : List R whose entries do not generate the unit ideal (Ideal.span {x | x ∈ fs} ≠ ⊤, i.e. (f_1, …, f_r) ≠ R), the three conditions are equivalent. The proof is the 3-cycle 1 → 2 → 3 → 1: 1 → 2 extends a sublist to a permutation; 2 → 3 is sg_two_to_three (Stacks 07DV); 3 → 1 is sg_three_to_one (variable-permutation automorphism + descent).

theorem tfae_isRegular_perm_sublist_polySeq (fs : List R) (hfs : Ideal.span {x | x ∈ fs} ≠ ⊤) :
    List.TFAE
      [ ∀ l' : List R, l'.Perm fs → IsRegular R l',
        ∀ l' : List R, l' <+ fs → IsRegular R l',
        IsRegular (MvPolynomial (Fin fs.length) R) (polySeq fs) ]
Sources
LeanRingTheory.Sequence.IsRegular · RingTheory.Sequence.isRegular_iff · RingTheory.Sequence.IsWeaklyRegular · RingTheory.Sequence.isWeaklyRegular_iff · regularSequence_xyz_one_sub_x · not_regularSequence_permuted_xyz_one_sub_x · IsLocalRing.isRegular_of_perm · RingTheory.Sequence.isRegular_map_algebraMap_iff_of_faithfullyFlat_of_isBaseChange

Section10.69 Quasi-regular sequences#

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

Tag 061N, an equation

Tag 061N in the Stacks Project.

quasiRegularCanonicalMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/QuasiRegular/Defs.lean, line 220. References: EGA 0 (15.1.1); EGA 0 (15.1.4); EGA 0 (15.1.5), “special case”; EGA 0 (15.2.1), “special case”; EGA 0 (17.1.1), “more general”; EGA IV (19.5.1); EGA IV (19.5.4), “more general”; EGA IV (19.6.2), “special case”; EGA IV (19.7.1), “special case”.

The canonical map φ : S → T, the (R/J)-linear map induced by canonicalBilin. On a monomial generator it sends X^e ⊗ m̄ ↦ (f^e · m mod J^{|e|+1}M).

noncomputable def quasiRegularCanonicalMap {c : ℕ} (f : Fin c → R) :
    Source M f →ₗ[qrRbar f] Target M f
Tag 061P, a definition

Tag 061P in the Stacks Project.

RingTheory.Sequence.IsQuasiRegular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/QuasiRegular/Defs/Defs.lean, line 50. References: EGA 0 (15.1.7), “quasi-regular half”; EGA 0 (15.1.4), “M-quasi-regular”; EGA 0 (15.2.2), “special case”; EGA IV (19.5.1); EGA IV (19.5.5.2), “more general”.

A sequence rs = f_1, …, f_c of elements of a commutative ring R is M-quasi-regular, for an R-module M, if the canonical map of graded (R/J)[X_1, …, X_c]-modules Φ_M : (R/J)[X_1, …, X_c] ⊗_{R/J} (M/JM) → ⨁_{n ≥ 0} J^n M / J^{n+1} M, X_1^{e_1} ⋯ X_c^{e_c} ⊗ m̄ ↦ f_1^{e_1} ⋯ f_c^{e_c} m mod J^{e_1 + … + e_c + 1} M, is an isomorphism, where J = (f_1, …, f_c). An R-quasi-regular sequence is called simply a quasi-regular sequence.

def IsQuasiRegular {R : Type*} [CommRing R] (M : Type*) [AddCommGroup M] [Module R M]
    (rs : List R) : Prop
Tag 00LN, a lemma

Tag 00LN in the Stacks Project.

Stacks.QuasiregularSequence.isRegular_isQuasiregularSeq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/QuasiRegular/Basic/RegularIsQuasiRegular.lean, line 900. The attribute's comment: “(2)”. References: EGA 0 (15.1.10), “necessity”; EGA 0 (15.1.9), “first assertion”; EGA IV (19.5.1), “a) ⇒ c)”.

Statement 2. An M-regular sequence (Mathlib's IsRegular, i.e. the full Definition 1 including M/JM ≠ 0) is M-quasi-regular.

Proved by REVERSE induction (last-element peel) on rs via List.reverseRecOn, using isQuasiregularSeq_snoc for the step.

theorem isRegular_isQuasiregularSeq (M : Type*) [AddCommGroup M] [Module R M] (rs : List R)
    (h : RingTheory.Sequence.IsRegular M rs) : IsQuasiregularSeq rs M

Stacks.QuasiregularSequence.isRegular_isQuasiregularSeq_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/QuasiRegular/Basic/RegularIsQuasiRegular.lean, line 921. The attribute's comment: “(1)”. References: EGA 0 (15.1.9), “first part, M = R”; EGA IV (19.5.1), “a) ⇒ c) for M = A”.

Statement 1. A regular sequence of R (the case M = R) is a quasi-regular sequence. This is the special case M = R of Statement 2.

theorem isRegular_isQuasiregularSeq_self (rs : List R) (h : RingTheory.Sequence.IsRegular R rs) :
    IsQuasiregularSeq rs R
Tag 065L, a lemma

Tag 065L in the Stacks Project.

RingTheory.Sequence.IsQuasiRegular.of_flat_of_isBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/QuasiRegular/Basic/FlatBaseChangeAndLocalConverse.lean, line 357.

Stacks 065L. Let R → S be a flat ring map, M an R-module and rs = f_1, …, f_r an M-quasi-regular sequence in R. Then the images of f_1, …, f_r in S form a M ⊗_R S-quasi-regular sequence, where the base change is taken abstractly: N is any S-module receiving an R-linear f : M →ₗ[R] N that exhibits it as the base change of M.

public theorem IsQuasiRegular.of_flat_of_isBaseChange {R S M N : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module S N]
    [IsScalarTower R S N] [Module.Flat R S] {f : M →ₗ[R] N} (hf : IsBaseChange S f) {rs : List R}
    (reg : IsQuasiRegular M rs) : IsQuasiRegular N (rs.map (algebraMap R S))
Tag 061Q, a lemma

Tag 061Q in the Stacks Project.

RingTheory.Sequence.exists_notMem_isQuasiRegular_away_of_isQuasiRegular_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/QuasiRegular/Basic/SpreadToStandardOpen.lean, line 502.

Stacks 061Q. Let R be a Noetherian ring, M a finite R-module, 𝔭 ⊂ R a prime and rs = x₁, …, x_c a sequence of elements of R whose image in R_𝔭 is M_𝔭-quasi-regular. Then there is a g ∈ R, g ∉ 𝔭, such that the image of rs in R_g is M_g-quasi-regular.

public theorem exists_notMem_isQuasiRegular_away_of_isQuasiRegular_atPrime {R : Type*} [CommRing R]
    [IsNoetherianRing R] {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M]
    (p : Ideal R) [p.IsPrime] (rs : List R) (Rₚ : Type*) [CommRing Rₚ] [Algebra R Rₚ]
    [IsLocalization.AtPrime Rₚ p] (Mₚ : Type*) [AddCommGroup Mₚ] [Module R Mₚ] [Module Rₚ Mₚ]
    [IsScalarTower R Rₚ Mₚ] (fₚ : M →ₗ[R] Mₚ) [IsLocalizedModule p.primeCompl fₚ]
    (hp : IsQuasiRegular Mₚ (rs.map (algebraMap R Rₚ))) :
    ∃ g ∉ p,
      ∀ (Rg : Type*) [CommRing Rg] [Algebra R Rg] [IsLocalization.Away g Rg] (Mg : Type*)
        [AddCommGroup Mg] [Module R Mg] [Module Rg Mg] [IsScalarTower R Rg Mg] (fg : M →ₗ[R] Mg)
        [IsLocalizedModule (Submonoid.powers g) fg],
        IsQuasiRegular Mg (rs.map (algebraMap R Rg))
Tag 061R, a lemma

Tag 061R in the Stacks Project.

RingTheory.Sequence.IsQuasiRegular.quasiRegular_drop_mod_prev, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/QuasiRegular/Basic/QuotientByPrefix.lean, line 554.

Stacks 061R. Let M be a module over a commutative ring R and let rs = f_1, …, f_c be an M-quasi-regular sequence in R. For any i, the images f̄_{i+1}, …, f̄_c of the remaining elements in R̄ = R/(f_1, …, f_i) form an M̄-quasi-regular sequence, where M̄ = M/(f_1, …, f_i)M.

public theorem IsQuasiRegular.quasiRegular_drop_mod_prev {R M : Type*} [CommRing R]
    [AddCommGroup M] [Module R M] {rs : List R} (reg : IsQuasiRegular M rs) (i : ℕ) :
    IsQuasiRegular (M ⧸ (Ideal.ofList (rs.take i) • ⊤ : Submodule R M))
      ((rs.drop i).map (Ideal.Quotient.mk (Ideal.ofList (rs.take i))))
Tag 061S, a lemma

Tag 061S in the Stacks Project.

RingTheory.Sequence.IsRegular.of_isQuasiRegular_of_mem_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/QuasiRegular/Basic/FlatBaseChangeAndLocalConverse.lean, line 708. References: EGA 0 (15.1.9), “converse, local”; EGA 0 (15.1.11), “converse, local case”; EGA 0 (15.2.2), “converse: q-reg ⇒ reg”; EGA IV (16.9.11), “local Noetherian ring”; EGA 0 (15.1.10), “sufficiency”; EGA 0 (15.1.3), “partial”; EGA IV (16.9.12), “parenthetical”; EGA IV (19.5.1), “special case”.

Stacks 061S. Let (R, 𝔪) be a local Noetherian ring and let M be a nonzero finite R-module. An M-quasi-regular sequence f_1, …, f_c of elements of 𝔪 is an M-regular sequence.

public theorem IsRegular.of_isQuasiRegular_of_mem_maximalIdeal {R M : Type*} [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R] [AddCommGroup M] [Module R M] [Nontrivial M]
    [Module.Finite R M] {rs : List R} (mem : ∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R)
    (reg : IsQuasiRegular M rs) : IsRegular M rs
Tag 065N, a lemma

Tag 065N in the Stacks Project.

isMQuasiregular_iff_isMQuasiregular_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Sequence/QuasiRegular/Graded.lean, line 704.

Theorem (Stacks Tag 065N, Lemma 10.69.9). The sequence f_1, ..., f_r is M-quasi-regular (over R, with respect to M) if and only if the image sequence f̄_1, ..., f̄_r is M̄-quasi-regular (over R̄ = R / I_R, with respect to M̄ = M / I_M).

theorem isMQuasiregular_iff_isMQuasiregular_quotient {c : ℕ} (f : Fin c → R) :
    letI := mbarModule (M := M) f
    IsMQuasiregular (M := M) f ↔
      IsMQuasiregular (R := Rbar f) (M := Mbar (M := M) f) (fbar f)
Sources
LeanquasiRegularCanonicalMap · RingTheory.Sequence.IsQuasiRegular · Stacks.QuasiregularSequence.isRegular_isQuasiregularSeq · Stacks.QuasiregularSequence.isRegular_isQuasiregularSeq_self · RingTheory.Sequence.IsQuasiRegular.of_flat_of_isBaseChange · RingTheory.Sequence.exists_notMem_isQuasiRegular_away_of_isQuasiRegular_atPrime · RingTheory.Sequence.IsQuasiRegular.quasiRegular_drop_mod_prev · RingTheory.Sequence.IsRegular.of_isQuasiRegular_of_mem_maximalIdeal

Section10.70 Blow up algebras#

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

Tag 052Q, a definition

Tag 052Q in the Stacks Project.

affineBlowupAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Defs.lean, line 85.

The affine blowup algebra R[I/a] of an ideal I of a ring R and an element a : R, defined as the R-subalgebra of a localization S of R away from a generated by the fractions y/a with y ∈ I. For a ∈ I its elements are exactly the fractions x/aⁿ with x ∈ Iⁿ.

public def affineBlowupAlgebra (I : Ideal R) (a : R) (S : Type*) [CommRing S] [Algebra R S]
    [IsLocalization.Away a S] : Subalgebra R S
Tag 07Z3, a lemma

Tag 07Z3 in the Stacks Project.

blowup_image_a_mem_nonZeroDivisors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Basic.lean, line 647. The attribute's comment: “(1)”. References: EGA IV (19.4.1), “partial”.

The image of a in R[I/a] is a nonzerodivisor.

theorem blowup_image_a_mem_nonZeroDivisors {R : Type*} [CommRing R] (I : Ideal R) (a : R)
    (ha : a ∈ I) :
    haveI : Fact (a ∈ I) := ⟨ha⟩
    (algebraMap R (Blowup I a)) a ∈ nonZeroDivisors (Blowup I a)

blowup_idealMap_eq_span, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Basic.lean, line 668. The attribute's comment: “(2)”. References: EGA IV (19.4.1), “partial”.

The ideal of R[I/a] generated by the image of I equals the principal ideal generated by the image of a.

theorem blowup_idealMap_eq_span {R : Type*} [CommRing R] (I : Ideal R) (a : R) (ha : a ∈ I) :
    haveI : Fact (a ∈ I) := ⟨ha⟩
    Ideal.map (algebraMap R (Blowup I a)) I
      = Ideal.span {(algebraMap R (Blowup I a)) a}

blowup_localization_away_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Basic.lean, line 701. The attribute's comment: “(3)”.

The map R_a → (R[I/a])_a induced by the structure map R → R[I/a] on localizations at the powers of a is bijective.

theorem blowup_localization_away_bijective {R : Type*} [CommRing R] (I : Ideal R) (a : R)
    (ha : a ∈ I) :
    haveI : Fact (a ∈ I) := ⟨ha⟩
    Function.Bijective (Localization.awayMap (Blowup.of : R →+* Blowup I a) a)
Tag 0BIP, a lemma

Tag 0BIP in the Stacks Project.

affineBlowup_baseChange_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Basic.lean, line 1422.

The map Φ of affineBlowup_baseChange induces an isomorphism of S-algebras (S ⊗[R] R[I/a]) / (S ⊗[R] R[I/a])[b^∞] ≅ S[J/b].

theorem affineBlowup_baseChange_iso :
    Nonempty <|
      (TensorProduct R S (affineBlowup0BIP I a ha) ⧸
        torsionIdeal (TensorProduct R S (affineBlowup0BIP I a ha))
          (algebraMap S _ (algebraMap R S a)))
      ≃ₐ[S]
      (affineBlowup0BIP (I.map (algebraMap R S)) (algebraMap R S a)
        (Ideal.mem_map_of_mem _ ha))
Tag 0G8S, a lemma

Tag 0G8S in the Stacks Project.

Ideal.range_eq_affineBlowup_and_ker_eq_saturation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Affine.lean, line 279.

Stacks 0G8S. Let R be a ring, let I = (a, bᵢ : i ∈ ι) be an ideal of R generated by a together with a family b : ι → R, and let Rₐ be the localization of R at a. Let φ : R[xᵢ : i ∈ ι] → Rₐ be the R-algebra map with φ xᵢ = bᵢ/a. Then the range of φ is the affine blowup algebra R[I/a] = {x/aⁿ : x ∈ Iⁿ}, and φ f = 0 if and only if aⁿ f lies in the ideal of relations (a xᵢ - bᵢ) for some n; that is, φ induces a surjection R[xᵢ]/(a xᵢ - bᵢ) → R[I/a] whose kernel is the a-power torsion of the source.

public theorem Ideal.range_eq_affineBlowup_and_ker_eq_saturation
    {R : Type*} [CommRing R] {ι : Type*} {Rₐ : Type*} [CommRing Rₐ] [Algebra R Rₐ]
    {a : R} {b : ι → R} {I : Ideal R} [IsLocalization.Away a Rₐ]
    (hI : I = Ideal.span (insert a (Set.range b)))
    (φ : MvPolynomial ι R →ₐ[R] Rₐ)
    (hφ : ∀ i, φ (X i) * algebraMap R Rₐ a = algebraMap R Rₐ (b i)) :
    Set.range φ =
        {y : Rₐ | ∃ n : ℕ, ∃ x ∈ I ^ n, y * algebraMap R Rₐ a ^ n = algebraMap R Rₐ x} ∧
      ∀ f : MvPolynomial ι R, φ f = 0 ↔
        ∃ n : ℕ, a ^ n • f ∈ Ideal.span (Set.range fun i ↦ C a * X i - C (b i))
Tag 080U, a lemma

Tag 080U in the Stacks Project.

AffineBlowup.fImage_mem_nonZeroDivisors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Basic.lean, line 950. The attribute's comment: “f nonzerodivisor in R'”.

If a ∈ I and V(f) = V(I), then the image of f in R' = R[I/a] is a nonzerodivisor.

theorem fImage_mem_nonZeroDivisors (ha : a ∈ I) (f : R)
    (hf : PrimeSpectrum.zeroLocus ({f} : Set R) = PrimeSpectrum.zeroLocus (I : Set R)) :
    fImage I a f ∈ nonZeroDivisors (Rprime I a)

AffineBlowup.blowup_localization_f_iso_a, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Basic.lean, line 996. The attribute's comment: “R'_f = R'_a”.

Assume a ∈ I and V(f) = V(I). Let R'f be a localization of R' = R[I/a] away from the image of f, and R'a a localization of R' away from the image of a. Then R'f is also a localization of R' away from the image of a, and R'f ≃ₐ[R] R'a.

theorem blowup_localization_f_iso_a (ha : a ∈ I) (f : R)
    (hf : PrimeSpectrum.zeroLocus ({f} : Set R) = PrimeSpectrum.zeroLocus (I : Set R))
    (R'f R'a : Type*) [CommRing R'f] [CommRing R'a]
    [Algebra (Rprime I a) R'f] [Algebra (Rprime I a) R'a]
    [Algebra R R'f] [Algebra R R'a]
    [IsScalarTower R (Rprime I a) R'f] [IsScalarTower R (Rprime I a) R'a]
    [IsLocalization.Away (fImage I a f) R'f]
    [IsLocalization.Away (algebraMap R (Rprime I a) a) R'a] :
    IsLocalization.Away (algebraMap R (Rprime I a) a) R'f ∧
      Nonempty (R'f ≃ₐ[R] R'a)

AffineBlowup.ringLocalization_a_iso_blowup_localization_a, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Basic.lean, line 1029. The attribute's comment: “R'_a = R_a”.

Let R'a be a localization of R' = R[I/a] away from the image of a, and Ra' a localization of R away from a. Then the canonical map R_a → R'_a induced by R → R' is bijective.

theorem ringLocalization_a_iso_blowup_localization_a
    (R'a Ra' : Type*) [CommRing R'a] [CommRing Ra']
    [Algebra (Rprime I a) R'a] [Algebra R Ra'] [Algebra R R'a]
    [IsScalarTower R (Rprime I a) R'a]
    [IsLocalization.Away (algebraMap R (Rprime I a) a) R'a]
    [IsLocalization.Away a Ra'] :
    Function.Bijective
      (IsLocalization.Away.map Ra' R'a (algebraMap R (Rprime I a)) a)
Tag 0BBI, a lemma

Tag 0BBI in the Stacks Project.

IsLocalization.Away.map_affineBlowupAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Affine.lean, line 459.

Stacks 0BBI, surjectivity. Let R be a ring, I ⊆ R an ideal and a f : R. The canonical R-algebra map from a localization A of R away from a to a localization B of R away from f * a maps the affine blowup algebra R[I/a] ⊆ A onto the affine blowup algebra R[fI/(fa)] ⊆ B.

public theorem IsLocalization.Away.map_affineBlowupAlgebra {R : Type*} [CommRing R]
    (I : Ideal R) (a f : R) (A : Type*) [CommRing A] [Algebra R A] [IsLocalization.Away a A]
    (B : Type*) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
    [IsLocalization.Away (f * a) B] :
    (affineBlowupAlgebra I a A).map (IsScalarTower.toAlgHom R A B) =
      affineBlowupAlgebra (Ideal.span {f} * I) (f * a) B

IsLocalization.Away.map_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Affine.lean, line 473.

Stacks 0BBI, the kernel. Let A be an algebra over a commutative semiring R, let f : R and let B be a localization of A away from the image of f. Then y : A maps to 0 in B if and only if y is f-power torsion. Restricted to the affine blowup algebra R[I/a] ⊆ A this describes the kernel of the map R[I/a] → R[fI/(fa)] of IsLocalization.Away.map_affineBlowupAlgebra.

public theorem IsLocalization.Away.map_eq_zero_iff {R : Type*} [CommSemiring R] {A : Type*}
    [CommSemiring A] [Algebra R A] {B : Type*} [CommSemiring B] [Algebra A B]
    (f : R) [IsLocalization.Away (algebraMap R A f) B] (y : A) :
    algebraMap A B y = 0 ↔ ∃ n : ℕ, f ^ n • y = 0
Tag 052S, a lemma

Tag 052S in the Stacks Project.

isReduced_affineBlowup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Basic.lean, line 293.

If R is reduced and a ∈ I, then the affine blowup algebra R[I/a] is reduced.

theorem isReduced_affineBlowup [IsReduced R] (ha : a ∈ I) :
    IsReduced (affineBlowupAlgebraAway I a)
Tag 052R, a lemma

Tag 052R in the Stacks Project.

affineBlowup_isDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Basic.lean, line 143.

If R is a domain, I ⊆ R an ideal, and a ∈ I is a nonzero element, then the affine blowup algebra R[I/a] is a domain.

theorem affineBlowup_isDomain [IsDomain R] (ha : a ≠ 0) :
    IsDomain (affineBlowup I a)
Tag 052T, a lemma

Tag 052T in the Stacks Project.

PrimeSpectrum.denseRange_comap_of_notMem_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Dominant.lean, line 148.

Blowing up is dominant. Let f : R →+* S be a ring map and a : R an element such that every element of the kernel of f is annihilated by a power of a. If a is contained in no minimal prime of R, then Spec S → Spec R has dense image.

Applied to the affine blowup algebra S = R[I/a] of an ideal I ∋ a — whose structure map kills exactly the a-power torsion of R — this is Stacks Tag 052T; see PrimeSpectrum.denseRange_comap_algebraMap_affineBlowupAlgebra.

public theorem denseRange_comap_of_notMem_minimalPrimes {R S : Type*} [CommSemiring R]
    [CommSemiring S] (f : R →+* S) (a : R)
    (hker : ∀ x : R, f x = 0 → ∃ n : ℕ, a ^ n * x = 0)
    (ha : ∀ p ∈ minimalPrimes R, a ∉ p) :
    DenseRange (comap f)

PrimeSpectrum.denseRange_comap_algebraMap_affineBlowupAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/Dominant.lean, line 163.

Blowing up is dominant. Let R be a ring, I ⊆ R an ideal and a : R. If a is contained in no minimal prime of R, then Spec (R[I/a]) → Spec R has dense image, where R[I/a] = affineBlowupAlgebra I a S is the affine blowup algebra of (R, I) at a, realized inside a localization S of R away from a.

The source assumes a ∈ I; the statement holds without it, since for arbitrary a the algebra affineBlowupAlgebra I a S is the affine blowup algebra of I + (a) at a.

public theorem denseRange_comap_algebraMap_affineBlowupAlgebra {R : Type*} [CommRing R]
    (I : Ideal R) (a : R) (S : Type*) [CommRing S] [Algebra R S] [IsLocalization.Away a S]
    (ha : ∀ p ∈ minimalPrimes R, a ∉ p) :
    DenseRange (comap (algebraMap R (affineBlowupAlgebra I a S)))
Tag 052M, a lemma

Tag 052M in the Stacks Project.

Stacks.AffineBlowup.stacks052M_main, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AffineBlowup/Valuation.lean, line 743.

Theorem 1 (Stacks Tag 052M, main case 𝔪 ≠ 0). Let (R, 𝔪) be a local domain with fraction field K, and assume 𝔪 ≠ 0. Let A be a valuation ring of K which dominates R. Then the family 𝒮 of admissible affine blowup algebras of Definition 7:

  1. is nonempty and directed under inclusion, and moreover for any two admissible pairs (I, a), (J, b) (Definition 7'), the explicit displayed product pair (I*J, a*b) is again an admissible pair, and its associated subring affineBlowupImage (I*J) (a*b) contains both affineBlowupImage I a and affineBlowupImage J b; and
  2. has directed union equal to A: an element x ∈ K lies in A iff it lies in some member of 𝒮.

Assembled from the four conjunct lemmas stacks052M_C1_nonempty, stacks052M_C2_directed, stacks052M_C3_refinement, stacks052M_C4_union.

theorem stacks052M_main
    [IsDomain R] [IsLocalRing R]
    (hm : IsLocalRing.maximalIdeal R ≠ ⊥)
    (A : ValuationSubring K) (hdom : Dominates R A) :
    -- (1a) nonemptiness
    (∃ B, IsAdmissibleBlowup R A B) ∧
    -- (1b) abstract directedness under inclusion
    DirectedOn (· ≤ ·) {B | IsAdmissibleBlowup R A B} ∧
    -- (1c) the explicit common refinement `R[IJ/(ab)]` of two admissible pairs:
    -- the displayed product pair `(I*J, a*b)` is itself an admissible pair, and
    -- its subring contains both factors.
    (∀ (I J : Ideal R) (a b : R) (ha : a ∈ I) (hb : b ∈ J),
        IsAdmissiblePair R A I a ha →
        IsAdmissiblePair R A J b hb →
        ∃ (hab : a * b ∈ I * J),
          IsAdmissiblePair R A (I * J) (a * b) hab ∧
          (affineBlowupImage I a ha : Subring K) ≤ affineBlowupImage (I * J) (a * b) hab ∧
          (affineBlowupImage J b hb : Subring K) ≤ affineBlowupImage (I * J) (a * b) hab) ∧
    -- (2) the directed union equals A
    (∀ x : K, x ∈ A ↔ ∃ B, IsAdmissibleBlowup R A B ∧ x ∈ B)
Sources
LeanaffineBlowupAlgebra · blowup_image_a_mem_nonZeroDivisors · blowup_idealMap_eq_span · blowup_localization_away_bijective · affineBlowup_baseChange_iso · Ideal.range_eq_affineBlowup_and_ker_eq_saturation · AffineBlowup.fImage_mem_nonZeroDivisors · AffineBlowup.blowup_localization_f_iso_a

Section10.71 Ext groups#

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

Tag 00LP, a lemma

Tag 00LP in the Stacks Project.

exists_free_resolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/Existence.lean, line 278. The attribute's comment: “(1)”.

(Existence of a free resolution.) For any commutative ring R and any R-module M, there exists an exact complex of R-modules ... → F₂ → F₁ → F₀ → M → 0 in which every Fᵢ is free.

theorem exists_free_resolution
    (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] :
    ∃ P : FreeResolutionData R M, P.IsExact ∧ P.IsFree

exists_finite_free_resolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/Existence.lean, line 294. The attribute's comment: “(2)”. References: EGA 0 (11.9.2), “special case”; EGA IV (12.3.2), “(i), special case”; SGA 2 VIII (1.2), “partial”; SGA 4 IX (2.3), “partial”; SGA 6 VI (1.6), “partial”.

(Finite free resolution in the Noetherian finite case.) If R is a Noetherian commutative ring and M is a finite R-module, then there exists an exact complex of R-modules ... → F₂ → F₁ → F₀ → M → 0 in which every Fᵢ is finite free.

theorem exists_finite_free_resolution
    (R : Type u) [CommRing R] [IsNoetherianRing R]
    (M : Type u) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    ∃ P : FreeResolutionData R M, P.IsExact ∧ P.IsFiniteFree
Tag 00LQ, a definition

Tag 00LQ in the Stacks Project.

CategoryTheory.ObjectProperty.LeftResolution, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/Defs/Comparison.lean, line 95.

A P.LeftResolution Z consists of a bundled ℕ-indexed chain complex whose terms lie in the class P, along with a quasi-isomorphism to the complex consisting of just Z supported in degree 0; equivalently, an exact complex … → F₁ → F₀ → Z → 0 with all Fᵢ in P.

public structure LeftResolution (P : ObjectProperty C) (Z : C)

ModuleResolution, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/Defs/Comparison.lean, line 131. The attribute's comment: “resolution”. References: SGA 4½ Etat 0 (3.1.8), “special case”.

A (left) resolution F_• → M of an R-module M: an exact chain complex … → F₂ → F₁ → F₀ → M → 0 of R-modules, encoded as an ℕ-indexed chain complex together with a quasi-isomorphism to M in degree 0.

structure ModuleResolution (R : Type u) [Ring R] (M : Type v)
    [AddCommGroup M] [Module R M]

FreeModuleResolution, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/Defs/Comparison.lean, line 146. The attribute's comment: “free resolution”. References: EGA 0 (11.4.1).

A resolution of M by free R-modules: a resolution F_• → M such that every F_i is a free R-module.

structure FreeModuleResolution (R : Type u) [Ring R] (M : Type v)
    [AddCommGroup M] [Module R M] extends ModuleResolution R M

FiniteFreeModuleResolution, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/Defs/Comparison.lean, line 154. The attribute's comment: “finite free resolution”.

A resolution of M by finite free R-modules: a resolution F_• → M such that every F_i is a free and finitely generated R-module.

structure FiniteFreeModuleResolution (R : Type u) [Ring R] (M : Type v)
    [AddCommGroup M] [Module R M] extends FreeModuleResolution R M
Tag 00LR, a lemma

Tag 00LR in the Stacks Project.

Declarations registered for the tag:

Tag 00LS, a lemma

Tag 00LS in the Stacks Project.

exists_lift_along_resolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/Comparison.lean, line 372. The attribute's comment: “(1)”.

Statement (1): Existence of a lift. Let φ : M → N be a map of R-modules, let C be an (arbitrary) resolution of N, and let F be a complex over M whose terms are all free R-modules. Then there exists a map of complexes α : F → C lifting φ.

theorem exists_lift_along_resolution {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N]
    [Module R N]
    (φ : M →ₗ[R] N) (F : ComplexOver R M) (C : ComplexOver R N)
    (hC : IsResolution C) (hF : IsFreeComplex F) :
    ∃ α : ∀ i, F.obj i →ₗ[R] C.obj i, IsLift φ F C α

lift_unique_up_to_homotopy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/Comparison.lean, line 412. The attribute's comment: “(2)”. References: EGA III (6.3.8), “partial”.

Statement (2): Uniqueness up to homotopy. Any two maps of complexes α, β : F → C lifting the same φ are chain homotopic.

theorem lift_unique_up_to_homotopy {M N : Type*} [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N]
    (φ : M →ₗ[R] N) (F : ComplexOver R M) (C : ComplexOver R N)
    (hC : IsResolution C) (hF : IsFreeComplex F)
    (α β : ∀ i, F.obj i →ₗ[R] C.obj i)
    (hα : IsLift φ F C α) (hβ : IsLift φ F C β) :
    HomotopicComplexOver F C α β
Tag 00LT, a lemma

Tag 00LT in the Stacks Project.

ModuleCat.homologyMap_linearYoneda_eq_and_isIso_and_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/Resolution/Comparison.lean, line 192. The attribute's comment: “A free resolution is an ObjectProperty.LeftResolution for the class of free modules (00LQ) and Hom_R(F_•, N) is the image of F_• under (linearYoneda R (ModuleCat R)).obj N, so H^i(α) is a homologyMap. The source's display has the two cohomology groups interchanged, since Hom_R(-, N) is contravariant; see the module docstring.”.

Stacks 00LT. Let R be a ring, let M₁, M₂, N be R-modules, let F be a free resolution of M₁, let G be a free resolution of M₂, let φ : M₁ → M₂ be a module map and let α : F_• → G_• be a map of complexes inducing φ. Then, for every i, the map H^i(α) : H^i(Hom_R(G_•, N)) → H^i(Hom_R(F_•, N)) is independent of the choice of α; it is an isomorphism if φ is one; and a map F_• → F_• inducing the identity of M₁ induces the identity on H^i(Hom_R(F_•, N)).

public theorem homologyMap_linearYoneda_eq_and_isIso_and_eq_id {R : Type u} [CommRing R]
    {M₁ M₂ : ModuleCat.{v} R} (N : ModuleCat.{v} R)
    (F : ObjectProperty.LeftResolution (fun P : ModuleCat.{v} R => Module.Free R P) M₁)
    (G : ObjectProperty.LeftResolution (fun P : ModuleCat.{v} R => Module.Free R P) M₂)
    (φ : M₁ ⟶ M₂) (α : F.complex ⟶ G.complex)
    (hα : α ≫ G.π = F.π ≫ (ChainComplex.single₀ (ModuleCat.{v} R)).map φ) (i : ℕ) :
    (∀ β : F.complex ⟶ G.complex,
        β ≫ G.π = F.π ≫ (ChainComplex.single₀ (ModuleCat.{v} R)).map φ →
        homologyMap ((opFunctor _ _ ⋙
            ((linearYoneda R (ModuleCat.{v} R)).obj N).mapHomologicalComplex _).map β.op) i =
          homologyMap ((opFunctor _ _ ⋙
            ((linearYoneda R (ModuleCat.{v} R)).obj N).mapHomologicalComplex _).map α.op) i) ∧
      (IsIso φ → IsIso (homologyMap ((opFunctor _ _ ⋙
          ((linearYoneda R (ModuleCat.{v} R)).obj N).mapHomologicalComplex _).map α.op) i)) ∧
      (∀ γ : F.complex ⟶ F.complex, γ ≫ F.π = F.π →
        homologyMap ((opFunctor _ _ ⋙
          ((linearYoneda R (ModuleCat.{v} R)).obj N).mapHomologicalComplex _).map γ.op) i
            = 𝟙 _)
Tag 00LU, a lemma

Tag 00LU in the Stacks Project.

Declarations registered for the tag:

Tag 065P, a lemma

Tag 065P in the Stacks Project.

Declarations registered for the tag:

Tag 00LV, a lemma

Tag 00LV in the Stacks Project.

ext_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ext/Finiteness.lean, line 527.

Stacks 00LV. If x annihilates N or x annihilates M, then x annihilates every Ext group \(\operatorname{Ext}^i_R(M, N)\).

theorem ext_annihilated (M N : ModuleCat.{u} R) (x : R)
    (h : x ∈ Module.annihilator R N ∨ x ∈ Module.annihilator R M) (i : ℕ) :
    ∀ ξ : extModule M N i, x • ξ = 0
Tag 08YR, a lemma

Tag 08YR in the Stacks Project.

ext_finite_of_noetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ext/Finiteness.lean, line 315. References: EGA III (4.5.1), “special case”; SGA 6 I (3.7), “Clause b), special case”.

For a Noetherian ring R and finite R-modules M, N, each Ext^i_R(M, N) is a finite R-module.

theorem ext_finite_of_noetherian (R : Type) [CommRing R] [IsNoetherianRing R]
    (M N : ModuleCat.{0} R) [Module.Finite R M] [Module.Finite R N] (i : ℕ) :
    Module.Finite R (((Ext R (ModuleCat R) i).obj (Opposite.op M)).obj N)
Sources
Leanexists_free_resolution · exists_finite_free_resolution · CategoryTheory.ObjectProperty.LeftResolution · ModuleResolution · FreeModuleResolution · FiniteFreeModuleResolution · Homotopy.homologyMap_eq · exists_lift_along_resolution

Section10.72 Depth#

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

Tag 00LI, a definition

Tag 00LI in the Stacks Project.

Module.depth, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/Defs/Defs.lean, line 53. References: EGA 0 (16.4.5), “more general”; EGA IV (5.7.1), “more general”; EGA IV (6.10.3); SGA 2 III (2.8), “special case”; SGA 2 IV (5.3); SGA 2 XI (3.10).

The I-depth of an R-module M, for I an ideal of R: the supremum in ℕ∞ = {0, 1, 2, …, ∞} of the lengths of the M-regular sequences with all terms in I, except that the depth is ⊤ when I • M = M (which happens for instance when M = 0).

public noncomputable def Module.depth (R : Type*) [CommRing R] (I : Ideal R) (M : Type*)
    [AddCommGroup M] [Module R M] : ℕ∞
Tag 0AUI, a lemma

Tag 0AUI in the Stacks Project.

Module.depth_eq_iSup_isWeaklyRegular_length, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/Criteria.lean, line 202. References: EGA 0 (16.4.5), “more general”.

The I-depth of a finite R-module M is the supremum of the lengths of the sequences f₁, …, f_r ∈ I such that fᵢ is a nonzerodivisor on M/(f₁, …, f_{i-1})M; that is, the nonvanishing requirement M/(f₁, …, f_r)M ≠ 0 on regular sequences and the case distinction I • M = M in the definition of the depth may be dropped together.

public theorem depth_eq_iSup_isWeaklyRegular_length (R : Type*) [CommRing R] (I : Ideal R)
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    depth R I M =
      ⨆ rs ∈ {rs : List R | (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsWeaklyRegular M rs},
        (rs.length : ℕ∞)
Tag 00LK, a lemma

Tag 00LK in the Stacks Project.

Module.depth_le_supportDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/Dimension.lean, line 264. References: EGA 0 (16.4.5), “(16.4.5.1)”.

Depth is at most the dimension of the support. If M is a finite R-module and I is an ideal of R with I • M ≠ M, then depth_I(M) ≤ dim(Supp(M)). For R Noetherian local, I the maximal ideal and M nonzero, this is depth(M) ≤ dim(Supp(M)).

public theorem depth_le_supportDim (R : Type*) [CommRing R] (I : Ideal R) (M : Type*)
    [AddCommGroup M] [Module R M] [Module.Finite R M] (hI : I • (⊤ : Submodule R M) ≠ ⊤) :
    (depth R I M : WithBot ℕ∞) ≤ supportDim R M
Tag 0AUJ, a lemma

Tag 0AUJ in the Stacks Project.

Module.depth_lt_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/Dimension.lean, line 470.

Depth along an ideal is finite over a Noetherian ring. If R is Noetherian, M is a finite R-module and I is an ideal of R with I • M ≠ M, then depth_I(M) < ∞; that is, the lengths of the M-regular sequences contained in I are bounded. The hypothesis I • M ≠ M also forces M ≠ 0.

public theorem depth_lt_top (R : Type*) [CommRing R] [IsNoetherianRing R] (I : Ideal R)
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (hI : I • (⊤ : Submodule R M) ≠ ⊤) :
    depth R I M < ⊤
Tag 00LW, a lemma

Tag 00LW in the Stacks Project.

depth_eq_least_nonzero_ext, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/Ext.lean, line 1002. References: EGA 0 (16.4.4), “depth = least n Ext≠0”; EGA 0 (16.4.5), “partial”; SGA 2 III (2.8), “local case”; SGA 2 III (3.4), “(1) <=> (3)”; SGA 2 III (2.4), “(3)⇔(4)”; SGA 2 III (2.7), “special case”; SGA 2 III (3.3), “special case”.

Stacks Tag 00LW (Lemma 10.72.5). Let R be a Noetherian local ring with maximal ideal 𝔪, residue field κ = R/𝔪, and let M be a nonzero finite R-module. Then there is a least index n for which Ext^n_R(κ, M) is nonzero, and the depth of M equals this index n: depth(M) = min { i | Ext^i_R(κ, M) ≠ 0 }.

theorem depth_eq_least_nonzero_ext {R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    {M : Type u} [AddCommGroup M] [Module R M] [Module.Finite R M] (hM : Nontrivial M) :
    ∃ n : ℕ,
      IsLeast
          {i : ℕ |
            Nontrivial
              (Ext (ModuleCat.of R (R ⧸ IsLocalRing.maximalIdeal R)) (ModuleCat.of R M) i)}
          n ∧
        Module.depthSup R (IsLocalRing.maximalIdeal R) M = (n : ℕ∞)
Tag 00LX, a lemma

Tag 00LX in the Stacks Project.

Module.min_depth_le_depth_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/ShortExact.lean, line 279.

Depth in a short exact sequence. Let R be a Noetherian ring, I ⊆ R an ideal, and let 0 → N' → N → N'' → 0 be a short exact sequence of finite R-modules, given by f : N' →ₗ[R] N injective, g : N →ₗ[R] N'' surjective and Function.Exact f g. Then

  1. min {depth_I(N'), depth_I(N'')} ≤ depth_I(N),
  2. min {depth_I(N), depth_I(N') - 1} ≤ depth_I(N''),
  3. min {depth_I(N), depth_I(N'') + 1} ≤ depth_I(N'),

the subtraction being the truncated one of ℕ∞.

public theorem min_depth_le_depth_of_exact {R : Type*} [CommRing R] [IsNoetherianRing R]
    (I : Ideal R) {N' N N'' : Type*} [AddCommGroup N'] [Module R N'] [AddCommGroup N]
    [Module R N] [AddCommGroup N''] [Module R N''] [Module.Finite R N] {f : N' →ₗ[R] N}
    {g : N →ₗ[R] N''} (h : Function.Exact f g) (hf : Function.Injective f)
    (hg : Function.Surjective g) :
    min (depth R I N') (depth R I N'') ≤ depth R I N ∧
      min (depth R I N) (depth R I N' - 1) ≤ depth R I N'' ∧
      min (depth R I N) (depth R I N'' + 1) ≤ depth R I N'
Tag 090R, a lemma

Tag 090R in the Stacks Project.

Module.depth_quotSMulTop_succ_eq_depth_and_exists_isRegular_append, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/Criteria.lean, line 612. The attribute's comment: “Stated for an arbitrary ideal of a Noetherian ring; M nonzero is used only as I • M ≠ M, and only by part (2), so both parameters are bound inside the conclusion.”. References: SGA 2 III (2.6).

Depth drops by one modulo a nonzerodivisor, and regular sequences extend to length equal to the depth. Let R be a Noetherian ring, I ⊆ R an ideal and M a finite R-module.

  1. If x ∈ I is a nonzerodivisor on M, then depth_I(M/xM) + 1 = depth_I(M).
  2. If I • M ≠ M, then every M-regular sequence rs with all terms in I extends to an M-regular sequence rs ++ ss with all terms in I and (rs ++ ss).length = depth_I(M).

The source states this for I the maximal ideal of a Noetherian local ring and M nonzero, and writes (1) as depth(M/xM) = depth(M) - 1; the equality with + 1 on the left is the sharper form in ℕ∞, where subtraction is truncated.

public theorem depth_quotSMulTop_succ_eq_depth_and_exists_isRegular_append {R : Type*}
    [CommRing R] [IsNoetherianRing R] (I : Ideal R) (M : Type*) [AddCommGroup M] [Module R M]
    [Module.Finite R M] :
    (∀ x ∈ I, IsSMulRegular M x → depth R I (QuotSMulTop x M) + 1 = depth R I M) ∧
      (I • (⊤ : Submodule R M) ≠ ⊤ → ∀ rs : List R, (∀ r ∈ rs, r ∈ I) →
        RingTheory.Sequence.IsRegular M rs →
          ∃ ss : List R, (∀ s ∈ ss, s ∈ I) ∧ RingTheory.Sequence.IsRegular M (rs ++ ss) ∧
            ((rs ++ ss).length : ℕ∞) = depth R I M)
Tag 0CN5, a lemma

Tag 0CN5 in the Stacks Project.

exists_mem_associatedPrimes_quotSMulTop_pow_of_mem_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/MinimalPrimes.lean, line 221. The attribute's comment: “Stated over an arbitrary Noetherian ring for an arbitrary x: the source's locality is unused, and x ∈ 𝔪 is implied to the extent it matters by 𝔮 being a minimal prime over 𝔭 + (x).”.

A minimal prime over 𝔭 + (x) is an associated prime of M/xⁿM. Let R be a Noetherian ring, M a finite R-module and x ∈ R. If 𝔭 is an associated prime of M and 𝔮 is a minimal prime over 𝔭 + (x), then 𝔮 is an associated prime of M/xⁿM for some n ≥ 1.

The source states this for x in the maximal ideal of a Noetherian local ring; neither restriction is used, and x ∉ 𝔪 makes 𝔭 + (x) = ⊤, which has no minimal primes.

public theorem exists_mem_associatedPrimes_quotSMulTop_pow_of_mem_minimalPrimes {R : Type*}
    [CommRing R] [IsNoetherianRing R] {M : Type*} [AddCommGroup M] [Module R M]
    [Module.Finite R M] (x : R) {p q : Ideal R} (hp : p ∈ associatedPrimes R M)
    (hq : q ∈ (p + Ideal.span {x}).minimalPrimes) :
    ∃ n : ℕ, 0 < n ∧ q ∈ associatedPrimes R (QuotSMulTop (x ^ n) M)
Tag 0BK4, a lemma

Tag 0BK4 in the Stacks Project.

Module.depth_le_ringKrullDim_quotient_of_mem_associatedPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/Criteria.lean, line 865. References: EGA 0 (16.4.6), “(iii), first inequality”.

Stacks 0BK4. Let (R, 𝔪) be a Noetherian local ring and M a finite R-module. If 𝔭 is an associated prime of M, then depth(M) ≤ dim(R/𝔭), the depth being taken along 𝔪.

The source states this as dim(R/𝔭) ≥ depth(M).

public theorem depth_le_ringKrullDim_quotient_of_mem_associatedPrimes {R : Type*} [CommRing R]
    [IsNoetherianRing R] [IsLocalRing R] {M : Type*} [AddCommGroup M] [Module R M]
    [Module.Finite R M] {p : Ideal R} (hp : p ∈ associatedPrimes R M) :
    (depth R (IsLocalRing.maximalIdeal R) M : WithBot ℕ∞) ≤ ringKrullDim (R ⧸ p)
Tag 0FCC, a lemma

Tag 0FCC in the Stacks Project.

Module.depth_le_depth_localized_add_ringKrullDim_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/Localization.lean, line 702. The attribute's comment: “Stated in WithBot ℕ∞ with the smaller side on the left, for Module.depth (Tag 00LI) along the maximal ideals of R and of Rₚ, and with the localizations presented by IsLocalization.AtPrime and IsLocalizedModule. See the module docstring.”.

Depth drops by at most dim(R/𝔭) under localization. Let (R, 𝔪) be a Noetherian local ring, M a finite R-module and 𝔭 ⊆ R a prime ideal. Then depth_𝔪(M) ≤ depth_{𝔭R_𝔭}(M_𝔭) + dim(R/𝔭). The localization is presented abstractly: Rₚ is any localization of R at 𝔭 and f : M →ₗ[R] Mₚ any localization of M at 𝔭. The inequality is read in WithBot ℕ∞, where ringKrullDim lives.

public theorem depth_le_depth_localized_add_ringKrullDim_quotient {R : Type*} [CommRing R]
    [IsNoetherianRing R] [IsLocalRing R] (M : Type*) [AddCommGroup M] [Module R M]
    [Module.Finite R M] (p : Ideal R) [p.IsPrime] (Rₚ : Type*) [CommRing Rₚ] [Algebra R Rₚ]
    [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] (Mₚ : Type*) [AddCommGroup 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 ℕ∞) ≤
      (depth Rₚ (IsLocalRing.maximalIdeal Rₚ) Mₚ : WithBot ℕ∞) + ringKrullDim (R ⧸ p)
Tag 0AUK, a lemma

Tag 0AUK in the Stacks Project.

Module.depth_eq_iInf_depth_isLocalized_maximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/Localization.lean, line 438. References: EGA 0 (16.4.8), “B finite over A”; SGA 2 III (2.10), “S finite over local R”.

Depth is the minimum of the depths of the localizations at the maximal ideals. Let (R, 𝔪) be a Noetherian local ring, let R → S be a finite ring map and let N be a finite S-module. Then the depth of N as an R-module along 𝔪 is the infimum, over the maximal ideals 𝔪ᵢ of S, of the depths of the localizations N_{𝔪ᵢ} over the local rings S_{𝔪ᵢ}. Since S is semilocal the infimum is a minimum over a finite nonempty set, unless S is the zero ring, in which case both sides are ⊤.

public theorem depth_eq_iInf_depth_isLocalized_maximal
    {R S : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [CommRing S] [Algebra R S]
    [Module.Finite R S] {N : Type*} [AddCommGroup N] [Module S N] [Module.Finite S N]
    [Module R N] [IsScalarTower R S N]
    (Sₘ : MaximalSpectrum S → Type*) [∀ P, CommRing (Sₘ P)] [∀ P, Algebra S (Sₘ P)]
    [∀ P, IsLocalization.AtPrime (Sₘ P) P.asIdeal]
    (Nₘ : MaximalSpectrum S → Type*) [∀ P, AddCommGroup (Nₘ P)] [∀ P, Module S (Nₘ P)]
    [∀ P, Module (Sₘ P) (Nₘ P)] [∀ P, IsScalarTower S (Sₘ P) (Nₘ P)]
    (f : ∀ P, N →ₗ[S] Nₘ P) [∀ P, IsLocalizedModule P.asIdeal.primeCompl (f P)] :
    depth R (IsLocalRing.maximalIdeal R) N =
      ⨅ P : MaximalSpectrum S,
        haveI : IsLocalRing (Sₘ P) := IsLocalization.AtPrime.isLocalRing (Sₘ P) P.asIdeal
        depth (Sₘ P) (IsLocalRing.maximalIdeal (Sₘ P)) (Nₘ P)
Sources
LeanModule.depth · Module.depth_eq_iSup_isWeaklyRegular_length · Module.depth_le_supportDim · Module.depth_lt_top · depth_eq_least_nonzero_ext · Module.min_depth_le_depth_of_exact · Module.depth_quotSMulTop_succ_eq_depth_and_exists_isRegular_append · exists_mem_associatedPrimes_quotSMulTop_pow_of_mem_minimalPrimes

Section10.73 Functorialities for Ext#

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

Tag 087N, a lemma

Tag 087N in the Stacks Project.

flat_base_change_ext, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ext/BaseChange.lean, line 203.

Flat base change for Ext. For a flat ring map f : R → R', an R-module M, an R'-module N', and each i ≥ 0, the comparison map c^i of extFlatBaseChangeComparison is an isomorphism of abelian groups (here phrased as bijectivity of the underlying group homomorphism).

theorem flat_base_change_ext {R R' : Type} [CommRing R] [CommRing R']
    (f : R →+* R') (hf : f.Flat) (M : ModuleCat.{0} R) (N' : ModuleCat.{0} R') (i : ℕ) :
    Function.Bijective (extFlatBaseChangeComparison f M N' i)
Sources
Leanflat_base_change_ext

Section10.74 An application of Ext groups#

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

Tag 02HO, a lemma

Tag 02HO in the Stacks Project.

split_injection_of_arbitrarily_large_split_mod_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/SplitInjection.lean, line 439. References: EGA 0 (19.1.8), “partial”.

Theorem (Stacks Tag 02HO, Lemma 10.74.1). Let R be a Noetherian commutative ring, I ⊆ R an ideal contained in the Jacobson radical of R, and N, M finite R-modules. Let φ : N → M be R-linear. If for arbitrarily large n the induced map φ̄ₙ : N / Iⁿ N → M / Iⁿ M is a split injection, then φ itself is a split injection.

theorem split_injection_of_arbitrarily_large_split_mod_pow
    {R N M : Type*} [CommRing R] [IsNoetherianRing R]
    [AddCommGroup N] [Module R N] [Module.Finite R N]
    [AddCommGroup M] [Module R M] [Module.Finite R M]
    (I : Ideal R) (hI : I ≤ Ideal.jacobson ⊥) (φ : N →ₗ[R] M)
    (h : ForArbitrarilyLarge (fun n => IsSplitInjection (inducedMapModPow φ I n))) :
    IsSplitInjection φ
Sources
Leansplit_injection_of_arbitrarily_large_split_mod_pow

Section10.75 Tor groups and flatness#

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

Tag 00LZ, a lemma

Tag 00LZ in the Stacks Project.

torMap_independent_of_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/Finiteness.lean, line 442.

The induced map on homology is independent of the choice of the lift: two chain maps α, β : F.complex ⟶ G.complex both lifting φ : M₁ ⟶ M₂ induce equal maps H_i(F ⊗ N) ⟶ H_i(G ⊗ N).

theorem torMap_independent_of_lift {R : Type} [CommRing R] {M₁ M₂ : ModuleCat R}
    (F : FreeResolution M₁) (G : FreeResolution M₂) (N : ModuleCat R) {φ : M₁ ⟶ M₂}
    (α β : F.complex ⟶ G.complex) (hα : IsLift F G φ α) (hβ : IsLift F G φ β) (i : ℕ) :
    torMap F G N α i = torMap F G N β i
Tag 00M0, a lemma

Tag 00M0 in the Stacks Project.

CategoryTheory.ShortComplex.ShortExact.exists_Tor'_one_composableArrows_exact_and_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/Vanishing.lean, line 210.

Let R be a commutative ring, let M be an R-module and let S : 0 → N' → N → N'' → 0 be a short exact sequence of R-modules. Then there is a connecting homomorphism δ : Tor₁(M, N'') ⟶ M ⊗ N' making

Tor₁(M, N') → Tor₁(M, N) → Tor₁(M, N'') →δ M ⊗ N' → M ⊗ N → M ⊗ N''

exact, and M ⊗ N → M ⊗ N'' is surjective. Here Tor₁(M, -) is (Tor' (ModuleCat R) 1).obj M, the first left derived functor of - ⊗ N evaluated at M, and the maps other than δ are the functorial ones.

public theorem exists_Tor'_one_composableArrows_exact_and_epi {R : Type u} [CommRing R]
    {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact) (M : ModuleCat.{u} R) :
    (∃ δ : ((Tor' (ModuleCat.{u} R) 1).obj M).obj S.X₃ ⟶ M ⊗ S.X₁,
        (ComposableArrows.mk₅ (((Tor' (ModuleCat.{u} R) 1).obj M).map S.f)
          (((Tor' (ModuleCat.{u} R) 1).obj M).map S.g) δ (M ◁ S.f) (M ◁ S.g)).Exact) ∧
      Epi (M ◁ S.g)
Tag 00M1, a lemma

Tag 00M1 in the Stacks Project.

Stacks.Tor.DoubleComplex.statement1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/Balancing/CanonicalIso.lean, line 408. The attribute's comment: “(1)”.

For a double complex A whose rows are resolutions of the horizontal cokernels and whose columns are resolutions of the vertical cokernels, there is an isomorphism of R-modules H_i(R(A)_•) ≅ H_i(U(A)_•) for every i ≥ 0.

theorem statement1 (A : DoubleCx R) (hrow : A.RowResolution) (hcol : A.ColResolution)
    (i : ℕ) : Nonempty (A.RHom i ≃ₗ[R] A.UHom i)

Stacks.Tor.DoubleComplex.statement2, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/Balancing/CanonicalIso.lean, line 417. The attribute's comment: “(2)”.

The isomorphisms H_i(R(A)_•) ≅ H_i(U(A)_•) can be chosen naturally in A: there is an assignment, to every double complex A satisfying the resolution hypotheses and every i, of an isomorphism e A : H_i(R(A)_•) ≅ H_i(U(A)_•), such that H_i(U(Ψ)) ∘ e A = e B ∘ H_i(R(Ψ)) for every morphism Ψ : A → B of such double complexes.

theorem statement2 :
    ∃ e : ∀ (A : DoubleCx R), A.RowResolution → A.ColResolution → ∀ i,
        (A.RHom i ≃ₗ[R] A.UHom i),
      ∀ (A B : DoubleCx R) (hrowA : A.RowResolution) (hcolA : A.ColResolution)
        (hrowB : B.RowResolution) (hcolB : B.ColResolution)
        (Ψ : DCxHom A B) (i : ℕ),
        (Ψ.UHomMap i).comp (e A hrowA hcolA i : A.RHom i →ₗ[R] A.UHom i) =
          ((e B hrowB hcolB i : B.RHom i →ₗ[R] B.UHom i)).comp (Ψ.RHomMap i)
Tag 00M3, a lemma

Tag 00M3 in the Stacks Project.

tor_symm_canonically_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/Balancing/Naturality.lean, line 740. References: EGA III (6.3.5), “(i), special case”; EGA III (6.5.5), “S = X = Y = Spec R”; EGA III (6.7.13), “special case”.

For every i ≥ 0 the two functors (M, N) ↦ Tor_i^R(M, N) and (M, N) ↦ Tor_i^R(N, M) are canonically isomorphic: there is a natural isomorphism between the bifunctor Tor (ModuleCat R) i and the swap bifunctor (Tor (ModuleCat R) i).flip in the functor category ModuleCat R ⥤ ModuleCat R ⥤ ModuleCat R.

theorem tor_symm_canonically_iso (i : ℕ) :
    Nonempty (Tor (ModuleCat.{u} R) i ≅ (Tor (ModuleCat.{u} R) i).flip)
Tag 00M4, a remark

Tag 00M4 in the Stacks Project.

swap_eigenspace_dim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/TensorProduct/Swap.lean, line 394.

Eigenspace dimensions in characteristic ≠ 2. Assume char k ≠ 2 and dim_k V = n. Then the +1-eigenspace of the swap map has dimension (n^2 + n)/2 and the -1-eigenspace has dimension (n^2 - n)/2.

Argument: the -1-eigenspace has dimension (n^2 − n)/2 by swap_finrank_antisymm. Since E₊₁ and E₋₁ are complementary (swap_isCompl_eigenspaces), their dimensions add to finrank (V ⊗ V) = n * n = n^2 (Submodule.finrank_add_eq_of_isCompl and Module.finrank_tensorProduct). The remaining +1-dimension is then n^2 − (n^2 − n)/2 = (n^2 + n)/2, a nat-arithmetic identity (both n^2 ± n are even).

theorem swap_eigenspace_dim
    (hk : (2 : k) ≠ 0) (n : ℕ) (hn : Module.finrank k V = n) :
    Module.finrank k (swapEigenspace k V (1 : k)) = (n ^ 2 + n) / 2 ∧
    Module.finrank k (swapEigenspace k V (-1 : k)) = (n ^ 2 - n) / 2

swap_not_isDiagonalizable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/TensorProduct/Swap.lean, line 483.

Non-diagonalizability in characteristic 2. Assume char k = 2 and dim_k V ≥ 2. Then the swap map is not diagonalizable.

Argument: if σ were diagonalizable then ⨆ λ, eigenspace λ = ⊤. But in characteristic 2 every eigenspace is contained in eigenspace 1 (swap_eigenspace_le_one_char2), so ⨆ λ, eigenspace λ ≤ eigenspace 1, whence eigenspace 1 = ⊤, i.e. σ x = x for all x. This contradicts swap_ne_id, which produces a tensor moved by σ.

theorem swap_not_isDiagonalizable
    (hk : (2 : k) = 0) (hn : 2 ≤ Module.finrank k V) :
    ¬ IsDiagonalizable (swapMap k V)
Tag 0AZ4, a lemma

Tag 0AZ4 in the Stacks Project.

tor_finite_of_noetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/Finiteness.lean, line 317. References: EGA III (6.5.13), “special case”; EGA III (6.7.9), “special case”; EGA III (7.4.7), “(i), special case”.

Let R be a Noetherian ring and let M, N be finite R-modules. Then Tor_p^R(M, N) is a finite R-module for every p.

theorem tor_finite_of_noetherian (R : Type u) [CommRing R] [IsNoetherianRing R]
    (M N : ModuleCat.{u} R) [Module.Finite R M] [Module.Finite R N] (p : ℕ) :
    Module.Finite R (((Tor (ModuleCat.{u} R) p).obj M).obj N)
Tag 00M5, a lemma

Tag 00M5 in the Stacks Project.

Module.Flat.tfae_isZero_Tor', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/Flatness.lean, line 192. References: EGA 0 (6.1.1).

Let R be a commutative ring and let M be an R-module. The following are equivalent: (1) M is flat over R; (2) for all i > 0 the functor Tor_i(M, -) is zero; (3) the functor Tor₁(M, -) is zero; (4) Tor₁(M, R/I) = 0 for all ideals I ⊆ R; (5) Tor₁(M, R/I) = 0 for all finitely generated ideals I ⊆ R. Here Tor_i(M, -) is (Tor' (ModuleCat R) i).obj M, the i-th left derived functor of - ⊗ N evaluated at M.

public theorem tfae_isZero_Tor' {R : Type u} [CommRing R] (M : ModuleCat.{u} R) :
    List.TFAE
      [Module.Flat R M,
        ∀ i, 0 < i → IsZero ((Tor' (ModuleCat.{u} R) i).obj M),
        IsZero ((Tor' (ModuleCat.{u} R) 1).obj M),
        ∀ I : Ideal R,
          IsZero (((Tor' (ModuleCat.{u} R) 1).obj M).obj (ModuleCat.of R (R ⧸ I))),
        ∀ I : Ideal R, I.FG →
          IsZero (((Tor' (ModuleCat.{u} R) 1).obj M).obj (ModuleCat.of R (R ⧸ I)))]
Sources
LeantorMap_independent_of_lift · CategoryTheory.ShortComplex.ShortExact.exists_Tor'_one_composableArrows_exact_and_epi · Stacks.Tor.DoubleComplex.statement1 · Stacks.Tor.DoubleComplex.statement2 · tor_symm_canonically_iso · swap_eigenspace_dim · swap_not_isDiagonalizable · tor_finite_of_noetherian

Section10.76 Functorialities for Tor#

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

Tag 00M8, a lemma

Tag 00M8 in the Stacks Project.

flat_base_change_tor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/BaseChange.lean, line 172.

Flat base change for Tor. Let R → R' be a flat ring map of commutative rings and let M, N be R-modules. Then for every i the base-change map (torBaseChangeIso i M N).hom : Tor_i^R(M, N) ⊗_R R' ⟶ Tor_i^{R'}(M ⊗_R R', N ⊗_R R') is an isomorphism of R'-modules.

theorem flat_base_change_tor [Module.Flat R R'] (i : ℕ) (M N : ModuleCat.{0} R) :
    IsIso (torBaseChangeIso (R' := R') i M N).hom

flat_base_change_tor_of_universe, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/BaseChangeOfUniverse.lean, line 132.

Flat base change for Tor (Stacks Tag 00M8), for rings in an arbitrary universe.

Let S -> S' be a flat ring map of commutative rings (encoded as an S-algebra S' with Module.Flat S S'), and let M, N be S-modules. Then for every i the canonical base-change map Tor_i^S(M, N) (x)_S S' -> Tor_i^{S'}(M (x)_S S', N (x)_S S') — the underlying morphism (torBaseChangeIsoOfUniverse i M N).hom of the comparison — is an isomorphism of S'-modules.

theorem flat_base_change_tor_of_universe [Module.Flat S S'] (i : ℕ) (M N : ModuleCat.{u} S) :
    IsIso (torBaseChangeIsoOfUniverse (S' := S') i M N).hom
Tag 0BNF, a lemma

Tag 0BNF in the Stacks Project.

tor_commutes_filtered_colimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/BaseChange.lean, line 438. References: EGA III (6.3.12), “special case”; EGA III (6.3.6), “special case”; EGA III (6.5.6), “special case”.

Tor commutes with filtered colimits. Applying Tor_n^R(-, N) to the direct-limit colimit cocone of a directed system (G i) of R-modules yields again a colimit cocone, i.e. the canonical map colim_i Tor_n^R(G i, N) → Tor_n^R(colim_i G i, N) is an isomorphism.

The ring R : Type u, the index type ι : Type v, the modules G : ι → Type w and the second argument N : ModuleCat.{x} R live in four independent universes, and the conclusion is stated about their canonical ULifts into max u v w x.

theorem tor_commutes_filtered_colimits
    {R : Type u} [CommRing R]
    {ι : Type v} [DecidableEq ι] [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (G : ι → Type w) [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
    (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
    [DirectedSystem G (fun i j h => f i j h)]
    (N : ModuleCat.{x} R) (n : ℕ) :
    Nonempty (CategoryTheory.Limits.IsColimit
      (((CategoryTheory.Tor (ModuleCat.{max u v w x} (ULift.{max v w x, u} R)) n).flip.obj
            (ModuleCat.of (ULift.{max v w x, u} R) (ULift.{max u v w, x} N))).mapCocone
        (ModuleCat.directLimitCocone
          (fun i : ULift.{max u w x, v} ι => ULift.{max u v x, w} (G i.down))
          (torULiftTransition.{u, v, w, x} G f))))
Sources
Leanflat_base_change_tor · flat_base_change_tor_of_universe · tor_commutes_filtered_colimits

Section10.77 Projective modules#

Section 10.77 of the Stacks Project, Tag 05CD. 8 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05CE, a definition

Tag 05CE in the Stacks Project.

Module.projective_iff_homLeft_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/HomExact.lean, line 65. The attribute's comment: “elementwise form, any ring”.

An R-module P is projective if and only if Hom_R(P, -) carries every short exact sequence 0 → N₁ → N₂ → N₃ → 0 to a short exact sequence 0 → Hom(P, N₁) → Hom(P, N₂) → Hom(P, N₃) → 0.

theorem projective_iff_homLeft_shortExact :
    Module.Projective R P ↔ ∀ (N₁ N₂ N₃ : Type (max u v)) [AddCommGroup N₁] [Module R N₁]
      [AddCommGroup N₂] [Module R N₂] [AddCommGroup N₃] [Module R N₃]
      (f : N₁ →ₗ[R] N₂) (g : N₂ →ₗ[R] N₃), Function.Injective f → Function.Exact f g →
        Function.Surjective g →
        Function.Injective (LinearMap.compRight (M := P) ℕ f) ∧
        Function.Exact (LinearMap.compRight (M := P) ℕ f) (LinearMap.compRight (M := P) ℕ g) ∧
        Function.Surjective (LinearMap.compRight (M := P) ℕ g)

Module.projective_iff_shortExact_map_linearCoyoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/HomExact.lean, line 91.

An R-module P is projective if and only if the functor Hom_R(P, -) : ModuleCat R ⥤ ModuleCat R sends short exact sequences to short exact sequences.

theorem projective_iff_shortExact_map_linearCoyoneda :
    Module.Projective R P ↔ ∀ S : ShortComplex (ModuleCat.{max u v} R), S.ShortExact →
      (S.map ((linearCoyoneda R (ModuleCat.{max u v} R)).obj
        (op (ModuleCat.of R P)))).ShortExact

Module.projective_iff_preservesFiniteLimits_and_preservesFiniteColimits_linearCoyoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/HomExact.lean, line 121. The attribute's comment: “exact functor as preserving finite limits and finite colimits”.

An R-module P is projective if and only if the functor Hom_R(P, -) : ModuleCat R ⥤ ModuleCat R is exact, in the sense that it preserves finite limits and finite colimits.

theorem projective_iff_preservesFiniteLimits_and_preservesFiniteColimits_linearCoyoneda :
    Module.Projective R P ↔
      PreservesFiniteLimits ((linearCoyoneda R (ModuleCat.{max u v} R)).obj
        (op (ModuleCat.of R P))) ∧
      PreservesFiniteColimits ((linearCoyoneda R (ModuleCat.{max u v} R)).obj
        (op (ModuleCat.of R P)))
Tag 05CF, a lemma

Tag 05CF in the Stacks Project.

characterize_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/Characterization.lean, line 130. References: EGA 0 (17.2.1), “n = 0”; SGA 5 XV (3.Lemma3), “more general”.

Theorem (Stacks Tag 05CF). For an R-module P, the three conditions "P is projective (lifting property)", "P is a direct summand of a free module", and "Ext^1_R(P, M) = 0 for all M" are equivalent.

theorem characterize_projective (P : Type u) [AddCommGroup P] [Module R P] :
    List.TFAE
      [IsProjectiveLifting R P, IsDirectSummandOfFree R P, ExtOneVanishes R P]
Tag 0G8T, a lemma

Tag 0G8T in the Stacks Project.

projective_of_ext_one_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ext/Finiteness.lean, line 607. References: EGA 0 (17.2.1), “n = 0”; EGA 0 (17.2.8), “special case”.

Stacks tag 0G8T (Lemma 10.77.3): a finite module P over a Noetherian ring R is projective as soon as Ext¹_R(P, M) vanishes for every finite R-module M.

theorem projective_of_ext_one_eq_zero {R : Type} [CommRing R] [IsNoetherianRing R]
    (P : Type) [AddCommGroup P] [Module R P] [Module.Finite R P]
    (h : ∀ (M : Type) [AddCommGroup M] [Module R M] [Module.Finite R M],
      Subsingleton (Abelian.Ext (C := ModuleCat R) (ModuleCat.of R P) (ModuleCat.of R M) 1)) :
    Module.Projective R P
Tag 065Q, a lemma

Tag 065Q in the Stacks Project.

Declarations registered for the tag:

Tag 07LV, a lemma

Tag 07LV in the Stacks Project.

Module.exists_projective_quotient_smul_top_linearEquiv_of_isNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/Lifting.lean, line 376. References: SGA 5 XV (3.Lemma3), “(ii), existence”.

Stacks 07LV. Let R be a ring, let I ⊆ R be a nilpotent two-sided ideal and let Q be a projective R ⧸ I-module. Then there is a projective R-module P together with an isomorphism P/IP ≅ Q of R ⧸ I-modules.

public theorem Module.exists_projective_quotient_smul_top_linearEquiv_of_isNilpotent
    {R : Type u} [Ring R] {I : Ideal R} [I.IsTwoSided] {Q : Type v} [AddCommGroup Q]
    [Module (R ⧸ I) Q] [Module.Projective (R ⧸ I) Q] (hI : IsNilpotent I) :
    ∃ (P : Type (max u v)) (_ : AddCommGroup P) (_ : Module R P),
      Module.Projective R P ∧ Nonempty ((P ⧸ I • (⊤ : Submodule R P)) ≃ₗ[R ⧸ I] Q)
Tag 0D47, a lemma

Tag 0D47 in the Stacks Project.

lift_finite_projective_of_locallyNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/Lifting.lean, line 393. References: SGA 5 XV (3.Lemma3), “(ii) existence, finite”.

Stacks Tag 0D47 (Lemma 10.77.6). Let R be a commutative ring and I ⊆ R a locally nilpotent ideal. Let Pbar be a finite projective R/I-module. Then there exists a finite projective R-module P together with an isomorphism of R/I-modules P / I P ≅ Pbar.

theorem lift_finite_projective_of_locallyNilpotent
    {R : Type u} [CommRing R] (I : Ideal R)
    (hI : I.IsLocallyNilpotent)
    (Pbar : Type u) [AddCommGroup Pbar] [Module (R ⧸ I) Pbar]
    [Module.Finite (R ⧸ I) Pbar] [Module.Projective (R ⧸ I) Pbar] :
    ∃ (P : Type u) (_ : AddCommGroup P) (_ : Module R P),
      Module.Finite R P ∧ Module.Projective R P ∧
      Nonempty ((P ⧸ (I • (⊤ : Submodule R P))) ≃ₗ[R ⧸ I] Pbar)
Tag 05CG, a lemma

Tag 05CG in the Stacks Project.

Module.Flat.projective_of_isNilpotent_of_projective_quotient_smul_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/NilpotentIdeal.lean, line 193. References: SGA 5 XV (3.Lemma3), “(ii) flat ⇒ projective”.

Stacks 05CG. Let R be a ring, let I ⊆ R be a nilpotent ideal and let M be a flat R-module such that M/IM is a projective R ⧸ I-module. Then M is a projective R-module.

public theorem Module.Flat.projective_of_isNilpotent_of_projective_quotient_smul_top
    {R : Type u} [CommRing R] {I : Ideal R} {M : Type v} [AddCommGroup M] [Module R M]
    [Module.Flat R M] (hI : IsNilpotent I)
    (hM : Module.Projective (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M))) :
    Module.Projective R M
Tag 0H7M, a lemma

Tag 0H7M in the Stacks Project.

projective_of_projective_quotient_inter_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/Lifting.lean, line 943.

Stacks Tag 0H7M, Lemma 10.77.8: if \(I \cap J = 0\) and both \(P/IP\) (as an \(R/I\)-module) and \(P/JP\) (as an \(R/J\)-module) are projective, then \(P\) is a projective \(R\)-module.

theorem projective_of_projective_quotient_inter_zero
    (R : Type*) [CommRing R] (I J : Ideal R) (hIJ : I ⊓ J = ⊥)
    (P : Type*) [AddCommGroup P] [Module R P]
    (hI : Module.Projective (R ⧸ I) (P ⧸ (I • (⊤ : Submodule R P))))
    (hJ : Module.Projective (R ⧸ J) (P ⧸ (J • (⊤ : Submodule R P)))) :
    Module.Projective R P
Sources
LeanModule.projective_iff_homLeft_shortExact · Module.projective_iff_shortExact_map_linearCoyoneda · Module.projective_iff_preservesFiniteLimits_and_preservesFiniteColimits_linearCoyoneda · characterize_projective · projective_of_ext_one_eq_zero · Module.instProjectiveDFinsupp · Module.exists_projective_quotient_smul_top_linearEquiv_of_isNilpotent · lift_finite_projective_of_locallyNilpotent

Section10.78 Finite projective modules#

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

Tag 00NW, a definition

Tag 00NW in the Stacks Project.

Module.IsLocallyFree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/LocallyFree/SheafBridge.lean, line 116. The attribute's comment: “(1)”. References: EGA 0 (5.4.1), “affine case”; EGA II (6.5.1), “(I)”; EGA III (7.9.1); EGA IV (21.5.3), “special case”; SGA 3 XV (2.10).

M is a locally free R-module: there is a family f : ι → R whose basic opens cover Spec R (equivalently, generate the unit ideal) and such that each localization M_{f i} is a free R_{f i}-module.

def Module.IsLocallyFree (R : Type u) [CommRing R] (M : Type u)
    [AddCommGroup M] [Module R M] : Prop

Module.IsFiniteLocallyFree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/LocallyFree/SheafBridge.lean, line 132. The attribute's comment: “(2)”. References: EGA 0 (5.4.1), “affine case”; EGA II (6.5.1), “(I), special case”; EGA III (7.9.1); EGA IV (18.2.7), “partial”; EGA IV (21.5.3), “special case”; SGA 1 VIII (7.6), “affine module condition”; SGA 6 IV (2.1), “special case”.

M is a finite locally free R-module: as above, but each localization M_{f i} is in addition finitely generated (hence finite free) over R_{f i}.

def Module.IsFiniteLocallyFree (R : Type u) [CommRing R] (M : Type u)
    [AddCommGroup M] [Module R M] : Prop

Module.IsFiniteLocallyFreeOfRank, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/LocallyFree/SheafBridge.lean, line 167. The attribute's comment: “(3)”. References: EGA 0 (5.4.1), “affine case, rank n”; EGA II (6.5.1), “(I), special case”; EGA IV (18.2.7), “partial”; SGA 4½ Arcata (1.4.2); SGA 6 X (6.1), “partial”.

M is finite locally free of rank r: there is a covering family f : ι → R of Spec R such that each localization M_{f i} is free of rank r over R_{f i}, i.e. has a basis indexed by Fin r.

def Module.IsFiniteLocallyFreeOfRank (R : Type u) [CommRing R] (M : Type v)
    [AddCommGroup M] [Module R M] (r : ℕ) : Prop
Tag 00NX, a lemma

Tag 00NX in the Stacks Project.

Module.finite_projective_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/LocallyFree/FiniteProjective.lean, line 362. References: EGA III (7.3.4), “(1) => (8)”; EGA IV (2.1.12), “affine, flat everywhere”; EGA III (7.9.1); SGA 6 I (1.3.1), “affine case; (i)⇔(iii)”; SGA 6 I (2.15.1), “affine case, (3)⇒(7)”; SGA 6 I (5.8.3), “commutative ring case”; SGA 6 I (6.0), “special case”.

Characterizations of finite projective modules. For a module M over a commutative ring R the following are equivalent: (1) M is finitely presented and flat; (2) M is finite projective; (3) M is a direct summand of a finite free module; (4) M is finitely presented and free at every prime; (5) M is finitely presented and free at every maximal ideal; (6) M is finite and locally free; (7) M is finite locally free; (8) M is finite, free at every prime, and its rank function ρ_M = Module.rankAtStalk M is locally constant on Spec(R).

public theorem Module.finite_projective_tfae (R : Type u) [CommRing R] (M : Type v)
    [AddCommGroup M] [Module R M] :
    List.TFAE
      [Module.FinitePresentation R M ∧ Module.Flat R M,
       Module.Finite R M ∧ Module.Projective R M,
       ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M) (g : M →ₗ[R] (Fin n → R)), f ∘ₗ g = LinearMap.id,
       Module.FinitePresentation R M ∧ Module.freeLocus R M = Set.univ,
       Module.FinitePresentation R M ∧ ∀ (𝔪 : Ideal R) (_ : 𝔪.IsMaximal),
         Module.Free (Localization.AtPrime 𝔪) (LocalizedModule 𝔪.primeCompl M),
       Module.Finite R M ∧ ∃ s : Set R, Ideal.span s = ⊤ ∧
         ∀ f ∈ s, Module.Free (Localization.Away f) (LocalizedModule.Away f M),
       ∃ s : Set R, Ideal.span s = ⊤ ∧ ∀ f ∈ s,
         Module.Free (Localization.Away f) (LocalizedModule.Away f M) ∧
           Module.Finite (Localization.Away f) (LocalizedModule.Away f M),
       Module.Finite R M ∧ Module.freeLocus R M = Set.univ ∧
         IsLocallyConstant (Module.rankAtStalk (R := R) M)]
Tag 0FWG, a lemma

Tag 0FWG in the Stacks Project.

Module.projective_iff_isLocallyConstant_finrank_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/LocallyConstantRank.lean, line 407. References: SGA 6 III (5.6), “affine, E = M in deg 0”; SGA 6 I (6.0), “special case”; SGA 6 III (5.4.1), “special case”.

A finite module over a reduced ring is projective iff its fibre dimension is locally constant. For R a reduced commutative ring and M a finite R-module, M is projective (equivalently, by Module.finite_projective_tfae, finite locally free) if and only if the function ρ_M : Spec(R) → ℕ, 𝔭 ↦ dim_{κ(𝔭)} M ⊗_R κ(𝔭), is locally constant. This is item (9) in the list of characterizations of finite projective modules.

public theorem Module.projective_iff_isLocallyConstant_finrank_fiber (R : Type u) [CommRing R]
    [IsReduced R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    Module.Projective R M ↔
      IsLocallyConstant fun p : PrimeSpectrum R ↦
        Module.finrank p.asIdeal.ResidueField (p.asIdeal.Fiber M)
Tag 00NY, a remark

Tag 00NY in the Stacks Project.

Stacks.FiniteFlatNotProjective.quotientModule_not_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/LocallyFree/Basic.lean, line 214.

M = R/I is not a projective R-module, although it is finite and flat.

theorem quotientModule_not_projective : ¬ Module.Projective SmoothFunReal QuotientModule
Tag 00O1, a lemma

Tag 00O1 in the Stacks Project.

finite_projective_iff_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/LocallyFree/Basic.lean, line 256. References: SGA 3 VIB (11.8.2), “special case”.

Stacks 00O1 (Lemma 10.78.6). Let R → S be a flat local homomorphism of local rings, and let M be a finite R-module. Then M is finite projective over R if and only if M ⊗_R S is finite projective over S.

theorem finite_projective_iff_baseChange {R : Type*} {S : Type*} {M : Type*}
    [CommRing R] [CommRing S] [Algebra R S]
    [AddCommGroup M] [Module R M]
    [IsLocalRing R] [IsLocalRing S]
    [IsLocalHom (algebraMap R S)]
    [Module.Flat R S]
    [Module.Finite R M] :
    (Module.Finite R M ∧ Module.Projective R M) ↔
      (Module.Finite S (S ⊗[R] M) ∧ Module.Projective S (S ⊗[R] M))
Tag 02M9, a lemma

Tag 02M9 in the Stacks Project.

Module.free_of_flat_of_preconnectedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalRing/Module.lean, line 232. The attribute's comment: “The second assertion; the first, for a module of constant rank, is Mathlib's Module.free_of_flat_of_finrank_eq.”. References: EGA IV (11.3.12), “more general”; EGA IV (15.2.4), “Freeness clause”.

A finite locally free module over a semi-local ring with connected spectrum is free. Let R be a semi-local ring, so with finitely many maximal ideals, whose spectrum is (pre)connected, and let M be a finite locally free R-module, spelled here as finitely presented and flat. Then M is free. The rank of M is a locally constant function on Spec(R), hence constant, and a finite locally free module of constant rank over a semi-local ring is free (Module.free_of_flat_of_finrank_eq).

public theorem Module.free_of_flat_of_preconnectedSpace (R : Type u) [CommRing R]
    [Finite (MaximalSpectrum R)] [PreconnectedSpace (PrimeSpectrum R)] (M : Type v)
    [AddCommGroup M] [Module R M] [Module.FinitePresentation R M] [Module.Flat R M] :
    Module.Free R M
Tag 03C1, a lemma

Tag 03C1 in the Stacks Project.

contains_sBasis_of_generates, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Free/Basis.lean, line 612. References: SGA 3 V (4.2).

Let R be a local ring with maximal ideal m and infinite residue field. Let R → S be a ring map, M an S-module, and N ⊆ M an R-submodule. If S is semi-local with m S ⊆ Jac(S), M is finite free over S, and N generates M as an S-module, then N contains an S-basis of M.

theorem contains_sBasis_of_generates
    {R S M : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [AddCommGroup M] [Module S M] [Module R M] [IsScalarTower R S M]
    [IsLocalRing R] [Infinite (IsLocalRing.ResidueField R)]
    (hSsemilocal : Finite (MaximalSpectrum S))
    (hmS : Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) ≤ Ring.jacobson S)
    [Module.Free S M] [Module.Finite S M]
    (N : Submodule R M)
    (hN : GeneratesAsSModule S N) :
    ContainsSBasis S N
Tag 0DVB, a lemma

Tag 0DVB in the Stacks Project.

Declarations registered for the tag:

Sources
LeanModule.IsLocallyFree · Module.IsFiniteLocallyFree · Module.IsFiniteLocallyFreeOfRank · Module.finite_projective_tfae · Module.projective_iff_isLocallyConstant_finrank_fiber · Stacks.FiniteFlatNotProjective.quotientModule_not_projective · finite_projective_iff_baseChange · Module.free_of_flat_of_preconnectedSpace

Section10.79 Open loci defined by module maps#

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

Tag 05GE, a lemma

Tag 05GE in the Stacks Project.

LinearMap.setOf_localizedMap_atPrime_surjective_eq_setOf_baseChange_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/SurjectivityLocus.lean, line 122. The attribute's comment: “the equality of the two loci in the displayed formula”.

Let R be a ring and let φ : M →ₗ[R] N be a map of R-modules whose cokernel N ⧸ φ.range is a finite R-module. Then the set of primes p of R such that the localized map φ_p : M_p → N_p is surjective is the set of primes p such that the fibre map φ ⊗ κ(p) : M ⊗_R κ(p) → N ⊗_R κ(p) is surjective.

public theorem LinearMap.setOf_localizedMap_atPrime_surjective_eq_setOf_baseChange_surjective
    {R M N : Type*} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    (φ : M →ₗ[R] N) [Module.Finite R (N ⧸ φ.range)] :
    {p : PrimeSpectrum R | Function.Surjective (LocalizedModule.map p.asIdeal.primeCompl φ)} =
      {p | Function.Surjective (φ.baseChange p.asIdeal.ResidueField)}
Tag 05GF, a lemma

Tag 05GF in the Stacks Project.

LinearMap.isOpen_setOf_localizedMap_atPrime_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/FinitePresentation/Locus.lean, line 102.

Let R be a ring and let φ : M →ₗ[R] N be a map of R-modules with M a finite R-module and N a finitely presented R-module. Then the set of primes p of R such that the localized map φ_p : M_p → N_p is an isomorphism is an open subset of Spec(R).

public theorem LinearMap.isOpen_setOf_localizedMap_atPrime_bijective
    {R M N : Type*} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    (φ : M →ₗ[R] N) [Module.Finite R M] [Module.FinitePresentation R N] :
    IsOpen {p : PrimeSpectrum R |
      Function.Bijective (LocalizedModule.map p.asIdeal.primeCompl φ)}
Tag 0GWM, a lemma

Tag 0GWM in the Stacks Project.

Declarations registered for the tag:

Tag 00O0, a lemma

Tag 00O0 in the Stacks Project.

Stacks.FiniteProjective.MapLocus.isOpen_injLocus_and_localized, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/Locus.lean, line 882. The attribute's comment: “(1)”. References: EGA 0 (19.1.12), “P₁,P₂ finite projective”; EGA IV (11.3.7), “affine case, b)=>a)”.

(Injectivity locus.) The injectivity locus U is open, and for every f with D(f) ⊆ U: (a) the localized map φ_f is injective; and (b) Coker(φ)_f is finite projective over R_f.

theorem isOpen_injLocus_and_localized
    (φ : P₁ →ₗ[R] P₂) [Module.Finite R P₁] [Module.Projective R P₁]
    [Module.Finite R P₂] [Module.Projective R P₂] :
    IsOpen (injLocus φ) ∧
    ∀ f : R, (PrimeSpectrum.basicOpen f : Set (PrimeSpectrum R)) ⊆ injLocus φ →
      Function.Injective (localizedMap φ f) ∧
      Module.Finite (Localization.Away f)
        (Localization.Away f ⊗[R] (P₂ ⧸ LinearMap.range φ)) ∧
      Module.Projective (Localization.Away f)
        (Localization.Away f ⊗[R] (P₂ ⧸ LinearMap.range φ))

Stacks.FiniteProjective.MapLocus.isOpen_surjLocus_and_localized, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/Locus.lean, line 901. The attribute's comment: “(2)”.

(Surjectivity locus.) The surjectivity locus W is open, and for every f with D(f) ⊆ W: (a) the localized map φ_f is surjective; and (b) Ker(φ)_f is finite projective over R_f.

theorem isOpen_surjLocus_and_localized
    (φ : P₁ →ₗ[R] P₂) [Module.Finite R P₁] [Module.Projective R P₁]
    [Module.Finite R P₂] [Module.Projective R P₂] :
    IsOpen (surjLocus φ) ∧
    ∀ f : R, (PrimeSpectrum.basicOpen f : Set (PrimeSpectrum R)) ⊆ surjLocus φ →
      Function.Surjective (localizedMap φ f) ∧
      Module.Finite (Localization.Away f)
        (Localization.Away f ⊗[R] (LinearMap.ker φ)) ∧
      Module.Projective (Localization.Away f)
        (Localization.Away f ⊗[R] (LinearMap.ker φ))

Stacks.FiniteProjective.MapLocus.isOpen_isoLocus_and_localized, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/Locus.lean, line 924. The attribute's comment: “(3)”.

(Isomorphism locus.) The isomorphism locus V is open, and for every f with D(f) ⊆ V, the localized map φ_f is bijective.

Formal consequence of Theorems 1 and 2: isoLocus φ = injLocus φ ∩ surjLocus φ (isoLocus_eq), so it is open as an intersection of two opens; and on D(f) ⊆ isoLocus φ ⊆ injLocus φ (resp. ⊆ surjLocus φ) the localized map is both injective (injective_localizedMap_of_subset) and surjective (surjective_localizedMap_of_subset), hence bijective.

theorem isOpen_isoLocus_and_localized
    (φ : P₁ →ₗ[R] P₂) [Module.Finite R P₁] [Module.Projective R P₁]
    [Module.Finite R P₂] [Module.Projective R P₂] :
    IsOpen (isoLocus φ) ∧
    ∀ f : R, (PrimeSpectrum.basicOpen f : Set (PrimeSpectrum R)) ⊆ isoLocus φ →
      Function.Bijective (localizedMap φ f)
Sources
LeanLinearMap.setOf_localizedMap_atPrime_surjective_eq_setOf_baseChange_surjective · LinearMap.isOpen_setOf_localizedMap_atPrime_bijective · Module.FinitePresentation.exists_free_localizedModule_powers · Stacks.FiniteProjective.MapLocus.isOpen_injLocus_and_localized · Stacks.FiniteProjective.MapLocus.isOpen_surjLocus_and_localized · Stacks.FiniteProjective.MapLocus.isOpen_isoLocus_and_localized

Section10.81 Characterizing flatness#

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

Tag 058E, a lemma

Tag 058E in the Stacks Project.

Module.Flat.iff_exists_factorization_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/EquationalCriterion.lean, line 172.

Stacks 058E. An R-module M is flat if and only if every R-linear map to M from a finitely presented R-module P factors through a free finite R-module: there are k : ℕ and maps h : P → (Fin k →₀ R) and g : (Fin k →₀ R) → M with f = g ∘ h.

public theorem Module.Flat.iff_exists_factorization_of_finitePresentation {R : Type u} {M : Type v}
    [CommRing R] [AddCommGroup M] [Module R M] :
    Module.Flat R M ↔ ∀ ⦃P : Type u⦄ [AddCommGroup P] [Module R P]
      [Module.FinitePresentation R P] (f : P →ₗ[R] M),
      ∃ (k : ℕ) (h : P →ₗ[R] (Fin k →₀ R)) (g : (Fin k →₀ R) →ₗ[R] M), f = g ∘ₗ h
Tag 058F, a lemma

Tag 058F in the Stacks Project.

Module.Flat.iff_surjective_compRight_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/EquationalCriterion.lean, line 250.

Stacks 058F. An R-module M is flat if and only if for every finitely presented R-module P and every surjection φ : N → M of R-modules the induced map Hom_R(P, N) → Hom_R(P, M), postcomposition with φ, is surjective.

public theorem Module.Flat.iff_surjective_compRight_of_finitePresentation {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]
        ⦃N : Type v⦄ [AddCommGroup N] [Module R N] (φ : N →ₗ[R] M), Function.Surjective φ →
        Function.Surjective (LinearMap.compRight (M := P) R φ)
Tag 058G, a theorem

Tag 058G in the Stacks Project.

flat_iff_directLimit_free_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Lazard.lean, line 714. References: EGA 0 (6.1.2), “special case”; EGA 0 (6.2.3), “special case”; EGA 0 (6.3.4), “partial”; SGA 3 VIIA (4.2.1), “more general”; SGA 4 V (1.2), “Reverse implication only”; SGA 4 V (8.2.12), “special case”; SGA 4 VI (8.6.4), “special case”; SGA 4 XVII (5.5.1.1), “special case”; SGA 4 XVII (5.5.1.2), “partial”; SGA 4 XVII (5.5.6.3), “partial”.

Lazard's theorem. An R-module M over a commutative ring R is flat if and only if M is the colimit of a directed system of free finite R-modules: there exists a directed (nonempty, filtered) preorder ι, a family of R-modules G : ι → Type with R-linear transition maps f forming a DirectedSystem, such that every G i is free and finite, together with an R-linear isomorphism between the direct limit Module.DirectLimit G f and M.

theorem flat_iff_directLimit_free_finite {R : Type u} [CommRing R] (M : Type u)
    [AddCommGroup M] [Module R M] :
    Module.Flat R M ↔
      ∃ (ι : Type u) (_ : Preorder ι) (_ : IsDirected ι (· ≤ ·)) (_ : Nonempty ι)
        (_ : DecidableEq ι) (G : ι → Type u) (_ : (i : ι) → AddCommGroup (G i))
        (_ : (i : ι) → Module R (G i)) (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
        (_ : DirectedSystem G fun i j h => f i j h),
        (∀ i, Module.Free R (G i)) ∧ (∀ i, Module.Finite R (G i)) ∧
          Nonempty (Module.DirectLimit G f ≃ₗ[R] M)
Sources
LeanModule.Flat.iff_exists_factorization_of_finitePresentation · Module.Flat.iff_surjective_compRight_of_finitePresentation · flat_iff_directLimit_free_finite

Section10.82 Universally injective module maps#

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

Tag 058I, a definition

Tag 058I in the Stacks Project.

UniversallyInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjective.lean, line 342. References: EGA IV (11.9.14), “special case”; EGA IV (11.9.18), “special case”; SGA 1 II (4.5).

Universally injective module map. A homomorphism of R-modules f : M →ₗ[R] N is universally injective if for every R-module Q, the induced map f ⊗ id_Q : M ⊗_R Q → N ⊗_R Q (i.e. f.rTensor Q) is injective.

def UniversallyInjective {M N : Type v} [AddCommGroup M] [AddCommGroup N]
    [Module R M] [Module R N] (f : M →ₗ[R] N) : Prop
Tag 058J, an example

Tag 058J in the Stacks Project.

split_universallyExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyExact.lean, line 289. The attribute's comment: “(1)”.

A split short exact sequence is universally exact; equivalently its first map f₁ is universally injective.

theorem split_universallyExact
    {M₁ M₂ M₃ : Type v} [AddCommGroup M₁] [Module R M₁]
    [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃]
    (S : ShortExact (R := R) M₁ M₂ M₃) (hS : S.IsSplit) :
    S.UniversallyExact

colim_universallyExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyExact.lean, line 385. The attribute's comment: “(2)”.

Filtered colimits preserve universally exact short exact sequences.

theorem colim_universallyExact
    {ι : Type v} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι] [DecidableEq ι]
    {M₁ M₂ M₃ : ι → Type v}
    [∀ i, AddCommGroup (M₁ i)] [∀ i, Module R (M₁ i)]
    [∀ i, AddCommGroup (M₂ i)] [∀ i, Module R (M₂ i)]
    [∀ i, AddCommGroup (M₃ i)] [∀ i, Module R (M₃ i)]
    (D : DirectedSES (R := R) ι M₁ M₂ M₃)
    (hD : ∀ i, (D.seq i).UniversallyExact) :
    Function.Injective D.colimF₁ ∧
      Function.Surjective D.colimF₂ ∧
      LinearMap.range D.colimF₁ = LinearMap.ker D.colimF₂ ∧
      UniversallyInjective D.colimF₁
Tag 058K, a theorem

Tag 058K in the Stacks Project.

Function.Exact.universallyExact_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversallyExact.lean, line 1168. The attribute's comment: “Items (1)-(6), in the source's order, as a List.TFAE.”.

Stacks 058K. Let 0 → M₁ →[f₁] M₂ →[f₂] M₃ → 0 be a short exact sequence of R-modules. The following are equivalent: 1. the sequence is universally exact, that is, f₁ ⊗ id_Q is injective for every R-module Q; 2. for every finitely presented R-module Q the sequence 0 → M₁ ⊗ Q → M₂ ⊗ Q → M₃ ⊗ Q → 0 is exact; 3. whenever x i ∈ M₁, y j ∈ M₂ and a i j ∈ R satisfy f₁ (x i) = ∑ j, a i j • y j for all i, there are z j ∈ M₁ with x i = ∑ j, a i j • z j for all i; 4. every commutative square f₁ ∘ β = γ ∘ α with α : Rⁿ → Rᵐ, β : Rⁿ → M₁ and γ : Rᵐ → M₂ admits δ : Rᵐ → M₁ with δ ∘ α = β; 5. for every finitely presented R-module P the map Hom_R(P, M₂) → Hom_R(P, M₃) given by postcomposition with f₂ is surjective; 6. the sequence is the colimit of a directed system of split exact sequences 0 → M₁ → M_{2,j} → M_{3,j} → 0 with M_{3,j} finitely presented.

public theorem Function.Exact.universallyExact_tfae {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.Injective f₁) (h₂ : Function.Surjective f₂) :
    List.TFAE
      [ ∀ (Q : Type v) [AddCommGroup Q] [Module R Q], Function.Injective (f₁.rTensor Q),
        ∀ (Q : Type v) [AddCommGroup Q] [Module R Q] [Module.FinitePresentation R Q],
          Function.Injective (f₁.rTensor Q) ∧ Function.Exact (f₁.rTensor Q) (f₂.rTensor Q) ∧
            Function.Surjective (f₂.rTensor Q),
        ∀ (n m : ℕ) (x : Fin n → M₁) (y : Fin m → M₂) (a : Fin n → Fin m → R),
          (∀ i, f₁ (x i) = ∑ j, a i j • y j) → ∃ z : Fin m → M₁, ∀ i, x i = ∑ j, a i j • z j,
        ∀ (n m : ℕ) (α : (Fin n →₀ R) →ₗ[R] (Fin m →₀ R)) (β : (Fin n →₀ R) →ₗ[R] M₁)
          (γ : (Fin m →₀ R) →ₗ[R] M₂), f₁ ∘ₗ β = γ ∘ₗ α →
            ∃ δ : (Fin m →₀ R) →ₗ[R] M₁, δ ∘ₗ α = β,
        ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P],
          Function.Surjective (LinearMap.compRight (M := P) R f₂),
        ∃ (J : Type v) (_ : Preorder J) (_ : IsDirected J (· ≤ ·)) (_ : Nonempty J)
            (F : J ⥤ ShortComplex (ModuleCat.{v} R)) (c : Cocone F) (_ : IsColimit c)
            (_ : c.pt ≅ ModuleCat.shortComplexOfCompEqZero f₁ f₂ h.linearMap_comp_eq_zero),
          ∀ j, Nonempty (F.obj j).Splitting ∧ Module.FinitePresentation R (F.obj j).X₃ ∧
            IsIso ((c.ι.app j).τ₁) ]
Tag 058L, a lemma

Tag 058L in the Stacks Project.

Function.Exact.split_iff_forall_rTensor_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/UniversallyExact.lean, line 1354. The attribute's comment: “Exactness is hypothesised; splitness is the existence of a section of f₂.”.

Stacks 058L. Let 0 → M₁ →[f₁] M₂ →[f₂] M₃ → 0 be a short exact sequence of R-modules with M₃ of finite presentation. Then f₂ admits an R-linear section — equivalently, the sequence is split — if and only if the sequence is universally exact, that is, if and only if f₁ ⊗ id_Q : M₁ ⊗ Q → M₂ ⊗ Q is injective for every R-module Q.

public theorem Function.Exact.split_iff_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₃] [Module.FinitePresentation R M₃]
    {f₁ : M₁ →ₗ[R] M₂} {f₂ : M₂ →ₗ[R] M₃} (h : Function.Exact f₁ f₂)
    (h₁ : Function.Injective f₁) (h₂ : Function.Surjective f₂) :
    (∃ l : M₃ →ₗ[R] M₂, f₂ ∘ₗ l = LinearMap.id) ↔
      ∀ (Q : Type v) [AddCommGroup Q] [Module R Q],
        Function.Injective (f₁.rTensor Q)
Tag 058M, a lemma

Tag 058M in the Stacks Project.

Module.Flat.iff_forall_rTensor_injective_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjective.lean, line 132. The attribute's comment: “Exactness is hypothesised; universal injectivity of f₁ is spelled out.”.

An R-module M is flat if and only if every short exact sequence 0 → M₁ →[f₁] M₂ →[f₂] M → 0 of R-modules is universally exact, that is, if and only if f₁ ⊗ id_Q : M₁ ⊗ Q → M₂ ⊗ Q is injective for every such sequence and every R-module Q.

public theorem Module.Flat.iff_forall_rTensor_injective_of_exact {R : Type u} [CommRing R]
    [Small.{v} R] {M : Type v} [AddCommGroup M] [Module R M] :
    Module.Flat R M ↔
      ∀ ⦃M₁ M₂ : Type v⦄ [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂]
        (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M), Function.Injective f₁ →
        Function.Exact f₁ f₂ → Function.Surjective f₂ →
          ∀ (Q : Type v) [AddCommGroup Q] [Module R Q],
            Function.Injective (f₁.rTensor Q)
Tag 058P, a lemma

Tag 058P in the Stacks Project.

UniversallyExact.flat_of_middle_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyExact.lean, line 481. References: EGA 0 (6.7.4), “partial”.

Theorem (Stacks Tag 058P, Lemma 10.82.7). Let 0 -> M_1 ->[u] M_2 ->[v] M_3 -> 0 be a universally exact sequence of R-modules with M_2 flat. Then M_1 is flat and M_3 is flat.

theorem UniversallyExact.flat_of_middle_flat
    {M₁ M₂ M₃ : Type u} [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃]
    [Module R M₁] [Module R M₂] [Module R M₃]
    (u : M₁ →ₗ[R] M₂) (v : M₂ →ₗ[R] M₃)
    (hue : UniversallyExact u v) (hM₂ : Module.Flat R M₂) :
    Module.Flat R M₁ ∧ Module.Flat R M₃
Tag 05CH, a lemma

Tag 05CH in the Stacks Project.

universallyInjective_rTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjective.lean, line 358.

If u : M →ₗ[R] M' is universally injective, then for any R-module N the induced map u ⊗ id_N : M ⊗_R N → M' ⊗_R N (i.e. LinearMap.rTensor N u) is again universally injective.

theorem universallyInjective_rTensor {R : Type} [CommRing R]
    {M : Type} [AddCommGroup M] [Module R M]
    {M' : Type} [AddCommGroup M'] [Module R M']
    (u : M →ₗ[R] M') (hu : UniversallyInjective u)
    (N : Type) [AddCommGroup N] [Module R N] :
    UniversallyInjective (LinearMap.rTensor N u)
Tag 05CI, a lemma

Tag 05CI in the Stacks Project.

comp_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjective.lean, line 392.

A composition of universally injective R-module maps is universally injective.

theorem comp_universallyInjective {R : Type u} [CommRing R] {M N P : Type*}
    [AddCommGroup M] [AddCommGroup N] [AddCommGroup P]
    [Module R M] [Module R N] [Module R P]
    (f : M →ₗ[R] N) (g : N →ₗ[R] P)
    (hf : IsPureMono.{u, v} f) (hg : IsPureMono.{u, v} g) :
    IsPureMono.{u, v} (g ∘ₗ f)
Tag 05CJ, a lemma

Tag 05CJ in the Stacks Project.

Function.Injective.of_rTensor_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/TensorProduct/InjectiveComposition.lean, line 77. The attribute's comment: “Stated for one test module Q; the source's form is its closure over Q.”.

Let f : M →ₗ[R] M' and g : M' →ₗ[R] M'' be R-module maps and let Q be an R-module. If (g ∘ₗ f) ⊗ id_Q is injective, then so is f ⊗ id_Q. Quantifying over Q: if the composition g ∘ₗ f is universally injective, then f is universally injective.

public theorem Function.Injective.of_rTensor_comp {R : Type*} [CommSemiring R] {M M' M'' Q : Type*}
    [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [AddCommMonoid M'']
    [Module R M''] [AddCommMonoid Q] [Module R Q] {f : M →ₗ[R] M'} {g : M' →ₗ[R] M''}
    (h : Function.Injective ((g ∘ₗ f).rTensor Q)) : Function.Injective (f.rTensor Q)
Tag 05CL, a lemma

Tag 05CL in the Stacks Project.

Stacks.UniversalInjectivity.LocalizationCriteria.universally_injective_check_stalks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjective.lean, line 867.

For a ring map R → S and a map f : M → M' of S-modules, universal injectivity of f as a map of R-modules can be checked on localizations: the following are equivalent: f is universally injective over R; f_q is, for every prime q of S; f_m is, for every maximal ideal m of S; and the corresponding statements over the localizations R_p.

theorem universally_injective_check_stalks
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    {M : Type w} {M' : Type w'}
    [AddCommGroup M] [Module S M] [Module R M] [IsScalarTower R S M]
    [AddCommGroup M'] [Module S M'] [Module R M'] [IsScalarTower R S M']
    (f : M →ₗ[S] M') :
    [ -- (1) f is universally injective as a map of R-modules
      UniversallyInjective.{max u t} (f.restrictScalars R),
      -- (2) for every prime q of S, f_q is universally injective as a map of R-modules
      ∀ (q : Ideal S) [q.IsPrime], UniversallyInjective.{max u t} (A := R) (localizedMapR f q),
      -- (3) for every maximal m of S, f_m is universally injective as a map of R-modules
      ∀ (m : Ideal S) [m.IsMaximal], UniversallyInjective.{max u t} (A := R) (localizedMapR f m),
      -- (4) for every prime q of S, f_q is universally injective as a map of R_p-modules
      ∀ (q : Ideal S) [q.IsPrime],
        UniversallyInjective.{max u t} (A := Localization.AtPrime (q.under R)) (localizedMapRp f q),
      -- (5) for every maximal m of S, f_m is universally injective as a map of R_p-modules
      ∀ (m : Ideal S) [m.IsMaximal],
        UniversallyInjective.{max u t} (A := Localization.AtPrime (m.under R)) (localizedMapRp f m)
    ].TFAE
Tag 05CM, a lemma

Tag 05CM in the Stacks Project.

IsLocalizedModule.rTensor_injective_of_rTensor_injective_and_iff_extendScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Localization/UniversalInjectivity.lean, line 372. The attribute's comment: “Items (1) and (2) together, for one test module Q; the source's form is the closure over Q.”.

Stacks 05CM. Let A → B be a ring map, let S ⊆ A and S' ⊆ B be multiplicative subsets, let f : M → M' be a map of B-modules and let fₛ : N → N' be its localization at S', pinned by the square fₛ ∘ₗ g = g' ∘ₗ f. Let Q be an A-module with localization S⁻¹Q at S. Then:

  1. if f ⊗ id_Q is injective, so is fₛ ⊗ id_Q, both tensor products taken over A;
  2. fₛ ⊗_A id_Q is injective if and only if fₛ ⊗_{S⁻¹A} id_{S⁻¹Q} is injective.

This is the source's own sentence, about one localized map. The two items are independent of each other and each is stated separately, over its own data alone, as IsLocalizedModule.rTensor_injective_of_rTensor_injective and LinearMap.rTensor_injective_iff_extendScalarsOfIsLocalization; those are the forms to cite.

public theorem IsLocalizedModule.rTensor_injective_of_rTensor_injective_and_iff_extendScalars
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] (S : Submonoid A) (S' : Submonoid B)
    (Aₛ : Type*) [CommRing Aₛ] [Algebra A Aₛ] [IsLocalization S Aₛ] {M M' N N' Q Qₛ : Type*}
    [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M]
    [AddCommGroup M'] [Module A M'] [Module B M'] [IsScalarTower A B M']
    [AddCommGroup N] [Module A N] [Module B N] [IsScalarTower A B N]
    [Module Aₛ N] [IsScalarTower A Aₛ N]
    [AddCommGroup N'] [Module A N'] [Module B N'] [IsScalarTower A B N']
    [Module Aₛ N'] [IsScalarTower A Aₛ N']
    [AddCommGroup Q] [Module A Q] [AddCommGroup Qₛ] [Module A Qₛ] [Module Aₛ Qₛ]
    [IsScalarTower A Aₛ Qₛ] (g : M →ₗ[B] N) (g' : M' →ₗ[B] N') [IsLocalizedModule S' g]
    [IsLocalizedModule S' g'] (q : Q →ₗ[A] Qₛ) [IsLocalizedModule S q] (f : M →ₗ[B] M')
    (fₛ : N →ₗ[B] N') (hf : fₛ ∘ₗ g = g' ∘ₗ f) :
    (Function.Injective ((f.restrictScalars A).rTensor Q) →
        Function.Injective ((fₛ.restrictScalars A).rTensor Q)) ∧
      (Function.Injective ((fₛ.restrictScalars A).rTensor Q) ↔
        Function.Injective ((LinearMap.extendScalarsOfIsLocalization S Aₛ
          (fₛ.restrictScalars A)).rTensor Qₛ))

IsLocalizedModule.rTensor_injective_of_rTensor_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Localization/UniversalInjectivity.lean, line 403. The attribute's comment: “Item (1), for one test module Q; the source's form is the closure over Q.”.

Stacks 05CM, item (1). Let A → B be a ring map, let S' ⊆ B be a multiplicative subset, let f : M → M' be a map of B-modules and let fₛ : N → N' be its localization at S', pinned by the square fₛ ∘ₗ g = g' ∘ₗ f. Let Q be an A-module. If f ⊗ id_Q is injective, so is fₛ ⊗ id_Q, both tensor products taken over A.

Quantifying over Q: if f is universally injective as a map of A-modules, then so is its localization at S'. Composed with LinearMap.rTensor_injective_iff_extendScalarsOfIsLocalization this gives the universal injectivity of the localization as a map of S⁻¹A-modules as well, for any S ⊆ A with φ(S) ⊆ S'.

public theorem IsLocalizedModule.rTensor_injective_of_rTensor_injective
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] (S' : Submonoid B)
    {M M' N N' : Type*}
    [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M]
    [AddCommGroup M'] [Module A M'] [Module B M'] [IsScalarTower A B M']
    [AddCommGroup N] [Module A N] [Module B N] [IsScalarTower A B N]
    [AddCommGroup N'] [Module A N'] [Module B N'] [IsScalarTower A B N']
    (g : M →ₗ[B] N) (g' : M' →ₗ[B] N') [IsLocalizedModule S' g] [IsLocalizedModule S' g']
    (f : M →ₗ[B] M') (fₛ : N →ₗ[B] N') (hf : fₛ ∘ₗ g = g' ∘ₗ f) (Q : Type*) [AddCommGroup Q]
    [Module A Q] (h : Function.Injective ((f.restrictScalars A).rTensor Q)) :
    Function.Injective ((fₛ.restrictScalars A).rTensor Q)

LinearMap.rTensor_injective_iff_extendScalarsOfIsLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Localization/UniversalInjectivity.lean, line 428. The attribute's comment: “Item (2), for one test module Q and one localization S⁻¹Q of it; stated for an A-linear map between S⁻¹A-modules, of which the source's B-linear map between (S')⁻¹B-modules is a case.”.

Stacks 05CM, item (2). Let S ⊆ A be a multiplicative subset, let fₛ : N → N' be a map of A-modules between two S⁻¹A-modules and let Q be an A-module with localization S⁻¹Q at S. Then fₛ ⊗_A id_Q is injective if and only if fₛ ⊗_{S⁻¹A} id_{S⁻¹Q} is injective.

Quantifying over Q: for a map between S⁻¹A-modules — in particular between (S')⁻¹B-modules, for a multiplicative S' ⊆ B with φ(S) ⊆ S', which is the case the source states — universal injectivity as a map of A-modules and universal injectivity as a map of S⁻¹A-modules are the same condition.

public theorem LinearMap.rTensor_injective_iff_extendScalarsOfIsLocalization
    {A : Type*} [CommRing A] (S : Submonoid A) (Aₛ : Type*) [CommRing Aₛ] [Algebra A Aₛ]
    [IsLocalization S Aₛ] {N N' Q Qₛ : Type*}
    [AddCommGroup N] [Module A N] [Module Aₛ N] [IsScalarTower A Aₛ N]
    [AddCommGroup N'] [Module A N'] [Module Aₛ N'] [IsScalarTower A Aₛ N']
    [AddCommGroup Q] [Module A Q] [AddCommGroup Qₛ] [Module A Qₛ] [Module Aₛ Qₛ]
    [IsScalarTower A Aₛ Qₛ] (q : Q →ₗ[A] Qₛ) [IsLocalizedModule S q] (fₛ : N →ₗ[A] N') :
    Function.Injective (fₛ.rTensor Q) ↔
      Function.Injective ((LinearMap.extendScalarsOfIsLocalization S Aₛ fₛ).rTensor Qₛ)
Tag 0AS5, a lemma

Tag 0AS5 in the Stacks Project.

Module.Flat.rTensor_injective_iff_injective_mapQ_smul_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjective.lean, line 318. The attribute's comment: “M/IM is M ⧸ I • ⊤ and the induced map is Submodule.mapQ along f; the left-hand side spells out universal injectivity, which Mathlib has no name for.”.

Let f : M →ₗ[R] M' be a map of R-modules with M' flat. Then f is universally injective, that is f ⊗ id_Q is injective for every R-module Q, if and only if the induced map M/IM → M'/IM' is injective for every finitely generated ideal I ⊆ R.

public theorem Module.Flat.rTensor_injective_iff_injective_mapQ_smul_top {R : Type u} [CommRing R]
    [Small.{v} R] {M M' : Type v} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M']
    [Module.Flat R M'] (f : M →ₗ[R] M') :
    (∀ (Q : Type v) [AddCommGroup Q] [Module R Q], Function.Injective (f.rTensor Q)) ↔
      ∀ ⦃I : Ideal R⦄, I.FG →
        Function.Injective ((I • ⊤ : Submodule R M).mapQ (I • ⊤ : Submodule R M') f
          (Submodule.smul_top_le_comap_smul_top I f))
Tag 0H9I, a lemma

Tag 0H9I in the Stacks Project.

reflects_injections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjective.lean, line 973. The attribute's comment: “(1)”.

Base change along a universally injective ring map reflects injections. If R → S is universally injective as a map of R-modules and f ⊗_R id_S : M ⊗[R] S → N ⊗[R] S is injective, then f is injective.

theorem reflects_injections
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S]
    (hRS : UniversallyInjective (Algebra.linearMap R S))
    {M : Type u} [AddCommGroup M] [Module R M]
    {N : Type u} [AddCommGroup N] [Module R N]
    (f : M →ₗ[R] N)
    (hf : Function.Injective (LinearMap.rTensor S f)) :
    Function.Injective f

reflects_surjections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjective.lean, line 988. The attribute's comment: “(2)”. References: EGA IV (2.2.7), “partial”; EGA IV (2.5.4.1), “more general”.

Base change along a universally injective ring map reflects surjections. If R → S is universally injective as a map of R-modules and f ⊗_R id_S : M ⊗[R] S → N ⊗[R] S is surjective, then f is surjective.

theorem reflects_surjections
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S]
    (hRS : UniversallyInjective (Algebra.linearMap R S))
    {M : Type u} [AddCommGroup M] [Module R M]
    {N : Type u} [AddCommGroup N] [Module R N]
    (f : M →ₗ[R] N)
    (hf : Function.Surjective (LinearMap.rTensor S f)) :
    Function.Surjective f

reflects_isomorphisms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjective.lean, line 1019. The attribute's comment: “(3)”.

Base change along a universally injective ring map reflects isomorphisms. If R → S is universally injective as a map of R-modules and f ⊗_R id_S : M ⊗[R] S → N ⊗[R] S is bijective, then f is bijective.

theorem reflects_isomorphisms
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S]
    (hRS : UniversallyInjective (Algebra.linearMap R S))
    {M : Type u} [AddCommGroup M] [Module R M]
    {N : Type u} [AddCommGroup N] [Module R N]
    (f : M →ₗ[R] N)
    (hf : Function.Bijective (LinearMap.rTensor S f)) :
    Function.Bijective f
Tag 05CK, a lemma

Tag 05CK in the Stacks Project.

faithfullyFlat_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjective.lean, line 485. References: EGA 0 (6.5.1), “B faithfully flat”; EGA IV (2.2.8), “affine case”; EGA 0 (6.6.1), “(a)”; SGA 3 VIB (11.14), “necessity”.

For a faithfully flat ring map φ : R → S, the structure map R → S viewed as an R-linear map (Algebra.linearMap R S, where S is given its R-module structure via φ) is universally injective: for every R-module Q, the induced map R ⊗_R Q → S ⊗_R Q is injective.

theorem faithfullyFlat_universallyInjective
    {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) (hφ : φ.FaithfullyFlat) :
    haveI := φ.toAlgebra
    UniversallyInjectivePoly (Algebra.linearMap R S)

faithfullyFlat_comap_map_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjective.lean, line 525. The attribute's comment: “in particular”. References: EGA 0 (6.6.3), “first part, M = A”; EGA 0 (6.5.1), “B faithfully flat”; EGA 0 (22.4.8), “more general”; EGA 0 (6.5.2), “φ⁻¹(aB) = a”; EGA 0 (6.6.1), “(a) ⇒ φ⁻¹(aB) = a in (d)”; SGA 1 IV (2.6), “(i)”; SGA 3 V (9.1), “partial”.

For a faithfully flat ring map φ : R → S and every ideal I ⊆ R, the contraction of the extended ideal I S back to R equals I, i.e. φ⁻¹(I S) = I.

This is Mathlib's Ideal.comap_map_eq_self_of_faithfullyFlat, restated for a bare ring map.

theorem faithfullyFlat_comap_map_eq
    {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) (hφ : φ.FaithfullyFlat)
    (I : Ideal R) :
    Ideal.comap φ (Ideal.map φ I) = I
Sources
LeanUniversallyInjective · split_universallyExact · colim_universallyExact · Function.Exact.universallyExact_tfae · Function.Exact.split_iff_forall_rTensor_injective · Module.Flat.iff_forall_rTensor_injective_of_exact · UniversallyExact.flat_of_middle_flat · universallyInjective_rTensor

Section10.83 Descent for finite projective modules#

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

Tag 058R, a lemma

Tag 058R in the Stacks Project.

Declarations registered for the tag:

Tag 03C4, a lemma

Tag 03C4 in the Stacks Project.

Module.FinitePresentation.of_isBaseChange_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Descent.lean, line 184. The attribute's comment: “Part (2). Part (1) is Module.Finite.of_finite_tensorProduct_of_faithfullyFlat and part (3) is Module.Flat.of_flat_tensorProduct, both in Mathlib.”. References: EGA IV (2.5.2), “(ii), descent, affine”; EGA IV (2.5.3), “fin. pres., descent”; EGA IV (2.5.2), “(ii), descent, affine”; SGA 1 VIII (1.11), “fin. pres., descent”; SGA 1 VIII (1.10), “fin. pres., affine”; SGA 4½ Arcata (1.4.2), “(ii), fin. presentation”; SGA 1 VIII (1.11), “fin. pres., descent”; SGA 4½ Arcata (1.4.2), “(ii), fin. presentation”.

Stacks 03C4 (part 2). Let R → S be a faithfully flat ring map, let M be an R-module and let f : M →ₗ[R] N exhibit the S-module N as the base change of M along R → S. If N is a finitely presented S-module, then M is a finitely presented R-module.

theorem FinitePresentation.of_isBaseChange_of_faithfullyFlat {R : Type*} [CommRing R]
    {S : Type*} [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S]
    {M : Type*} [AddCommGroup M] [Module R M]
    {N : Type*} [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N]
    (f : M →ₗ[R] N) (h : IsBaseChange S f) [Module.FinitePresentation S N] :
    Module.FinitePresentation R M
Tag 058S, a proposition

Tag 058S in the Stacks Project.

Module.Projective.of_finite_of_isBaseChange_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Descent.lean, line 209. The attribute's comment: “The projectivity half of the conclusion; the finiteness half is Mathlib's Module.Finite.of_finite_tensorProduct_of_faithfullyFlat.”. References: SGA 1 VIII (1.10), “loc. free, affine”; SGA 3 VIB (11.8.2), “finite projective case”; SGA 3 VIB (11.8.1), “(ii), special case”; SGA 3 VIB (11.9.1), “special case”.

Stacks 058S (the projectivity half). Let R → S be a faithfully flat ring map, let M be an R-module and let f : M →ₗ[R] N exhibit the S-module N as the base change of M along R → S. If N is a finite projective S-module, then M is a projective R-module. Together with Module.Finite.of_finite_tensorProduct_of_faithfullyFlat this says that being a finite projective module descends along a faithfully flat ring map.

theorem Projective.of_finite_of_isBaseChange_of_faithfullyFlat {R : Type*} [CommRing R]
    {S : Type*} [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S]
    {M : Type*} [AddCommGroup M] [Module R M]
    {N : Type*} [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N]
    (f : M →ₗ[R] N) (h : IsBaseChange S f)
    [Module.Finite S N] [Module.Projective S N] :
    Module.Projective R M
Sources
LeanModule.finitePresentation_of_projective · Module.Flat.of_projective · Module.Flat.projective_of_finitePresentation · Module.FinitePresentation.of_isBaseChange_of_faithfullyFlat · Module.Projective.of_finite_of_isBaseChange_of_faithfullyFlat

Section10.84 Transfinite dévissage of modules#

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

Tag 058U, a definition

Tag 058U in the Stacks Project.

Submodule.IsDirectSumDevissage, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Devissage.lean, line 290. The attribute's comment: “direct sum devissage”.

A direct sum dévissage of an R-module M is an increasing family N of submodules of M, indexed by the ordinals α < s, with N 0 = 0, with union M, continuous at limit ordinals, and with N α a direct summand of N (α + 1) whenever α + 1 < s.

public structure IsDirectSumDevissage (s : Ordinal.{w}) (N : Ordinal.{w} → Submodule R M) :
    Prop

Submodule.IsKaplanskyDevissage, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Devissage.lean, line 309. The attribute's comment: “Kaplansky devissage”.

A Kaplansky dévissage of an R-module M is a direct sum dévissage all of whose quotients N (α + 1) / N α are countably generated, which is to say that N (α + 1) is generated over N α by countably many elements of M.

public structure IsKaplanskyDevissage (s : Ordinal.{w}) (N : Ordinal.{w} → Submodule R M) : Prop
    extends IsDirectSumDevissage s N
Tag 058V, a lemma

Tag 058V in the Stacks Project.

devissage_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Devissage.lean, line 121.

Stacks Tag 058V (Lemma 10.84.2). Given a direct sum dévissage of N, the module N is isomorphic to the direct sum of the successive quotients M_{α+1} / M_α over all ordinals α with α + 1 < S.

Here the α-th summand M_{α+1}/M_α is realized as the quotient of the submodule M (Order.succ α) of N by the image of M α inside it ((M α).submoduleOf (M (Order.succ α)), which is M α ⊓ M (succ α) = M α viewed as a submodule of ↥(M (succ α))).

theorem devissage_iso (D : DirectSumDevissage.{u} R N) :
    Nonempty (N ≃ₗ[R] DirectSum {α : Ordinal.{u} // Order.succ α < D.S}
      (fun a => (D.M (Order.succ a.1)) ⧸ (D.M a.1).submoduleOf (D.M (Order.succ a.1))))
Tag 058W, a lemma

Tag 058W in the Stacks Project.

Submodule.exists_sSupIndep_countable_span_iff_exists_isKaplanskyDevissage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Devissage.lean, line 604. The attribute's comment: “Countable generation written as a countable spanning set, and the direct sum decomposition internally, as an independent set of submodules of M with supremum ⊤.”.

Stacks 058W. Let M be a module over a ring R. Then M is a direct sum of countably generated R-modules — that is, M is the internal direct sum of an independent set of countably generated submodules — if and only if M admits a Kaplansky dévissage.

public theorem exists_sSupIndep_countable_span_iff_exists_isKaplanskyDevissage
    (R : Type v) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] :
    (∃ S : Set (Submodule R M), sSupIndep S ∧ sSup S = ⊤ ∧
        ∀ N ∈ S, ∃ t : Set M, t.Countable ∧ span R t = N) ↔
      ∃ (s : Ordinal.{u}) (N : Ordinal.{u} → Submodule R M),
        IsKaplanskyDevissage s N
Tag 058X, a theorem

Tag 058X in the Stacks Project.

Submodule.exists_sSupIndep_countable_span_of_isCompl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/DirectSum/CountablyGenerated.lean, line 557. The attribute's comment: “Being a direct sum of countably generated modules written internally, as in 058W: an independent set of submodules with supremum ⊤, each spanned by a countable set. P is a direct summand of M in the sense of a complement in the submodule lattice of M.”.

Stacks 058X. Let M be a module over a ring R which is a direct sum of countably generated R-modules — that is, M is the internal direct sum of an independent set of countably generated submodules. If P is a direct summand of M, with complement Q, then P is also a direct sum of countably generated R-modules.

public theorem exists_sSupIndep_countable_span_of_isCompl {R : Type*} {M : Type*} [Ring R]
    [AddCommGroup M] [Module R M]
    (hM : ∃ S : Set (Submodule R M), sSupIndep S ∧ sSup S = ⊤ ∧
      ∀ N ∈ S, ∃ t : Set M, t.Countable ∧ span R t = N)
    (P Q : Submodule R M) (hPQ : IsCompl P Q) :
    ∃ S : Set (Submodule R ↥P), sSupIndep S ∧ sSup S = ⊤ ∧
      ∀ N ∈ S, ∃ t : Set ↥P, t.Countable ∧ span R t = N
Tag 058Y, a theorem

Tag 058Y in the Stacks Project.

Submodule.exists_sSupIndep_countable_span_projective_of_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/DirectSum/ProjectiveCountablyGenerated.lean, line 247. The attribute's comment: “Being a direct sum of countably generated projective modules is written internally, as in 058W and 058X: an independent set of submodules with supremum ⊤, each spanned by a countable set and each projective. Countable generation is a countable spanning set.”.

Let M be a projective module over a ring R. Then M is a direct sum of countably generated projective R-modules: there is an independent set of submodules of M with supremum ⊤, each spanned by a countable set and each projective over R.

public theorem exists_sSupIndep_countable_span_projective_of_projective {R : Type*} {M : Type*}
    [Ring R] [AddCommGroup M] [Module R M] [Module.Projective R M] :
    ∃ S : Set (Submodule R M), sSupIndep S ∧ sSup S = ⊤ ∧
      ∀ N ∈ S, (∃ t : Set M, t.Countable ∧ span R t = N) ∧ Module.Projective R ↥N
Sources
LeanSubmodule.IsDirectSumDevissage · Submodule.IsKaplanskyDevissage · devissage_iso · Submodule.exists_sSupIndep_countable_span_iff_exists_isKaplanskyDevissage · Submodule.exists_sSupIndep_countable_span_of_isCompl · Submodule.exists_sSupIndep_countable_span_projective_of_projective

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.