The Frobenius trace pairing on the dual numbers

This file equips the dual numbers over a commutative semiring with the perfect symmetric associative bilinear form obtained by taking the infinitesimal coefficient of a product.

Main results

• TauCeti.dualNumberTracePairing: the Frobenius trace pairing on the dual numbers.
• TauCeti.dualNumberTracePairing_isPerfPair: the trace pairing is perfect.
• TauCeti.dualNumberTracePairing_isSymm: the trace pairing is symmetric.
• TauCeti.dualNumberTracePairing_mul_assoc: the trace pairing is associative.

noncomputable def TauCeti.dualNumberTracePairing (k : Type w) [CommSemiring k] : LinearMap.BilinForm k (DualNumber k)

The Frobenius pairing on the dual numbers, obtained by taking the infinitesimal coefficient of a product.

Equations

• TauCeti.dualNumberTracePairing k = (LinearMap.mul k (DualNumber k)).compr₂ (TrivSqZeroExt.sndHom k k)

@[simp]

theorem TauCeti.dualNumberTracePairing_apply (k : Type w) [CommSemiring k] (x y : DualNumber k) : ((dualNumberTracePairing k) x) y = TrivSqZeroExt.fst x * TrivSqZeroExt.snd y + TrivSqZeroExt.snd x * TrivSqZeroExt.fst y

Evaluation of the dual-number Frobenius pairing in scalar and infinitesimal coordinates.

theorem TauCeti.dualNumberTracePairing_isSymm (k : Type w) [CommSemiring k] : (dualNumberTracePairing k).IsSymm

The Frobenius trace pairing on the dual numbers is symmetric.

instance TauCeti.dualNumberTracePairing_isPerfPair (k : Type w) [CommSemiring k] : LinearMap.IsPerfPair (dualNumberTracePairing k)

The Frobenius trace pairing on the dual numbers is perfect.

theorem TauCeti.dualNumberTracePairing_mul_assoc (k : Type w) [CommSemiring k] (x y z : DualNumber k) : ((dualNumberTracePairing k) (x * y)) z = ((dualNumberTracePairing k) x) (y * z)

The Frobenius trace pairing on the dual numbers is associative with multiplication.