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. They are a special case of TrivSqZeroExt R M with M = R.

Notation #

In the DualNumber locale:

Main definitions #

Implementation notes #

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

References #

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

The type of dual numbers, numbers of the form $a + bε$ where $ε^2 = 0$.

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

    The unit element $ε$ that squares to zero.

    Instances For
      source
      def DualNumber.termε :
      Lean.ParserDescr
      Instances For
        source
        def DualNumber.«term_[ε]» :
        Lean.TrailingParserDescr
        Instances For
          source
          @[simp]
          theorem DualNumber.fst_eps {R : Type u_1} [Zero R] [One R] :
          TrivSqZeroExt.fst DualNumber.eps = 0
          source
          @[simp]
          theorem DualNumber.snd_eps {R : Type u_1} [Zero R] [One R] :
          TrivSqZeroExt.snd DualNumber.eps = 1
          source
          @[simp]
          theorem DualNumber.snd_mul {R : Type u_1} [Semiring R] (x : DualNumber R) (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 •.

          source
          @[simp]
          theorem DualNumber.eps_mul_eps {R : Type u_1} [Semiring R] :
          DualNumber.eps * DualNumber.eps = 0
          source
          @[simp]
          theorem DualNumber.inr_eq_smul_eps {R : Type u_1} [MulZeroOneClass R] (r : R) :
          TrivSqZeroExt.inr r = r • DualNumber.eps
          source
          theorem DualNumber.algHom_ext {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] ⦃f : DualNumber R →ₐ[R] A⦄ ⦃g : DualNumber R →ₐ[R] A⦄ (h : ↑f DualNumber.eps = ↑g DualNumber.eps) :
          f = g

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

          source
          @[simp]
          theorem DualNumber.lift_apply_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
          ∀ (a : { e // e * e = 0 }) (a_1 : TrivSqZeroExt R R), ↑(↑DualNumber.lift a) a_1 = ↑(algebraMap R A) (TrivSqZeroExt.fst a_1) + TrivSqZeroExt.snd a_1 • ↑a
          source
          @[simp]
          theorem DualNumber.lift_symm_apply_coe {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
          ∀ (a : DualNumber R →ₐ[R] A), ↑(↑DualNumber.lift.symm a) = ↑↑(LinearMap.ringLmapEquivSelf R ℕ A) (LinearMap.comp (AlgHom.toLinearMap a) (TrivSqZeroExt.inrHom R R))
          source
          def DualNumber.lift {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
          { e // e * e = 0 } ≃ (DualNumber 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.

          Instances For
            source
            theorem DualNumber.lift_apply_eps {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (e : { e // e * e = 0 }) :
            ↑(↑DualNumber.lift e) DualNumber.eps = ↑e
            source
            @[simp]
            theorem DualNumber.lift_eps {R : Type u_1} [CommSemiring R] :
            ↑DualNumber.lift { val := DualNumber.eps, property := (_ : DualNumber.eps * DualNumber.eps = 0) } = AlgHom.id R (DualNumber R)