The Jacobian locus of a nodal chart

For the equation xy = a, the first Fitting ideal of the relative differentials is generated by x and y. Its quotient is the base ring modulo a. Thus the closed subscheme cut out by the Jacobian ideal is precisely the zero locus of the smoothing parameter, with no assumption that the base is reduced or that a is a non-zero-divisor.

References

• Stacks Project, Example 55.14.1, Tag 0CDC.

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

The ideal generated by the two coordinates in the nodal equation xy = a.

Equations

• TauCeti.NodeAlgebra.jacobianIdeal a = Ideal.span {TauCeti.NodeAlgebra.coord a 0, TauCeti.NodeAlgebra.coord a 1}

@[simp]

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

Each coordinate belongs to the Jacobian ideal.

noncomputable def TauCeti.NodeAlgebra.jacobianQuotientEquiv {R : Type u_1} [CommRing R] (a : R) : (NodeAlgebra R a ⧸ jacobianIdeal a) ≃ₐ[R] R ⧸ Ideal.span {a}

The Jacobian quotient of R[x,y]/(xy-a) is canonically R/(a).

Equations

• TauCeti.NodeAlgebra.jacobianQuotientEquiv a = (Ideal.quotientEquivAlgOfEq R ⋯).trans (Ideal.quotientKerAlgEquivOfSurjective ⋯)

noncomputable def TauCeti.NodeAlgebra.differentialFittingQuotientEquiv {R : Type u_1} [CommRing R] (a : R) : (NodeAlgebra R a ⧸ fittingIdeal (NodeAlgebra R a) Ω[NodeAlgebra R a⁄R] 1) ≃ₐ[R] R ⧸ Ideal.span {a}

The closed subscheme cut out by the first Fitting ideal of the relative differentials has coordinate ring R/(a).

Equations

• TauCeti.NodeAlgebra.differentialFittingQuotientEquiv a = (Ideal.quotientEquivAlgOfEq R ⋯).trans (TauCeti.NodeAlgebra.jacobianQuotientEquiv a)

@[simp]

theorem TauCeti.NodeAlgebra.jacobianQuotientEquiv_coord {R : Type u_1} [CommRing R] (a : R) (i : Fin 2) : (jacobianQuotientEquiv a) ((Ideal.Quotient.mk (jacobianIdeal a)) (coord a i)) = 0

Both coordinates vanish in the Jacobian quotient.

@[simp]

theorem TauCeti.NodeAlgebra.jacobianQuotientEquiv_symm_mk {R : Type u_1} [CommRing R] (a r : R) : (jacobianQuotientEquiv a).symm ((Ideal.Quotient.mk (Ideal.span {a})) r) = (Ideal.Quotient.mk (jacobianIdeal a)) ((algebraMap R (NodeAlgebra R a)) r)

The inverse equivalence sends a base class to its image in the Jacobian quotient.

@[simp]

theorem TauCeti.NodeAlgebra.differentialFittingQuotientEquiv_coord {R : Type u_1} [CommRing R] (a : R) (i : Fin 2) : (differentialFittingQuotientEquiv a) ((Ideal.Quotient.mk (fittingIdeal (NodeAlgebra R a) Ω[NodeAlgebra R a⁄R] 1)) (coord a i)) = 0

Both coordinates vanish under the Fitting quotient equivalence.

@[simp]

theorem TauCeti.NodeAlgebra.differentialFittingQuotientEquiv_symm_mk {R : Type u_1} [CommRing R] (a r : R) : (differentialFittingQuotientEquiv a).symm ((Ideal.Quotient.mk (Ideal.span {a})) r) = (Ideal.Quotient.mk (fittingIdeal (NodeAlgebra R a) Ω[NodeAlgebra R a⁄R] 1)) ((algebraMap R (NodeAlgebra R a)) r)

The inverse Fitting quotient equivalence sends a base class to its image.