Documentation

Mathlib.Algebra.DualNumber

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 #

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ε$ 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

Instances For

def DualNumber.termε :

Lean.ParserDescr

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

Equations

Instances For

def DualNumber.«term_[ε]» :

Lean.TrailingParserDescr

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 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] :

@[simp]

theorem DualNumber.inv_eps {R : Type u_1} [DivisionRing R] :

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

ε commutes with every element of the algebra.

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

ε 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

Instances For

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_comp_inlHom {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).comp (TrivSqZeroExt.inlAlgHom R A A) = (↑fe).1

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

@[simp]

theorem DualNumber.range_inlAlgHom_sup_adjoin_eps {R : Type u_1} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] :

(TrivSqZeroExt.inlAlgHom R A A).range ⊔ Algebra.adjoin R {eps } = ⊤

@[simp]

theorem DualNumber.range_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 : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }) :

(lift fe).range = (↑fe).1.range ⊔ Algebra.adjoin R {(↑fe).2}

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