Basis on a quaternion-like algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
quaternion_algebra.basis A c₁ c₂: a basis for a subspace of anR-algebraAthat has the same algebra structure asℍ[R,c₁,c₂].quaternion_algebra.basis.self R: the canonical basis forℍ[R,c₁,c₂].quaternion_algebra.basis.comp_hom b f: transform a basisbby an alg_homf.quaternion_algebra.lift: Define analg_homout ofℍ[R,c₁,c₂]by its action on the basis elementsi,j, andk. In essence, this is a universal property. Analogous tocomplex.lift, but takes a bundledquaternion_algebra.basisinstead of just asubtypeas the amount of data / proves is non-negligeable.
structure
quaternion_algebra.basis
{R : Type u_1}
(A : Type u_2)
[comm_ring R]
[ring A]
[algebra R A]
(c₁ c₂ : R) :
Type u_2
- i : A
- j : A
- k : A
- i_mul_i : self.i * self.i = c₁ • 1
- j_mul_j : self.j * self.j = c₂ • 1
- i_mul_j : self.i * self.j = self.k
- j_mul_i : self.j * self.i = -self.k
A quaternion basis contains the information both sufficient and necessary to construct an
R-algebra homomorphism from ℍ[R,c₁,c₂] to A; or equivalently, a surjective
R-algebra homomorphism from ℍ[R,c₁,c₂] to an R-subalgebra of A.
Note that for definitional convenience, k is provided as a field even though i_mul_j fully
determines it.
Instances for quaternion_algebra.basis
- quaternion_algebra.basis.has_sizeof_inst
- quaternion_algebra.basis.inhabited
@[protected, ext]
theorem
quaternion_algebra.basis.ext
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{c₁ c₂ : R}
⦃q₁ q₂ : quaternion_algebra.basis A c₁ c₂⦄
(hi : q₁.i = q₂.i)
(hj : q₁.j = q₂.j) :
q₁ = q₂
Since k is redundant, it is not necessary to show q₁.k = q₂.k when showing q₁ = q₂.
@[protected]
def
quaternion_algebra.basis.self
(R : Type u_1)
[comm_ring R]
{c₁ c₂ : R} :
quaternion_algebra.basis (quaternion_algebra R c₁ c₂) c₁ c₂
There is a natural quaternionic basis for the quaternion_algebra.
@[protected, instance]
def
quaternion_algebra.basis.inhabited
{R : Type u_1}
[comm_ring R]
{c₁ c₂ : R} :
inhabited (quaternion_algebra.basis (quaternion_algebra R c₁ c₂) c₁ c₂)
Equations
def
quaternion_algebra.basis.lift
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{c₁ c₂ : R}
(q : quaternion_algebra.basis A c₁ c₂)
(x : quaternion_algebra R c₁ c₂) :
A
Intermediate result used to define quaternion_algebra.basis.lift_hom.
theorem
quaternion_algebra.basis.lift_zero
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{c₁ c₂ : R}
(q : quaternion_algebra.basis A c₁ c₂) :
theorem
quaternion_algebra.basis.lift_one
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{c₁ c₂ : R}
(q : quaternion_algebra.basis A c₁ c₂) :
theorem
quaternion_algebra.basis.lift_add
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{c₁ c₂ : R}
(q : quaternion_algebra.basis A c₁ c₂)
(x y : quaternion_algebra R c₁ c₂) :
theorem
quaternion_algebra.basis.lift_mul
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{c₁ c₂ : R}
(q : quaternion_algebra.basis A c₁ c₂)
(x y : quaternion_algebra R c₁ c₂) :
theorem
quaternion_algebra.basis.lift_smul
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{c₁ c₂ : R}
(q : quaternion_algebra.basis A c₁ c₂)
(r : R)
(x : quaternion_algebra R c₁ c₂) :
@[simp]
theorem
quaternion_algebra.basis.lift_hom_apply
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{c₁ c₂ : R}
(q : quaternion_algebra.basis A c₁ c₂)
(ᾰ : quaternion_algebra R c₁ c₂) :
def
quaternion_algebra.basis.lift_hom
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{c₁ c₂ : R}
(q : quaternion_algebra.basis A c₁ c₂) :
quaternion_algebra R c₁ c₂ →ₐ[R] A
A quaternion_algebra.basis implies an alg_hom from the quaternions.
def
quaternion_algebra.basis.comp_hom
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[comm_ring R]
[ring A]
[ring B]
[algebra R A]
[algebra R B]
{c₁ c₂ : R}
(q : quaternion_algebra.basis A c₁ c₂)
(F : A →ₐ[R] B) :
quaternion_algebra.basis B c₁ c₂
Transform a quaternion_algebra.basis through an alg_hom.
@[simp]
theorem
quaternion_algebra.lift_apply
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{c₁ c₂ : R}
(q : quaternion_algebra.basis A c₁ c₂) :
def
quaternion_algebra.lift
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{c₁ c₂ : R} :
quaternion_algebra.basis A c₁ c₂ ≃ (quaternion_algebra R c₁ c₂ →ₐ[R] A)
A quaternionic basis on A is equivalent to a map from the quaternion algebra to A.
Equations
- quaternion_algebra.lift = {to_fun := quaternion_algebra.basis.lift_hom c₂, inv_fun := (quaternion_algebra.basis.self R).comp_hom, left_inv := _, right_inv := _}
@[simp]
theorem
quaternion_algebra.lift_symm_apply
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{c₁ c₂ : R}
(F : quaternion_algebra R c₁ c₂ →ₐ[R] A) :