15.123 A regular local ring is… to 15.130 Big projective modules…

Section15.123 A regular local ring is a UFD #

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

Tag 0AFZ, a lemma

Tag 0AFZ in the Stacks Project.

IsRegularLocalRing.pic_subsingleton_localization_away, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/UniqueFactorization.lean, line 306.

Stacks 0AFZ. The Picard group of the localization of a regular local ring at an element is trivial.

public theorem pic_subsingleton_localization_away
    (R : Type u) [CommRing R] [IsRegularLocalRing R] (f : R) :
    Subsingleton (CommRing.Pic (Localization.Away f))

Tag 0AG0, a lemma

Tag 0AG0 in the Stacks Project.

IsRegularLocalRing.uniqueFactorizationMonoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/UniqueFactorization.lean, line 549. References: SGA 2 XI (3.13); SGA 6 X (7.8), “more general”; SGA 7 VIII (6.5.1), “special case”.

Stacks 0AG0. A regular local ring is a unique factorization domain.

public theorem uniqueFactorizationMonoid
    (R : Type u) [CommRing R] [IsRegularLocalRing R] :
    UniqueFactorizationMonoid R

Tag 0DLQ, a lemma

Tag 0DLQ in the Stacks Project.

ValuationRing.subsingleton_pic_genericFibre_of_isRegular_specialFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularLocalRing/PicardGenericFibre.lean, line 297. References: SGA 6 X (7.8), “special case”.

Stacks 0DLQ. Let R be a valuation ring with fraction field K, and let A be a flat local R-algebra, essentially of finite type, whose special fibre is regular. Then the Picard group of the generic fibre is trivial.

public theorem subsingleton_pic_genericFibre_of_isRegular_specialFibre
    {R : Type u} {A : Type v} {K : Type w}
    [CommRing R] [IsDomain R] [ValuationRing R]
    [CommRing A] [IsLocalRing A] [Algebra R A] [IsLocalHom (algebraMap R A)]
    [Module.Flat R A] [Algebra.EssFiniteType R A]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [IsRegularRing (A ⊗[R] (IsLocalRing.ResidueField R))] :
    Subsingleton (CommRing.Pic (A ⊗[R] K))

Sources

LeanIsRegularLocalRing.pic_subsingleton_localization_away · IsRegularLocalRing.uniqueFactorizationMonoid · ValuationRing.subsingleton_pic_genericFibre_of_isRegular_specialFibre

Section15.124 Determinants of complexes #

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

Tag 0FJJ, a lemma

Tag 0FJJ in the Stacks Project.

TwoTermComplex.determinantEquivOfSurjectiveQuasiIso_apply_delta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/DeterminantLine/CanonicalElement.lean, line 143.

Stacks 0FJJ. The canonical determinant equivalence associated to a degreewise-surjective quasi-isomorphism of two-term finite-projective complexes maps the canonical determinant element of the source to that of the target.

public theorem determinantEquivOfSurjectiveQuasiIso_apply_delta
    {R : Type u} [CommRing R]
    {K₁ : Type v₁} {K₀ : Type v₀} {L₁ : Type w₁} {L₀ : Type w₀}
    [AddCommGroup K₁] [Module R K₁] [Module.Finite R K₁] [Module.Projective R K₁]
    [AddCommGroup K₀] [Module R K₀] [Module.Finite R K₀] [Module.Projective R K₀]
    [AddCommGroup L₁] [Module R L₁] [Module.Finite R L₁] [Module.Projective R L₁]
    [AddCommGroup L₀] [Module R L₀] [Module.Finite R L₀] [Module.Projective R L₀]
    (K : K₁ →ₗ[R] K₀) (L : L₁ →ₗ[R] L₀) (a : TwoTermComplex.Hom K L)
    (ha : a.IsDegreewiseSurjective) (hqa : a.IsQuasiIso) (hL : TwoTermComplex.IsRankZero L) :
    letI : Module.Finite R (LinearMap.ker a.neg) :=
      TwoTermComplex.kernel_finite a.neg ha.1
    letI : Module.Projective R (LinearMap.ker a.neg) :=
      TwoTermComplex.kernel_projective a.neg ha.1
    letI : Module.Finite R (LinearMap.ker a.zero) :=
      TwoTermComplex.kernel_finite a.zero ha.2
    letI : Module.Projective R (LinearMap.ker a.zero) :=
      TwoTermComplex.kernel_projective a.zero ha.2
    let D := TwoTermComplex.determinantEquivOfSurjectiveQuasiIso K L a ha hqa
    ∃ hK : TwoTermComplex.IsRankZero K,
      D.equiv (TwoTermComplex.delta K hK) = TwoTermComplex.delta L hL

Tag 0FJK, a lemma

Tag 0FJK in the Stacks Project.

TwoTermComplex.determinantEquiv_eq_of_homotopic_surjections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/DeterminantLine/Homotopy.lean, line 652.

Stacks 0FJK. Homotopic degreewise-surjective quasi-isomorphisms between two-term complexes of finite projective modules induce the same canonical equivalence of determinant lines.

public theorem determinantEquiv_eq_of_homotopic_surjections
    {R : Type u} [CommRing R]
    {K₁ : Type v₁} {K₀ : Type v₀} {L₁ : Type w₁} {L₀ : Type w₀}
    [AddCommGroup K₁] [Module R K₁] [Module.Finite R K₁] [Module.Projective R K₁]
    [AddCommGroup K₀] [Module R K₀] [Module.Finite R K₀] [Module.Projective R K₀]
    [AddCommGroup L₁] [Module R L₁] [Module.Finite R L₁] [Module.Projective R L₁]
    [AddCommGroup L₀] [Module R L₀] [Module.Finite R L₀] [Module.Projective R L₀]
    (K : K₁ →ₗ[R] K₀) (L : L₁ →ₗ[R] L₀) (a : TwoTermComplex.Hom K L)
    (ha : a.IsDegreewiseSurjective) (hqa : a.IsQuasiIso) (h : K₀ →ₗ[R] L₁)
    (hbneg : Function.Surjective (a.neg + h.comp K))
    (hbzero : Function.Surjective (a.zero + L.comp h)) :
    let b : TwoTermComplex.Hom K L :=
      { neg := a.neg + h.comp K
        zero := a.zero + L.comp h
        comm
    := by
          ext x
          simp only [LinearMap.add_apply, LinearMap.comp_apply, map_add]
          rw [show a.zero (K x) = L (a.neg x) from LinearMap.congr_fun a.comm x] }
    b.IsQuasiIso ∧ ∀ hqb : b.IsQuasiIso,
      letI : Module.Finite R (LinearMap.ker a.neg) :=
        TwoTermComplex.kernel_finite a.neg ha.1
      letI : Module.Projective R (LinearMap.ker a.neg) :=
        TwoTermComplex.kernel_projective a.neg ha.1
      letI : Module.Finite R (LinearMap.ker a.zero) :=
        TwoTermComplex.kernel_finite a.zero ha.2
      letI : Module.Projective R (LinearMap.ker a.zero) :=
        TwoTermComplex.kernel_projective a.zero ha.2
      letI : Module.Finite R (LinearMap.ker b.neg) :=
        TwoTermComplex.kernel_finite b.neg hbneg
      letI : Module.Projective R (LinearMap.ker b.neg) :=
        TwoTermComplex.kernel_projective b.neg hbneg
      letI : Module.Finite R (LinearMap.ker b.zero) :=
        TwoTermComplex.kernel_finite b.zero hbzero
      letI : Module.Projective R (LinearMap.ker b.zero) :=
        TwoTermComplex.kernel_projective b.zero hbzero
      let Da := TwoTermComplex.determinantEquivOfSurjectiveQuasiIso K L a ha hqa
      let Db := TwoTermComplex.determinantEquivOfSurjectiveQuasiIso K L b
        ⟨hbneg, hbzero⟩ hqb
      Da.equiv = Db.equiv

Tag 0FJL, a lemma

Tag 0FJL in the Stacks Project.

TwoTermComplex.determinantEquivOfSurjectiveQuasiIso_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/DeterminantLine/Composition.lean, line 253.

Stacks 0FJL. The canonical determinant equivalence associated to a composite of degreewise-surjective quasi-isomorphisms of two-term finite-projective complexes is the composite of their canonical determinant equivalences.

