mathlib3 documentation

algebra.dual_number

Dual numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The dual numbers over R are of the form a + bε, where a and b are typically elements of a commutative ring R, and ε is a symbol satisfying ε^2 = 0. They are a special case of triv_sq_zero_ext R M with M = R.

Notation #

In the dual_number locale:

Main definitions #

Implementation notes #

Rather than duplicating the API of triv_sq_zero_ext, this file reuses the functions there.

References #

@[reducible]
def dual_number (R : Type u_1) :
Type u_1

The type of dual numbers, numbers of the form $a + bε$ where $ε^2 = 0$.

def dual_number.eps {R : Type u_1} [has_zero R] [has_one R] :

The unit element $ε$ that squares to zero.

Equations
@[simp]

A version of triv_sq_zero_ext.snd_mul with * instead of .

@[ext]
theorem dual_number.alg_hom_ext {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] ⦃f g : dual_number R →ₐ[R] A⦄ (h : f dual_number.eps = g dual_number.eps) :
f = g

For two algebra morphisms out of R[ε] to agree, it suffices for them to agree on ε.

def dual_number.lift {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
{e // e * e = 0} (dual_number R →ₐ[R] A)

A universal property of the dual numbers, providing a unique R[ε] →ₐ[R] A for every element of A which squares to 0.

This isomorphism is named to match the very similar complex.lift.

Equations
theorem dual_number.lift_apply_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (ᾰ : {e // e * e = 0}) (ᾰ_1 : triv_sq_zero_ext R R) :
(dual_number.lift ᾰ) ᾰ_1 = (algebra_map R A) ᾰ_1.fst + ᾰ_1.snd
@[simp]
theorem dual_number.lift_apply_eps {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (e : {e // e * e = 0}) :