Kähler differentials of the nodal equation

For B = R[x,y]/(xy-a), the module of relative Kähler differentials is the quotient of B² by the single relation y dx + x dy. This presentation describes the singularity of the nodal equation in terms of a finite module and is the input to its first Fitting ideal.

References

• Stacks Project, Section 10.131 (Differentials), Tag 00RM.

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

The Jacobian relation vector (y, x) for the equation xy = a.

Equations

• TauCeti.NodeAlgebra.differentialRelation a = ![TauCeti.NodeAlgebra.coord a 1, TauCeti.NodeAlgebra.coord a 0]

@[reducible, inline]

abbrev TauCeti.NodeAlgebra.PresentedDifferential {R : Type u_1} [CommRing R] (a : R) : Type u_1

The module generated by dx,dy subject to y dx + x dy = 0.

Equations

• TauCeti.NodeAlgebra.PresentedDifferential a = ((Fin 2 → TauCeti.NodeAlgebra R a) ⧸ TauCeti.NodeAlgebra R a ∙ TauCeti.NodeAlgebra.differentialRelation a)

noncomputable def TauCeti.NodeAlgebra.differentialEquivPresented {R : Type u_1} [CommRing R] (a : R) : Ω[NodeAlgebra R a⁄R] ≃ₗ[NodeAlgebra R a] PresentedDifferential a

The Jacobian presentation of the relative Kähler differentials of xy = a.

Equations

• TauCeti.NodeAlgebra.differentialEquivPresented a = LinearEquiv.ofLinearMap (TauCeti.NodeAlgebra.differentialToPresented✝ a) (TauCeti.NodeAlgebra.presentedToDifferential✝ a) ⋯ ⋯

@[simp]

theorem TauCeti.NodeAlgebra.differentialEquivPresented_D_coord {R : Type u_1} [CommRing R] (a : R) (i : Fin 2) : (differentialEquivPresented a) ((KaehlerDifferential.D R (NodeAlgebra R a)) (coord a i)) = Submodule.Quotient.mk (Pi.single i 1)

Under the presentation, the differential of a coordinate is its corresponding basis class.

@[simp]

theorem TauCeti.NodeAlgebra.differentialEquivPresented_symm_basis {R : Type u_1} [CommRing R] (a : R) (i : Fin 2) : (differentialEquivPresented a).symm (Submodule.Quotient.mk (Pi.single i 1)) = (KaehlerDifferential.D R (NodeAlgebra R a)) (coord a i)

The inverse presentation map sends each basis class to the differential of its coordinate.

@[simp]

theorem TauCeti.NodeAlgebra.fittingIdeal_differential_one {R : Type u_1} [CommRing R] (a : R) : fittingIdeal (NodeAlgebra R a) Ω[NodeAlgebra R a⁄R] 1 = Ideal.span {coord a 0, coord a 1}

The first Fitting ideal of the nodal differentials is generated by the two coordinates.