Regularity of the local model xy = πⁿ of a node

Let R be a regular local ring with maximal ideal 𝔪_R, for instance a discrete valuation ring, and let π ∈ 𝔪_R \ 𝔪_R², for instance a uniformizer. The ring R[x, y] ⧸ (xy - πⁿ) is the local model of a node in a family of curves over R: its special fibre xy = 0 is the union of two lines meeting transversally at the origin, while for n ≥ 1 its generic fibre over a discrete valuation ring is smooth. This file determines when its total space is regular at the singular point (𝔪_R, x, y) of the special fibre: exactly when n = 1.

Write P = R[x, y] and 𝔪 = (𝔪_R, x, y), the ideal of polynomials whose constant coefficient lies in 𝔪_R. The localization P_𝔪 is a regular local ring, and the local ring in question is P_𝔪 ⧸ (xy - πⁿ). For n ≥ 1 the equation lies in 𝔪, and a quotient of a regular local ring by a nonzero element of its maximal ideal is regular exactly when the element does not lie in the square of the maximal ideal (TauCeti.IsRegularLocalRing.quotient_span_singleton_iff). For n ≥ 2 the equation lies in 𝔪², so the quotient is not regular. For n = 1 its constant coefficient -π does not lie in 𝔪_R², so the quotient is regular. For n = 0 the point (𝔪_R, x, y) does not lie on the model at all, since xy = 1 there.

Away from the origin, that is at a prime not containing both coordinates, the model is smooth over R, hence regular whenever R is a regular ring. Over a discrete valuation ring with uniformizer π, the origin is the only prime of R[x, y] ⧸ (xy - π) containing both coordinates, so the whole ring R[x, y] ⧸ (xy - πⁿ) is regular exactly when n ≤ 1.

This is the regularity statement behind the resolution of the singularities of a nodal model of a curve over a discrete valuation ring by repeated blowups, each of which replaces n by n - 2, until the thickness of every node is at most one.

Main results

• TauCeti.isRegularLocalRing_quotient_X_mul_X_sub_C_pow_iff: the ring R[x, y]_𝔪 ⧸ (xy - πⁿ) is a regular local ring exactly when n = 1.
• TauCeti.isPrime_map_quotient_X_mul_X_sub_C_pow_iff: the image of 𝔪 in R[x, y] ⧸ (xy - πⁿ) is a prime ideal exactly when n ≠ 0.
• TauCeti.isRegularLocalRing_localization_quotient_X_mul_X_sub_C_pow_iff: the local ring of R[x, y] ⧸ (xy - πⁿ) at the image of 𝔪 is regular exactly when n = 1.
• TauCeti.isRegularLocalRing_localization_quotient_X_mul_X_sub_C_pow_iff_of_irreducible: the same statement for a uniformizer π of a discrete valuation ring.
• TauCeti.NodeAlgebra.isRegularLocalRing_localization_of_coord_notMem: over a regular ring, R[x, y] ⧸ (xy - a) is regular at every prime not containing both coordinates.
• TauCeti.NodeAlgebra.isRegularRing_of_isUnit: over a regular ring, R[x, y] ⧸ (xy - a) is a regular ring when a is a unit.
• TauCeti.NodeAlgebra.isRegularRing_pow_iff: for a uniformizer π of a discrete valuation ring, R[x, y] ⧸ (xy - πⁿ) is a regular ring exactly when n ≤ 1.

Implementation notes

The base ring R is assumed to be a local ring satisfying IsRegularRing. This gives regularity of R[x, y] via MvPolynomial.isRegularRing_of_isRegularRing, and hence of its localization R[x, y]_𝔪. Discrete valuation rings satisfy this hypothesis through the Dedekind-domain instance. The point (𝔪_R, x, y) is written as the preimage of 𝔪_R under the constant coefficient, so that it is visibly a prime ideal of R[x, y].

References

• The Stacks Project, Example 55.14.1

theorem TauCeti.isRegularLocalRing_quotient_X_mul_X_sub_C_pow_iff {R : Type u_1} [CommRing R] [IsLocalRing R] [IsRegularRing R] {π : R} (hπ : π ∈ IsLocalRing.maximalIdeal R) (hπ2 : π ∉ IsLocalRing.maximalIdeal R ^ 2) (n : ℕ) : IsRegularLocalRing (Localization.AtPrime (Ideal.comap MvPolynomial.constantCoeff (IsLocalRing.maximalIdeal R)) ⧸ Ideal.span {(algebraMap (MvPolynomial (Fin 2) R) (Localization.AtPrime (Ideal.comap MvPolynomial.constantCoeff (IsLocalRing.maximalIdeal R)))) (MvPolynomial.X 0 * MvPolynomial.X 1 - MvPolynomial.C π ^ n)}) ↔ n = 1

