The Spin group in dimension one

In dimension one the even Clifford algebra has dimension one over the base field. Thus every even Clifford unit is a scalar unit. When the form represents a unit, scalar units belong to Mathlib's Lipschitz group, so the even unitary carrier and the Spin carrier coincide in this dimension.

The rank-one equality identifies spinGroup with the unitary group of the even Clifford algebra inside Clifford units. The zero-dimensional case is different: its Lipschitz group is trivial.

For a nondegenerate form, the special orthogonal group of a line is trivial, so the Spin action is trivial and the Spin group is the kernel {1, -1} of its double cover. Thus Spin(Q) = {±1} is cyclic of order two, and the double cover Spin(Q) → SO(Q) is the trivial two-sheeted cover of a point.

Main results

• CliffordAlgebra.range_spinGroup_toUnits_eq_evenUnitaryGroup_of_finrank_eq_one: Spin fills the even unitary carrier when the form represents a unit.
• CliffordAlgebra.ker_spinToSpecialOrthogonal_eq_top_of_finrank_eq_one: the Spin action on a line is trivial.
• CliffordAlgebra.mem_spinGroup_iff_of_finrank_eq_one: for a nondegenerate form, the Spin group consists of 1 and -1.
• CliffordAlgebra.zmodTwoMulEquivSpinGroupOfFinrankEqOne: for a nondegenerate form, the Spin group is Multiplicative (ZMod 2), with the generator sent to -1.

The scalar description follows the standard Clifford algebra calculation; see H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §2.

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

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

theorem CliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup_of_finrank_eq_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hQ : ∃ (v : V), IsUnit (Q v)) (hV : Module.finrank K V = 1) : evenUnitaryGroup Q ≤ lipschitzGroup Q

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

theorem CliffordAlgebra.range_spinGroup_toUnits_eq_evenUnitaryGroup_of_finrank_eq_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hQ : ∃ (v : V), IsUnit (Q v)) (hV : Module.finrank K V = 1) : spinGroup.toUnits.range = evenUnitaryGroup Q

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

theorem CliffordAlgebra.ker_spinToSpecialOrthogonal_eq_top_of_finrank_eq_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hV : Module.finrank K V = 1) : (spinToSpecialOrthogonal Q).ker = ⊤

In dimension one the Spin action is trivial: the special orthogonal group of a line is trivial, so the whole Spin group is the kernel of its action.

theorem CliffordAlgebra.spinGroup.eq_one_or_eq_negOne_of_finrank_eq_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 1) (x : ↥(spinGroup Q)) : x = 1 ∨ x = negOne Q ⋯

In dimension one the Spin group of a nondegenerate form is {1, -1}.

theorem CliffordAlgebra.mem_spinGroup_iff_of_finrank_eq_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 1) {x : CliffordAlgebra Q} : x ∈ spinGroup Q ↔ x = 1 ∨ x = -1

In dimension one the Spin group of a nondegenerate form consists of exactly the Clifford elements 1 and -1.

noncomputable def CliffordAlgebra.zmodTwoMulEquivSpinGroupOfFinrankEqOne {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 1) : Multiplicative (ZMod 2) ≃* ↥(spinGroup Q)

In dimension one the Spin group of a nondegenerate form is cyclic of order two, generated by -1: the inclusion of the Spin double cover is an isomorphism, since its projection lands in the trivial special orthogonal group.

@[simp]

theorem CliffordAlgebra.zmodTwoMulEquivSpinGroupOfFinrankEqOne_apply_ofAdd_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 1) : (zmodTwoMulEquivSpinGroupOfFinrankEqOne Q hQ hV) (Multiplicative.ofAdd 1) = spinGroup.negOne Q ⋯

The rank-one cyclic equivalence sends the generator of Multiplicative (ZMod 2) to -1.