Documentation

TauCeti.Algebra.Quaternion.BaseChange

Base change of quaternion algebras #

Extending scalars in a quaternion algebra amounts to applying the algebra map to its three parameters. The equivalence TauCeti.QuaternionAlgebra.baseChange identifies S ⊗[R] ℍ[R,a,b,c] with ℍ[S,algebraMap R S a,algebraMap R S b,algebraMap R S c]. It lets quaternion algebras and their splitting isomorphisms be transported along extensions. The construction works over arbitrary commutative rings, including in characteristic two.

The formula baseChange_tmul sends a pure tensor to the scalar multiple of the coefficientwise image. The inverse formula baseChange_symm_mk expands a quaternion in the basis 1, i, j, k. For the two-parameter notation, baseChangeTwoParams gives the equivalence directly with ℍ[S,algebraMap R S a,algebraMap R S b].

source
def TauCeti.QuaternionAlgebra.map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (a b c : R) (f : R →+* S) :
QuaternionAlgebra R a b c →+* QuaternionAlgebra S (f a) (f b) (f c)

Apply a ring homomorphism to the coefficients of a quaternion.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.QuaternionAlgebra.map_mk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (a b c : R) (f : R →+* S) (w x y z : R) :
    (map a b c f) { re := w, imI := x, imJ := y, imK := z } = { re := f w, imI := f x, imJ := f y, imK := f z }
    source
    @[simp]
    theorem TauCeti.QuaternionAlgebra.re_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (a b c : R) (f : R →+* S) (q : QuaternionAlgebra R a b c) :
    ((map a b c f) q).re = f q.re
    source
    @[simp]
    theorem TauCeti.QuaternionAlgebra.imI_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (a b c : R) (f : R →+* S) (q : QuaternionAlgebra R a b c) :
    ((map a b c f) q).imI = f q.imI
    source
    @[simp]
    theorem TauCeti.QuaternionAlgebra.imJ_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (a b c : R) (f : R →+* S) (q : QuaternionAlgebra R a b c) :
    ((map a b c f) q).imJ = f q.imJ
    source
    @[simp]
    theorem TauCeti.QuaternionAlgebra.imK_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (a b c : R) (f : R →+* S) (q : QuaternionAlgebra R a b c) :
    ((map a b c f) q).imK = f q.imK
    source
    @[simp]
    theorem TauCeti.QuaternionAlgebra.map_star {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (a b c : R) (f : R →+* S) (q : QuaternionAlgebra R a b c) :
    (map a b c f) (star q) = star ((map a b c f) q)
    source
    @[simp]
    theorem TauCeti.QuaternionAlgebra.map_coe {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (a b c : R) (f : R →+* S) (r : R) :
    (map a b c f) ↑r = ↑(f r)
    source
    @[simp]
    theorem TauCeti.QuaternionAlgebra.map_id {R : Type u_1} [CommRing R] (a b c : R) :
    map a b c (RingHom.id R) = RingHom.id (QuaternionAlgebra R a b c)
    source
    @[simp]
    theorem TauCeti.QuaternionAlgebra.map_comp {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {T : Type u_3} [CommRing T] (a b c : R) (f : R →+* S) (g : S →+* T) :
    map a b c (g.comp f) = (map (f a) (f b) (f c) g).comp (map a b c f)
    source
    noncomputable def TauCeti.QuaternionAlgebra.baseChange (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (a b c : R) :
    TensorProduct R S (QuaternionAlgebra R a b c) ≃ₐ[S] QuaternionAlgebra S ((algebraMap R S) a) ((algebraMap R S) b) ((algebraMap R S) c)

    Extending scalars in a quaternion algebra applies the algebra map to its parameters.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.QuaternionAlgebra.baseChange_tmul (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (a b c : R) (s : S) (q : QuaternionAlgebra R a b c) :
      (baseChange R S a b c) (s ⊗ₜ[R] q) = s • (map a b c (algebraMap R S)) q

      Base change sends a pure tensor to the scalar multiple of the coefficientwise image.

      source
      @[simp]
      theorem TauCeti.QuaternionAlgebra.baseChange_symm_mk (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (a b c : R) (w x y z : S) :
      (baseChange R S a b c).symm { re := w, imI := x, imJ := y, imK := z } = w ⊗ₜ[R] 1 + x ⊗ₜ[R] { re := 0, imI := 1, imJ := 0, imK := 0 } + y ⊗ₜ[R] { re := 0, imI := 0, imJ := 1, imK := 0 } + z ⊗ₜ[R] { re := 0, imI := 0, imJ := 0, imK := 1 }

      The inverse base-change equivalence expands a quaternion in the basis 1, i, j, k.

      source
      noncomputable def TauCeti.QuaternionAlgebra.baseChangeTwoParams (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (a b : R) :
      TensorProduct R S (QuaternionAlgebra R a 0 b) ≃ₐ[S] QuaternionAlgebra S ((algebraMap R S) a) 0 ((algebraMap R S) b)

      Scalar extension of the two-parameter quaternion algebra, with zero middle parameter.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.QuaternionAlgebra.baseChangeTwoParams_tmul (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (a b : R) (s : S) (q : QuaternionAlgebra R a 0 b) :
        (baseChangeTwoParams R S a b) (s ⊗ₜ[R] q) = s • { re := (algebraMap R S) q.re, imI := (algebraMap R S) q.imI, imJ := (algebraMap R S) q.imJ, imK := (algebraMap R S) q.imK }

        Two-parameter base change applies the algebra map to each coefficient of a pure tensor.

        source
        @[simp]
        theorem TauCeti.QuaternionAlgebra.baseChangeTwoParams_symm_mk (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (a b : R) (w x y z : S) :
        (baseChangeTwoParams R S a b).symm { re := w, imI := x, imJ := y, imK := z } = w ⊗ₜ[R] 1 + x ⊗ₜ[R] { re := 0, imI := 1, imJ := 0, imK := 0 } + y ⊗ₜ[R] { re := 0, imI := 0, imJ := 1, imK := 0 } + z ⊗ₜ[R] { re := 0, imI := 0, imJ := 0, imK := 1 }

        The inverse two-parameter base change expands a quaternion in the basis 1, i, j, k.