The quotient of a regular local ring by a nonzero element of 𝔪² is not regular

The algebra behind the example showing that "the restriction of a smooth blow-up sequence need not be a smooth blow-up sequence" [Kol07, 30.2]: the cuspidal cubic V(y² − x³) ⊂ 𝔸² is singular at the origin (HironakaExamples/Sequence/CuspWitness.lean). Its local ring there is R/(g) with R = k[x, y]_{(x, y)} regular and g = y² − x³ ∈ 𝔪². If R/(g) were regular, IsRegularLocalRing.exists_span_eq_maximalIdeal_and_eq_span_image_lt ([TSPA, Tag 00NR]) would make (g) the ideal of an initial segment x_0, …, x_{c-1} of a regular system of parameters of R: for c = 0 this forces g = 0, and for c ≥ 1 it puts x_0 ∈ (g) ⊆ 𝔪², against notMem_sq_of_span_eq (no member of a regular system of parameters lies in 𝔪²). Standard; also used for the real circle example of the analytic part (HironakaExamples/RealPlaneCircle.lean).

theorem Hironaka.Local.not_isRegularLocalRing_quotient_span_singleton {R : Type u} [CommRing R] [IsRegularLocalRing R] {g : R} (hg0 : g ∈ nonZeroDivisors R) (hg : g ∈ IsLocalRing.maximalIdeal R ^ 2) : ¬IsRegularLocalRing (R ⧸ Ideal.span {g})

A regular local ring modulo a nonzero element of 𝔪² is not a regular local ring ([TSPA, Tag 00NR] would make the element part of a regular system of parameters, which never lies in 𝔪²).