Mathlib_RingTheory_SmoothAlgebraOverFieldRegularStalks.lean

def SmoothFieldFiberRegularStalksInput : Prop

theorem isRegularLocalRing_of_isField (R : Type*) [CommRing R] (hf : IsField R) :
    IsRegularLocalRing R

theorem isRegularLocalRing_atPrime_of_artinian_reduced
    (A : Type*) [CommRing A] [IsArtinianRing A] [IsReduced A]
    (p : Ideal A) [p.IsPrime] :
    IsRegularLocalRing (Localization.AtPrime p)

theorem isRegularRing_of_isArtinianRing_of_isReduced
    (A : Type*) [CommRing A] [IsArtinianRing A] [IsReduced A] :
    IsRegularRing A

theorem isRegularLocalRing_localization_atPrime_of_formallyUnramified
    (k A : Type*) [Field k] [CommRing A] [Algebra k A]
    [Algebra.FormallyUnramified k A] [Algebra.EssFiniteType k A]
    (p : Ideal A) [p.IsPrime] :
    IsRegularLocalRing (Localization.AtPrime p)

theorem isRegularLocalRing_localization_atPrime_of_etale
    (k A : Type*) [Field k] [CommRing A] [Algebra k A] [Algebra.Etale k A]
    (p : Ideal A) [p.IsPrime] :
    IsRegularLocalRing (Localization.AtPrime p)

theorem isRegularRing_of_etale
    (k A : Type*) [Field k] [CommRing A] [Algebra k A] [Algebra.Etale k A] :
    IsRegularRing A

theorem smoothFieldFiberRegularStalksInput_iff :
    SmoothFieldFiberRegularStalksInput.{u} ↔
      ∀ (k A : Type u) [Field k] [CommRing A] [Algebra k A],
        Algebra.Smooth k A → ∀ (p : Ideal A) [p.IsPrime],
          IsRegularLocalRing (Localization.AtPrime p)

theorem isRegularRing_of_smooth_of_input
    (hinput : SmoothFieldFiberRegularStalksInput.{u})
    (k A : Type u) [Field k] [CommRing A] [Algebra k A] [Algebra.Smooth k A] :
    IsRegularRing A

theorem eps_ne_zero (K : Type*) [Field K] : (DualNumber.eps : DualNumber K) ≠ 0

theorem nilradical_dualNumber_eq_span_eps (K : Type*) [Field K] :
    nilradical (DualNumber K) = Ideal.span {(DualNumber.eps : DualNumber K)}

theorem ringKrullDim_dualNumber_eq_zero (K : Type*) [Field K] :
    ringKrullDim (DualNumber K) = 0

theorem spanFinrank_maximalIdeal_dualNumber_eq_one (K : Type*) [Field K] :
    (maximalIdeal (DualNumber K)).spanFinrank = 1

theorem not_isRegularLocalRing_dualNumber (K : Type*) [Field K] :
    ¬ IsRegularLocalRing (DualNumber K)

theorem isField_of_isRegularLocalRing_of_krullDimLE_zero
    (R : Type*) [CommRing R] [Ring.KrullDimLE 0 R] [IsRegularLocalRing R] :
    IsField R

theorem not_isRegularLocalRing_localization_atPrime_dualNumber (K : Type*) [Field K] :
    ¬ IsRegularLocalRing (Localization.AtPrime (maximalIdeal (DualNumber K)))

theorem not_forall_regular_stalks_without_smooth :
    ¬ (∀ (k A : Type) [Field k] [CommRing A] [Algebra k A] (p : Ideal A) [p.IsPrime],
        IsRegularLocalRing (Localization.AtPrime p))