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:

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

Main definitions #

Implementation notes #

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

References #

https://en.wikipedia.org/wiki/Dual_number

source

@[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$.

source

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

dual_number R

The unit element $ε$ that squares to zero.

Equations

dual_number.eps = triv_sq_zero_ext.inr 1

source

@[simp]

theorem dual_number.fst_eps {R : Type u_1} [has_zero R] [has_one R] :

triv_sq_zero_ext.fst dual_number.eps = 0

source

@[simp]

theorem dual_number.snd_eps {R : Type u_1} [has_zero R] [has_one R] :

triv_sq_zero_ext.snd dual_number.eps = 1

source

@[simp]

theorem dual_number.snd_mul {R : Type u_1} [semiring R] (x y : dual_number R) :

(x * y).snd = triv_sq_zero_ext.fst x * triv_sq_zero_ext.snd y + triv_sq_zero_ext.snd x * triv_sq_zero_ext.fst y

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

source

@[simp]

theorem dual_number.eps_mul_eps {R : Type u_1} [semiring R] :

dual_number.eps * dual_number.eps = 0

source

@[simp]

theorem dual_number.inr_eq_smul_eps {R : Type u_1} [mul_zero_one_class R] (r : R) :

triv_sq_zero_ext.inr r = r • dual_number.eps

source

@[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 ε.

source

theorem dual_number.lift_symm_apply_coe {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (ᾰ : dual_number R →ₐ[R] A) :

↑(⇑(dual_number.lift.symm) ᾰ) = ⇑ᾰ (triv_sq_zero_ext.inr 1)

source

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

dual_number.lift = (show {e // e * e = 0} ≃ {f // ∀ (x y : R), ⇑f x * ⇑f y = 0}, from (linear_map.ring_lmap_equiv_self R ℕ A).symm.to_equiv.subtype_equiv dual_number.lift._proof_7).trans triv_sq_zero_ext.lift

source

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 • ↑ᾰ

source

@[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}) :

⇑(⇑dual_number.lift e) dual_number.eps = ↑e

source

@[simp]

theorem dual_number.lift_eps {R : Type u_1} [comm_semiring R] :

⇑dual_number.lift ⟨dual_number.eps (add_monoid_with_one.to_has_one R), _⟩ = alg_hom.id R (dual_number R)