The local model xy = πⁿ of a node is regular at the origin exactly when n = 1. For π ∈ 𝔪_R \ 𝔪_R² in a regular local ring R and 𝔪 = (𝔪_R, x, y), the ring R[x, y]_𝔪 ⧸ (xy - πⁿ) is a regular local ring exactly when n = 1. For n = 0 it is the zero ring.

theorem TauCeti.isPrime_map_quotient_X_mul_X_sub_C_pow_iff {R : Type u_1} [CommRing R] [IsLocalRing R] {π : R} (hπ : π ∈ IsLocalRing.maximalIdeal R) (n : ℕ) : (Ideal.map (NodeAlgebra.mk (π ^ n)).toRingHom (Ideal.comap MvPolynomial.constantCoeff (IsLocalRing.maximalIdeal R))).IsPrime ↔ n ≠ 0

The image of 𝔪 = (𝔪_R, x, y) in R[x, y] ⧸ (xy - πⁿ) is a prime ideal exactly when n ≠ 0, that is, exactly when the origin of the special fibre lies on the model.

theorem TauCeti.isRegularLocalRing_localization_quotient_X_mul_X_sub_C_pow_iff {R : Type u_1} [CommRing R] [IsLocalRing R] [IsRegularRing R] {π : R} (hπ : π ∈ IsLocalRing.maximalIdeal R) (hπ2 : π ∉ IsLocalRing.maximalIdeal R ^ 2) (n : ℕ) [(Ideal.map (NodeAlgebra.mk (π ^ n)).toRingHom (Ideal.comap MvPolynomial.constantCoeff (IsLocalRing.maximalIdeal R))).IsPrime] : IsRegularLocalRing (Localization.AtPrime (Ideal.map (NodeAlgebra.mk (π ^ n)).toRingHom (Ideal.comap MvPolynomial.constantCoeff (IsLocalRing.maximalIdeal R)))) ↔ n = 1

The local ring of R[x, y] ⧸ (xy - πⁿ) at the origin of its special fibre is regular exactly when n = 1. Here π ∈ 𝔪_R \ 𝔪_R² for a regular local ring R, and the origin is the image of 𝔪 = (𝔪_R, x, y), which is a prime ideal exactly when n ≠ 0 (TauCeti.isPrime_map_quotient_X_mul_X_sub_C_pow_iff).

theorem TauCeti.isRegularLocalRing_localization_quotient_X_mul_X_sub_C_pow_iff_of_irreducible {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {π : R} (hπ : Irreducible π) (n : ℕ) [(Ideal.map (NodeAlgebra.mk (π ^ n)).toRingHom (Ideal.comap MvPolynomial.constantCoeff (IsLocalRing.maximalIdeal R))).IsPrime] : IsRegularLocalRing (Localization.AtPrime (Ideal.map (NodeAlgebra.mk (π ^ n)).toRingHom (Ideal.comap MvPolynomial.constantCoeff (IsLocalRing.maximalIdeal R)))) ↔ n = 1

The local model xy = πⁿ of a node over a discrete valuation ring is regular at the origin exactly when n = 1. For a uniformizer π of a discrete valuation ring R, the local ring of R[x, y] ⧸ (xy - πⁿ) at the image of (π, x, y) is regular exactly when n = 1.

Regularity of the whole node

theorem TauCeti.NodeAlgebra.isRegularLocalRing_localization_of_coord_notMem {R : Type u_1} [CommRing R] [IsRegularRing R] (a : R) (p : Ideal (NodeAlgebra R a)) [p.IsPrime] (h : ∃ (i : Fin 2), coord a i ∉ p) : IsRegularLocalRing (Localization.AtPrime p)

The node xy = a is regular away from its origin. Over a regular ring R, the local ring of R[x, y] ⧸ (xy - a) at a prime not containing both coordinates is regular, since xy = a is smooth over R there.

theorem TauCeti.NodeAlgebra.isRegularRing_of_isUnit {R : Type u_1} [CommRing R] [IsRegularRing R] {a : R} (ha : IsUnit a) : IsRegularRing (NodeAlgebra R a)

If a is a unit of a regular ring R, then R[x, y] ⧸ (xy - a) is a regular ring, since it is smooth over R.

theorem TauCeti.NodeAlgebra.isRegularRing_pow_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {π : R} (hπ : Irreducible π) (n : ℕ) : IsRegularRing (NodeAlgebra R (π ^ n)) ↔ n ≤ 1

The node xy = πⁿ over a discrete valuation ring is regular exactly when n ≤ 1. For a uniformizer π of a discrete valuation ring R, every local ring of R[x, y] ⧸ (xy - πⁿ) is regular exactly when n ≤ 1; for n ≥ 2 the local ring at the origin (π, x, y) is not regular.