Mathlib_RingTheory_RegularLocalRingQuotientRegular.lean

theorem isLocalRing_quotient_span_singleton [IsLocalRing R] {x : R}
    (hx : x ∈ maximalIdeal R) : IsLocalRing (R ⧸ Ideal.span {x})

theorem exists_span_eq_maximalIdeal_ncard_le [IsLocalRing R] [IsNoetherianRing R]
    {x : R} (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2) :
    ∃ S : Set R, x ∈ S ∧ S.Finite ∧ S.ncard ≤ (maximalIdeal R).spanFinrank ∧
      Ideal.span S = maximalIdeal R

theorem one_le_spanFinrank_maximalIdeal_of_notMem_sq [IsLocalRing R] [IsNoetherianRing R]
    {x : R} (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2) :
    1 ≤ (maximalIdeal R).spanFinrank

theorem spanFinrank_map_quotientMk_le_sub_one [IsLocalRing R] [IsNoetherianRing R]
    {x : R} (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2) :
    ((maximalIdeal R).map (Ideal.Quotient.mk (Ideal.span {x}))).spanFinrank ≤
      (maximalIdeal R).spanFinrank - 1

theorem spanFinrank_maximalIdeal_quotient_le_sub_one [IsLocalRing R] [IsNoetherianRing R]
    {x : R} [IsLocalRing (R ⧸ Ideal.span {x})]
    (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2) :
    (maximalIdeal (R ⧸ Ideal.span {x})).spanFinrank ≤ (maximalIdeal R).spanFinrank - 1

theorem ringKrullDim_lt_top_of_isNoetherianRing_of_isLocalRing
    [IsNoetherianRing R] [IsLocalRing R] : ringKrullDim R < ⊤

theorem exists_ringKrullDim_eq_natCast [IsNoetherianRing R] [IsLocalRing R] :
    ∃ d : ℕ, ringKrullDim R = (d : WithBot ℕ∞)

theorem isRegularLocalRing_quotient_and_ringKrullDim_succ_eq [IsRegularLocalRing R]
    {x : R} (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2) :
    IsRegularLocalRing (R ⧸ Ideal.span {x}) ∧
      ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem isRegularLocalRing_quotient_span_singleton [IsRegularLocalRing R]
    {x : R} (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2) :
    IsRegularLocalRing (R ⧸ Ideal.span {x})

theorem ringKrullDim_quotient_span_singleton_succ_eq [IsRegularLocalRing R]
    {x : R} (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2) :
    ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem spanFinrank_maximalIdeal_quotient_succ_eq [IsRegularLocalRing R]
    {x : R} [IsLocalRing (R ⧸ Ideal.span {x})]
    (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2) :
    (maximalIdeal (R ⧸ Ideal.span {x})).spanFinrank + 1 = (maximalIdeal R).spanFinrank