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 #

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

      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.eps_mul_eps {R : Type u_1} [Semiring R] :
          DualNumber.eps * DualNumber.eps = 0
          @[simp]
          theorem DualNumber.inv_eps {R : Type u_1} [DivisionRing R] :
          DualNumber.eps⁻¹ = 0
          @[simp]
          theorem DualNumber.inr_eq_smul_eps {R : Type u_1} [MulZeroOneClass R] (r : R) :
          TrivSqZeroExt.inr r = r DualNumber.eps
          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.

          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.

          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 : f.comp (TrivSqZeroExt.inlAlgHom R A A) = g.comp (TrivSqZeroExt.inlAlgHom R A A)) (hinr : f.toLinearMap ∘ₗ R (LinearMap.toSpanSingleton A (DualNumber A) DualNumber.eps) = g.toLinearMap ∘ₗ 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 ε.

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

          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
            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
            @[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) = (F.comp (TrivSqZeroExt.inlAlgHom R A A), F DualNumber.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) :
            (DualNumber.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) :
            (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

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

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

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

            Lifting DualNumber.eps itself gives the identity.

            instance DualNumber.instRepr {R : Type u_1} [Repr 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.