A Noetherian Local Ring is Regular if its Maximal Ideal has Finite Projective Dimension

def QuotSMulTop_map {R : Type u} [CommRing R] (x : R) {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M →ₗ[R] N) : QuotSMulTop x M →ₗ[R ⧸ Ideal.span {x}] QuotSMulTop x N

The linear map M⧸xM →ₗ[R] N⧸xN induced by a linear map M →ₗ[R] N.

Equations

• QuotSMulTop_map x f = { toAddHom := ((x • ⊤).mapQ (x • ⊤) f ⋯).toAddHom, map_smul' := ⋯ }

theorem QuotSMulTop_map_surjective {R : Type u} [CommRing R] (x : R) {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {f : M →ₗ[R] N} (surj : Function.Surjective ⇑f) : Function.Surjective ⇑(QuotSMulTop_map x f)

theorem QuotSMulTop_map_exact {R : Type u} [CommRing R] (x : R) {M : Type u_1} {N : Type u_2} {L : Type u_3} [AddCommGroup M] [AddCommGroup N] [AddCommGroup L] [Module R M] [Module R N] [Module R L] {f : M →ₗ[R] N} {g : N →ₗ[R] L} (exact : Function.Exact ⇑f ⇑g) (surj : Function.Surjective ⇑g) : Function.Exact ⇑(QuotSMulTop_map x f) ⇑(QuotSMulTop_map x g)

theorem IsSMulRegular.of_free {R : Type u} [CommRing R] {x : R} (reg : IsSMulRegular R x) (M : Type u_1) [AddCommGroup M] [Module R M] [free : Module.Free R M] : IsSMulRegular M x

theorem projectiveDimension_eq_quotient (R : Type u) [CommRing R] [Small.{v, u} R] [IsLocalRing R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] (x : R) (reg1 : IsSMulRegular R x) (reg2 : IsSMulRegular (↑M) x) (mem : x ∈ IsLocalRing.maximalIdeal R) : CategoryTheory.projectiveDimension M = CategoryTheory.projectiveDimension (ModuleCat.of (R ⧸ Ideal.span {x}) (QuotSMulTop x ↑M))

theorem exist_isSMulRegular_of_exist_hasProjectiveDimensionLE_aux {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (nebot : IsLocalRing.maximalIdeal R ≠ ⊥) (h : ∃ (n : ℕ), CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of R (Shrink.{v, u} ↥(IsLocalRing.maximalIdeal R))) n) : ∃ x ∈ IsLocalRing.maximalIdeal R, IsSMulRegular R x

theorem exist_isSMulRegular_of_exist_hasProjectiveDimensionLE {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (nebot : IsLocalRing.maximalIdeal R ≠ ⊥) (h : ∃ (n : ℕ), CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of R (Shrink.{v, u} ↥(IsLocalRing.maximalIdeal R))) n) : ∃ x ∈ IsLocalRing.maximalIdeal R, x ∉ IsLocalRing.maximalIdeal R ^ 2 ∧ IsSMulRegular R x

theorem spanFinrank_maximalIdeal_quotient {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (x : R) (mem : x ∈ IsLocalRing.maximalIdeal R) (nmem : x ∉ IsLocalRing.maximalIdeal R ^ 2) : Submodule.spanFinrank (IsLocalRing.maximalIdeal (R ⧸ Ideal.span {x})) = Submodule.spanFinrank (IsLocalRing.maximalIdeal R) - 1

theorem generate_by_regular_aux {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (h : ∃ (n : ℕ), CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of R (Shrink.{v, u} ↥(IsLocalRing.maximalIdeal R))) n) (n : ℕ) : Submodule.spanFinrank (IsLocalRing.maximalIdeal R) = n → ∃ (rs : List R), RingTheory.Sequence.IsRegular R rs ∧ Ideal.ofList rs = IsLocalRing.maximalIdeal R

theorem generate_by_regular {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (h : ∃ (n : ℕ), CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of R (Shrink.{v, u} ↥(IsLocalRing.maximalIdeal R))) n) : ∃ (rs : List R), RingTheory.Sequence.IsRegular R rs ∧ Ideal.ofList rs = IsLocalRing.maximalIdeal R

theorem IsRegularLocalRing.of_maximalIdeal_hasProjectiveDimensionLE {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (h : ∃ (n : ℕ), CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of R (Shrink.{v, u} ↥(IsLocalRing.maximalIdeal R))) n) : IsRegularLocalRing R

theorem IsRegularLocalRing.of_globalDimension_lt_top {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (h : globalDimension R < ⊤) : IsRegularLocalRing R