Derivations of the nodal equation

For B = R[x,y]/(xy-a) and any B-module M, an R-derivation from B to M is determined by its values u and v on x and y. The equation imposes precisely y • u + x • v = 0. This calculation gives the Jacobian relation used in the presentation of the relative differentials of a node.

The statement holds over any commutative coefficient ring and for any smoothing parameter.

References

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

noncomputable def TauCeti.NodeAlgebra.DerivationValues {R : Type u_1} [CommRing R] (a : R) {M : Type u_2} [AddCommMonoid M] [Module (NodeAlgebra R a) M] : Submodule (NodeAlgebra R a) (Fin 2 → M)

The pairs of possible values in M of an R-derivation on the two coordinates of xy=a.

Equations

• TauCeti.NodeAlgebra.DerivationValues a = { toFun := fun (u : Fin 2 → M) => TauCeti.NodeAlgebra.coord a 1 • u 0 + TauCeti.NodeAlgebra.coord a 0 • u 1, map_add' := ⋯, map_smul' := ⋯ }.ker

@[simp]

theorem TauCeti.NodeAlgebra.mem_derivationValues_iff {R : Type u_1} [CommRing R] (a : R) {M : Type u_2} [AddCommMonoid M] [Module (NodeAlgebra R a) M] (u : Fin 2 → M) : u ∈ DerivationValues a ↔ coord a 1 • u 0 + coord a 0 • u 1 = 0

A pair belongs to DerivationValues exactly when it satisfies the differentiated equation yu+xv=0.

@[simp]

theorem Derivation.coord_one_smul_apply_coord_zero_add_coord_zero_smul_apply_coord_one {R : Type u_1} [CommRing R] {a : R} {M : Type u_2} [AddCommMonoid M] [Module (TauCeti.NodeAlgebra R a) M] [Module R M] (D : Derivation R (TauCeti.NodeAlgebra R a) M) : TauCeti.NodeAlgebra.coord a 1 • D (TauCeti.NodeAlgebra.coord a 0) + TauCeti.NodeAlgebra.coord a 0 • D (TauCeti.NodeAlgebra.coord a 1) = 0

The coordinate values of any derivation satisfy the Jacobian relation of xy = a.

theorem TauCeti.NodeAlgebra.derivation_ext {R : Type u_1} [CommRing R] (a : R) {M : Type u_2} [AddCommMonoid M] [Module (NodeAlgebra R a) M] [Module R M] {D E : Derivation R (NodeAlgebra R a) M} (h : ∀ (i : Fin 2), D (coord a i) = E (coord a i)) : D = E

An R-derivation of the nodal algebra is uniquely determined by its values on the two coordinates.

theorem TauCeti.NodeAlgebra.derivation_ext_iff {R : Type u_1} [CommRing R] {a : R} {M : Type u_2} [AddCommMonoid M] [Module (NodeAlgebra R a) M] [Module R M] {D E : Derivation R (NodeAlgebra R a) M} : D = E ↔ ∀ (i : Fin 2), D (coord a i) = E (coord a i)

noncomputable def TauCeti.NodeAlgebra.derivationEquivValues {R : Type u_1} [CommRing R] (a : R) {M : Type u_2} [AddCommMonoid M] [Module (NodeAlgebra R a) M] [Module R M] [IsScalarTower R (NodeAlgebra R a) M] : Derivation R (NodeAlgebra R a) M ≃ₗ[NodeAlgebra R a] ↥(DerivationValues a)

Derivations of R[x,y]/(xy-a) into any module are linearly equivalent to pairs of values satisfying y • u + x • v = 0.

Equations

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

@[simp]

theorem TauCeti.NodeAlgebra.derivationEquivValues_apply {R : Type u_1} [CommRing R] (a : R) {M : Type u_2} [AddCommMonoid M] [Module (NodeAlgebra R a) M] [Module R M] [IsScalarTower R (NodeAlgebra R a) M] (D : Derivation R (NodeAlgebra R a) M) (i : Fin 2) : ↑((derivationEquivValues a) D) i = D (coord a i)

Evaluation of the derivation equivalence at a coordinate.

@[simp]

theorem TauCeti.NodeAlgebra.derivationEquivValues_symm_apply {R : Type u_1} [CommRing R] (a : R) {M : Type u_2} [AddCommMonoid M] [Module (NodeAlgebra R a) M] [Module R M] [IsScalarTower R (NodeAlgebra R a) M] (u : ↥(DerivationValues a)) (i : Fin 2) : ((derivationEquivValues a).symm u) (coord a i) = ↑u i

Evaluation of the inverse equivalence at a coordinate.