Regular systems of parameters: bases of 𝔪/𝔪² and regular sequences

R is a Noetherian local ring with maximal ideal 𝔪, residue field K and cotangent space 𝔪/𝔪². This file proves the two ring-level facts about regular systems of parameters that the chart ring of a blow-up and the Cohen structure theorem need: a regular system of parameters is a basis of 𝔪/𝔪², and it is a regular sequence whose initial segments cut out regular local quotients.

Generating systems and the cotangent space

By Nakayama's lemma a family s ⊆ 𝔪 generates 𝔪 iff its classes span 𝔪/𝔪² (Mathlib's IsLocalRing.CotangentSpace.span_image_eq_top_iff, transported from submodules of 𝔪 to ideals of R along the inclusion 𝔪 ⊆ R). Since spanFinrank 𝔪 = dim_K 𝔪/𝔪² (spanFinrank_maximalIdeal_eq_finrank_cotangentSpace), a generating family of spanFinrank 𝔪 elements has linearly independent classes (a spanning family of the right cardinality is a basis) and conversely a basis of classes comes from a minimal generating system. For a regular local ring spanFinrank 𝔪 = dim R, so a regular system of parameters x₁, …, xₙ is a basis of 𝔪/𝔪²; in particular no xᵢ lies in 𝔪² (notMem_sq_of_span_eq, the fact the induction below needs). An element y ∈ 𝔪 ∖ 𝔪² is completed to a regular system of parameters by the exchange lemma of Hironaka/Algebra/Local/Regular.lean (exists_span_insert_eq_maximalIdeal: 𝔪 = ⟨y⟩ + ⟨t⟩ with card t + 1 = spanFinrank 𝔪 = n), enumerated by Fin n.

Quotients by initial segments and regular sequences

For a regular system of parameters x : Fin n → R and i ≤ n let Pᵢ = ⟨x₀, …, x_{i-1}⟩. By induction on i: R/Pᵢ is regular local with dim R/Pᵢ + i = dim R. The step uses that the maximal ideal of R/Pᵢ is generated by the classes of xᵢ, …, x_{n-1} (map_maximalIdeal_quotient_span_image_lt: the other generators die), so these n − i classes are a regular system of parameters of R/Pᵢ and the class of xᵢ is not in the square of the maximal ideal (the cotangent-space fact above, applied to R/Pᵢ); IsRegularLocalRing.quotient_span_singleton then makes (R/Pᵢ)/(x̄ᵢ) regular of one dimension less, and (R/Pᵢ)/(x̄ᵢ) ≅ R/P_{i+1} (DoubleQuot.quotQuotEquivQuotSup). Each R/Pᵢ is a domain (isDomain_of_isRegularLocalRing), so Pᵢ is prime and x̄ᵢ ≠ 0 is a nonzerodivisor of R/Pᵢ: a regular system of parameters is a regular sequence [TSPA, Tag 00NQ], stated in the list form isRegular_of_span_eq_maximalIdeal of Mathlib pull request 28683. For i ≥ n, Pᵢ = 𝔪.