public theorem determinantEquivOfSurjectiveQuasiIso_comp
    {R : Type u} [CommRing R]
    {K₁ : Type v₁} {K₀ : Type v₀} {L₁ : Type w₁} {L₀ : Type w₀}
    {M₁ : Type x₁} {M₀ : Type x₀}
    [AddCommGroup K₁] [Module R K₁] [Module.Finite R K₁] [Module.Projective R K₁]
    [AddCommGroup K₀] [Module R K₀] [Module.Finite R K₀] [Module.Projective R K₀]
    [AddCommGroup L₁] [Module R L₁] [Module.Finite R L₁] [Module.Projective R L₁]
    [AddCommGroup L₀] [Module R L₀] [Module.Finite R L₀] [Module.Projective R L₀]
    [AddCommGroup M₁] [Module R M₁] [Module.Finite R M₁] [Module.Projective R M₁]
    [AddCommGroup M₀] [Module R M₀] [Module.Finite R M₀] [Module.Projective R M₀]
    (K : K₁ →ₗ[R] K₀) (L : L₁ →ₗ[R] L₀) (M : M₁ →ₗ[R] M₀)
    (a : TwoTermComplex.Hom K L) (b : TwoTermComplex.Hom L M)
    (ha : a.IsDegreewiseSurjective) (hqa : a.IsQuasiIso)
    (hb : b.IsDegreewiseSurjective) (hqb : b.IsQuasiIso) :
    let c : TwoTermComplex.Hom K M :=
      { neg := b.neg.comp a.neg
        zero := b.zero.comp a.zero
        comm
    := by rw [LinearMap.comp_assoc, a.comm, ← LinearMap.comp_assoc, b.comm,
          LinearMap.comp_assoc] }
    let hc : c.IsDegreewiseSurjective :=
      ⟨hb.1.comp ha.1, hb.2.comp ha.2⟩
    ∃ hqc : c.IsQuasiIso,
      letI : Module.Finite R (LinearMap.ker a.neg) :=
        TwoTermComplex.kernel_finite a.neg ha.1
      letI : Module.Projective R (LinearMap.ker a.neg) :=
        TwoTermComplex.kernel_projective a.neg ha.1
      letI : Module.Finite R (LinearMap.ker a.zero) :=
        TwoTermComplex.kernel_finite a.zero ha.2
      letI : Module.Projective R (LinearMap.ker a.zero) :=
        TwoTermComplex.kernel_projective a.zero ha.2
      letI : Module.Finite R (LinearMap.ker b.neg) :=
        TwoTermComplex.kernel_finite b.neg hb.1
      letI : Module.Projective R (LinearMap.ker b.neg) :=
        TwoTermComplex.kernel_projective b.neg hb.1
      letI : Module.Finite R (LinearMap.ker b.zero) :=
        TwoTermComplex.kernel_finite b.zero hb.2
      letI : Module.Projective R (LinearMap.ker b.zero) :=
        TwoTermComplex.kernel_projective b.zero hb.2
      letI : Module.Finite R (LinearMap.ker c.neg) :=
        TwoTermComplex.kernel_finite c.neg hc.1
      letI : Module.Projective R (LinearMap.ker c.neg) :=
        TwoTermComplex.kernel_projective c.neg hc.1
      letI : Module.Finite R (LinearMap.ker c.zero) :=
        TwoTermComplex.kernel_finite c.zero hc.2
      letI : Module.Projective R (LinearMap.ker c.zero) :=
        TwoTermComplex.kernel_projective c.zero hc.2
      let Da := TwoTermComplex.determinantEquivOfSurjectiveQuasiIso K L a ha hqa
      let Db := TwoTermComplex.determinantEquivOfSurjectiveQuasiIso L M b hb hqb
      let Dc := TwoTermComplex.determinantEquivOfSurjectiveQuasiIso K M c hc hqc
      Da.equiv.trans Db.equiv = Dc.equiv

Tag 0FJM, a lemma

Tag 0FJM in the Stacks Project.

TwoTermDeterminant.exists_determinantFunctor_natural_delta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/DeterminantFunctor.lean, line 996.

Stacks 0FJM. There is a determinant functor from perfect complexes of Tor-amplitude [-1, 0] and isomorphisms to invertible modules and isomorphisms. Its value is canonically identified with the determinant line of every finite-projective two-term presentation; on rank-zero objects the determinant of the differential defines an element natural under all isomorphisms.

public theorem exists_determinantFunctor_natural_delta {R : Type u} [CommRing R] :
    ∃ (det : Core (PerfectTwoTermComplex R) ⥤ Core (InvertibleModule R))
      (comparison : ∀ (K : PerfectTwoTermComplex R) (P : TwoTermPresentation K.obj),
        letI := P.finite (-1)
        letI := P.projective (-1)
        letI := P.finite 0
        letI := P.projective 0
        (det.obj ⟨K⟩).of.obj ≃ₗ[R]
          TwoTermComplex.determinantLine (P.complex.d (-1) 0).hom)
      (delta : ∀ (K : PerfectTwoTermComplex R),
        IsRankZero K.obj → (det.obj ⟨K⟩).of.obj),
      (∀ (K : PerfectTwoTermComplex R) (P : TwoTermPresentation K.obj)
          (hP : P.IsRankZero),
        letI := P.finite (-1)
        letI := P.projective (-1)
        letI := P.finite 0
        letI := P.projective 0
        (comparison K P).toLinearMap (delta K ⟨P, hP⟩) =
          TwoTermComplex.delta (P.complex.d (-1) 0).hom hP) ∧
      (∀ (K L : PerfectTwoTermComplex R) (P : TwoTermPresentation K.obj)
          (Q : TwoTermPresentation L.obj)
          (a : (⟨K⟩ : Core (PerfectTwoTermComplex R)) ⟶ ⟨L⟩)
          (f : P.complex ⟶ Q.complex)
          (_hf : P.iso.hom ≫ DerivedCategory.Q.map f ≫ Q.iso.inv = a.iso.hom.hom)
          (hs : (P.hom Q f).IsDegreewiseSurjective) (hq : (P.hom Q f).IsQuasiIso),
        letI := P.finite (-1)
        letI := P.projective (-1)
        letI := P.finite 0
        letI := P.projective 0
        letI := Q.finite (-1)
        letI := Q.projective (-1)
        letI := Q.finite 0
        letI := Q.projective 0
        let g := P.hom Q f
        letI := TwoTermComplex.kernel_finite g.neg hs.1
        letI := TwoTermComplex.kernel_projective g.neg hs.1
        letI := TwoTermComplex.kernel_finite g.zero hs.2
        letI := TwoTermComplex.kernel_projective g.zero hs.2
        ∀ x,
          (comparison L Q).toLinearMap ((det.map a).iso.hom x) =
            (TwoTermComplex.determinantEquivOfSurjectiveQuasiIso
              (P.complex.d (-1) 0).hom (Q.complex.d (-1) 0).hom g hs hq).equiv
                ((comparison K P).toLinearMap x)) ∧
      ∀ (K L : PerfectTwoTermComplex R)
        (a : (⟨K⟩ : Core (PerfectTwoTermComplex R)) ⟶ ⟨L⟩)
        (hK : IsRankZero K.obj) (hL : IsRankZero L.obj),
        (det.map a).iso.hom (delta K hK) = delta L hL

TwoTermDeterminant.det, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/DeterminantFunctor.lean, line 1102. The attribute's comment: “the determinant functor as a named definition, rather than as the subject of an existential quantifier”.

Stacks 0FJM. The determinant functor, from perfect objects of the derived category of R-modules of Tor-amplitude in [-1, 0] with isomorphisms as morphisms, to invertible R-modules with isomorphisms as morphisms.

public noncomputable def det (R : Type u) [CommRing R] :
    Core (PerfectTwoTermComplex R) ⥤ Core (InvertibleModule R)

TwoTermDeterminant.delta, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/DeterminantFunctor.lean, line 1122. The attribute's comment: “the canonical section δ of the determinant of a rank-zero object, as a named definition”.

Stacks 0FJM. The canonical element of the determinant of a perfect object of Tor-amplitude in [-1, 0] and rank zero, given by the determinant of the differential of a two-term presentation of it.

public noncomputable def delta {R : Type u} [CommRing R] (K : PerfectTwoTermComplex R)
    (hK : IsRankZero K.obj) : ((det R).obj ⟨K⟩).of.obj

TwoTermDeterminant.det_map_delta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/DeterminantFunctor.lean, line 1158. The attribute's comment: “the compatibility det(a)(δ(L)) = δ(K) of the canonical section with isomorphisms, as a named theorem”.

Stacks 0FJM. The determinant functor carries the canonical element of a rank-zero perfect object of Tor-amplitude in [-1, 0] to the canonical element of any isomorphic object.

