The Spin group in dimension two #

In dimension two the odd part of a Clifford algebra is exactly the image of its generating space. If the quadratic form represents a unit, multiply an even Clifford unit by the corresponding invertible vector. The product is odd, hence is another vector; solving for the original unit expresses it as a product of two Lipschitz generators. Consequently every even unitary Clifford unit belongs to the Lipschitz group, and the even unitary carrier is exactly the Spin carrier.

For the sum of two squares on K², write J = ι e₀ * ι e₁, so that J * J = -1. Every even element is ι e₀ * ι w = w₀ + w₁ J, so the even Clifford algebra is K[J]. When 2 is invertible in K and K contains a square root i of -1, the character CliffordAlgebra.evenWeightedSumSquaresOneAlgHom, sending u + v J ↦ u + i v, restricts to an isomorphism from the Spin group, the elements with u² + v² = 1, onto Kˣ. Its inverse sends z to u + v J with u = (z + z⁻¹) / 2 and v = i (z⁻¹ - z) / 2, a product of two vectors of norm one. Over ℂ this is the isomorphism Spin₂(ℂ) ≅ ℂˣ.

The argument is the standard low-dimensional Clifford calculation; see H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §2.

Main definitions #

CliffordAlgebra.spinGroupEquivUnitsWeightedSumSquaresOne: the isomorphism from the Spin group of the sum of two squares onto Kˣ.

Main results #

CliffordAlgebra.mem_lipschitzGroup_of_mem_even_of_finrank_eq_two: every even Clifford unit is Lipschitz when the form represents a unit.
CliffordAlgebra.range_spinGroup_toUnits_eq_evenUnitaryGroup_of_finrank_eq_two: the Spin image and even unitary carrier coincide.

source

theorem CliffordAlgebra.mem_lipschitzGroup_of_mem_even_of_finrank_eq_two {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : ∃ (v : V), IsUnit (Q v)) (hV : Module.finrank K V = 2) (x : (CliffordAlgebra Q)ˣ) (hx : ↑x ∈ even Q) :

x ∈ lipschitzGroup Q

For a two-dimensional quadratic space representing a unit, every even Clifford unit lies in Mathlib's Lipschitz group.

source

theorem CliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup_of_finrank_eq_two {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : ∃ (v : V), IsUnit (Q v)) (hV : Module.finrank K V = 2) :

evenUnitaryGroup Q ≤ lipschitzGroup Q

For a two-dimensional quadratic space representing a unit, the even unitary carrier lies in the Lipschitz group.

source

theorem CliffordAlgebra.range_spinGroup_toUnits_eq_evenUnitaryGroup_of_finrank_eq_two {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : ∃ (v : V), IsUnit (Q v)) (hV : Module.finrank K V = 2) :

spinGroup.toUnits.range = evenUnitaryGroup Q

For a two-dimensional quadratic space representing a unit, the Spin group fills the even unitary carrier inside Clifford units.

The sum of two squares when `-1` is a square #

source

noncomputable def CliffordAlgebra.spinGroupEquivUnitsWeightedSumSquaresOne {K : Type u} [Field K] (i : K) (hi : i * i = -1) [Invertible 2] :

↥(spinGroup (QuadraticMap.weightedSumSquares K ![1, 1])) ≃* Kˣ

The Spin group of the sum of two squares is the multiplicative group of a field K in which 2 is invertible and which contains a square root i of -1. The isomorphism is the character evenWeightedSumSquaresOneAlgHom, sending u + v J to u + i v; its inverse sends z to u + v J with u = (z + z⁻¹) / 2 and v = i (z⁻¹ - z) / 2.