Documentation

Mathlib.Algebra.QuaternionBasis

Basis on a quaternion-like algebra #

Main definitions #

structure QuaternionAlgebra.Basis {R : Type u_1} (A : Type u_2) [CommRing R] [Ring A] [Algebra R A] (c₁ c₂ c₃ : R) :
Type u_2

A quaternion basis contains the information both sufficient and necessary to construct an R-algebra homomorphism from ℍ[R,c₁,c₂,c₃] to A; or equivalently, a surjective R-algebra homomorphism from ℍ[R,c₁,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.

  • i : A

    The first imaginary unit

  • j : A

    The second imaginary unit

  • k : A

    The third imaginary unit

  • i_mul_i : self.i * self.i = c₁ 1 + c₂ self.i
  • 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 = c₂ self.j - self.k
theorem QuaternionAlgebra.Basis.ext {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} q₁ q₂ : Basis A c₁ 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₂.

theorem QuaternionAlgebra.Basis.ext_iff {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} {q₁ q₂ : Basis A c₁ c₂ c₃} :
q₁ = q₂ q₁.i = q₂.i q₁.j = q₂.j
def QuaternionAlgebra.Basis.self (R : Type u_1) [CommRing R] {c₁ c₂ c₃ : R} :
Basis (QuaternionAlgebra R c₁ c₂ c₃) c₁ c₂ c₃

There is a natural quaternionic basis for the QuaternionAlgebra.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem QuaternionAlgebra.Basis.self_j (R : Type u_1) [CommRing R] {c₁ c₂ c₃ : R} :
(Basis.self R).j = { re := 0, imI := 0, imJ := 1, imK := 0 }
@[simp]
theorem QuaternionAlgebra.Basis.self_k (R : Type u_1) [CommRing R] {c₁ c₂ c₃ : R} :
(Basis.self R).k = { re := 0, imI := 0, imJ := 0, imK := 1 }
@[simp]
theorem QuaternionAlgebra.Basis.self_i (R : Type u_1) [CommRing R] {c₁ c₂ c₃ : R} :
(Basis.self R).i = { re := 0, imI := 1, imJ := 0, imK := 0 }
instance QuaternionAlgebra.Basis.instInhabited {R : Type u_1} [CommRing R] {c₁ c₂ c₃ : R} :
Inhabited (Basis (QuaternionAlgebra R c₁ c₂ c₃) c₁ c₂ c₃)
Equations
@[simp]
theorem QuaternionAlgebra.Basis.i_mul_k {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) :
q.i * q.k = c₁ q.j + c₂ q.k
@[simp]
theorem QuaternionAlgebra.Basis.k_mul_i {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) :
q.k * q.i = -c₁ q.j
@[simp]
theorem QuaternionAlgebra.Basis.k_mul_j {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) :
q.k * q.j = c₃ q.i
@[simp]
theorem QuaternionAlgebra.Basis.j_mul_k {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) :
q.j * q.k = (c₂ * c₃) 1 - c₃ q.i
@[simp]
theorem QuaternionAlgebra.Basis.k_mul_k {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) :
q.k * q.k = -((c₁ * c₃) 1)
def QuaternionAlgebra.Basis.lift {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (x : QuaternionAlgebra R c₁ c₂ c₃) :
A

Intermediate result used to define QuaternionAlgebra.Basis.liftHom.

Equations
theorem QuaternionAlgebra.Basis.lift_zero {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) :
q.lift 0 = 0
theorem QuaternionAlgebra.Basis.lift_one {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) :
q.lift 1 = 1
theorem QuaternionAlgebra.Basis.lift_add {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (x y : QuaternionAlgebra R c₁ c₂ c₃) :
q.lift (x + y) = q.lift x + q.lift y
theorem QuaternionAlgebra.Basis.lift_mul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (x y : QuaternionAlgebra R c₁ c₂ c₃) :
q.lift (x * y) = q.lift x * q.lift y
theorem QuaternionAlgebra.Basis.lift_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (r : R) (x : QuaternionAlgebra R c₁ c₂ c₃) :
q.lift (r x) = r q.lift x
def QuaternionAlgebra.Basis.liftHom {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) :
QuaternionAlgebra R c₁ c₂ c₃ →ₐ[R] A

A QuaternionAlgebra.Basis implies an AlgHom from the quaternions.

Equations
@[simp]
theorem QuaternionAlgebra.Basis.liftHom_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (a : QuaternionAlgebra R c₁ c₂ c₃) :
q.liftHom a = q.lift a
def QuaternionAlgebra.Basis.compHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (F : A →ₐ[R] B) :
Basis B c₁ c₂ c₃

Transform a QuaternionAlgebra.Basis through an AlgHom.

Equations
  • q.compHom F = { i := F q.i, j := F q.j, k := F q.k, i_mul_i := , j_mul_j := , i_mul_j := , j_mul_i := }
@[simp]
theorem QuaternionAlgebra.Basis.compHom_k {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (F : A →ₐ[R] B) :
(q.compHom F).k = F q.k
@[simp]
theorem QuaternionAlgebra.Basis.compHom_j {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (F : A →ₐ[R] B) :
(q.compHom F).j = F q.j
@[simp]
theorem QuaternionAlgebra.Basis.compHom_i {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (F : A →ₐ[R] B) :
(q.compHom F).i = F q.i
def QuaternionAlgebra.lift {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} :
Basis A c₁ c₂ c₃ (QuaternionAlgebra R c₁ c₂ c₃ →ₐ[R] A)

A quaternionic basis on A is equivalent to a map from the quaternion algebra to A.

Equations
@[simp]
theorem QuaternionAlgebra.lift_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) :
@[simp]
theorem QuaternionAlgebra.lift_symm_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (F : QuaternionAlgebra R c₁ c₂ c₃ →ₐ[R] A) :
theorem QuaternionAlgebra.hom_ext {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} f g : QuaternionAlgebra R c₁ c₂ c₃ →ₐ[R] A (hi : f (Basis.self R).i = g (Basis.self R).i) (hj : f (Basis.self R).j = g (Basis.self R).j) :
f = g

Two R-algebra morphisms from a quaternion algebra are equal if they agree on i and j.

theorem QuaternionAlgebra.hom_ext_iff {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} {f g : QuaternionAlgebra R c₁ c₂ c₃ →ₐ[R] A} :
f = g f (Basis.self R).i = g (Basis.self R).i f (Basis.self R).j = g (Basis.self R).j

Two R-algebra morphisms from the quaternions are equal if they agree on i and j.