public theorem det_map_delta {R : Type u} [CommRing R] {K L : PerfectTwoTermComplex R}
    (a : (⟨K⟩ : Core (PerfectTwoTermComplex R)) ⟶ ⟨L⟩)
    (hK : IsRankZero K.obj) (hL : IsRankZero L.obj) :
    ((det R).map a).iso.hom (delta K hK) = delta L hL

Sources

LeanTwoTermComplex.determinantEquivOfSurjectiveQuasiIso_apply_delta · TwoTermComplex.determinantEquiv_eq_of_homotopic_surjections · TwoTermComplex.determinantEquivOfSurjectiveQuasiIso_comp · TwoTermDeterminant.exists_determinantFunctor_natural_delta · TwoTermDeterminant.det · TwoTermDeterminant.delta · TwoTermDeterminant.det_map_delta

Section15.125 Extensions of valuation rings #

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

Tag 0ASG, a definition

Tag 0ASG in the Stacks Project.

ValuationRing.IsExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Extension/Defs.lean, line 43. The attribute's comment: “extension of valuation rings”.

An extension of valuation rings is an injective local ring homomorphism.

def IsExtension {A : Type u} {B : Type v}
    [CommRing A] [IsDomain A] [ValuationRing A]
    [CommRing B] [IsDomain B] [ValuationRing B]
    (f : A →+* B) : Prop

ValuationRing.valueGroupMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Extension/Defs.lean, line 52. The attribute's comment: “map on value groups”.

The canonical homomorphism Γ_A → Γ_B induced by an extension of valuation rings. Here K and L are arbitrary fraction fields of A and B, respectively.

