Smooth coordinate charts of the nodal equation

The algebra NodeAlgebra R a = R[x,y]/(xy-a) is the local model for smoothing a node. Inverting either coordinate gives a standard smooth algebra of relative dimension one. Consequently a prime at which at least one coordinate is nonzero belongs to the smooth locus. These assertions hold over any commutative base ring.

For a discrete valuation ring and a = πⁿ, this supplies the smooth charts away from the origin in the local model used to resolve nodal curves.

References

• Stacks Project, Example 55.14.1, Tag 0CDC.

def TauCeti.NodeAlgebra (R : Type u_1) [CommRing R] (a : R) : Type u_1

The coordinate algebra of the equation xy = a over R.

Equations

• TauCeti.NodeAlgebra R a = (MvPolynomial (Fin 2) R ⧸ Ideal.span {MvPolynomial.X 0 * MvPolynomial.X 1 - MvPolynomial.C a})

@[instance_reducible]

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

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.NodeAlgebra.instAlgebra {R : Type u_1} [CommRing R] (a : R) : Algebra R (NodeAlgebra R a)

Equations

• TauCeti.NodeAlgebra.instAlgebra a = { smul := TauCeti.NodeAlgebra.instAlgebra._aux_1 a, algebraMap := TauCeti.NodeAlgebra.instAlgebra._aux_3 a, commutes' := ⋯, smul_def' := ⋯ }

noncomputable def TauCeti.NodeAlgebra.mk {R : Type u_1} [CommRing R] (a : R) : MvPolynomial (Fin 2) R →ₐ[R] NodeAlgebra R a

The quotient algebra map from polynomials to the nodal algebra.

Equations

• TauCeti.NodeAlgebra.mk a = Ideal.Quotient.mkₐ R (Ideal.span {MvPolynomial.X 0 * MvPolynomial.X 1 - MvPolynomial.C a})

theorem TauCeti.NodeAlgebra.mk_surjective {R : Type u_1} [CommRing R] (a : R) : Function.Surjective ⇑(mk a)

Every element of the nodal algebra is represented by a polynomial.

@[simp]

theorem TauCeti.NodeAlgebra.ker_mk {R : Type u_1} [CommRing R] (a : R) : RingHom.ker ↑(mk a) = Ideal.span {MvPolynomial.X 0 * MvPolynomial.X 1 - MvPolynomial.C a}

The kernel of the quotient map is generated by the nodal equation.

noncomputable def TauCeti.NodeAlgebra.coord {R : Type u_1} [CommRing R] (a : R) (i : Fin 2) : NodeAlgebra R a

The two coordinate functions on xy = a.

Equations

• TauCeti.NodeAlgebra.coord a i = (TauCeti.NodeAlgebra.mk a) (MvPolynomial.X i)

@[simp]

theorem TauCeti.NodeAlgebra.mk_X {R : Type u_1} [CommRing R] (a : R) (i : Fin 2) : (mk a) (MvPolynomial.X i) = coord a i

The quotient map sends each polynomial variable to its coordinate function.

@[simp]

theorem TauCeti.NodeAlgebra.coord_zero_mul_coord_one {R : Type u_1} [CommRing R] (a : R) : coord a 0 * coord a 1 = (algebraMap R (NodeAlgebra R a)) a

The defining equation of the nodal algebra.

noncomputable def TauCeti.NodeAlgebra.lift {R : Type u_1} [CommRing R] (a : R) {A : Type u_2} [CommSemiring A] [Algebra R A] (x y : A) (h : x * y = (algebraMap R A) a) : NodeAlgebra R a →ₐ[R] A

Evaluate the nodal algebra at two elements satisfying its defining equation.

Equations

• TauCeti.NodeAlgebra.lift a x y h = Ideal.Quotient.liftₐ (Ideal.span {MvPolynomial.X 0 * MvPolynomial.X 1 - MvPolynomial.C a}) (MvPolynomial.aeval ![x, y]) ⋯

@[simp]

theorem TauCeti.NodeAlgebra.lift_mk {R : Type u_1} [CommRing R] (a : R) {A : Type u_2} [CommSemiring A] [Algebra R A] (x y : A) (h : x * y = (algebraMap R A) a) (p : MvPolynomial (Fin 2) R) : (lift a x y h) ((mk a) p) = (MvPolynomial.aeval ![x, y]) p

Evaluation on a polynomial representative is polynomial evaluation at the two elements.

theorem TauCeti.NodeAlgebra.lift_coord_zero {R : Type u_1} [CommRing R] (a : R) {A : Type u_2} [CommSemiring A] [Algebra R A] (x y : A) (h : x * y = (algebraMap R A) a) : (lift a x y h) (coord a 0) = x

Evaluation sends the first coordinate to the chosen first element.

