theorem isRegularLocal_iff_eq (R : Type u) [CommRing R] [IsLocalRing R] : IsRegularLocal R ↔ ringKrullDim R = ↑(embDim R)

A local ring R is regular iff its Krull dimension equals its embedding dimension; the definitional unfolding of regularity.

theorem isRegularLocal_iff_le (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocal R ↔ ↑(embDim R) ≤ ringKrullDim R

For a Noetherian local ring, regularity is equivalent to the inequality embDim ≤ krullDim, combined with the general bound krullDim ≤ embDim.

theorem prop30_inequality (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : ringKrullDim R ≤ ↑(embDim R)

Prop 30 (Lec, regularity): the Krull dimension of a Noetherian local ring is bounded above by its embedding dimension.

theorem isRegularLocal_iff_embDim_eq (R : Type u) [CommRing R] [IsLocalRing R] : IsRegularLocal R ↔ ↑(embDim R) = ringKrullDim R

Symmetric reformulation: regular ⇔ embDim = krullDim.

theorem cotangentSpace_finiteDimensional_regular (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : FiniteDimensional (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)

The cotangent space m/m² of a Noetherian local ring is a finite-dimensional vector space over the residue field.

theorem cotangentSpace_subsingleton_iff (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : Subsingleton (IsLocalRing.CotangentSpace R) ↔ IsField R

The cotangent space vanishes iff R is a field, i.e. dim_k m/m² = 0.

theorem cotangentSpace_finrank_le_one_iff (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (IsLocalRing.maximalIdeal R)

dim_k m/m² ≤ 1 iff the maximal ideal is principal (a discrete valuation ring or a field).

theorem smooth_at_implies_exists_smooth_localization {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Algebra.FinitePresentation R A] (p : Ideal A) [p.IsPrime] [Algebra.IsSmoothAt R p] : ∃ f ∉ p, Algebra.Smooth R (Localization.Away f)

Smoothness at a prime is detected by smoothness on a Zariski-open neighborhood; if R → A is smooth at p, there exists f ∉ p with A_f smooth.

theorem smooth_locus_regularity_criterion {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Algebra.EssFiniteType R A] : Algebra.smoothLocus R A = (Module.support A (Algebra.H1Cotangent R A))ᶜ ∩ Module.freeLocus A Ω[A⁄R]

Characterization of the smooth locus: complement of the support of H¹ of the cotangent intersected with the free locus of Ω[A/R].

theorem smooth_iff_all_local_rings_in_smooth_locus {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Algebra.FinitePresentation R A] : Algebra.smoothLocus R A = Set.univ ↔ Algebra.FormallySmooth R A

An R-algebra A is formally smooth iff its smooth locus is all of Spec A.

theorem field_isRegular (k : Type u) [Field k] (hk : IsField k) : IsRegularLocal k

A field is a regular local ring (trivial case of regularity).

theorem DVR_isRegular (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : IsRegularLocal R

Every discrete valuation ring is a regular local ring of dimension one.

theorem polynomial_ring_dim (k : Type u) [Field k] (n : ℕ) : ringKrullDim (MvPolynomial (Fin n) k) = ↑n

The Krull dimension of the polynomial ring k[X_1, …, X_n] over a field is n.

theorem prop30_for_polynomial_localization (k : Type u) [Field k] (n : ℕ) (𝔭 : Ideal (MvPolynomial (Fin n) k)) [𝔭.IsPrime] : ringKrullDim (Localization.AtPrime 𝔭) ≤ ↑(embDim (Localization.AtPrime 𝔭))

Prop 30 applied to localizations of a polynomial ring at a prime: Krull dimension is bounded by embedding dimension.