DualNumber.lift_smul
theorem DualNumber.lift_smul :
∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (fe : { fe // 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
This theorem, named `DualNumber.lift_smul`, states that for all types `R`, `B`, `A` where `R` is a commutative semiring, `A` and `B` are semirings, and `A` and `B` are both `R`-algebras, along with a given element `fe` of type `DualNumber`, and elements `a` of `A` and `ad` of `DualNumber A`, scaling on the left in the domain of the `DualNumber.lift` function corresponds to multiplication on the left in the codomain. That is, applying `DualNumber.lift` to `a` scaled by `ad` is equal to multiplying the image of `a` under `fe` with the image of `ad` under `DualNumber.lift fe`. The `fe` element is a dual number such that when squared, it equals zero and commutes with every element of `A`.
More concisely: For all commutative semirings R, R-algebras A and B, and given dual number fe with sqr(fe) = 0 and commuting with every element of A, the application of DualNumber.lift to the product of an element a in A and a dual number ad is equivalent to multiplying the images of a and ad under DualNumber.lift(fe).
|
DualNumber.lift_apply_eps
theorem DualNumber.lift_apply_eps :
∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }),
(DualNumber.lift fe) DualNumber.eps = (↑fe).2
The theorem `DualNumber.lift_apply_eps` states that, given any types `R`, `A`, `B` where `R` is a commutative semiring, `A` and `B` are semirings, and given `R`-algebra structures on `A` and `B`, if we have an element `fe` of `B` that squares to zero and commutes with all elements `a` in `A`, when the function `DualNumber.lift` is applied to `fe` and ε (the unit element of the dual number that squares to zero), it produces the same result as the second component of `fe` (which is the element of `B` that squares to zero by definition).
More concisely: Given a commutative semiring R, R-algebras A and B, an element fe of B squaring to zero and commuting with all elements a in A, the application of DualNumber.lift to fe and ε (the unit of dual numbers squaring to zero) equals the second component of fe.
|
DualNumber.snd_mul
theorem DualNumber.snd_mul :
∀ {R : Type u_1} [inst : Semiring R] (x y : DualNumber R),
TrivSqZeroExt.snd (x * y) =
TrivSqZeroExt.fst x * TrivSqZeroExt.snd y + TrivSqZeroExt.snd x * TrivSqZeroExt.fst y
This theorem, `DualNumber.snd_mul`, states that for any type `R` equipped with a semiring structure and for any two dual numbers `x` and `y` over `R`, the second component of the product of `x` and `y` (as retrieved by `TrivSqZeroExt.snd`) is equal to the sum of the product of the first component of `x` and the second component of `y` and the product of the second component of `x` and the first component of `y`. In mathematical terms, if dual numbers are represented as $a + bε$, then the theorem asserts that the "bε" part of the product of two dual numbers $(a_1 + b_1ε)(a_2 + b_2ε)$ is $a_1b_2 + a_2b_1$. This theorem provides a rule for multiplication in the context of dual numbers.
More concisely: The second component of the product of two dual numbers is equal to the sum of the product of their first components and the product of their second components.
|
DualNumber.algHom_ext'
theorem DualNumber.algHom_ext' :
∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] ⦃f g : DualNumber A →ₐ[R] B⦄,
f.comp (TrivSqZeroExt.inlAlgHom R A A) = g.comp (TrivSqZeroExt.inlAlgHom R A A) →
f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A (DualNumber A) DualNumber.eps) =
g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A (DualNumber A) DualNumber.eps) →
f = g
This theorem states that for two algebra morphisms `f` and `g` from the dual numbers over `A`, denoted `A[ε]`, to an `R`-algebra `B`, if these morphisms agree on the elements of `A` and on the scalar multiples of the dual number unit element `ε` by elements of `A`, then the two morphisms are identical. Here, an algebra morphism is a function that respects the structure of the algebra, which includes operations such as addition and multiplication as well as scalar multiplication by elements of `R`. The element `ε` in the dual numbers is a special unit element that squares to zero. The scalar multiples of `ε` by elements of `A` form a subset of the dual numbers, and a morphism's behavior on this subset is significant for its overall behavior.
More concisely: If two algebra morphisms from `A[ε]` to an `R-`algebra `B` agree on elements of `A` and scalar multiples of the dual number unit `ε` by elements of `A`, then they are equal.
|
DualNumber.lift_apply_inl
theorem DualNumber.lift_apply_inl :
∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) })
(a : A), (DualNumber.lift fe) (TrivSqZeroExt.inl a) = (↑fe).1 a
The theorem `DualNumber.lift_apply_inl` states that for any commutative semiring `R`, semirings `A` and `B`, and algebras `A` and `B` over `R`, if a map `fe` satisfies the conditions that the square of `fe.2` is zero and `fe.2` commutes with the image of any element `a` under `fe.1`, then applying the function `DualNumber.lift` to the canonical inclusion of `a` into the trivial square zero extension of `R` by `M` (represented by `TrivSqZeroExt.inl a`) results in the application of the map `fe.1` to `a`. In other words, in this context, `DualNumber.lift` behaves like the original map `fe.1` when applied to elements of `A` included into the trivial square zero extension.
More concisely: If `fe` is a map between commutative semirings `R`-algebras `A` and `B` with `fe.2^2 = 0` and `fe.2` commuting with images of `A` elements under `fe.1`, then `DualNumber.lift(TrivSqZeroExt.inl a) = fe.1 a` for all `a` in `A`.
|
DualNumber.commute_eps_left
theorem DualNumber.commute_eps_left :
∀ {R : Type u_1} [inst : Semiring R] (x : DualNumber R), Commute DualNumber.eps x
The theorem `DualNumber.commute_eps_left` states that for any semiring `R` and any dual number `x` over that semiring, the unit element `ε` (which squares to zero) commutes with `x`. This means that the multiplication of `ε` and `x` is the same as the multiplication of `x` and `ε`, i.e., `ε * x = x * ε`.
More concisely: For any semiring `R` and dual number `x` over `R`, the unit element `ε` of the dual numbers commutes with `x`, i.e., `ε * x = x * ε`.
|
DualNumber.commute_eps_right
theorem DualNumber.commute_eps_right :
∀ {R : Type u_1} [inst : Semiring R] (x : DualNumber R), Commute x DualNumber.eps
The theorem `DualNumber.commute_eps_right` states that for any semiring `R` and any element `x` of the dual numbers over `R`, the element `x` commutes with `ε`, the dual number's unit element that squares to zero. In other words, in the algebra of dual numbers, the multiplication of `x` and `ε` is commutative, meaning `x * ε = ε * x`.
More concisely: For any semiring R and dual number x over R, x * ε = ε * x, where ε is the unit element of dual numbers squaring to zero.
|
DualNumber.lift_inlAlgHom_eps
theorem DualNumber.lift_inlAlgHom_eps :
∀ {R : Type u_1} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
DualNumber.lift ⟨(TrivSqZeroExt.inlAlgHom R A A, DualNumber.eps), ⋯⟩ = AlgHom.id R (DualNumber A)
This theorem states that for any types R and A, where R is a commutative semiring, A is a semiring, and there is an algebra structure over R and A, if we lift the dual number epsilon itself (which is the unit element that squares to zero), it results in the identity map on the type of dual numbers over A. In other words, the process of lifting the unit dual number is equivalent to applying the identity algebra homomorphism on the dual number space.
More concisely: For any commutative semirings R and A with an algebra structure over R in A, the algebra homomorphism identity map on the dual number space over A is equivalent to lifting the dual number unit epsilon.
|
DualNumber.lift_op_smul
theorem DualNumber.lift_op_smul :
∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (fe : { fe // 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
This theorem states that for any commutative semiring `R`, semirings `A` and `B`, two algebra structures over `R` on `A` and `B` respectively, and a pair `fe` of elements in `A`, where the second element squares to zero and commutes with the image of every element of `A` under the first element of the pair, the operation of scaling an element `ad` of the dual numbers over `A` by `a` on the right is equivalent to multiplying the lift of `ad` under the dual number extension of `fe` by the lift of `a` under the first element of `fe`. Essentially, it's describing how the operation of scaling in the underlying structure is related to multiplication in the dual number structure.
More concisely: For any commutative semiring `R`, and algebra structures `α:` Algebra R A and `β:` Algebra R B, if `fe = (a, b)` is a pair in `A` with `b² = 0` and `b` commutes with every image of `A` under `a`, then for all `ad` in dual numbers over `A` and `a` in `A`, the operation of scaling `ad` by `a` on the right equals the multiplication of the lifted `ad` by the lifted `a` under `fe`.
|
DualNumber.algHom_ext
theorem DualNumber.algHom_ext :
∀ {R : Type u_1} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
⦃f g : DualNumber R →ₐ[R] A⦄, f DualNumber.eps = g DualNumber.eps → f = g
This theorem states that for any two algebra morphisms, `f` and `g`, from the dual numbers over a commutative semiring `R` to a semiring `A` with a given `R`-algebra structure, if these two morphisms agree on the value of the dual number unit element `ε` (which squares to zero), then these two morphisms are indeed the same. In other words, the morphisms are completely determined by their values on `ε`.
More concisely: Given two algebra morphisms from the dual numbers over a commutative semiring to a semiring with a given algebra structure, if they agree on the value of the dual number unit element, then they are equal.
|