Paths to normalized reflection-pair lifts

A path between two unit vectors maps to a path from the identity to their reflection-pair lift by Clifford multiplication by the first vector. For the positive-definite real Clifford form, the Euclidean unit sphere supplies such a path for every pair of unit vectors.

The dimension bound in the real specialization is sharp for this construction: the unit sphere is path-connected precisely from dimension two onward. The resulting path is the input needed to place reflection-pair lifts in the identity path component of the compact real Spin group.

Main results

• CliffordAlgebra.continuous_spinReflectionPair shows that continuously varying unit vectors determine continuously varying reflection-pair lifts.
• CliffordAlgebra.joined_one_spinReflectionPair_of_joined maps a path in a unit quadric to a path from the identity to its reflection-pair lift.
• CliffordAlgebra.joined_one_spinReflectionPair_realCliffordForm_zero joins every normalized reflection-pair lift to the identity in the positive-definite real form of dimension at least two.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, Section 2.

theorem CliffordAlgebra.continuous_spinReflectionPair {R : Type u} [CommRing R] [TopologicalSpace R] {M : Type v} [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsModuleTopology R M] {Q : QuadraticForm R M} [ContinuousMul (CliffordAlgebra Q)] {X : Type w} [TopologicalSpace X] (v w : X → M) (hv : ∀ (x : X), Q (v x) = 1) (hw : ∀ (x : X), Q (w x) = 1) (hvc : Continuous v) (hwc : Continuous w) : Continuous fun (x : X) => spinReflectionPair Q (v x) (w x) ⋯ ⋯

Two continuous families of unit vectors determine a continuous family of their normalized reflection-pair lifts.

theorem CliffordAlgebra.joined_one_spinReflectionPair_of_joined {R : Type u} [CommRing R] [TopologicalSpace R] {M : Type v} [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsModuleTopology R M] {Q : QuadraticForm R M} [ContinuousMul (CliffordAlgebra Q)] (v w : M) (hv : Q v = 1) (hw : Q w = 1) (h : Joined ⟨v, hv⟩ ⟨w, hw⟩) : Joined 1 (spinReflectionPair Q v w hv hw)

Mapping a path between unit vectors by Clifford multiplication with the first vector joins the identity to their normalized reflection-pair lift.

theorem CliffordAlgebra.joined_one_spinReflectionPair_realCliffordForm_zero {n : ℕ} (hn : 2 ≤ n) (v w : Fin n → ℝ) (hv : (TauCeti.realCliffordForm n 0) v = 1) (hw : (TauCeti.realCliffordForm n 0) w = 1) : Joined 1 (spinReflectionPair (TauCeti.realCliffordForm n 0) v w hv hw)

In dimension at least two, every normalized reflection-pair lift for the positive-definite real Clifford form is joined to the identity in the Spin group.