Regular local rings: quotient by a parameter, domain, converse #
This file proves four facts about regular local rings that Mathlib lacks: the quotient of a
regular local ring by an element of 𝔪 ∖ 𝔪² is regular of one dimension less, a regular local
ring is a domain, and the converse of the first statement for a nonzerodivisor. Names follow
the open Mathlib pull request 28683 (IsRegularLocalRing.quotient_span_singleton,
isDomain_of_isRegularLocalRing and its instance), so that a later Mathlib version can
replace them without renaming; the converse has no upstream counterpart and is called
IsRegularLocalRing.of_quotient_span_singleton. Everything lives in the namespace
Hironaka.Local; the prime-avoidance step is
exists_mem_maximalIdeal_notMem_sq_notMem_minimalPrimes without an IsLocalRing. prefix, so
that this file creates no namespace Hironaka.Local.IsLocalRing and open IsLocalRing stays
unambiguous in every file of Hironaka.Local.
The argument #
Throughout, R is a Noetherian local ring with maximal ideal 𝔪, residue field K = R/𝔪,
and n := spanFinrank 𝔪 the minimal number of generators of 𝔪; R is regular when
n = dim R. Two inequalities from Mathlib drive everything: Krull's height theorem
dim R ≤ spanFinrank 𝔪 (ringKrullDim_le_spanFinrank_maximalIdeal) and the one-equation
bound dim R ≤ dim R/I + spanFinrank I for I ⊆ 𝔪
(ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank).
Exchange of a generator (exists_span_insert_eq_maximalIdeal). Let 𝔪 = ⟨s₁, …, sₙ⟩ be a
minimal generating system and x ∈ 𝔪 ∖ 𝔪². Writing x = ∑ fᵢ sᵢ, not every fᵢ lies in 𝔪
(otherwise x ∈ 𝔪 · 𝔪 = 𝔪²), so some fᵢ₀ is a unit and sᵢ₀ = fᵢ₀⁻¹ (x − ∑_{i ≠ i₀} fᵢ sᵢ);
hence 𝔪 = ⟨x, sᵢ : i ≠ i₀⟩, a generating system of n elements containing x. In the
quotient R̄ = R/⟨x⟩ the image of this system minus the (now zero) image of x generates
𝔪̄, so spanFinrank 𝔪̄ + 1 ≤ n (spanFinrank_maximalIdeal_quotient_add_one_le).
Quotient by a parameter ([TSPA, Tag 00NQ]). For R regular and x ∈ 𝔪 ∖ 𝔪²,
the one-equation bound gives n = dim R ≤ dim R̄ + 1, Krull gives dim R̄ ≤ spanFinrank 𝔪̄, and
the exchange gives spanFinrank 𝔪̄ + 1 ≤ n. With dim R̄ = m ∈ ℕ these read
n ≤ m + 1, m ≤ spanFinrank 𝔪̄ ≤ n − 1, so spanFinrank 𝔪̄ = m = n − 1: R̄ is regular
(IsRegularLocalRing.of_spanFinrank_maximalIdeal_le) and dim R̄ + 1 = dim R. No
nonzerodivisor hypothesis is needed.
Prime avoidance. If dim R > 0, then 𝔪 ⊄ 𝔪² ∪ P₁ ∪ ⋯ ∪ P_k for the
finitely many minimal primes Pᵢ (Noetherian): 𝔪 ⊆ 𝔪² is excluded because 𝔪² ⊊ 𝔪 in
positive dimension (IsLocalRing.maximalIdeal_sq_lt_of_ringKrullDim_ne_zero), and 𝔪 ⊆ Pᵢ
would make 𝔪 a minimal prime, of height 0 = dim R (Ideal.height_eq_zero_iff,
IsLocalRing.maximalIdeal_height_eq_ringKrullDim). Mathlib's Ideal.subset_union_prime
allows two non-prime members of the family; 𝔪² occupies one of them.
Regular implies domain ([TSPA, Tag 00NP], proved as in [Mat89, Theorem 14.3], by induction on
dim R). If dim R = 0 then spanFinrank 𝔪 = 0, so
𝔪 = 0 is prime and R is a field. If dim R = m + 1, pick x ∈ 𝔪 ∖ 𝔪² outside every
minimal prime (prime avoidance). By the quotient theorem R/⟨x⟩ is regular of dimension m,
hence a domain by induction, so ⟨x⟩ is prime. Let P ⊆ ⟨x⟩ be a minimal prime. For
y ∈ P write y = z x; since x ∉ P and P is prime, z ∈ P, so P = x P ⊆ 𝔪 P, and
Nakayama (Submodule.eq_bot_of_le_smul_of_le_jacobson_bot) gives P = 0. A prime zero ideal
makes R a domain (IsDomain.of_bot_isPrime). The Stacks Project's own proof through the
associated graded ring is not followed, since the associated graded ring is absent from Mathlib.
Converse ([TSPA, Tag 00NU]). For x ∈ 𝔪 a nonzerodivisor with R̄ = R/⟨x⟩
regular, Mathlib already has dim R̄ + 1 = dim R
(ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors). Lifting a
minimal generating system of 𝔪̄ to R and adjoining x generates 𝔪 (an element of 𝔪 is
congruent modulo ⟨x⟩ to a combination of the lifts), so
spanFinrank 𝔪 ≤ spanFinrank 𝔪̄ + 1 = dim R̄ + 1 = dim R
(spanFinrank_maximalIdeal_le_spanFinrank_maximalIdeal_quotient_add_one), and R is regular.
The adapted-generator theorem #
The adapted-generator theorem ([TSPA, Tag 00NR]: a prime P with R/P regular is generated by
part of a regular system of parameters; Kollár's silent "choose local coordinates such that
Z = (x₁ = ⋯ = x_r = 0)" in [Kol07, Definition 60]) is also absent from Mathlib; it is proved
in Hironaka/Algebra/Local/QuotientParameters.lean, using isDomain_of_isRegularLocalRing below.
Dimension bookkeeping #
A ring of finite Krull dimension has a natural number as its dimension.
Quotients of a local ring #
The quotient of a local ring by a proper ideal is local.
The maximal ideal of a local quotient is the image of 𝔪.
The exchange step: an element x ∈ 𝔪 ∖ 𝔪² replaces one member of a minimal generating system
of 𝔪: 𝔪 = ⟨x⟩ + ⟨t⟩ with t.card + 1 = spanFinrank 𝔪.
For x ∈ 𝔪 ∖ 𝔪² the maximal ideal of R/⟨x⟩ needs one generator fewer than 𝔪.
For x ∈ 𝔪, lifting generators of the maximal ideal of R/⟨x⟩ and adjoining x generates
𝔪.
Prime avoidance #
The first step of [TSPA, Tag 00NP] and [Mat89, Theorem 14.3]: in a Noetherian local ring of
positive dimension there is x ∈ 𝔪 ∖ 𝔪² in no minimal prime, since
𝔪 ⊄ 𝔪² ∪ P₁ ∪ ⋯ ∪ P_k by prime avoidance (Ideal.subset_union_prime, with 𝔪² in one of the
two non-prime slots).
Quotient by a parameter #
For x ∈ 𝔪 ∖ 𝔪² in a regular local ring, R/⟨x⟩ is regular local and
dim R/⟨x⟩ + 1 = dim R [TSPA, Tag 00NQ] (named as in Mathlib pull request 28683). No
nonzerodivisor hypothesis is used.
Regular local rings are domains #
The induction on the dimension of [Mat89, Theorem 14.3]: a regular local ring of dimension
n is a domain.
A regular local ring is a domain ([TSPA, Tag 00NP], [Mat89, Theorem 14.3]; named as in Mathlib pull request 28683).
A regular local ring is a domain, as an instance (as in Mathlib pull request 28683). Its
priority is low, so that where Mathlib derives IsDomain otherwise (for a field, say) Mathlib's
derivation is found and statements elaborate as against Mathlib alone.
The converse #
If x ∈ 𝔪 is a nonzerodivisor of the Noetherian local ring R and R/⟨x⟩ is regular local,
then R is regular local and dim R/⟨x⟩ + 1 = dim R [TSPA, Tag 00NU].
A monomial in elements of an ideal J lies in the power of J given by its degree (used
in Hironaka/Algebra/Local/CohenMap.lean).