The singular subscheme of a node chart

For every commutative ring R and smoothing parameter a : R, the relative singular subscheme of Spec R[x,y]/(xy-a) is canonically Spec R/(a) over Spec R. In particular its structure morphism is a closed immersion and is unramified. This supplies the singular-locus condition in the scheme-theoretic criterion for nodal curves. The identification retains the scheme structure even when a is nilpotent or a zero divisor.

The relative singular locus is cut out by the two coordinates x and y (NodeAlgebra.singularLocus_ideal_top). The construction uses the first Fitting ideal of the relative differentials and the algebraic identification NodeAlgebra.jacobianQuotientEquiv.

References

• Stacks Project, Lemma 53.20.1, Tag 0C58.
• Stacks Project, Example 55.14.1, Tag 0CDC.

@[instance_reducible]

noncomputable def TauCeti.NodeAlgebra.nodeSpecOverSpec {R : Type u} [CommRing R] (a : R) : (AlgebraicGeometry.Spec ↧(NodeAlgebra R a)).Over (AlgebraicGeometry.Spec ↧R)

The direct structure morphism on the node chart, used to avoid the Spec-over-Spec instance diamond when applying the singular-locus API.

Equations

• TauCeti.NodeAlgebra.nodeSpecOverSpec a = { hom := AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (TauCeti.NodeAlgebra R a))) }

theorem TauCeti.NodeAlgebra.instFlatOverSchemeSpecOfInferInstanceOverClass {R : Type u} [CommRing R] (a : R) : AlgebraicGeometry.Flat (AlgebraicGeometry.Spec ↧(NodeAlgebra R a) ↘ AlgebraicGeometry.Spec ↧R)

theorem TauCeti.NodeAlgebra.instLocallyOfFinitePresentationOverSchemeSpecOfInferInstanceOverClass {R : Type u} [CommRing R] (a : R) : AlgebraicGeometry.LocallyOfFinitePresentation (AlgebraicGeometry.Spec ↧(NodeAlgebra R a) ↘ AlgebraicGeometry.Spec ↧R)

theorem TauCeti.NodeAlgebra.instPureRelativeDimensionOfNatNatOverSchemeSpecOfInferInstanceOverClass {R : Type u} [CommRing R] (a : R) : AlgebraicGeometry.PureRelativeDimension 1 (AlgebraicGeometry.Spec ↧(NodeAlgebra R a) ↘ AlgebraicGeometry.Spec ↧R)

theorem TauCeti.NodeAlgebra.singularLocus_ideal_top {R : Type u} [CommRing R] (a : R) : (AlgebraicGeometry.Scheme.singularLocus R (AlgebraicGeometry.Spec ↧(NodeAlgebra R a))).ideal ⟨⊤, ⋯⟩ = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧(NodeAlgebra R a)).inv) (Ideal.span {coord a 0, coord a 1})

The relative singular locus of the local model of a node Spec R[x, y] ⧸ (xy - a) over R is cut out by the ideal (x, y) of the two coordinates.

noncomputable def TauCeti.NodeAlgebra.singularLocusIso {R : Type u} [CommRing R] (a : R) : (AlgebraicGeometry.Scheme.singularLocus R (AlgebraicGeometry.Spec ↧(NodeAlgebra R a))).subscheme ≅ AlgebraicGeometry.Spec ↧(R ⧸ Ideal.span {a})

The relative singular subscheme of the node chart xy = a is Spec R/(a).

Equations

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

@[simp]

theorem TauCeti.NodeAlgebra.singularLocusIso_inv_comp {R : Type u} [CommRing R] (a : R) : CategoryTheory.CategoryStruct.comp (singularLocusIso a).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.singularLocus R (AlgebraicGeometry.Spec ↧(NodeAlgebra R a))).subschemeι (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (NodeAlgebra R a))))) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {a})))

The singular-locus identification is an isomorphism over Spec R.

@[simp]

theorem TauCeti.NodeAlgebra.singularLocusIso_inv_comp_assoc {R : Type u} [CommRing R] (a : R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularLocusIso a).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.singularLocus R (AlgebraicGeometry.Spec ↧(NodeAlgebra R a))).subschemeι (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (NodeAlgebra R a)))) h)) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {a})))) h

The singular-locus identification is an isomorphism over Spec R.

@[simp]

theorem TauCeti.NodeAlgebra.singularLocusIso_hom_comp {R : Type u} [CommRing R] (a : R) : CategoryTheory.CategoryStruct.comp (singularLocusIso a).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {a})))) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.singularLocus R (AlgebraicGeometry.Spec ↧(NodeAlgebra R a))).subschemeι (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (NodeAlgebra R a))))

The forward singular-locus identification commutes with the maps to Spec R.

@[simp]

theorem TauCeti.NodeAlgebra.singularLocusIso_hom_comp_assoc {R : Type u} [CommRing R] (a : R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularLocusIso a).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {a})))) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.singularLocus R (AlgebraicGeometry.Spec ↧(NodeAlgebra R a))).subschemeι (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (NodeAlgebra R a)))) h)

The forward singular-locus identification commutes with the maps to Spec R.

instance TauCeti.NodeAlgebra.isClosedImmersion_singularLocus {R : Type u} [CommRing R] (a : R) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.singularLocus R (AlgebraicGeometry.Spec ↧(NodeAlgebra R a))).subschemeι (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (NodeAlgebra R a)))))

The singular subscheme of xy = a maps to Spec R by a closed immersion. Consequently it is unramified over R, as required by the nodal-curve criterion.