Splitting a binary plane off a Clifford algebra

For units a and b of a commutative ring R and an arbitrary quadratic module (M, Q), the Clifford algebra of the orthogonal sum ⟨a, b⟩ ⊥ Q is an ordinary (ungraded) tensor product

C(⟨a, b⟩ ⊥ Q) ≅ ℍ[R, a, b] ⊗ C(-a⁻¹b⁻¹ · Q).

The plane ⟨a, b⟩ is Mathlib's CliffordAlgebraQuaternion.Q a b, whose Clifford algebra is the quaternion algebra ℍ[R, a, b]. The mechanism is the plane's volume element ω = e₁e₂, which is the quaternion unit k: it squares to -ab, anticommutes with the plane vectors, and commutes with the vectors of M. Hence m ↦ ι m · ω turns the generators of C(Q) into elements commuting with the plane, squaring to -ab · Q m; rescaling the form by (-ab)⁻¹ = -a⁻¹b⁻¹ compensates.

Iterating this over a diagonal form expresses the Clifford algebra of an even-dimensional diagonal form as a tensor product of quaternion algebras, which is how the Clifford invariant of a quadratic form is computed in terms of quaternion symbols (Lam, Chapter V, §2 and V.3.20).

Main definitions

• CliffordAlgebra.quaternionPlaneEquivTensor: the algebra equivalence C(⟨a, b⟩ ⊥ Q) ≃ₐ[R] ℍ[R, a, b] ⊗[R] C(-a⁻¹b⁻¹ · Q).

Main results

• CliffordAlgebra.quaternionPlaneEquivTensor_ι: it sends a generator (v, m) to (v₁ i + v₂ j) ⊗ 1 + k ⊗ ι m.
• CliffordAlgebra.quaternionPlaneEquivTensor_symm_tmul_one and CliffordAlgebra.quaternionPlaneEquivTensor_symm_one_tmul: its inverse on each tensor factor.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Graduate Studies in Mathematics 67, American Mathematical Society (2005), Chapter V, §2.
• The construction adapts the volume-element argument of TauCeti.LinearAlgebra.CliffordAlgebra.NegativePlane (CliffordAlgebra.negativePlaneEquivTensor) from the real plane ⟨-1, -1⟩ to an arbitrary plane ⟨a, b⟩: the same generator lift, inclusions of the two factors, commutation argument, tensor-product lift, and check of the two composites.

Quaternion identities

The forward map

The inverse map

The two composites

The equivalence

noncomputable def CliffordAlgebra.quaternionPlaneEquivTensor {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a b : Rˣ) : CliffordAlgebra (QuadraticMap.prod (CliffordAlgebraQuaternion.Q ↑a ↑b) Q) ≃ₐ[R] TensorProduct R (QuaternionAlgebra R (↑a) 0 ↑b) (CliffordAlgebra (-(↑a⁻¹ * ↑b⁻¹) • Q))

Splitting a binary plane off a Clifford algebra. For units a and b, the Clifford algebra of ⟨a, b⟩ ⊥ Q is the tensor product of the quaternion algebra ℍ[R, a, b] with the Clifford algebra of the rescaled form -a⁻¹b⁻¹ · Q (Lam, Chapter V, §2).

@[simp]

theorem CliffordAlgebra.quaternionPlaneEquivTensor_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a b : Rˣ) (x : (R × R) × M) : (quaternionPlaneEquivTensor Q a b) ((ι (QuadraticMap.prod (CliffordAlgebraQuaternion.Q ↑a ↑b) Q)) x) = { re := 0, imI := x.1.1, imJ := x.1.2, imK := 0 } ⊗ₜ[R] 1 + { re := 0, imI := 0, imJ := 0, imK := 1 } ⊗ₜ[R] (ι (-(↑a⁻¹ * ↑b⁻¹) • Q)) x.2

quaternionPlaneEquivTensor sends a plane generator to the pure quaternion v₁ i + v₂ j and a generator of M to k ⊗ ι m.

@[simp]

theorem CliffordAlgebra.quaternionPlaneEquivTensor_symm_tmul_one {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a b : Rˣ) (x : QuaternionAlgebra R (↑a) 0 ↑b) : (quaternionPlaneEquivTensor Q a b).symm (x ⊗ₜ[R] 1) = (map (QuadraticMap.Isometry.inl (CliffordAlgebraQuaternion.Q ↑a ↑b) Q)) (CliffordAlgebraQuaternion.ofQuaternion x)

The inverse of quaternionPlaneEquivTensor on the quaternion factor is the inclusion of the plane's Clifford algebra ℍ[R, a, b] ≅ C(⟨a, b⟩).

@[simp]

theorem CliffordAlgebra.quaternionPlaneEquivTensor_symm_one_tmul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a b : Rˣ) (m : M) : (quaternionPlaneEquivTensor Q a b).symm (1 ⊗ₜ[R] (ι (-(↑a⁻¹ * ↑b⁻¹) • Q)) m) = -(↑a⁻¹ * ↑b⁻¹) • ((ι (QuadraticMap.prod (CliffordAlgebraQuaternion.Q ↑a ↑b) Q)) (0, m) * (ι (QuadraticMap.prod (CliffordAlgebraQuaternion.Q ↑a ↑b) Q)) ((1, 0), 0) * (ι (QuadraticMap.prod (CliffordAlgebraQuaternion.Q ↑a ↑b) Q)) ((0, 1), 0))

The inverse of quaternionPlaneEquivTensor sends 1 ⊗ ι m to -a⁻¹b⁻¹ · ι m · e₁e₂.