Clifford algebras in dimension two

The odd component of a two-dimensional Clifford algebra consists entirely of vector generators. Indeed, the generator image lies in the odd component, and both spaces have dimension two: the generator is injective, while the odd component has dimension 2 ^ (2 - 1).

This is a general grading fact, independent of the Lipschitz and Spin groups. Multiplying by a fixed vector a of invertible norm exchanges the two components, so every even element is a product ι a * ι w of a with another vector.

For the sum of two squares on R², write J = ι e₀ * ι e₁, so that J * J = -1. Every even element of a two-dimensional Clifford algebra over a field is ι e₀ * ι w = w₀ + w₁ J, so the even Clifford algebra is K[J]. Over any commutative ring R containing a square root i of -1, the even Clifford algebra has the character u + v J ↦ u + i v, built with even.lift.

Main definitions

• CliffordAlgebra.evenWeightedSumSquaresOneAlgHom: the character u + v J ↦ u + i v of the even Clifford algebra of the sum of two squares.

Main results

• CliffordAlgebra.range_ι_eq_evenOdd_one_of_finrank_eq_two: every odd Clifford element in dimension two is a vector generator.
• CliffordAlgebra.mem_even_iff_exists_ι_mul_ι_of_finrank_eq_two: every even Clifford element in dimension two is a product ι a * ι w, for any fixed a of invertible norm.
• CliffordAlgebra.evenWeightedSumSquaresOneAlgHom_ι and CliffordAlgebra.evenWeightedSumSquaresOneAlgHom_apply: the character on a product of two generators, and in coordinates.

theorem CliffordAlgebra.range_ι_eq_evenOdd_one_of_finrank_eq_two {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hV : Module.finrank K V = 2) : (ι Q).range = evenOdd Q 1

In dimension two, every odd Clifford element is a vector generator.

theorem CliffordAlgebra.mem_even_iff_exists_ι_mul_ι_of_finrank_eq_two {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hV : Module.finrank K V = 2) (a : V) [Invertible (Q a)] {x : CliffordAlgebra Q} : x ∈ even Q ↔ ∃ (w : V), x = (ι Q) a * (ι Q) w

In dimension two, the even Clifford elements are exactly the products ι a * ι w, for any fixed vector a of invertible norm.

The sum of two squares when -1 is a square

noncomputable def CliffordAlgebra.evenWeightedSumSquaresOneAlgHom {R : Type u} [CommRing R] (i : R) (hi : i * i = -1) : ↥(even (QuadraticMap.weightedSumSquares R ![1, 1])) →ₐ[R] R

The character of the even Clifford algebra of the sum of two squares attached to a square root i of -1. Writing J = ι e₀ * ι e₁, so that J * J = -1, every even element over a field is u + v J, and the character sends it to u + i v.

@[simp]

theorem CliffordAlgebra.evenWeightedSumSquaresOneAlgHom_ι {R : Type u} [CommRing R] (i : R) (hi : i * i = -1) (x y : Fin 2 → R) : (evenWeightedSumSquaresOneAlgHom i hi) (((even.ι (QuadraticMap.weightedSumSquares R ![1, 1])).bilin x) y) = x 0 * y 0 + x 1 * y 1 + i * (x 0 * y 1 - x 1 * y 0)

The character on a product of two generators: ι x * ι y ↦ (x₀ - i x₁) (y₀ + i y₁).

theorem CliffordAlgebra.evenWeightedSumSquaresOneAlgHom_apply {K : Type u} [Field K] [Invertible 2] (i : K) (hi : i * i = -1) (x : ↥(even (QuadraticMap.weightedSumSquares K ![1, 1]))) : (evenWeightedSumSquaresOneAlgHom i hi) x = (ιInv (QuadraticMap.weightedSumSquares K ![1, 1])) ((ι (QuadraticMap.weightedSumSquares K ![1, 1])) ![1, 0] * ↑x) 0 + i * (ιInv (QuadraticMap.weightedSumSquares K ![1, 1])) ((ι (QuadraticMap.weightedSumSquares K ![1, 1])) ![1, 0] * ↑x) 1

The character evenWeightedSumSquaresOneAlgHom in coordinates: an even element x is ι e₀ * ι w for the vector w = ιInv (ι e₀ * x), and is sent to w₀ + i w₁.