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

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

@[reducible, inline]

abbrev DualNumber (R : Type u_4) : Type u_4

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

Equations

• DualNumber R = TrivSqZeroExt R R

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

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

Equations

• DualNumber.eps = TrivSqZeroExt.inr 1

def DualNumber.termε : Lean.ParserDescr

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

Equations

• DualNumber.termε = Lean.ParserDescr.node `DualNumber.termε 1024 (Lean.ParserDescr.symbol "ε")

def DualNumber.«term_[ε]» : Lean.TrailingParserDescr

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

Equations

• DualNumber.«term_[ε]» = Lean.ParserDescr.trailingNode `DualNumber.«term_[ε]» 1024 1024 (Lean.ParserDescr.symbol "[ε]")

@[simp]

theorem DualNumber.fst_eps {R : Type u_1} [Zero R] [One R] : TrivSqZeroExt.fst eps = 0

@[simp]

theorem DualNumber.snd_eps {R : Type u_1} [Zero R] [One R] : TrivSqZeroExt.snd eps = 1

@[simp]

theorem DualNumber.snd_mul {R : Type u_1} [Semiring R] (x y : DualNumber R) : TrivSqZeroExt.snd (x * y) = TrivSqZeroExt.fst x * TrivSqZeroExt.snd y + TrivSqZeroExt.snd x * TrivSqZeroExt.fst y

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

@[simp]

theorem DualNumber.eps_mul_eps {R : Type u_1} [Semiring R] : eps * eps = 0

@[simp]

theorem DualNumber.inv_eps {R : Type u_1} [DivisionRing R] : eps⁻¹ = 0

@[simp]

theorem DualNumber.inr_eq_smul_eps {R : Type u_1} [MulZeroOneClass R] (r : R) : TrivSqZeroExt.inr r = r • eps

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

ε commutes with every element of the algebra.

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

ε commutes with every element of the algebra.

theorem DualNumber.algHom_ext' {R : Type u_1} {B : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] ⦃f g : DualNumber A →ₐ[R] B⦄ (hinl : f.comp (TrivSqZeroExt.inlAlgHom R A A) = g.comp (TrivSqZeroExt.inlAlgHom R A A)) (hinr : f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A (DualNumber A) eps) = g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A (DualNumber A) 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'_iff {R : Type u_1} {B : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {f g : DualNumber A →ₐ[R] B} : f = g ↔ f.comp (TrivSqZeroExt.inlAlgHom R A A) = g.comp (TrivSqZeroExt.inlAlgHom R A A) ∧ f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A (DualNumber A) eps) = g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A (DualNumber A) eps)

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

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

theorem DualNumber.algHom_ext_iff {R : Type u_1} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] {f g : DualNumber R →ₐ[R] A} : f = g ↔ f eps = g eps

def DualNumber.lift {R : Type u_1} {B : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) } ≃ (DualNumber 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.

theorem DualNumber.lift_apply_apply {R : Type u_1} {B : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [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 A) : (lift fe) a = (↑fe).1 (TrivSqZeroExt.fst a) + (↑fe).1 (TrivSqZeroExt.snd a) * (↑fe).2

@[simp]

theorem DualNumber.coe_lift_symm_apply {R : Type u_1} {B : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (F : DualNumber A →ₐ[R] B) : ↑(lift.symm F) = (F.comp (TrivSqZeroExt.inlAlgHom R A A), F eps)

@[simp]

theorem DualNumber.lift_apply_inl {R : Type u_1} {B : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [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) : (lift fe) (TrivSqZeroExt.inl a) = (↑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} [CommSemiring R] [Semiring A] [Semiring B] [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 : DualNumber A) : (lift fe) (a • ad) = (↑fe).1 a * (lift fe) 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} [CommSemiring R] [Semiring A] [Semiring B] [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 : DualNumber A) : (lift fe) (MulOpposite.op a • ad) = (lift fe) ad * (↑fe).1 a

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} [CommSemiring R] [Semiring A] [Semiring B] [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) }) : (lift fe) 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} [CommSemiring R] [Semiring A] [Algebra R A] : lift ⟨(TrivSqZeroExt.inlAlgHom R A A, eps), ⋯⟩ = AlgHom.id R (DualNumber A)

Lifting DualNumber.eps itself gives the identity.

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

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.