Regular quotients of a regular local ring

If R is a regular local ring and R/I is regular local, then I is generated by an initial segment x_1, …, x_c of a regular system of parameters x_1, …, x_n of R, and then c = dim R - dim R/I [TSPA, Tag 00NR]. This is Kollár's silent "choose local coordinates such that Z = (x₁ = ⋯ = x_r = 0)" for a smooth subvariety Z [Kol07, Definition 60], and the algebra behind the Jacobian criterion: the kernel of the map from a polynomial ring to the local ring of a smooth point is generated by part of a regular system of parameters (Hironaka/Algebra/RegularSmooth/RegularImpliesSmooth.lean).

The proof follows [TSPA, Tag 00NR]. The classes of I. Let t ⊆ 𝔪/𝔪² be the set of classes of the elements of I; a maximal linearly independent subset b ⊆ t spans the same subspace and has c := |b| elements (exists_linearIndependent). Counting. Lifting a minimal generating system ȳ_1, …, ȳ_d of 𝔪̄ = 𝔪/I to y_i ∈ 𝔪 (d = dim R/I by regularity of R/I) gives 𝔪 = (y_1, …, y_d) + I, so by Nakayama (Hironaka/Algebra/Local/RegularSystem.lean) the classes of the y_i together with t span 𝔪/𝔪², whence n := dim 𝔪/𝔪² ≤ d + c. The parameters. Extending b to a basis of 𝔪/𝔪² (Basis.sumExtend) and lifting, with the c elements of I first, produces x_1, …, x_n whose classes form a basis of 𝔪/𝔪², hence a regular system of parameters, with J := (x_1, …, x_c) ⊆ I. Equality. R/J is regular local of dimension n - c ≤ d, and R/J → R/I is surjective, so d ≤ dim R/J; hence dim R/J = dim R/I. A regular local ring is a domain (Hironaka/Algebra/Local/Regular.lean), and a nonzero element z of a Noetherian local domain drops the dimension by exactly one (Mathlib's ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors), so a proper ideal of R/J with a quotient of the full dimension is zero: I/J = 0, i.e. I = J.

theorem Ideal.eq_bot_of_ringKrullDim_quotient_eq {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] {J : Ideal R} (hJ : J ≤ IsLocalRing.maximalIdeal R) (hdim : ringKrullDim (R ⧸ J) = ringKrullDim R) : J = ⊥

In a Noetherian local domain, a proper ideal whose quotient has the full Krull dimension is zero, since a nonzero element of the maximal ideal is a nonzerodivisor and drops the dimension by one (the last step of [TSPA, Tag 00NR], "R/J → R/I is an isomorphism"; also used for the dimension theory of analytic germs, Hironaka/AnalyticSpace/ConvDimension.lean).

theorem IsRegularLocalRing.exists_span_eq_maximalIdeal_and_eq_span_image_lt {R : Type u} [CommRing R] [IsRegularLocalRing R] (I : Ideal R) [IsRegularLocalRing (R ⧸ I)] : ∃ (n : ℕ) (c : ℕ) (x : Fin n → R), c ≤ n ∧ ↑n = ringKrullDim R ∧ IsLocalRing.maximalIdeal R = Ideal.span (Set.range x) ∧ I = Ideal.span (x '' {j : Fin n | ↑j < c})

If R and R/I are regular local, then I is generated by an initial segment of a regular system of parameters x : Fin n → R of R [TSPA, Tag 00NR]; the argument is in the module docstring.