theorem IsLocalRing.span_eq_maximalIdeal_iff_span_toCotangent_eq_top {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {ι : Type v} (s : ι → R) (hs : ∀ (i : ι), s i ∈ maximalIdeal R) : maximalIdeal R = Ideal.span (Set.range s) ↔ Submodule.span (ResidueField R) (Set.range fun (i : ι) => (maximalIdeal R).toCotangent ⟨s i, ⋯⟩) = ⊤

By Nakayama's lemma, a family of elements of 𝔪 generates 𝔪 iff its classes span 𝔪/𝔪².

theorem IsLocalRing.span_eq_maximalIdeal_and_card_eq_spanFinrank_iff {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {ι : Type v} (s : ι → R) (hs : ∀ (i : ι), s i ∈ maximalIdeal R) [Fintype ι] : maximalIdeal R = Ideal.span (Set.range s) ∧ Fintype.card ι = Submodule.spanFinrank (maximalIdeal R) ↔ ∃ (b : Module.Basis ι (ResidueField R) (CotangentSpace R)), ∀ (i : ι), b i = (maximalIdeal R).toCotangent ⟨s i, ⋯⟩

Minimal generating systems of 𝔪 are exactly the families whose classes form a basis of 𝔪/𝔪².

theorem IsLocalRing.x_mem_maximalIdeal_of_span_eq {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (i : Fin n) : x i ∈ maximalIdeal R

A regular system of parameters lies in 𝔪.

theorem IsLocalRing.spanFinrank_maximalIdeal_eq_of_natCast_eq {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (hn : ↑n = ringKrullDim R) : Submodule.spanFinrank (maximalIdeal R) = n

In a regular local ring of dimension n, 𝔪 needs n generators.

theorem IsLocalRing.exists_basis_cotangentSpace_of_span_eq {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) : ∃ (b : Module.Basis (Fin n) (ResidueField R) (CotangentSpace R)), ∀ (i : Fin n), b i = (maximalIdeal R).toCotangent ⟨x i, ⋯⟩

A regular system of parameters is a basis of 𝔪/𝔪².

theorem IsLocalRing.notMem_sq_of_span_eq {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (k : Fin n) : x k ∉ maximalIdeal R ^ 2

No member of a regular system of parameters lies in 𝔪².

theorem IsLocalRing.exists_span_eq_maximalIdeal_of_notMem_sq {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (hn : ↑n = ringKrullDim R) {y : R} (hy : y ∈ maximalIdeal R) (hy2 : y ∉ maximalIdeal R ^ 2) : ∃ (x' : Fin n → R), (∃ (i : Fin n), x' i = y) ∧ maximalIdeal R = Ideal.span (Set.range x')

An element of 𝔪 ∖ 𝔪² can be completed to a regular system of parameters (by the exchange lemma exists_span_insert_eq_maximalIdeal).

Quotients by initial segments of a regular system of parameters

theorem IsLocalRing.span_image_lt_zero {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) : Ideal.span (x '' {j : Fin n | ↑j < 0}) = ⊥

theorem IsLocalRing.span_image_lt_of_le {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) {i : ℕ} (hi : n ≤ i) : Ideal.span (x '' {j : Fin n | ↑j < i}) = maximalIdeal R

theorem IsLocalRing.span_image_lt_succ {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) {i : ℕ} (hi : i < n) : Ideal.span (x '' {j : Fin n | ↑j < i + 1}) = Ideal.span (x '' {j : Fin n | ↑j < i}) ⊔ Ideal.span {x ⟨i, hi⟩}

theorem IsLocalRing.map_maximalIdeal_quotient_span_image_lt {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (i : ℕ) : Ideal.map (Ideal.Quotient.mk (Ideal.span (x '' {j : Fin n | ↑j < i}))) (maximalIdeal R) = Ideal.span (⇑(Ideal.Quotient.mk (Ideal.span (x '' {j : Fin n | ↑j < i}))) ∘ x '' {j : Fin n | i ≤ ↑j})

The classes of xᵢ, …, x_{n-1} generate the maximal ideal of R/Pᵢ.

theorem IsLocalRing.mk_notMem_maximalIdeal_sq_of {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) {i : ℕ} (hi : i < n) [IsRegularLocalRing (R ⧸ Ideal.span (x '' {j : Fin n | ↑j < i}))] (hdim : ringKrullDim (R ⧸ Ideal.span (x '' {j : Fin n | ↑j < i})) + ↑i = ringKrullDim R) : (Ideal.Quotient.mk (Ideal.span (x '' {j : Fin n | ↑j < i}))) (x ⟨i, hi⟩) ∉ maximalIdeal (R ⧸ Ideal.span (x '' {j : Fin n | ↑j < i})) ^ 2

The step of the induction: if R/Pᵢ is regular of dimension dim R − i, the class of xᵢ is not in the square of its maximal ideal, because the classes of xᵢ, …, x_{n-1} are a regular system of parameters of R/Pᵢ.

theorem IsLocalRing.isRegularLocalRing_quotient_span_image_lt_and_ringKrullDim {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) {i : ℕ} (hi : i ≤ n) : IsRegularLocalRing (R ⧸ Ideal.span (x '' {j : Fin n | ↑j < i})) ∧ ringKrullDim (R ⧸ Ideal.span (x '' {j : Fin n | ↑j < i})) + ↑i = ringKrullDim R

The induction: for i ≤ n, R/Pᵢ is regular local with dim R/Pᵢ + i = dim R [TSPA, Tag 00NQ].

theorem IsLocalRing.isRegularLocalRing_quotient_span_image_lt {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (i : ℕ) : IsRegularLocalRing (R ⧸ Ideal.span (x '' {j : Fin n | ↑j < i}))

R/Pᵢ is a regular local ring.

theorem IsLocalRing.ringKrullDim_quotient_span_image_lt {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) {i : ℕ} (hi : i ≤ n) : ringKrullDim (R ⧸ Ideal.span (x '' {j : Fin n | ↑j < i})) + ↑i = ringKrullDim R

dim R/Pᵢ + i = dim R for i ≤ n.

theorem IsLocalRing.isPrime_span_image_lt {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (i : ℕ) : (Ideal.span (x '' {j : Fin n | ↑j < i})).IsPrime

Pᵢ = ⟨x₀, …, x_{i-1}⟩ is prime.

theorem IsLocalRing.notMem_span_image_lt {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) {i : ℕ} (hi : i < n) : x ⟨i, hi⟩ ∉ Ideal.span (x '' {j : Fin n | ↑j < i})

xᵢ ∉ Pᵢ.

theorem IsLocalRing.isRegular_of_span_eq_maximalIdeal {R : Type u} [CommRing R] [IsRegularLocalRing R] (rs : List R) (hspan : Ideal.ofList rs = maximalIdeal R) (len : ↑rs.length = ringKrullDim R) : RingTheory.Sequence.IsRegular R rs

A regular system of parameters is a regular sequence [TSPA, Tag 00NQ] (named as in Mathlib pull request 28683).

theorem IsLocalRing.exists_regularSystem (R : Type u) [CommRing R] [IsRegularLocalRing R] : ∃ (d : ℕ) (x : Fin d → R), maximalIdeal R = Ideal.span (Set.range x) ∧ ↑d = ringKrullDim R

A regular local ring has a regular system of parameters — a family x : Fin d → R with 𝔪 = ⟨x⟩ and d = dim R (a generating finset of 𝔪 of cardinality spanFinrank 𝔪 = dim R).