noncomputable def valueGroupMap {A : Type u} {B : Type v} {K : Type w} {L : Type x}
    [CommRing A] [IsDomain A] [ValuationRing A]
    [CommRing B] [IsDomain B] [ValuationRing B]
    [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
    [Algebra B L] [IsFractionRing B L]
    (f : A →+* B) (hf : IsExtension f) :
    (ValueGroup A K)ˣ →* (ValueGroup B L)ˣ

ValuationRing.IsWeaklyUnramified, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Extension/Defs.lean, line 86. The attribute's comment: “weakly unramified”.

An extension of valuation rings is weakly unramified when its canonical map on value groups is bijective.

def IsWeaklyUnramified {A : Type u} {B : Type v}
    [CommRing A] [IsDomain A] [ValuationRing A]
    [CommRing B] [IsDomain B] [ValuationRing B]
    (f : A →+* B) (hf : IsExtension f) : Prop

ValuationRing.residueDegree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Extension/Defs.lean, line 96. The attribute's comment: “residue degree”.

The residue degree of an extension of valuation rings, namely [κ_B : κ_A] for the residue-field map induced by the local homomorphism, and zero when that extension is infinite.

noncomputable def residueDegree {A : Type u} {B : Type v}
    [CommRing A] [IsDomain A] [ValuationRing A]
    [CommRing B] [IsDomain B] [ValuationRing B]
    (f : A →+* B) (hf : IsExtension f) : ℕ

ValuationRing.valueGroupMap_valuation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Extension/Defs.lean, line 108. The attribute's comment: “commutative value-group diagram”.

The canonical map on value groups sends the valuation class of every nonzero element of the smaller valuation ring to the valuation class of its image. This is the commutative square in the definition of an extension of valuation rings.

theorem valueGroupMap_valuation {A : Type u} {B : Type v} {K : Type w} {L : Type x}
    [CommRing A] [IsDomain A] [ValuationRing A]
    [CommRing B] [IsDomain B] [ValuationRing B]
    [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
    [Algebra B L] [IsFractionRing B L]
    (f : A →+* B) (hf : IsExtension f) (a : A) (ha : a ≠ 0) :
    ((valueGroupMap (K := K) (L := L) f hf)
      (Units.mk0 ((valuation A K) (algebraMap A K a)) (by simp [ha])) :
        ValueGroup B L) =
      (valuation B L) (algebraMap B L (f a))

Tag 0ASH, a lemma

Tag 0ASH in the Stacks Project.

ext_valuation_rings_degree_ineq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Extension/FundamentalInequality.lean, line 392.

Let A ⊆ B be an extension of valuation rings with fraction fields K ⊆ L, and assume the field extension L/K is finite. Then:

the residue field extension κ_A ⊆ κ_B is finite (Module.Finite, i.e. [κ_B : κ_A] < ∞);

the value group Γ_A has finite index in Γ_B ((valueGroupHom B K L).range.index ≠ 0, i.e. [Γ_B : Γ_A] < ∞); and

[Γ_B : Γ_A] · [κ_B : κ_A] ≤ [L : K].

The residue field degree [κ_B : κ_A] is computed with respect to the algebra structure on κ_B over κ_A induced by Mathlib's IsLocalRing.ResidueField.map (algebraMap A B).

theorem ext_valuation_rings_degree_ineq
    (A B K L : Type*)
    [CommRing A] [IsDomain A] [ValuationRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [CommRing B] [IsDomain B] [ValuationRing B] [Field L] [Algebra B L] [IsFractionRing B L]
    [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
    [IsLocalHom (algebraMap A B)]
    (hfin : Module.Finite K L) :
    letI : Algebra (ResidueField A) (ResidueField B) :=
      (ResidueField.map (algebraMap A B)).toAlgebra
    Module.Finite (ResidueField A) (ResidueField B) ∧
    (valueGroupHom B K L).range.index ≠ 0 ∧
    (valueGroupHom B K L).range.index * Module.finrank (ResidueField A) (ResidueField B)
      ≤ Module.finrank K L

Tag 0H37, a lemma

Tag 0H37 in the Stacks Project.

integralClosure_isValuationRing_of_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Extension/PurelyInseparable.lean, line 115.

Let A be a valuation ring with fraction field K of exponential characteristic p, and let L/K be a purely inseparable field extension. Then the integral closure B of A in L satisfies the valuation-ring criterion, has fraction field L, and the inclusion A → B is an injective local homomorphism.

theorem integralClosure_isValuationRing_of_isPurelyInseparable [ExpChar K p] [IsPurelyInseparable K
  L] :
    -- (1) `B` is a valuation ring: the valuation criterion holds.
    (∀ x : L, x ∈ integralClosure A L ∨ x⁻¹ ∈ integralClosure A L) ∧
    -- (2) `Frac(B) = L`.
    IsFractionRing (integralClosure A L) L ∧
    -- (3) the inclusion `A → B` is injective and a local homomorphism.
    (Function.Injective (algebraMap A (integralClosure A L)) ∧
      IsLocalHom (algebraMap A (integralClosure A L)))

Tag 0ASI, a lemma

Tag 0ASI in the Stacks Project.

ValuationRing.exists_eq_unit_mul_pow_of_flat_local, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Extension/Descent.lean, line 310.

Let A → B be a flat local homomorphism of Noetherian local normal domains. Suppose every height-one prime of A has a weakly unramified height-one prime of B lying over it. If an element of A becomes an nth power times a unit in B, for n > 1, then it is already an nth power times a unit in A.

theorem exists_eq_unit_mul_pow_of_flat_local
    (A B : Type*) [CommRing A] [IsDomain A] [IsNoetherianRing A]
    [IsLocalRing A] [IsIntegrallyClosed A]
    [CommRing B] [IsDomain B] [IsNoetherianRing B]
    [IsLocalRing B] [IsIntegrallyClosed B]
    [Algebra A B] [Module.Flat A B] [IsLocalHom (algebraMap A B)]
    (n : ℕ) (hn : 1 < n) (f : A) (h : B) (w : Bˣ)
    (hfh : algebraMap A B f = (w : B) * h ^ n)
    (hunramified : ∀ (p : Ideal A) (hp : p.IsPrime), p.height = 1 →
      ∃ (q : Ideal B) (hq : q.IsPrime), q.height = 1 ∧
        ∃ hlo : q.LiesOver p,
          (letI : p.IsPrime := hp
           letI : q.IsPrime := hq
           letI : q.LiesOver p := hlo
           letI : Algebra (Localization.AtPrime p) (Localization.AtPrime q) :=
             Localization.AtPrime.algebraOfLiesOver p q
           (IsLocalRing.maximalIdeal (Localization.AtPrime q)).ramificationIdx
             (Localization.AtPrime p) = 1)) :
    ∃ (g : A) (u : Aˣ), f = (u : A) * g ^ n

Tag 0ASJ, a lemma

Tag 0ASJ in the Stacks Project.

ValuationRing.isWeaklyUnramified_localization_atPrime_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Extension/Etale.lean, line 525.

Stacks Tag 0ASJ. If A is a valuation ring, A → B is étale, and m is a prime of B lying over the maximal ideal of A, then the canonical map from A to Bₘ is a weakly unramified extension of valuation rings.

theorem isWeaklyUnramified_localization_atPrime_of_etale
    (A : Type u) (B : Type v)
    [CommRing A] [IsDomain A] [ValuationRing A]
    [CommRing B] [Algebra A B] [Algebra.Etale A B]
    (m : Ideal B) [m.IsPrime] (hm : m.LiesOver (maximalIdeal A)) :
    ∃ (_ : IsDomain (Localization.AtPrime m))
      (_ : ValuationRing (Localization.AtPrime m))
      (h : IsExtension
        (algebraMap A (Localization.AtPrime m))),
      IsWeaklyUnramified (algebraMap A (Localization.AtPrime m)) h

Tag 0ASK, a lemma

Tag 0ASK in the Stacks Project.

ValuationRing.isWeaklyUnramified_henselization_and_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Extension/Etale.lean, line 1037.

Stacks Tag 0ASK. The henselization and strict henselization of a valuation ring are valuation rings, and both canonical inclusions induce bijections on value groups.

theorem isWeaklyUnramified_henselization_and_strictHenselization
    (A Ah Ash : Type u)
    [CommRing A] [IsDomain A] [ValuationRing A]
    [CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
    [IsHenselization A (ResidueField A) Ah]
    (ksep : Type v) [Field ksep] [Algebra (ResidueField A) ksep]
    [IsSepClosure (ResidueField A) ksep]
    [CommRing Ash] [IsLocalRing Ash] [Algebra A Ash] [Algebra Ah Ash]
    [IsScalarTower A Ah Ash] [IsHenselization A ksep Ash]
    [IsLocalHom (algebraMap Ah Ash)] :
    ∃ (_ : IsDomain Ah) (_ : ValuationRing Ah)
      (_ : IsDomain Ash) (_ : ValuationRing Ash)
      (hAh : IsExtension (algebraMap A Ah))
      (hAsh : IsExtension (algebraMap Ah Ash)),
      IsWeaklyUnramified (algebraMap A Ah) hAh ∧
        IsWeaklyUnramified (algebraMap Ah Ash) hAsh

Sources

LeanValuationRing.IsExtension · ValuationRing.valueGroupMap · ValuationRing.IsWeaklyUnramified · ValuationRing.residueDegree · ValuationRing.valueGroupMap_valuation · ext_valuation_rings_degree_ineq · integralClosure_isValuationRing_of_isPurelyInseparable · ValuationRing.exists_eq_unit_mul_pow_of_flat_local

Section15.126 Structure of modules over a PID #

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

Tag 0ASM, a lemma

Tag 0ASM in the Stacks Project.

summand_sum_cyclic_iff_lifting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Warfield.lean, line 163.

For a commutative ring R and an R-module P, P is a direct summand of a direct sum of modules R / f R if and only if every linear map from P lifts along every short exact sequence 0 → A → B → C → 0 satisfying f A = A ∩ f B for all f ∈ R.

theorem summand_sum_cyclic_iff_lifting
    (R : Type u) [CommRing R] (P : Type v) [AddCommGroup P] [Module R P] :
    IsSummandOfSumCyclic R P ↔ LiftingProperty R P

Tag 0ASN, a lemma

Tag 0ASN in the Stacks Project.

generalizedValuationRing_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Generalized.lean, line 107.

For a nonzero commutative ring, total divisibility, being a local Bézout ring, and total inclusion of ideals are equivalent. In particular, all three properties hold for a valuation ring.

theorem generalizedValuationRing_tfae (R : Type u) [CommRing R] [Nontrivial R] :
    List.TFAE
        [@Std.Total R (· ∣ ·),
          IsBezout R ∧ IsLocalRing R,
          @Std.Total (Ideal R) (· ≤ ·)] ∧
      (∀ [IsDomain R] [ValuationRing R],
        @Std.Total R (· ∣ ·) ∧
          (IsBezout R ∧ IsLocalRing R) ∧
          @Std.Total (Ideal R) (· ≤ ·))

Tag 0ASP, a lemma

Tag 0ASP in the Stacks Project.

finitePresentation_equiv_directSum_quotient_span_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Generalized.lean, line 407.

Every finitely presented module over a local Bézout ring is isomorphic to a finite direct sum of quotients by principal ideals.

theorem finitePresentation_equiv_directSum_quotient_span_singleton
    (R : Type u) [CommRing R] [IsBezout R] [IsLocalRing R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.FinitePresentation R M] :
    ∃ (n : ℕ) (f : Fin n → R),
      Nonempty (M ≃ₗ[R] ⨁ i : Fin n, R ⧸ Ideal.span {f i})

Tag 0ASQ, a lemma

Tag 0ASQ in the Stacks Project.

finitePresentation_summand_fin_directSum_quotient_span_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Valuation/Generalized.lean, line 652.

Every finitely presented module over a commutative ring whose localizations at maximal ideals are Bézout rings is a direct summand of a finite direct sum of quotients by principal ideals.

theorem finitePresentation_summand_fin_directSum_quotient_span_singleton
    (R : Type u) [CommRing R]
    (hR : ∀ (m : Ideal R) [m.IsMaximal], IsBezout (Localization.AtPrime m))
    (M : Type v) [AddCommGroup M] [Module R M] [Module.FinitePresentation R M] :
    ∃ (n : ℕ) (f : Fin n → R)
      (i : M →ₗ[R] ⨁ j, R ⧸ Ideal.span {f j})
      (p : (⨁ j, R ⧸ Ideal.span {f j}) →ₗ[R] M),
      p.comp i = LinearMap.id

Tag 0ASR, a definition

Tag 0ASR in the Stacks Project.

IsElementaryDivisorDomain, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ElementaryDivisorDomain.lean, line 90. The tag is given by the attribute command at StacksFrontier/RingTheory/ElementaryDivisorDomain.lean, line 101. The attribute's comment: “(2) An elementary divisor domain: every rectangular matrix with at least one row and one column can be brought into Smith normal form by invertible row and column operations.”.

R is an elementary divisor domain if for all n, m ≥ 1 and every n × m matrix A there exist invertible matrices U (size n) and V (size m) such that U * A * V is in Smith normal form.

class IsElementaryDivisorDomain (R : Type*) [CommRing R] : Prop

Declarations registered for the tag:

IsBezout registered with add_to_stacks in StacksFrontier/RingTheory/ElementaryDivisorDomain.lean, line 97 (StacksFrontier): “(1) A Bézout domain: every finitely generated ideal is principal.”.

Tag 0ASS, a lemma

Tag 0ASS in the Stacks Project.

isBezout_of_isElementaryDivisorDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ElementaryDivisorDomain.lean, line 164.

Stacks 0ASS. Every elementary divisor domain is a Bézout ring: if R is an elementary divisor domain, then every finitely generated ideal of R is principal (IsBezout R).

theorem isBezout_of_isElementaryDivisorDomain {R : Type*} [CommRing R]
    [IsElementaryDivisorDomain R] : IsBezout R

Tag 0AST, a lemma

Tag 0AST in the Stacks Project.

isBezout_localization_and_valuationRing_atPrime_and_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ElementaryDivisorDomain/Bezout.lean, line 70.

Localizations of a Bézout domain are Bézout, its local rings are valuation rings, and an arbitrary local domain is Bézout if and only if it is a valuation ring.

theorem isBezout_localization_and_valuationRing_atPrime_and_iff
    {R Rₘ A : Type*} [CommRing R] [IsDomain R] [IsBezout R]
    (M : Submonoid R) [CommRing Rₘ] [Algebra R Rₘ] [IsLocalization M Rₘ]
    (p : Ideal R) [p.IsPrime]
    [CommRing A] [IsDomain A] [IsLocalRing A] :
    IsBezout Rₘ ∧
      ValuationRing (Localization.AtPrime p) ∧
      (IsBezout A ↔ ValuationRing A)

Tag 0ASU, a lemma

Tag 0ASU in the Stacks Project.

finite_submodule_free_and_finitePresentation_split_torsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ElementaryDivisorDomain/Bezout.lean, line 455.

Over a Bézout domain, finite submodules of free modules are free. Every finitely presented module splits as the direct sum of its finite free torsion quotient and its torsion submodule, which is itself a summand of a finite direct sum of quotients by nonzero principal ideals.

theorem finite_submodule_free_and_finitePresentation_split_torsion
    (R : Type u) [CommRing R] [IsDomain R] [IsBezout R] :
    (∀ (F : Type v) [AddCommGroup F] [Module R F] [Module.Free R F]
      (N : Submodule R F) [Module.Finite R N], Module.Free R N) ∧
    (∀ (M : Type w) [AddCommGroup M] [Module R M] [Module.FinitePresentation R M],
      Module.Finite R (M ⧸ Submodule.torsion R M) ∧
      Module.Free R (M ⧸ Submodule.torsion R M) ∧
      Nonempty (M ≃ₗ[R] (M ⧸ Submodule.torsion R M) × Submodule.torsion R M) ∧
      ∃ (n : ℕ) (f : Fin n → R),
        (∀ j, f j ≠ 0) ∧
        ∃ (i : Submodule.torsion R M →ₗ[R] ⨁ j, R ⧸ Ideal.span {f j})
          (p : (⨁ j, R ⧸ Ideal.span {f j}) →ₗ[R] Submodule.torsion R M),
          p.comp i = LinearMap.id)

Tag 0ASV, a lemma

Tag 0ASV in the Stacks Project.

finite_equiv_free_prod_directSum_quotient_span_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ElementaryDivisorDomain/PID.lean, line 41.

Stacks 0ASV. Every finite module over a principal ideal domain is isomorphic to the direct sum of a finite-rank free module and finitely many cyclic modules defined by nonzero elements.

theorem finite_equiv_free_prod_directSum_quotient_span_singleton
    (R : Type u) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    ∃ (r n : ℕ) (f : Fin n → R),
      (∀ i, f i ≠ 0) ∧
        Nonempty (M ≃ₗ[R] (Fin r →₀ R) × ⨁ i : Fin n, R ⧸ Ideal.span {f i})

Tag 0ASW, a lemma

Tag 0ASW in the Stacks Project.

bezout_unimodular_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ElementaryDivisorDomain.lean, line 313.

Stacks 0ASW. Over a Bézout domain R, any row f : Fin n → R whose entries generate the unit ideal is the first row of some invertible n × n matrix over R.

theorem bezout_unimodular_completion {R : Type*} [CommRing R] [IsBezout R] [IsDomain R]
    {n : ℕ} [NeZero n] (f : Fin n → R)
    (hf : Ideal.span (Set.range f) = ⊤) :
    ∃ M : Matrix (Fin n) (Fin n) R, IsUnit M.det ∧ ∀ j : Fin n, M 0 j = f j

Sources

Leansummand_sum_cyclic_iff_lifting · generalizedValuationRing_tfae · finitePresentation_equiv_directSum_quotient_span_singleton · finitePresentation_summand_fin_directSum_quotient_span_singleton · IsElementaryDivisorDomain · IsBezout · isBezout_of_isElementaryDivisorDomain · isBezout_localization_and_valuationRing_atPrime_and_iff

Section15.127 Principal radical ideals #

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

Tag 0BWS, a lemma

Tag 0BWS in the Stacks Project.

length_quotient_span_pow_le_and_eq_of_mem_nonZeroDivisors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/PrincipalRadical/Length.lean, line 152. References: EGA IV (21.10.13), “(i) for M=A”.

Stacks 0BWS. The quotients by powers of a parameter in a one-dimensional Noetherian local ring have finite length. Their lengths grow at most linearly, and grow exactly linearly when the parameter is a non-zero-divisor.

theorem length_quotient_span_pow_le_and_eq_of_mem_nonZeroDivisors
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (hdim : ringKrullDim R = 1) {x : R}
    (hx : x ∈ IsLocalRing.maximalIdeal R)
    (hx_min : ∀ p ∈ minimalPrimes R, x ∉ p) :
    let P : ℕ → ℕ∞ := fun n ↦ Module.length R (R ⧸ Ideal.span {x ^ n})
    (∀ n, P n ≠ ⊤) ∧
      (∀ n, P n ≤ (n : ℕ∞) * P 1) ∧
      (x ∈ nonZeroDivisors R → ∀ n, P n = (n : ℕ∞) * P 1)

Tag 0BWT, a lemma

Tag 0BWT in the Stacks Project.

natCard_minimalPrimes_le_length_quotient_span_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/PrincipalRadical/Length.lean, line 392.

Stacks 0BWT. The number of minimal primes of a one-dimensional Noetherian local ring is at most the length of its quotient by a parameter avoiding all minimal primes.

theorem natCard_minimalPrimes_le_length_quotient_span_singleton
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (hdim : ringKrullDim R = 1) {x : R}
    (hx : x ∈ IsLocalRing.maximalIdeal R)
    (hx_min : ∀ p ∈ minimalPrimes R, x ∉ p) :
    Module.length R (R ⧸ Ideal.span {x}) ≠ ⊤ ∧
      (Nat.card (minimalPrimes R) : ℕ∞) ≤ Module.length R (R ⧸ Ideal.span {x})

Tag 0BWU, a lemma

Tag 0BWU in the Stacks Project.

exists_isSystemOfParameters_cons_of_avoids_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/PrincipalRadical/SystemOfParameters.lean, line 176.

Stacks 0BWU. In a Noetherian local ring of dimension d > 1, an element f of the maximal ideal which belongs to no minimal prime extends to a system of parameters f, g₁, ..., g_{d-1}, with every gᵢ lying in the prescribed power m ^ k.

theorem exists_isSystemOfParameters_cons_of_avoids_minimalPrimes
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (d : ℕ) (hdim : ringKrullDim R = d) (hd : 1 < d)
    (f : R) (hf : f ∈ maximalIdeal R)
    (hfmin : ∀ p ∈ minimalPrimes R, f ∉ p) (k : ℕ) :
    ∃ gs : List R,
      gs.length = d - 1 ∧
        (∀ g ∈ gs, g ∈ maximalIdeal R ^ k) ∧
          IsSystemOfParameters (f :: gs)

Tag 0BWV, a lemma

Tag 0BWV in the Stacks Project.

exists_isSystemOfParameters_pair_add_of_avoids_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/PrincipalRadical/SystemOfParameters.lean, line 255.

Stacks 0BWV. In a two-dimensional Noetherian local ring, an element f of the maximal ideal which belongs to no minimal prime can be completed by an element g to a system of parameters. For every sufficiently high-order perturbation f + h, the pair f + h, g remains a system of parameters and defines a quotient of the same length as the quotient defined by f, g.

theorem exists_isSystemOfParameters_pair_add_of_avoids_minimalPrimes
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (hdim : ringKrullDim R = 2) (f : R) (hf : f ∈ maximalIdeal R)
    (hfmin : ∀ p ∈ minimalPrimes R, f ∉ p) :
    ∃ g ∈ maximalIdeal R, ∃ N : ℕ,
      IsSystemOfParameters [f, g] ∧
        ∀ h ∈ maximalIdeal R ^ N,
          IsSystemOfParameters [f + h, g] ∧
            Module.length R (R ⧸ Ideal.ofList [f, g]) =
              Module.length R (R ⧸ Ideal.ofList [f + h, g])

Tag 0AXH, a lemma

Tag 0AXH in the Stacks Project.

exists_nonzero_mem_isReduced_quotient_of_height_one_primes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/PrincipalRadical/Basic.lean, line 661.

Stacks 0AXH. In a two-dimensional Noetherian normal local domain, finitely many height-one prime ideals contain a common nonzero element whose principal quotient is reduced.

theorem exists_nonzero_mem_isReduced_quotient_of_height_one_primes
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [IsDomain R]
    [IsIntegrallyClosed R] (hdim : ringKrullDim R = 2) (primes : Finset (Ideal R))
    (hprimes : ∀ p ∈ primes, p.IsPrime ∧ p.height = 1) :
    ∃ f : R, f ≠ 0 ∧ (∀ p ∈ primes, f ∈ p) ∧ IsReduced (R ⧸ Ideal.span {f})

Tag 0AXI, a lemma

Tag 0AXI in the Stacks Project.

exists_isReduced_quotient_and_dvd_pow, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/PrincipalRadical/Basic.lean, line 742.

Stacks 0AXI. In a two-dimensional Noetherian normal local domain, every nonzero element of the maximal ideal divides a power of an element whose principal quotient is reduced.

lemma exists_isReduced_quotient_and_dvd_pow
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [IsDomain R]
    [IsIntegrallyClosed R] (hdim : ringKrullDim R = 2) {a : R}
    (_ha : a ∈ IsLocalRing.maximalIdeal R) (ha0 : a ≠ 0) :
    ∃ c : R, IsReduced (R ⧸ Ideal.span {c}) ∧ ∃ n : ℕ, a ∣ c ^ n

Tag 0BWW, a lemma

Tag 0BWW in the Stacks Project.

multiplicity_le_length_quotient_of_isSystemOfParameters, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/PrincipalRadical/Length.lean, line 672.

Stacks 0BWW. If I is generated by a system of parameters and the leading coefficient of its Hilbert–Samuel polynomial is e / d!, then e ≤ length_R(R / I).

theorem multiplicity_le_length_quotient_of_isSystemOfParameters
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    {gs : List R} (hgs : IsSystemOfParameters gs) {P : ℚ[X]}
    (hP : HilbertSamuel.IsHilbertSamuelPoly (Ideal.ofList gs) R P) {e : ℕ}
    (hlead : P.leadingCoeff = (e : ℚ) / gs.length.factorial) :
    (e : ℕ∞) ≤ Module.length R (R ⧸ Ideal.ofList gs)

Tag 0BWX, a lemma

Tag 0BWX in the Stacks Project.

natCard_fullDimensionalMinimalPrimes_le_length_quotient_of_isSystemOfParameters, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/PrincipalRadical/Length.lean, line 1195.

Stacks 0BWX. In a Noetherian local ring, the number of minimal primes whose quotient has the full dimension of the ring is at most the length of the quotient by a system of parameters.

theorem natCard_fullDimensionalMinimalPrimes_le_length_quotient_of_isSystemOfParameters
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    {gs : List R} (hgs : IsSystemOfParameters gs) :
    Module.length R (R ⧸ Ideal.ofList gs) ≠ ⊤ ∧
      (Nat.card {p : Ideal R // p ∈ minimalPrimes R ∧
        ringKrullDim (R ⧸ p) = ringKrullDim R} : ℕ∞) ≤
        Module.length R (R ⧸ Ideal.ofList gs)

Tag 0BWY, a lemma

Tag 0BWY in the Stacks Project.

exists_isSystemOfParameters_cons_stable_under_add_of_avoids_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/PrincipalRadical/SystemOfParameters.lean, line 280.

Stacks 0BWY. A parameter in the maximal ideal of a Noetherian local ring which avoids all minimal primes can be completed to a system of parameters such that perturbing the parameter by an element of a sufficiently high power of the maximal ideal preserves both the parameter system and the length of its quotient.

theorem exists_isSystemOfParameters_cons_stable_under_add_of_avoids_minimalPrimes
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (d : ℕ) (hdim : ringKrullDim R = d)
    (f : R) (hf : f ∈ maximalIdeal R)
    (hfmin : ∀ p ∈ minimalPrimes R, f ∉ p) :
    ∃ gs : List R, ∃ N : ℕ,
      gs.length = d - 1 ∧
        (∀ g ∈ gs, g ∈ maximalIdeal R) ∧
          IsSystemOfParameters (f :: gs) ∧
            ∀ h ∈ maximalIdeal R ^ N,
              IsSystemOfParameters ((f + h) :: gs) ∧
                Module.length R (R ⧸ Ideal.ofList (f :: gs)) =
                  Module.length R (R ⧸ Ideal.ofList ((f + h) :: gs))

Tag 0BWZ, a proposition

Tag 0BWZ in the Stacks Project.

exists_nonzero_mem_isReduced_quotient_of_isRadical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/PrincipalRadical/Basic.lean, line 1304.

Stacks 0BWZ. A nonzero radical ideal in a catenary Noetherian local normal domain contains a nonzero element whose principal quotient is reduced.

theorem exists_nonzero_mem_isReduced_quotient_of_isRadical
    {R : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [IsDomain R]
    [IsIntegrallyClosed R] (hcat : Ring.IsCatenary R) (J : Ideal R) (hJ : J.IsRadical)
    (hJne : J ≠ ⊥) :
    ∃ f : R, f ≠ 0 ∧ f ∈ J ∧ IsReduced (R ⧸ Ideal.span {f})

Sources

Leanlength_quotient_span_pow_le_and_eq_of_mem_nonZeroDivisors · natCard_minimalPrimes_le_length_quotient_span_singleton · exists_isSystemOfParameters_cons_of_avoids_minimalPrimes · exists_isSystemOfParameters_pair_add_of_avoids_minimalPrimes · exists_nonzero_mem_isReduced_quotient_of_height_one_primes · exists_isReduced_quotient_and_dvd_pow · multiplicity_le_length_quotient_of_isSystemOfParameters · natCard_fullDimensionalMinimalPrimes_le_length_quotient_of_isSystemOfParameters

Section15.128 Invertible objects in the derived category #

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

Tag 0FNQ, a lemma

Tag 0FNQ in the Stacks Project.

DerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/Monoidal/Basic.lean, line 471.

Stacks 0FNQ. The derived category of modules over a commutative ring is symmetric monoidal under derived tensor product. Under the canonical comparison with tensor products of K-flat representatives, its associator is induced by the ordinary associator of complexes, and its braiding is the canonical Koszul symmetry.

public theorem derivedCategory_symmetricMonoidalCategory (R : Type u) [CommRing R] :
    let D := DerivedCategory (ModuleCat.{u} R)
    let C := CochainComplex (ModuleCat.{u} R) ℤ
    let Q := DerivedCategory.Q (C := ModuleCat.{u} R)
    let T := CochainComplex.DerivedTensor.canonicalSymmetricDerivedTensorProduct R
    ∃ m : MonoidalCategory D,
      letI := m
      ∃ s : SymmetricCategory D,
        letI := s
        ∃ e : curriedTensor D ≅ T.tensorProduct.tensor,
          (∀ K L : D,
              (β_ K L).hom ≫ ((e.app L).app K).hom =
                ((e.app K).app L).hom ≫ ((T.braiding.iso.app K).app L).hom) ∧
            ∀ (K L M : C) (hK : K.KFlat) (hL : L.KFlat) (hM : M.KFlat)
                (hKL : (K ⊗ L).KFlat) (hLM : (L ⊗ M).KFlat),
              let comparison : ∀ (A B : C), A.KFlat → B.KFlat →
                  (Q.obj A ⊗ Q.obj B ⟶ Q.obj (A ⊗ B)) :=
                fun A B hA hB =>
                  ((e.app (Q.obj A)).app (Q.obj B)).hom ≫
                    (T.tensorProduct.comparison A B hA hB).hom
              (α_ (Q.obj K) (Q.obj L) (Q.obj M)).hom ≫
                    (Q.obj K ◁ comparison L M hL hM) ≫
                    comparison K (L ⊗ M) hK hLM =
                ((comparison K L hK hL :
                    Q.obj K ⊗ Q.obj L ⟶ Q.obj (K ⊗ L)) ▷ Q.obj M) ≫
                  comparison (K ⊗ L) M hKL hM ≫
                  Q.map (HomologicalComplex.associator K L M).hom

Tag 0FNR, a lemma

Tag 0FNR in the Stacks Project.

exists_subcomplex_bounded_finiteFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/FiniteFreeSubcomplex.lean, line 357.

Stacks Tag 0FNR (Lemma 15.128.2). Let R be a ring and let F be a bounded above complex of free R-modules. Given a finite family of pairs (n i, f i) (indexed by i : Fin N), with n i ∈ ℤ and f i ∈ F^{n i}, there exists a subcomplex G ⊆ F such that: 1. f i ∈ G^{n i} for every i (i.e. G contains all the f i); 2. G is bounded; and 3. G consists of finite free R-modules.

theorem exists_subcomplex_bounded_finiteFree (F : ZComplex R) (hFa : F.BoundedAbove) (hFfree :
  F.IsFree)
    {N : ℕ} (n : Fin N → ℤ) (f : ∀ i, F.obj (n i)) :
    ∃ G : F.Subcomplex,
      (∀ i, f i ∈ G.carrier (n i)) ∧ G.Bounded ∧ G.FiniteFree

Tag 0FNS, a lemma

Tag 0FNS in the Stacks Project.

DerivedCategory.Invertible.isPerfect_iff_exists_leftDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/Monoidal/Dual.lean, line 1161.

Stacks 0FNS. An object of the derived category has a left dual exactly when it is perfect. For a perfect object the derived dual RHom(M, R) is a left dual, and every other left dual is isomorphic to it.

public theorem isPerfect_iff_exists_leftDual
    (M : DerivedCategory (ModuleCat.{max u v} (ULift.{v} R))) :
    ((∃ N : DerivedCategory (ModuleCat.{max u v} (ULift.{v} R)),
        Nonempty (DerivedLeftDualPairing M N)) ↔
        IsPerfect M) ∧
      (IsPerfect M →
        Nonempty (DerivedLeftDualPairing M (derivedDual M))) ∧
      (∀ (N : DerivedCategory (ModuleCat.{max u v} (ULift.{v} R))),
        DerivedLeftDualPairing M N →
        Nonempty (N ≅ derivedDual M))

Tag 0FNT, a lemma

Tag 0FNT in the Stacks Project.

DerivedCategory.Invertible.isInvertible_iff_locallyShiftedUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/Monoidal/Invertible.lean, line 1096.

Stacks 0FNT. A derived object is invertible if and only if it is locally a shift of the ring. In that case it is perfect, is the direct sum of its cohomology modules, every cohomology module is finite projective, and those modules are invertible on the factors of a finite product decomposition of the ring.

public theorem isInvertible_iff_locallyShiftedUnit
    (M : DerivedCategory (ModuleCat.{u} R)) :
    let derivedMonoidal := (derivedCategory_symmetricMonoidalCategory R).choose
    letI := derivedMonoidal
    (MonoidalCategory.IsInvertible M ↔ IsLocallyShiftedUnit M) ∧
      (MonoidalCategory.IsInvertible M →
        StacksDraft.Perfect.IsPerfect M ∧
          SplitsAsCohomology M ∧
          (∀ n : ℤ,
            Module.Finite R
                ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) n).obj M) ∧
              Module.Projective R
                ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) n).obj M)) ∧
          HasInvertibleCohomologyDecomposition M)

