Dual Number Multiplicativity Criterion

Abstract

The canonical dual-number lift is multiplicative exactly under the product rule.

Theorem 1.1 (Multiplicativity is equivalent to the product rule).

$$\begin{array}{c}\forall R,A:\mathrm{Type},D:A\to A,\\ \mathrm{CommSemiring}(R)\wedge \mathrm{Semiring}(A)\wedge \mathrm{Algebra}(R,A)\wedge \mathrm{LinearMap}(R,D,A,A)\Rightarrow \\ (\forall a,b:A,(\mathrm{inl}(a\cdot b)+\mathrm{inr}(D(a\cdot b)))=(\mathrm{inl}(a)+\mathrm{inr}(D(a)))\cdot (\mathrm{inl}(b)+\mathrm{inr}(D(b))))⟺(\forall a,b:A,D(a\cdot b)=a\cdot D(b)+D(a)\cdot b).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Algebra/DualNumberMultiplicativityCriterion.dual_number_lift_preserves_mul_iff_product_rule (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let A be an algebra over a commutative scalar semiring R, and let D : A -> A be R-linear.

The displayed map uses the canonical inclusions into the square-zero extension. It preserves products exactly when D obeys the displayed left-right product rule.

References

• Truth anchor: D5/S3/ConceptDynamics/Algebra/DualNumberMultiplicativityCriterion.dual_number_lift_preserves_mul_iff_product_rule