Orbits of compact real Spin groups

For n ≥ 2, the compact real Spin group acts transitively on the unit level set of its positive-definite quadratic form. This is the algebraic input for its continuous sphere orbit.

The transitivity result identifies the unit level as a homogeneous space for the compact Spin action, providing the algebraic boundary needed for the subsequent sphere-orbit construction. The underlying compact Spin geometry is discussed in Lawson--Michelsohn, Spin Geometry, Chapter I, Section 2.

noncomputable def CliffordAlgebra.realCliffordUnitLevel (n : ℕ) : SubMulAction (↥(realCliffordSpinGroupZero n)) (Fin n → ℝ)

The unit quadratic level as a subaction of the compact real Spin action.

@[simp]

theorem CliffordAlgebra.mem_realCliffordUnitLevel (n : ℕ) (x : Fin n → ℝ) : x ∈ realCliffordUnitLevel n ↔ (TauCeti.realCliffordForm n 0) x = 1

theorem CliffordAlgebra.exists_spinVectorAction_eq_of_posDef {V : Type u} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (Q : QuadraticForm ℝ V) (hQ : QuadraticMap.PosDef Q) (hrank : 2 ≤ Module.finrank ℝ V) {x y : V} (hxy : Q x = Q y) : ∃ (s : ↥(spinGroup Q)), (spinVectorAction Q s) x = y

A positive-definite real Spin group acts transitively on every quadratic level set in dimension at least two.

theorem CliffordAlgebra.exists_realCliffordSpinGroupZero_spinVectorAction_eq (n : ℕ) (hn : 2 ≤ n) {x y : Fin n → ℝ} (hx : (TauCeti.realCliffordForm n 0) x = 1) (hy : (TauCeti.realCliffordForm n 0) y = 1) : ∃ (s : ↥(realCliffordSpinGroupZero n)), (spinVectorAction (TauCeti.realCliffordForm n 0) s) x = y

The compact real Spin group Spin(n) acts transitively on the unit level set when n ≥ 2.

theorem CliffordAlgebra.isPretransitive_realCliffordUnitLevel (n : ℕ) (hn : 2 ≤ n) : MulAction.IsPretransitive ↥(realCliffordSpinGroupZero n) ↥(realCliffordUnitLevel n)

The compact real Spin action on the unit level is transitive in dimension at least two.