theorem TauCeti.NodeAlgebra.lift_coord_one {R : Type u_1} [CommRing R] (a : R) {A : Type u_2} [CommSemiring A] [Algebra R A] (x y : A) (h : x * y = (algebraMap R A) a) : (lift a x y h) (coord a 1) = y

Evaluation sends the second coordinate to the chosen second element.

theorem TauCeti.NodeAlgebra.coord_mul_coord_one_sub {R : Type u_1} [CommRing R] (a : R) (i : Fin 2) : coord a i * coord a (1 - i) = (algebraMap R (NodeAlgebra R a)) a

The defining equation xy = a, written for either coordinate and the other one.

@[simp]

theorem TauCeti.NodeAlgebra.lift_coord {R : Type u_1} [CommRing R] (a : R) {A : Type u_2} [CommSemiring A] [Algebra R A] (x y : A) (h : x * y = (algebraMap R A) a) (i : Fin 2) : (lift a x y h) (coord a i) = ![x, y] i

Evaluation sends each coordinate to the corresponding chosen element.

theorem TauCeti.NodeAlgebra.hom_ext {R : Type u_1} [CommRing R] (a : R) {A : Type u_2} [Semiring A] [Algebra R A] {f g : NodeAlgebra R a →ₐ[R] A} (h₀ : f (coord a 0) = g (coord a 0)) (h₁ : f (coord a 1) = g (coord a 1)) : f = g

Algebra maps out of the nodal algebra are determined by the two coordinates.

theorem TauCeti.NodeAlgebra.hom_ext_iff {R : Type u_1} [CommRing R] {a : R} {A : Type u_2} [Semiring A] [Algebra R A] {f g : NodeAlgebra R a →ₐ[R] A} : f = g ↔ f (coord a 0) = g (coord a 0) ∧ f (coord a 1) = g (coord a 1)

theorem TauCeti.NodeAlgebra.adjoin_range_coord {R : Type u_1} [CommRing R] (a : R) : Algebra.adjoin R (Set.range (coord a)) = ⊤

The two coordinates generate the nodal algebra as an R-algebra.

noncomputable def TauCeti.NodeAlgebra.presentation {R : Type u_1} [CommRing R] (a : R) : Algebra.Presentation R (NodeAlgebra R a) (Fin 2) Unit

The presentation of R[x, y] ⧸ (xy - a) by its two coordinates and the single relation xy - a.

Equations

• TauCeti.NodeAlgebra.presentation a = (Algebra.Presentation.naive (Function.surjInv ⋯) ⋯).ofAlgEquiv (Ideal.quotientEquivAlgOfEq R ⋯)

@[simp]

theorem TauCeti.NodeAlgebra.presentation_relation {R : Type u_1} [CommRing R] (a : R) (r : Unit) : (presentation a).relation r = MvPolynomial.X 0 * MvPolynomial.X 1 - MvPolynomial.C a

The single relation of NodeAlgebra.presentation is xy - a.

instance TauCeti.NodeAlgebra.instFinitePresentation {R : Type u_1} [CommRing R] (a : R) : Algebra.FinitePresentation R (NodeAlgebra R a)

The nodal equation is an algebra of finite presentation over its coefficient ring.

theorem TauCeti.NodeAlgebra.isStandardSmoothOfRelativeDimension_localizationAway_coord {R : Type u_1} [CommRing R] (a : R) (i : Fin 2) : Algebra.IsStandardSmoothOfRelativeDimension 1 R (Localization.Away (coord a i))

Each coordinate chart of xy = a is standard smooth of relative dimension one.

theorem TauCeti.NodeAlgebra.basicOpen_coord_subset_smoothLocus {R : Type u_1} [CommRing R] (a : R) (i : Fin 2) : ↑(PrimeSpectrum.basicOpen (coord a i)) ⊆ Algebra.smoothLocus R (NodeAlgebra R a)

The complement of either coordinate's zero locus lies in the smooth locus of xy = a.

theorem TauCeti.NodeAlgebra.isSmoothAt_of_coord_notMem {R : Type u_1} [CommRing R] (a : R) (p : Ideal (NodeAlgebra R a)) [p.IsPrime] (h : ∃ (i : Fin 2), coord a i ∉ p) : Algebra.IsSmoothAt R p

A point of xy = a is smooth whenever at least one coordinate is outside its prime ideal.

theorem TauCeti.NodeAlgebra.isStandardSmoothOfRelativeDimension_of_isUnit {R : Type u_1} [CommRing R] (a : R) (ha : IsUnit a) : Algebra.IsStandardSmoothOfRelativeDimension 1 R (NodeAlgebra R a)

If the smoothing parameter is invertible, the whole nodal algebra is standard smooth of relative dimension one. This includes xy = 1 and xy = a over a field with a ≠ 0.