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:

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_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
    source
    def DualNumber.eps {R : Type u_1} [Zero R] [One R] :
    DualNumber R

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

    Equations
    Instances For
      source
      def DualNumber.termε :
      Lean.ParserDescr

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

      Equations
      Instances For
        source
        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
          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.inv_eps {R : Type u_1} [DivisionRing R] :
          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.commute_eps_left {R : Type u_1} [Semiring R] (x : DualNumber R) :
          Commute DualNumber.eps x

          ε commutes with every element of the algebra.

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

          ε commutes with every element of the algebra.

          source
          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 : DualNumber A →ₐ[R] B⦄ ⦃g : DualNumber A →ₐ[R] B⦄ (hinl : AlgHom.comp f (TrivSqZeroExt.inlAlgHom R A A) = AlgHom.comp g (TrivSqZeroExt.inlAlgHom R A A)) (hinr : AlgHom.toLinearMap f ∘ₗ ↑R (LinearMap.toSpanSingleton A (DualNumber A) DualNumber.eps) = AlgHom.toLinearMap g ∘ₗ ↑R (LinearMap.toSpanSingleton A (DualNumber 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 ε.

          source
          theorem DualNumber.algHom_ext {R : Type u_1} {A : Type u_4} [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 R-algebra morphisms out of R[ε] to agree, it suffices for them to agree on ε.

          source
          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.
          Instances For
            source
            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) :
            (DualNumber.lift fe) a = (↑fe).1 (TrivSqZeroExt.fst a) + (↑fe).1 (TrivSqZeroExt.snd a) * (↑fe).2
            source
            @[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) :
            ↑(DualNumber.lift.symm F) = (AlgHom.comp F (TrivSqZeroExt.inlAlgHom R A A), F DualNumber.eps)
            source
            @[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) :
            (DualNumber.lift fe) (TrivSqZeroExt.inl a) = (↑fe).1 a

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

            source
            @[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) :
            (DualNumber.lift fe) (a • ad) = (↑fe).1 a * (DualNumber.lift fe) ad

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

            source
            @[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) :
            (DualNumber.lift fe) (MulOpposite.op a • ad) = (DualNumber.lift fe) ad * (↑fe).1 a

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

            source
            @[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) }) :
            (DualNumber.lift fe) DualNumber.eps = (↑fe).2

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

            source
            @[simp]
            theorem DualNumber.lift_inlAlgHom_eps {R : Type u_1} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] :
            DualNumber.lift { val := (TrivSqZeroExt.inlAlgHom R A A, DualNumber.eps), property := ⋯ } = AlgHom.id R (DualNumber A)

            Lifting DualNumber.eps itself gives the identity.