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₁ : R) (c₂ : R) :
Type u_2
  • i : A
  • j : A
  • k : A
  • i_mul_i : s.i * s.i = c₁ 1
  • j_mul_j : s.j * s.j = c₂ 1
  • i_mul_j : s.i * s.j = s.k
  • j_mul_i : s.j * s.i = -s.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
    theorem QuaternionAlgebra.Basis.ext {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} ⦃q₁ : QuaternionAlgebra.Basis A c₁ c₂ ⦃q₂ : QuaternionAlgebra.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₂.

    @[simp]
    theorem QuaternionAlgebra.Basis.self_j (R : Type u_1) [CommRing R] {c₁ : R} {c₂ : R} :
    (QuaternionAlgebra.Basis.self R).j = { re := 0, imI := 0, imJ := 1, imK := 0 }
    @[simp]
    theorem QuaternionAlgebra.Basis.self_i (R : Type u_1) [CommRing R] {c₁ : R} {c₂ : R} :
    (QuaternionAlgebra.Basis.self R).i = { re := 0, imI := 1, imJ := 0, imK := 0 }
    @[simp]
    theorem QuaternionAlgebra.Basis.self_k (R : Type u_1) [CommRing R] {c₁ : R} {c₂ : R} :
    (QuaternionAlgebra.Basis.self R).k = { re := 0, imI := 0, imJ := 0, imK := 1 }
    def QuaternionAlgebra.Basis.self (R : Type u_1) [CommRing R] {c₁ : R} {c₂ : R} :

    There is a natural quaternionic basis for the QuaternionAlgebra.

    Instances For
      @[simp]
      theorem QuaternionAlgebra.Basis.i_mul_k {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) :
      q.i * q.k = c₁ q.j
      @[simp]
      theorem QuaternionAlgebra.Basis.k_mul_i {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A 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₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A 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₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) :
      q.j * q.k = -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₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A 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₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (x : QuaternionAlgebra R c₁ c₂) :
      A

      Intermediate result used to define QuaternionAlgebra.Basis.liftHom.

      Instances For
        theorem QuaternionAlgebra.Basis.lift_zero {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) :
        theorem QuaternionAlgebra.Basis.lift_one {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) :
        theorem QuaternionAlgebra.Basis.lift_add {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (x : QuaternionAlgebra R c₁ c₂) (y : QuaternionAlgebra R c₁ c₂) :
        theorem QuaternionAlgebra.Basis.lift_mul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (x : QuaternionAlgebra R c₁ c₂) (y : QuaternionAlgebra R c₁ c₂) :
        theorem QuaternionAlgebra.Basis.lift_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (r : R) (x : QuaternionAlgebra R c₁ c₂) :
        @[simp]
        theorem QuaternionAlgebra.Basis.liftHom_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (a : QuaternionAlgebra R c₁ c₂) :
        def QuaternionAlgebra.Basis.liftHom {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) :

        A QuaternionAlgebra.Basis implies an AlgHom from the quaternions.

        Instances For
          @[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₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (F : A →ₐ[R] B) :
          @[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₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (F : A →ₐ[R] B) :
          @[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₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (F : A →ₐ[R] B) :
          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₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (F : A →ₐ[R] B) :

          Transform a QuaternionAlgebra.Basis through an AlgHom.

          Instances For
            @[simp]
            theorem QuaternionAlgebra.lift_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) :
            QuaternionAlgebra.lift q = QuaternionAlgebra.Basis.liftHom q
            @[simp]
            theorem QuaternionAlgebra.lift_symm_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (F : QuaternionAlgebra R c₁ c₂ →ₐ[R] A) :
            QuaternionAlgebra.lift.symm F = QuaternionAlgebra.Basis.compHom (QuaternionAlgebra.Basis.self R) F
            def QuaternionAlgebra.lift {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} :

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

            Instances For