# 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 that commutes with every other element. They are a special case of TrivSqZeroExt R M with M = R.

## Notation #

In the DualNumber locale:

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

## Main definitions #

• DualNumber
• DualNumber.eps
• DualNumber.lift

## Implementation notes #

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

## References #

@[reducible, inline]
abbrev DualNumber (R : Type u_4) :
Type u_4

The type of dual numbers, numbers of the form $a + bε$ where $ε^2 = 0$. R[ε] is notation for DualNumber R.

Equations
Instances For
def DualNumber.eps {R : Type u_1} [Zero R] [One R] :

The unit element $ε$ that squares to zero, with notation ε.

Equations
• DualNumber.eps =
Instances For

The unit element $ε$ that squares to zero, with notation ε.

Equations
Instances For

The type of dual numbers, numbers of the form $a + bε$ where $ε^2 = 0$. R[ε] is notation for DualNumber R.

Equations
Instances For
@[simp]
theorem DualNumber.fst_eps {R : Type u_1} [Zero R] [One R] :
TrivSqZeroExt.fst DualNumber.eps = 0
@[simp]
theorem DualNumber.snd_eps {R : Type u_1} [Zero R] [One R] :
TrivSqZeroExt.snd DualNumber.eps = 1
@[simp]
theorem DualNumber.snd_mul {R : Type u_1} [] (x : ) (y : ) :

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

@[simp]
theorem DualNumber.eps_mul_eps {R : Type u_1} [] :
DualNumber.eps * DualNumber.eps = 0
@[simp]
theorem DualNumber.inv_eps {R : Type u_1} [] :
DualNumber.eps⁻¹ = 0
@[simp]
theorem DualNumber.inr_eq_smul_eps {R : Type u_1} [] (r : R) :
= r DualNumber.eps
theorem DualNumber.commute_eps_left {R : Type u_1} [] (x : ) :
Commute DualNumber.eps x

ε commutes with every element of the algebra.

theorem DualNumber.commute_eps_right {R : Type u_1} [] (x : ) :
Commute x DualNumber.eps

ε commutes with every element of the algebra.

theorem DualNumber.algHom_ext' {R : Type u_1} {B : Type u_3} {A : Type u_4} [] [] [] [Algebra R A] [Algebra R B] ⦃f : →ₐ[R] B ⦃g : →ₐ[R] B (hinl : f.comp () = g.comp ()) (hinr : f.toLinearMap ∘ₗ R (LinearMap.toSpanSingleton A () DualNumber.eps) = g.toLinearMap ∘ₗ R (LinearMap.toSpanSingleton A () DualNumber.eps)) :
f = g

For two R-algebra morphisms out of A[ε] to agree, it suffices for them to agree on the elements of A and the A-multiples of ε.

theorem DualNumber.algHom_ext {R : Type u_1} {A : Type u_4} [] [] [Algebra R A] ⦃f : →ₐ[R] A ⦃g : →ₐ[R] A (hε : f DualNumber.eps = g DualNumber.eps) :
f = g

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

def DualNumber.lift {R : Type u_1} {B : Type u_3} {A : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :
{ fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∀ (a : A), Commute fe.2 (fe.1 a) } ( →ₐ[R] B)

A universal property of the dual numbers, providing a unique A[ε] →ₐ[R] B for every map f : A →ₐ[R] B and a choice of element e : B which squares to 0 and commutes with the range of f.

This isomorphism is named to match the similar Complex.lift. Note that when f : R →ₐ[R] B := Algebra.ofId R B, the commutativity assumption is automatic, and we are free to choose any element e : B.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem DualNumber.lift_apply_apply {R : Type u_1} {B : Type u_3} {A : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (fe : { _fe : (A →ₐ[R] B) × B // _fe.2 * _fe.2 = 0 ∀ (a : A), Commute _fe.2 (_fe.1 a) }) (a : ) :
(DualNumber.lift fe) a = (fe).1 + (fe).1 * (fe).2
@[simp]
theorem DualNumber.coe_lift_symm_apply {R : Type u_1} {B : Type u_3} {A : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (F : →ₐ[R] B) :
(DualNumber.lift.symm F) = (F.comp (), F DualNumber.eps)
@[simp]
theorem DualNumber.lift_apply_inl {R : Type u_1} {B : Type u_3} {A : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∀ (a : A), Commute fe.2 (fe.1 a) }) (a : A) :
(DualNumber.lift fe) = (fe).1 a

When applied to inl, DualNumber.lift applies the map f : A →ₐ[R] B.

@[simp]
theorem DualNumber.lift_smul {R : Type u_1} {B : Type u_3} {A : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∀ (a : A), Commute fe.2 (fe.1 a) }) (a : A) (ad : ) :

Scaling on the left is sent by DualNumber.lift to multiplication on the left

@[simp]
theorem DualNumber.lift_op_smul {R : Type u_1} {B : Type u_3} {A : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∀ (a : A), Commute fe.2 (fe.1 a) }) (a : A) (ad : ) :

Scaling on the right is sent by DualNumber.lift to multiplication on the right

@[simp]
theorem DualNumber.lift_apply_eps {R : Type u_1} {B : Type u_3} {A : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∀ (a : A), Commute fe.2 (fe.1 a) }) :
(DualNumber.lift fe) DualNumber.eps = (fe).2

When applied to ε, DualNumber.lift produces the element of B that squares to 0.

@[simp]
theorem DualNumber.lift_inlAlgHom_eps {R : Type u_1} {A : Type u_4} [] [] [Algebra R A] :
DualNumber.lift (, DualNumber.eps), = AlgHom.id R ()

Lifting DualNumber.eps itself gives the identity.

instance DualNumber.instRepr {R : Type u_1} [Repr R] :
Repr ()

Show DualNumber with values x and y as an "x + y*ε" string

Equations
• One or more equations did not get rendered due to their size.