Tensor products of quaternion algebras with a common slot #
Two quaternion algebras ℍ[R,a,b] and ℍ[R,a,c] sharing their first parameter have a tensor
product that is again a quaternion algebra up to a matrix factor:
ℍ[K,a,b] ⊗[K] ℍ[K,a,c] ≃ₐ[K] ℍ[K,a,bc] ⊗[K] M₂(K)
This is the common slot lemma (Lam III.2.11, Gille–Szamuely Lemma 1.5.2). In the Brauer group
it says that the quaternion symbol is multiplicative in each argument, which is what
TauCeti/Algebra/Quaternion/BrauerClass.lean proves from it.
The construction is the classical one. Writing i₁, j₁ and i₂, j₂ for the generators of the
two factors, the elements i₁ ⊗ 1 and j₁ ⊗ j₂ satisfy the relations of ℍ[R,a,bc]
(TauCeti.QuaternionAlgebra.linkedBasis), the elements i₁ ⊗ i₂ and 1 ⊗ j₂ satisfy those of
ℍ[R,a²,c] (TauCeti.QuaternionAlgebra.squareBasis), and the two pairs commute. The universal
property QuaternionAlgebra.Basis.liftHom, its compatibility with commuting generators
(QuaternionAlgebra.Basis.commute_liftHom in TauCeti/Algebra/Quaternion/Basis.lean) and
Algebra.TensorProduct.lift then produce an algebra map
ℍ[R,a,bc] ⊗[R] ℍ[R,a²,c] → ℍ[R,a,b] ⊗[R] ℍ[R,a,c], defined over any commutative ring. Over a
field with 2 invertible and unit parameters both sides are 16-dimensional and the source is a
simple ring, so the map is bijective; the factor ℍ[K,a²,c] is split because its first parameter
is a square.
Main results #
TauCeti.QuaternionAlgebra.linkedTensorHom: the algebra mapℍ[R,a,bc] ⊗[R] ℍ[R,a²,c] →ₐ[R] ℍ[R,a,b] ⊗[R] ℍ[R,a,c]over a commutative ring.TauCeti.QuaternionAlgebra.linkedTensorAlgEquiv: over a field with2invertible and unit parameters, that map is an isomorphism.TauCeti.QuaternionAlgebra.tensorAlgEquivTensorMatrix: the common slot lemmaℍ[K,a,b] ⊗[K] ℍ[K,a,c] ≃ₐ[K] ℍ[K,a,bc] ⊗[K] M₂(K).
References #
- T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter III, Theorem 2.11.
- P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology (2006), Lemma 1.5.2.
In ℍ[R,a,b] ⊗[R] ℍ[R,a,c] the elements i ⊗ 1, j ⊗ j and k ⊗ j satisfy the relations of
ℍ[R,a,bc]: they form a quaternion basis of type (a, bc).
Equations
- One or more equations did not get rendered due to their size.
Instances For
In ℍ[R,a,b] ⊗[R] ℍ[R,a,c] the elements i ⊗ i, 1 ⊗ j and i ⊗ k satisfy the relations of
ℍ[R,a²,c]: they form a quaternion basis of type (a², c).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The algebra map ℍ[R,a,bc] ⊗[R] ℍ[R,a²,c] → ℍ[R,a,b] ⊗[R] ℍ[R,a,c] of the common slot lemma,
sending the generators i ⊗ 1, j ⊗ 1 of the first factor to i ⊗ 1, j ⊗ j and the generators
1 ⊗ i, 1 ⊗ j of the second factor to i ⊗ i, 1 ⊗ j.
Equations
Instances For
Over a field with 2 invertible and unit parameters, the common-slot map
ℍ[K,a,bc] ⊗[K] ℍ[K,a²,c] → ℍ[K,a,b] ⊗[K] ℍ[K,a,c] is bijective.
The common slot lemma, first form. Over a field with 2 invertible and unit parameters,
ℍ[K,a,bc] ⊗[K] ℍ[K,a²,c] ≃ₐ[K] ℍ[K,a,b] ⊗[K] ℍ[K,a,c].
Equations
Instances For
The common slot lemma (Lam III.2.11, Gille–Szamuely 1.5.2): for units a b c of a field
with 2 invertible, ℍ[K,a,b] ⊗[K] ℍ[K,a,c] ≃ₐ[K] ℍ[K,a,bc] ⊗[K] M₂(K). In the Brauer group this
is the multiplicativity of the quaternion symbol in its second argument.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse of the common slot equivalence on a pure tensor: pull the matrix back to
ℍ[K,a²,c] through firstSquareEquivMatrix and multiply the images of the two factors.