Sources

LeanDerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory · exists_subcomplex_bounded_finiteFree · DerivedCategory.Invertible.isPerfect_iff_exists_leftDual · DerivedCategory.Invertible.isInvertible_iff_locallyShiftedUnit

Section15.129 Splitting off a free module #

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

Tag 0GV8, a situation

Tag 0GV8 in the Stacks Project.

ClosedPointSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/SplitFree/Fibres.lean, line 83.

The space of closed points of the prime spectrum of R, with its induced topology.

abbrev ClosedPointSpace (R : Type u) [CommRing R]

ClosedPointResidueField, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/SplitFree/Fibres.lean, line 88.

The residue field at a closed point x of Spec(R).

abbrev ClosedPointResidueField {R : Type u} [CommRing R] (x : ClosedPointSpace R)

ClosedPointFiber, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/SplitFree/Fibres.lean, line 105.

The fibre M(x) = M / xM of an R-module at a closed point x.

abbrev ClosedPointFiber {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M]
    (x : ClosedPointSpace R)

sectionAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/SplitFree/Fibres.lean, line 111.

The canonical image s(x) of a module element s in the fibre at x.

abbrev sectionAt {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
    (x : ClosedPointSpace R) (s : M) : ClosedPointFiber M x

finiteDimensional_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/SplitFree/Fibres.lean, line 118.

The fibre of a finite module at a closed point is finite-dimensional over the residue field at that point.

theorem finiteDimensional_fiber
    {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
    [Module.Finite R M] (x : ClosedPointSpace R) :
    FiniteDimensional (ClosedPointResidueField x) (ClosedPointFiber M x)

Tag 0GV9, a lemma

Tag 0GV9 in the Stacks Project.

canonicalKernel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/SplitFree/Fibres.lean, line 154.

The canonical subspace B(x) of the fibre: the common kernel of all fibre functionals induced by R-linear maps M → R.

noncomputable def canonicalKernel {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M] (x : ClosedPointSpace R) :
    Submodule (ClosedPointResidueField x) (ClosedPointFiber M x)

CanonicalQuotient, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/SplitFree/Fibres.lean, line 169.

The canonical quotient V(x) = M(x) / B(x).

abbrev CanonicalQuotient {R : Type u} [CommRing R]
    (M : Type v) [AddCommGroup M] [Module R M] (x : ClosedPointSpace R)

canonical_exact_and_splits_iff_linearIndependent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/SplitFree/Fibres.lean, line 368. References: EGA 0 (5.5.5), “affine case, closed pt”.

The canonical sequence 0 → B(x) → M(x) → V(x) → 0 is short exact. Moreover, a finite family of elements of M splits off a free direct summand after inverting an element outside x if and only if its images in V(x) are linearly independent.

theorem canonical_exact_and_splits_iff_linearIndependent
    {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
    [Module.FinitePresentation R M] (x : ClosedPointSpace R) :
    Function.Injective (canonicalKernel M x).subtype ∧
      Function.Exact (canonicalKernel M x).subtype (canonicalKernel M x).mkQ ∧
      Function.Surjective (canonicalKernel M x).mkQ ∧
      ∀ (r : ℕ) (s : Fin r → M),
        (∃ f : R, f ∉ x.1.asIdeal ∧ SplitsAfterInverting f s) ↔
          LinearIndependent (ClosedPointResidueField x)
            (fun i ↦ (canonicalKernel M x).mkQ (sectionAt x (s i)))

Tag 0GVA, a lemma

Tag 0GVA in the Stacks Project.

pi_canonicalQuotient_mkQ_sectionAt_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/SplitFree/Fibres.lean, line 390.

At finitely many distinct closed points, every family of values in the canonical quotients V(x) is induced by a single element of the module.

theorem pi_canonicalQuotient_mkQ_sectionAt_surjective
    {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
    {ι : Type w} [Finite ι] (x : ι → ClosedPointSpace R) (hx : Function.Injective x) :
    Function.Surjective fun s : M ↦
      fun i ↦ (canonicalKernel M (x i)).mkQ (sectionAt (x i) s)

Tag 0GVB, a proposition

Tag 0GVB in the Stacks Project.

exists_section_dependentLocus_subset_union_of_card_add_le_finrank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/SplitFree/Basic.lean, line 348.

Suppose that the dependent locus of h sections of a finitely presented module is contained in a closed set F of the Noetherian space of closed points. If every canonical quotient V(y) has dimension at least h + k, then one can choose a further section with arbitrary prescribed values at finitely many distinct points of F. The new dependent locus is contained in F together with a closed set all of whose irreducible components have codimension at least k.

theorem exists_section_dependentLocus_subset_union_of_card_add_le_finrank
    {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
    [Module.FinitePresentation R M] [NoetherianSpace (ClosedPointSpace R)]
    {h k : ℕ} (sections : Fin h → M) (F : Set (ClosedPointSpace R)) (hF : IsClosed F)
    (hsections :
      {y | ¬LinearIndependent (ClosedPointResidueField y)
        (fun i ↦ (canonicalKernel M y).mkQ (sectionAt y (sections i)))} ⊆ F)
    {ι : Type w} [Finite ι] (x : ι → ClosedPointSpace R) (hx : Function.Injective x)
    (hxF : ∀ i, x i ∈ F) (v : ∀ i, CanonicalQuotient M (x i))
    (hdim : ∀ y : ClosedPointSpace R,
      h + k ≤ Module.finrank (ClosedPointResidueField y) (CanonicalQuotient M y)) :
    ∃ (s : M) (F' : Set (ClosedPointSpace R)),
      (∀ i, (canonicalKernel M (x i)).mkQ (sectionAt (x i) s) = v i) ∧
        IsClosed F' ∧
        {y | ¬LinearIndependent (ClosedPointResidueField y)
          (fun i ↦ (canonicalKernel M y).mkQ
            (sectionAt y ((Fin.snoc sections s : Fin (h + 1) → M) i)))} ⊆ F ∪ F' ∧
        ∀ Z : IrreducibleCloseds (ClosedPointSpace R),
          Maximal (fun W : IrreducibleCloseds (ClosedPointSpace R) ↦
            (W : Set (ClosedPointSpace R)) ⊆ F') Z →
            (k : ℕ∞) ≤ codimension Z

Tag 0GVC, a theorem

Tag 0GVC in the Stacks Project.

exists_linearEquiv_prod_of_local_free_summand_rank_gt_dimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Projective/SplitFree/Basic.lean, line 716.

Let M be a finitely presented module over a commutative ring whose Noetherian space of closed points has dimension at most d. If at every closed point the localization of M has a free direct summand of some rank strictly greater than d, then a rank-one free summand splits from M.

theorem exists_linearEquiv_prod_of_local_free_summand_rank_gt_dimension
    {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
    [Module.FinitePresentation R M] [NoetherianSpace (ClosedPointSpace R)]
    (d : ℕ) (hdim : topologicalKrullDim (ClosedPointSpace R) ≤ (d : WithBot ℕ∞))
    (hlocal : ∀ x : ClosedPointSpace R,
      ∃ r : ℕ, d < r ∧
        ∃ s : Fin r → LocalizedModule x.1.asIdeal.primeCompl M,
          ∃ p : LocalizedModule x.1.asIdeal.primeCompl M →ₗ[Localization x.1.asIdeal.primeCompl]
              (Fin r → Localization x.1.asIdeal.primeCompl),
            p.comp (Fintype.linearCombination (Localization x.1.asIdeal.primeCompl) s) =
              LinearMap.id) :
    ∃ N : Submodule R M, Nonempty (M ≃ₗ[R] R × N)

Sources

LeanClosedPointSpace · ClosedPointResidueField · ClosedPointFiber · sectionAt · finiteDimensional_fiber · canonicalKernel · CanonicalQuotient · canonical_exact_and_splits_iff_linearIndependent

Section15.130 Big projective modules are free #

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

Tag 0GVF, a lemma

Tag 0GVF in the Stacks Project.

eilenberg_swindle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/EilenbergSwindle.lean, line 81.

Eilenberg's lemma / Eilenberg swindle (Stacks Tag 0GVF). Let R be a ring and P, Q, F left R-modules with P ⊕ Q ≅ F, where F is a free left R-module that is not finitely generated. Then P ⊕ F ≅ F.

theorem eilenberg_swindle {R : Type*} [Ring R] (P Q F : Type*) [AddCommGroup P] [Module R P]
    [AddCommGroup Q] [Module R Q] [AddCommGroup F] [Module R F] [Module.Free R F]
    (h : Nonempty ((P × Q) ≃ₗ[R] F)) (hnfg : ¬ Module.Finite R F) :
    Nonempty ((P × F) ≃ₗ[R] F)

Tag 0GVG, a lemma

Tag 0GVG in the Stacks Project.

exists_free_prod_of_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/EilenbergSwindle/BigProjective.lean, line 107.

A projective module is a direct summand of a free module with a free complementary summand.

theorem exists_free_prod_of_projective
    {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P]
    [Module.Projective R P] :
    ∃ (F : Type (max u v)) (_ : AddCommGroup F) (_ : Module R F)
      (_ : Module.Free R F), Module.Free R (P × F)

Tag 0GVH, a lemma

Tag 0GVH in the Stacks Project.

exists_finite_free_summand_containing_zero_prod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/EilenbergSwindle/BigProjective.lean, line 258.

For an element s of a projective module P, there is a finite free module F and a finite free direct summand of F × P containing (0, s).

theorem exists_finite_free_summand_containing_zero_prod
    {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P]
    [Module.Projective R P] (s : P) :
    ∃ (F : Type (max u v)) (_ : AddCommGroup F) (_ : Module R F)
      (_ : Module.Finite R F) (_ : Module.Free R F),
      ∃ (K : Submodule R (F × P)) (_ : Module.Finite R K) (_ : Module.Free R K),
        (0, s) ∈ K ∧ ∃ K' : Submodule R (F × P), IsCompl K K'

Tag 0GVI, a lemma

Tag 0GVI in the Stacks Project.

exists_mem_add_unimodular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/EilenbergSwindle/BigProjective.lean, line 637.

If P is projective and has infinite rank after localization at every maximal ideal, then an element which generates P together with M can be modified by an element of M to become unimodular.

theorem exists_mem_add_unimodular
    {R : Type u} [CommRing R] {P : Type v} [AddCommGroup P] [Module R P]
    [Module.Projective R P] (M : Submodule R P) (s : P)
    (hR : IsNoetherianRing (R ⧸ Ideal.jacobson (⊥ : Ideal R)))
    (hP : ∀ p : MaximalSpectrum R,
      ¬ Module.Finite (Localization.AtPrime p.asIdeal)
        (LocalizedModule p.asIdeal.primeCompl P))
    (hspan : Submodule.span R {s} ⊔ M = ⊤) :
    ∃ m ∈ M, ∃ φ : P →ₗ[R] R, φ (s + m) = 1

Tag 0GVJ, a lemma

Tag 0GVJ in the Stacks Project.

exists_finite_isStablyFree_summand_containing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/EilenbergSwindle/BigProjective.lean, line 1142.

Every element of a projective module of infinite rank at all maximal ideals lies in a finite stably free direct summand, provided the quotient by the Jacobson radical is Noetherian.

theorem exists_finite_isStablyFree_summand_containing
    {R : Type u} [CommRing R] {P : Type v} [AddCommGroup P] [Module R P]
    [Module.Projective R P] (s : P)
    (hR : IsNoetherianRing (R ⧸ Ideal.jacobson (⊥ : Ideal R)))
    (hP : ∀ p : MaximalSpectrum R,
      ¬ Module.Finite (Localization.AtPrime p.asIdeal)
        (LocalizedModule p.asIdeal.primeCompl P)) :
    ∃ M : Submodule R P,
      Module.Finite R M ∧ Module.IsStablyFree R M ∧ s ∈ M ∧
        ∃ M' : Submodule R P, IsCompl M M'

Tag 0GVK, a theorem

Tag 0GVK in the Stacks Project.

free_of_countablyGenerated_projective_of_localization_not_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/EilenbergSwindle/BigProjective.lean, line 1341.

A countably generated projective module over a commutative ring is free if the quotient by the Jacobson radical is Noetherian and every localization at a maximal ideal has infinite rank.

theorem free_of_countablyGenerated_projective_of_localization_not_finite
    {R : Type u} [CommRing R] {P : Type v} [AddCommGroup P] [Module R P]
    [Module.Projective R P]
    (hR : IsNoetherianRing (R ⧸ Ideal.jacobson (⊥ : Ideal R)))
    (hP : Module.CountablyGenerated R P)
    (hPinf : ∀ p : MaximalSpectrum R,
      ¬ Module.Finite (Localization.AtPrime p.asIdeal)
        (LocalizedModule p.asIdeal.primeCompl P)) :
    Module.Free R P

Sources

Leaneilenberg_swindle · exists_free_prod_of_projective · exists_finite_free_summand_containing_zero_prod · exists_mem_add_unimodular · exists_finite_isStablyFree_summand_containing · free_of_countablyGenerated_projective_of_localization_not_finite

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

15.123 A regular local ring is… to 15.130 Big projective modules…

Section15.123 A regular local ring is a UFD#

Tag 0AFZ, a lemma

Tag 0AG0, a lemma

Tag 0DLQ, a lemma

Sources

Section15.124 Determinants of complexes#

Tag 0FJJ, a lemma

Tag 0FJK, a lemma

Tag 0FJL, a lemma

Tag 0FJM, a lemma

Sources

Section15.125 Extensions of valuation rings#

Tag 0ASG, a definition

Tag 0ASH, a lemma

Tag 0H37, a lemma

Tag 0ASI, a lemma

Tag 0ASJ, a lemma

Tag 0ASK, a lemma

Sources

Section15.126 Structure of modules over a PID#

Tag 0ASM, a lemma

Tag 0ASN, a lemma

Tag 0ASP, a lemma

Tag 0ASQ, a lemma

Tag 0ASR, a definition

Tag 0ASS, a lemma

Tag 0AST, a lemma

Tag 0ASU, a lemma

Tag 0ASV, a lemma

Tag 0ASW, a lemma

Sources

Section15.127 Principal radical ideals#

Tag 0BWS, a lemma

Tag 0BWT, a lemma

Tag 0BWU, a lemma

Tag 0BWV, a lemma

Tag 0AXH, a lemma

Tag 0AXI, a lemma

Tag 0BWW, a lemma

Tag 0BWX, a lemma

Tag 0BWY, a lemma

Tag 0BWZ, a proposition

Sources

Section15.128 Invertible objects in the derived category#

Tag 0FNQ, a lemma

Tag 0FNR, a lemma

Tag 0FNS, a lemma

Tag 0FNT, a lemma

Sources

Section15.129 Splitting off a free module#

Tag 0GV8, a situation

Tag 0GV9, a lemma

Tag 0GVA, a lemma

Tag 0GVB, a proposition

Tag 0GVC, a theorem

Sources

Section15.130 Big projective modules are free#

Tag 0GVF, a lemma

Tag 0GVG, a lemma

Tag 0GVH, a lemma

Tag 0GVI, a lemma

Tag 0GVJ, a lemma

Tag 0GVK, a theorem

Sources

Section15.123 A regular local ring is a UFD #

Section15.124 Determinants of complexes #

Section15.125 Extensions of valuation rings #

Section15.126 Structure of modules over a PID #

Section15.127 Principal radical ideals #

Section15.128 Invertible objects in the derived category #

Section15.129 Splitting off a free module #

Section15.130 Big projective modules are free #