Quotients of a regular local ring by part of a regular system of parameters

The dimension part of [TSPA, Tag 00NQ]: if R is a regular local ring and f_1, …, f_c ∈ 𝔪 have linearly independent classes in 𝔪/𝔪², then R/(f_1, …, f_c) is a regular local ring of dimension dim R - c. This is the form used to show that a smooth algebra has regular local rings (Hironaka/Algebra/RegularSmooth/SmoothImpliesRegular.lean) and to count regular systems of parameters (Hironaka/Algebra/RegularSmooth/ParameterCount.lean). The proof is a count. Generators. The classes of the f_j extend to a basis of 𝔪/𝔪² (Basis.sumExtend); lifting the new basis vectors to y_1, …, y_e ∈ 𝔪, the family f_1, …, f_c, y_1, …, y_e spans 𝔪/𝔪², hence generates 𝔪 by Nakayama (Mathlib's CotangentSpace.span_image_eq_top_iff), so the maximal ideal of the quotient is generated by the images of the y_i alone: its span rank is at most e = dim 𝔪/𝔪² - c = dim R - c, the last equality being the definition of regularity together with spanFinrank_maximalIdeal_eq_finrank_cotangentSpace. Dimension. Krull's height theorem in the form dim R ≤ dim R/(f_1, …, f_c) + c (ringKrullDim_le_ringKrullDim_quotient_add_card). Together: the span rank of the quotient's maximal ideal is at most its dimension, which is regularity (IsRegularLocalRing.of_spanFinrank_maximalIdeal_le), and then the two inequalities pinch the dimension to dim R - c. No "regular implies domain" is needed; the case c = 1 is IsRegularLocalRing.quotient_span_singleton of Hironaka/Algebra/Local/Regular.lean, not used here. The dimension arithmetic lives in WithBot ℕ∞ and is done by extracting natural numbers.

theorem IsRegularLocalRing.quotient_span_range_of_linearIndependent {R : Type u} [CommRing R] [IsRegularLocalRing R] {ι : Type u_1} [Fintype ι] (f : ι → R) (hf : ∀ (i : ι), f i ∈ IsLocalRing.maximalIdeal R) (hli : LinearIndependent (IsLocalRing.ResidueField R) fun (i : ι) => (IsLocalRing.maximalIdeal R).toCotangent ⟨f i, ⋯⟩) : IsRegularLocalRing (R ⧸ Ideal.span (Set.range f)) ∧ ringKrullDim (R ⧸ Ideal.span (Set.range f)) + ↑(Fintype.card ι) = ringKrullDim R

The dimension part of [TSPA, Tag 00NQ]: if f : ι → R takes values in 𝔪 with linearly independent classes in 𝔪/𝔪², then R ⧸ (f i) is a regular local ring and dim R ⧸ (f i) + |ι| = dim R.