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
@[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
    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 eps = 0
          source
          @[simp]
          theorem DualNumber.snd_eps {R : Type u_1} [Zero R] [One R] :
          TrivSqZeroExt.snd eps = 1
          source
          @[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 •.

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

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

          source
          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
          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) :
            (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) :
            ↑(lift.symm F) = (F.comp (TrivSqZeroExt.inlAlgHom R A A), F 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) :
            (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_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
            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) :
            (lift fe) (a • ad) = (↑fe).1 a * (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) :
            (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

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

            Lifting DualNumber.eps itself gives the identity.

            source
            @[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} = ⊤
            source
            @[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}
            source
            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.