# mathlibdocumentation

algebra.dual_number

# Dual numbers #

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:

• R[ε] is a shorthand for dual_number R
• ε is a shorthand for dual_number.eps

## Main definitions #

• dual_number
• dual_number.eps
• dual_number.lift

## 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]
theorem dual_number.fst_eps {R : Type u_1} [has_zero R] [has_one R] :
@[simp]
theorem dual_number.snd_eps {R : Type u_1} [has_zero R] [has_one R] :
@[simp]
theorem dual_number.snd_mul {R : Type u_1} [semiring R] (x y : dual_number R) :

A version of triv_sq_zero_ext.snd_mul with * instead of •.

@[simp]
theorem dual_number.eps_mul_eps {R : Type u_1} [semiring R] :
@[simp]
theorem dual_number.inr_eq_smul_eps {R : Type u_1} (r : R) :
@[ext]
theorem dual_number.alg_hom_ext {R : Type u_1} {A : Type u_2} [semiring A] [ A] ⦃f g : →ₐ[R] A⦄ (h : = ) :
f = g

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

theorem dual_number.lift_symm_apply_coe {R : Type u_1} {A : Type u_2} [semiring A] [ A] (ᾰ : →ₐ[R] A) :
def dual_number.lift {R : Type u_1} {A : Type u_2} [semiring A] [ A] :
{e // e * e = 0} →ₐ[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} [semiring A] [ A] (ᾰ : {e // e * e = 0}) (ᾰ_1 : R) :
ᾰ_1 = A) ᾰ_1.fst + ᾰ_1.snd
@[simp]
theorem dual_number.lift_apply_eps {R : Type u_1} {A : Type u_2} [semiring A] [ A] (e : {e // e * e = 0}) :
@[simp]
theorem dual_number.lift_eps {R : Type u_1}  :