Quaternion.hom_ext
theorem Quaternion.hom_ext :
∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
⦃f g : Quaternion R →ₐ[R] A⦄,
f (QuaternionAlgebra.Basis.self R).i = g (QuaternionAlgebra.Basis.self R).i →
f (QuaternionAlgebra.Basis.self R).j = g (QuaternionAlgebra.Basis.self R).j → f = g
The theorem `Quaternion.hom_ext` states that for any commutative ring `R` and ring `A`, if `f` and `g` are two morphisms from the quaternions over `R` to `A` that preserve the ring structure and the scalar multiplications (i.e., they are `R`-algebra morphisms), and if these two morphisms agree on the `i` and `j` elements of a natural quaternionic basis for the `QuaternionAlgebra`, then `f` and `g` are equal. In other words, to check the equality of two `R`-algebra morphisms from the quaternions, it suffices to verify their action on `i` and `j` of the quaternionic basis.
More concisely: If `f` and `g` are `R-algorithm` morphisms from the quaternions over `R` to a ring `A` agreeing on the images of `i` and `j` in a natural quaternionic basis, then `f = g`.
|
QuaternionAlgebra.Basis.ext
theorem QuaternionAlgebra.Basis.ext :
∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ : R}
⦃q₁ q₂ : QuaternionAlgebra.Basis A c₁ c₂⦄, q₁.i = q₂.i → q₁.j = q₂.j → q₁ = q₂
This theorem states that for any two elements `q₁` and `q₂` of the `QuaternionAlgebra.Basis` of a ring `A` with coefficients `c₁` and `c₂` over a commutative ring `R`, if `q₁.i` is equal to `q₂.i` and `q₁.j` is equal to `q₂.j`, then `q₁` is equal to `q₂`. The element `k` is redundant in this context, meaning it is not necessary to show that `q₁.k` is equal to `q₂.k` in order to establish the equality of `q₁` and `q₂`.
More concisely: If two quaternions `q₁` and `q₂` in the basis of a ring `A` over a commutative ring `R` have identical real and imaginary parts, then they are equal.
|
QuaternionAlgebra.hom_ext
theorem QuaternionAlgebra.hom_ext :
∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ : R}
⦃f g : QuaternionAlgebra R c₁ c₂ →ₐ[R] A⦄,
f (QuaternionAlgebra.Basis.self R).i = g (QuaternionAlgebra.Basis.self R).i →
f (QuaternionAlgebra.Basis.self R).j = g (QuaternionAlgebra.Basis.self R).j → f = g
The theorem `QuaternionAlgebra.hom_ext` states that for any commutative ring `R` and ring `A`, with `A` being an `R`-algebra, and for any two elements `c₁` and `c₂` in `R`, if we have two `R`-algebra morphisms `f` and `g` from a quaternion algebra (constructed from `R`, `c₁`, and `c₂`) to `A`, then `f` and `g` are equal if they both map the `i` and `j` components of the natural quaternionic basis of the quaternion algebra to the same elements in `A`.
More concisely: If two `R-algebra` morphisms from the quaternion algebra over `R` with basis `{1, i, j, k}` and multiplication rules `i^2 = c₁, j^2 = c₂, ij = -ji = k`, where `c₁` and `c₂` are in `R`, map the basis elements `i` and `j` to the same elements in an `R-algebra` `A`, then `f` and `g` are equal.
|