The nodal equation is free over the sum of its coordinates

Put s = x + y on the curve xy = a. The coordinate x is then a root of the monic quadratic T² - sT + a over R[s], and y = s - x. Conversely, adjoining a root t of this quadratic to R[s] gives a solution x = t, y = s - t of the nodal equation. So the node algebra NodeAlgebra R a = R[x, y] ⧸ (xy - a) is R[s] with a root of a monic quadratic adjoined: it is free of rank two over the polynomial ring R[s], with basis 1, x (AdjoinRoot.powerBasis').

This finite free presentation controls the local model of a node over any base ring R:

• it is a free, hence flat, R-module, and faithfully flat when R is nontrivial;
• it is integral over R[s], which it contains, so it has the Krull dimension of R[s];
• over a field it is pure of dimension one: since it is flat over R[s], going down holds, so every minimal prime lies over the zero ideal of R[s], and each irreducible component is integral over the line Spec R[s], which it dominates.

Flatness over the base and pure one-dimensionality of the fibres are the fibrewise conditions, beside finite presentation, in the characterization of families of curves with at worst nodal singularities; the fibres of NodeAlgebra R a over R are node algebras over the residue fields by TauCeti.NodeAlgebra.baseChange.

Main definitions

• TauCeti.NodeAlgebra.quadratic a: the monic quadratic T² - sT + a over R[s].
• TauCeti.NodeAlgebra.adjoinRootEquiv a: the node algebra is R[s] with a root of quadratic a adjoined, with x corresponding to the root and x + y to s.

Main results

• TauCeti.NodeAlgebra.instFree: the node algebra is a free R-module.
• TauCeti.NodeAlgebra.coord_mem_nonZeroDivisors: if a is a nonzerodivisor of R, then, the node algebra being flat, both coordinates are nonzerodivisors.
• TauCeti.NodeAlgebra.ringKrullDim_eq_ringKrullDim_polynomial: its Krull dimension is that of R[s].
• TauCeti.NodeAlgebra.ringKrullDim_eq_ringKrullDim_add_one: over a Noetherian ring R it has Krull dimension dim R + 1.
• TauCeti.NodeAlgebra.isPureDimensional_primeSpectrum: over a field its spectrum is pure of dimension one.

References

• Stacks Project, Example 55.14.1, Tag 0CDC, the local model xy = πⁿ of a node over a discrete valuation ring.

noncomputable def TauCeti.NodeAlgebra.quadratic {R : Type u_1} [CommRing R] (a : R) : Polynomial (Polynomial R)

The monic quadratic T² - sT + a over the polynomial ring R[s]. On the node xy = a it has the root x when s = x + y.

Equations

• TauCeti.NodeAlgebra.quadratic a = Polynomial.X ^ 2 - Polynomial.C Polynomial.X * Polynomial.X + Polynomial.C (Polynomial.C a)

theorem TauCeti.NodeAlgebra.quadratic_def {R : Type u_1} [CommRing R] (a : R) : quadratic a = Polynomial.X ^ 2 - Polynomial.C Polynomial.X * Polynomial.X + Polynomial.C (Polynomial.C a)

The defining formula of quadratic a.

theorem TauCeti.NodeAlgebra.monic_quadratic {R : Type u_1} [CommRing R] (a : R) : (quadratic a).Monic

The quadratic T² - sT + a is monic.

theorem TauCeti.NodeAlgebra.natDegree_quadratic {R : Type u_1} [CommRing R] (a : R) [Nontrivial R] : (quadratic a).natDegree = 2

Over a nontrivial ring, quadratic a has degree two.

noncomputable def TauCeti.NodeAlgebra.adjoinRootEquiv {R : Type u_1} [CommRing R] (a : R) : AdjoinRoot (quadratic a) ≃ₐ[R] NodeAlgebra R a

The node algebra is the polynomial ring R[s] with a root of the monic quadratic T² - sT + a adjoined: the root corresponds to x, and s to x + y.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.NodeAlgebra.adjoinRootEquiv_root {R : Type u_1} [CommRing R] (a : R) : (adjoinRootEquiv a) (AdjoinRoot.root (quadratic a)) = coord a 0

@[simp]

theorem TauCeti.NodeAlgebra.adjoinRootEquiv_of {R : Type u_1} [CommRing R] (a : R) (p : Polynomial R) : (adjoinRootEquiv a) ((AdjoinRoot.of (quadratic a)) p) = (Polynomial.aeval (coord a 0 + coord a 1)) p

@[simp]

theorem TauCeti.NodeAlgebra.adjoinRootEquiv_symm_coord_zero {R : Type u_1} [CommRing R] (a : R) : (adjoinRootEquiv a).symm (coord a 0) = AdjoinRoot.root (quadratic a)

@[simp]

theorem TauCeti.NodeAlgebra.adjoinRootEquiv_symm_coord_one {R : Type u_1} [CommRing R] (a : R) : (adjoinRootEquiv a).symm (coord a 1) = (AdjoinRoot.of (quadratic a)) Polynomial.X - AdjoinRoot.root (quadratic a)

instance TauCeti.NodeAlgebra.instFree {R : Type u_1} [CommRing R] (a : R) : Module.Free R (NodeAlgebra R a)

The node algebra is a free R-module, being free of rank two over the free R-module R[s]. In particular it is flat, and faithfully flat.

instance TauCeti.NodeAlgebra.instNontrivial {R : Type u_1} [CommRing R] (a : R) [Nontrivial R] : Nontrivial (NodeAlgebra R a)

Over a nontrivial ring the node algebra is nontrivial; being free, it is then a faithfully flat R-algebra.

theorem TauCeti.NodeAlgebra.coord_mem_nonZeroDivisors {R : Type u_1} [CommRing R] {a : R} (ha : a ∈ nonZeroDivisors R) (i : Fin 2) : coord a i ∈ nonZeroDivisors (NodeAlgebra R a)

If a is a nonzerodivisor of R, then both coordinates are nonzerodivisors of the node algebra of xy = a.

theorem TauCeti.NodeAlgebra.ringKrullDim_eq_ringKrullDim_polynomial {R : Type u_1} [CommRing R] (a : R) : ringKrullDim (NodeAlgebra R a) = ringKrullDim (Polynomial R)

The node algebra has the Krull dimension of the polynomial ring R[s], over which it is integral and which it contains.

theorem TauCeti.NodeAlgebra.ringKrullDim_eq_ringKrullDim_add_one {R : Type u_1} [CommRing R] (a : R) [IsNoetherianRing R] : ringKrullDim (NodeAlgebra R a) = ringKrullDim R + 1

Over a Noetherian ring R, the node algebra has Krull dimension dim R + 1.

theorem TauCeti.NodeAlgebra.ringKrullDim_eq_one {k : Type u_2} [Field k] (c : k) : ringKrullDim (NodeAlgebra k c) = 1

Over a field, the node algebra has Krull dimension one.

theorem TauCeti.NodeAlgebra.isPureDimensional_primeSpectrum {k : Type u_2} [Field k] (c : k) : IsPureDimensional 1 (PrimeSpectrum (NodeAlgebra k c))

Over a field, every irreducible component of the node xy = c is a curve: the spectrum of the node algebra is pure of dimension one.