@[reducible, inline]

noncomputable abbrev embDim (R : Type u) [CommRing R] [IsLocalRing R] : ℕ

Embedding dimension of a Noetherian local ring R: the minimal number of generators of the maximal ideal, equivalently dim_κ(𝔪/𝔪²).

def IsRegularLocal (R : Type u) [CommRing R] [IsLocalRing R] : Prop

Regular local ring: Krull dimension equals embedding dimension.

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

General inequality: Krull dimension is at most embedding dimension.

theorem isRegularLocal_of_field (R : Type u) [CommRing R] [IsLocalRing R] (hR : IsField R) : IsRegularLocal R

A field is a regular local ring of dimension zero.

theorem formallySmooth_implies_kahler_projective (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] [Algebra.FormallySmooth R A] : Module.Projective A Ω[A⁄R]

For a formally smooth R-algebra A, Ω_{A/R} is projective.

theorem formallySmooth_iff_projective_and_H1_vanishes (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] : Algebra.FormallySmooth R A ↔ Module.Projective A Ω[A⁄R] ∧ Subsingleton (Algebra.H1Cotangent R A)

A is formally smooth over R iff Ω_{A/R} is projective and the first André–Quillen cotangent homology H₁(L_{A/R}) vanishes.

theorem smoothLocus_isOpen {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Algebra.FinitePresentation R A] : IsOpen (Algebra.smoothLocus R A)

Smooth locus is open: for a finitely presented R-algebra A, the smooth locus inside Spec A is open.

theorem smoothLocus_eq_kahler_free_locus {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]

The smooth locus equals the locus where H₁ cotangent vanishes intersected with the free locus of Ω_{A/R}.

theorem smoothLocus_eq_univ_of_smooth {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Algebra.Smooth R A] : Algebra.smoothLocus R A = Set.univ

For a smooth algebra, the smooth locus is the whole spectrum.

theorem smooth_iff_smoothLocus_univ {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

Smoothness is equivalent to the smooth locus being the whole spectrum (for finitely presented algebras).

theorem exists_localization_smooth_of_smooth_at {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)

Local-to-global smoothness: if A is smooth over R at the prime p, then some basic open D(f) with f ∉ p is smooth over R.

theorem isField_localization_atPrime_bot {A : Type u} [CommRing A] [IsDomain A] : IsField (Localization.AtPrime ⊥)

Localizing an integral domain at the zero ideal yields a field (the fraction field).

theorem isSmoothAt_genericPoint {K : Type u} [Field K] [PerfectField K] {A : Type u} [CommRing A] [IsDomain A] [Algebra K A] [Algebra.FiniteType K A] : Algebra.IsSmoothAt K ⊥

Smoothness at the generic point over a perfect field: a finite-type algebra over a perfect field K is smooth at the generic point of an integral variety.

theorem smoothLocus_isDense {K : Type u} [Field K] [PerfectField K] {A : Type u} [CommRing A] [IsDomain A] [Algebra K A] [Algebra.FiniteType K A] [Algebra.FinitePresentation K A] : Dense (Algebra.smoothLocus K A)

Smooth locus is dense over a perfect field: for an integral domain of finite type over a perfect field, the smooth locus is dense in Spec A. This is generic smoothness.

theorem smoothLocus_isOpen_and_dense {K : Type u} [Field K] [PerfectField K] {A : Type u} [CommRing A] [IsDomain A] [Algebra K A] [Algebra.FiniteType K A] [Algebra.FinitePresentation K A] : IsOpen (Algebra.smoothLocus K A) ∧ Dense (Algebra.smoothLocus K A)

Combination: the smooth locus over a perfect field is both open and dense.

theorem smoothLocus_isDense_scheme {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [PerfectField K] [AlgebraicGeometry.IsReduced X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFinitePresentation f] : Dense ↑(AlgebraicGeometry.Scheme.Hom.smoothLocus f)

Scheme-theoretic generic smoothness: the smooth locus of a finite-presentation morphism to Spec K from a reduced scheme is dense (when K is perfect).

theorem smoothLocus_isOpen_and_dense_scheme {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [PerfectField K] [AlgebraicGeometry.IsReduced X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFinitePresentation f] : IsOpen ↑(AlgebraicGeometry.Scheme.Hom.smoothLocus f) ∧ Dense ↑(AlgebraicGeometry.Scheme.Hom.smoothLocus f)

The scheme-theoretic smooth locus is open and dense.

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

dim k[x₁,…,xₙ] = n.

theorem smooth_ringKrullDim_polynomial (k : Type u) [Field k] : ringKrullDim (Polynomial k) = 1

dim k[x] = 1.

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

Localizing the polynomial ring at any prime gives a ring of Krull dimension at most n.

theorem mvPolynomial_smooth (k : Type u) [Field k] (n : ℕ) : Algebra.Smooth k (MvPolynomial (Fin n) k)

Affine space 𝔸ⁿ_k = Spec k[x₁,…,xₙ] is smooth over k.

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

For any prime in the polynomial ring, the localization satisfies the fundamental inequality dim ≤ embDim.

theorem maximalIdeal_generator_ne_zero (R : Type u) [CommRing R] [IsLocalRing R] [IsPrincipalIdealRing R] (hR : ¬IsField R) : Submodule.IsPrincipal.generator (IsLocalRing.maximalIdeal R) ≠ 0

In a non-field local PID, a generator of the maximal ideal is non-zero.

theorem embDim_eq_one_of_localPID (R : Type u) [CommRing R] [IsLocalRing R] [IsPrincipalIdealRing R] (hR : ¬IsField R) : embDim R = 1

The embedding dimension of a non-field local PID is 1.

theorem ringKrullDim_eq_one_of_localPID (R : Type u) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (hR : ¬IsField R) : ringKrullDim R = 1

The Krull dimension of a non-field PID is 1.

theorem isRegularLocal_of_localPID (R : Type u) [CommRing R] [IsDomain R] [IsLocalRing R] [IsPrincipalIdealRing R] (hR : ¬IsField R) : IsRegularLocal R

A non-field local PID is regular: dim = 1 = embDim.

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

Any discrete valuation ring is a regular local ring of dimension 1.

theorem smooth_powerSeries_isDVR (k : Type u) [Field k] : IsDiscreteValuationRing (PowerSeries k)

The formal power series ring k[[x]] is a discrete valuation ring.

theorem powerSeries_ringKrullDim (k : Type u) [Field k] : ringKrullDim (PowerSeries k) = 1

dim k[[x]] = 1.

theorem powerSeries_not_isField (k : Type u) [Field k] : ¬IsField (PowerSeries k)

The power series ring over a field is not itself a field.

theorem powerSeries_ringKrullDim_succ_le (R : Type u_1) [CommRing R] : ringKrullDim R + 1 ≤ ringKrullDim (PowerSeries R)

Adjoining a power series variable raises Krull dimension by at least one.

theorem mvPowerSeries_isLocalRing (k : Type u) [Field k] (d : ℕ) : IsLocalRing (MvPowerSeries (Fin d) k)

The multivariate power series ring k[[x₁,…,x_d]] is a local ring.

theorem powerSeries_maximalIdeal_eq (k : Type u) [Field k] : IsLocalRing.maximalIdeal (PowerSeries k) = Ideal.span {PowerSeries.X}

The maximal ideal of k[[x]] is the principal ideal (x).