The lower-rank subgroup of a compact real Spin group

Splitting the last positive coordinate identifies the quadratic space of Spin(n + 1) with the orthogonal sum of the space of Spin(n) and a positive line. Functoriality of the Spin group gives an injective homomorphism Spin(n) → Spin(n + 1). Its image fixes the last coordinate vector, so it canonically factors through that vector's stabilizer.

This is the algebraic half of the familiar stabilizer description Spin(n + 1) / Spin(n) ≃ Sⁿ. In positive rank the inclusion is exactly the full stabilizer: the special orthogonal stabilizer calculation lifts through the double cover, and its two possible lifts differ by the canonical -1, which is already in the image. The topology of the resulting homogeneous space is a separate result.

The split-coordinate action equation below compares the lower-rank inclusion with the Spin projection. When n > 0, the projection has kernel {1, -1}; since the inclusion preserves the canonical -1 whenever its source form is nonzero, every element sharing a projection with an included element is itself included. This is the residual kernel calculation needed by the converse stabilizer identification.

Main results

• CliffordAlgebra.realCliffordSpinInclusionIsometry is the quadratic isometry inducing the lower-rank inclusion.
• CliffordAlgebra.realCliffordSpinInclusion is the lower-rank Spin homomorphism.
• CliffordAlgebra.realCliffordSpinInclusionIsometry_map_injective proves injectivity of the induced Clifford-algebra map.
• CliffordAlgebra.realCliffordSpinLastStabilizer is the stabilizer of the last unit vector.
• CliffordAlgebra.realCliffordSpinStabilizerInclusion is the injective homomorphism into that stabilizer.
• CliffordAlgebra.realCliffordSpinEquivLastStabilizer identifies Spin(n) with the full last-vector stabilizer for positive n.
• CliffordAlgebra.realCliffordSpinInclusion_spinVectorAction_split computes the full vector action of the inclusion in split coordinates.
• eq_or_eq_realCliffordSpinInclusion_negOne_mul_of_spinToSpecialOrthogonal_eq identifies the two possible lifts of the spinToSpecialOrthogonal image of an included element.

References

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

def CliffordAlgebra.realCliffordSpinInclusionIsometry (n : ℕ) : TauCeti.realCliffordForm n 0 →qᵢ TauCeti.realCliffordForm (n + 1) 0

The quadratic isometry inducing the lower-rank inclusion Spin(n) → Spin(n + 1).

def CliffordAlgebra.realCliffordSpinInclusion (n : ℕ) : ↥(realCliffordSpinGroupZero n) →* ↥(realCliffordSpinGroupZero (n + 1))

The homomorphism Spin(n) → Spin(n + 1) induced by including the first summand after splitting off the last positive coordinate.

@[simp]

theorem CliffordAlgebra.coe_realCliffordSpinInclusion_apply (n : ℕ) (x : ↥(realCliffordSpinGroupZero n)) : ↑((realCliffordSpinInclusion n) x) = (map (realCliffordSpinInclusionIsometry n)) ↑x

The lower-rank Spin inclusion is induced by the corresponding Clifford-algebra map.

theorem CliffordAlgebra.realCliffordSpinInclusion_eq_spinGroupMap (n : ℕ) : realCliffordSpinInclusion n = (realCliffordSpinInclusionIsometry n).spinGroupMap

The lower-rank Spin inclusion is the map induced by its defining quadratic isometry.

@[simp]

theorem CliffordAlgebra.realCliffordSpinInclusion_fixed_last (n : ℕ) (x : ↥(realCliffordSpinGroupZero n)) : (spinVectorAction (TauCeti.realCliffordForm (n + 1) 0) ((realCliffordSpinInclusion n) x)) (Pi.single (Fin.last n) 1) = Pi.single (Fin.last n) 1

The image of the lower-rank Spin inclusion fixes the last coordinate vector.

@[simp]

theorem CliffordAlgebra.realCliffordSpinInclusion_spinVectorAction_split (n : ℕ) (x : ↥(realCliffordSpinGroupZero n)) (m : Fin n → ℝ) (r : ℝ) : (spinVectorAction (TauCeti.realCliffordForm (n + 1) 0) ((realCliffordSpinInclusion n) x)) ((TauCeti.realCliffordPositiveSplitIsometry n 0).symm (m, r)) = (TauCeti.realCliffordPositiveSplitIsometry n 0).symm ((spinVectorAction (TauCeti.realCliffordForm n 0) x) m, r)

In positive-split coordinates, the lower-rank Spin inclusion acts on the first summand by the original Spin element and fixes the complementary line.

theorem CliffordAlgebra.realCliffordSpinInclusionIsometry_map_injective (n : ℕ) : Function.Injective ⇑(map (realCliffordSpinInclusionIsometry n))

The Clifford-algebra map induced by the lower-rank inclusion is injective.

theorem CliffordAlgebra.realCliffordSpinInclusion_injective (n : ℕ) : Function.Injective ⇑(realCliffordSpinInclusion n)

The lower-rank homomorphism Spin(n) → Spin(n + 1) is injective.

noncomputable def CliffordAlgebra.realCliffordSpinLastStabilizer (n : ℕ) : Subgroup ↥(realCliffordSpinGroupZero (n + 1))

The subgroup of Spin(n + 1) fixing the last coordinate vector under the vector action.

@[simp]

theorem CliffordAlgebra.mem_realCliffordSpinLastStabilizer_iff {n : ℕ} {x : ↥(realCliffordSpinGroupZero (n + 1))} : x ∈ realCliffordSpinLastStabilizer n ↔ (spinVectorAction (TauCeti.realCliffordForm (n + 1) 0) x) (Pi.single (Fin.last n) 1) = Pi.single (Fin.last n) 1

Membership in the last-vector stabilizer means that the Spin vector action fixes that vector.

theorem CliffordAlgebra.realCliffordSpinInclusion_mem_lastStabilizer (n : ℕ) (x : ↥(realCliffordSpinGroupZero n)) : (realCliffordSpinInclusion n) x ∈ realCliffordSpinLastStabilizer n

The lower-rank Spin inclusion fixes the last coordinate vector.

noncomputable def CliffordAlgebra.realCliffordSpinStabilizerInclusion (n : ℕ) : ↥(realCliffordSpinGroupZero n) →* ↥(realCliffordSpinLastStabilizer n)

The injective homomorphism from Spin(n) to the last-vector stabilizer in Spin(n + 1).

@[simp]

theorem CliffordAlgebra.coe_realCliffordSpinStabilizerInclusion_apply (n : ℕ) (x : ↥(realCliffordSpinGroupZero n)) : ↑((realCliffordSpinStabilizerInclusion n) x) = (realCliffordSpinInclusion n) x

The stabilizer inclusion agrees with the lower-rank Spin inclusion after forgetting the stabilizer membership proof.

theorem CliffordAlgebra.realCliffordSpinStabilizerInclusion_injective (n : ℕ) : Function.Injective ⇑(realCliffordSpinStabilizerInclusion n)

The homomorphism from Spin(n) to the last-vector stabilizer is injective.

@[simp]

theorem CliffordAlgebra.realCliffordSpinInclusion_negOne (n : ℕ) [NeZero n] : (realCliffordSpinInclusion n) (spinGroup.negOne (TauCeti.realCliffordForm n 0) ⋯) = spinGroup.negOne (TauCeti.realCliffordForm (n + 1) 0) ⋯

The lower-rank compact Spin inclusion sends the canonical nontrivial kernel element to the corresponding kernel element in the higher-rank Spin group.

theorem CliffordAlgebra.eq_or_eq_realCliffordSpinInclusion_negOne_mul_of_spinToSpecialOrthogonal_eq (n : ℕ) [NeZero n] (x : ↥(realCliffordSpinGroupZero (n + 1))) (y : ↥(realCliffordSpinGroupZero n)) (h : (spinToSpecialOrthogonal (TauCeti.realCliffordForm (n + 1) 0)) x = (spinToSpecialOrthogonal (TauCeti.realCliffordForm (n + 1) 0)) ((realCliffordSpinInclusion n) y)) : x = (realCliffordSpinInclusion n) y ∨ x = (realCliffordSpinInclusion n) (spinGroup.negOne (TauCeti.realCliffordForm n 0) ⋯ * y)

An element of Spin(n + 1) over the projection of an included element of Spin(n) is that element or its translate by the canonical nontrivial kernel element.

theorem CliffordAlgebra.realCliffordSpinStabilizerInclusion_surjective (n : ℕ) [NeZero n] : Function.Surjective ⇑(realCliffordSpinStabilizerInclusion n)

For positive n, every element of Spin(n + 1) fixing the last coordinate vector comes from the lower-rank inclusion Spin(n) → Spin(n + 1).

noncomputable def CliffordAlgebra.realCliffordSpinEquivLastStabilizer (n : ℕ) [NeZero n] : ↥(realCliffordSpinGroupZero n) ≃* ↥(realCliffordSpinLastStabilizer n)

For positive n, Spin(n) is multiplicatively equivalent to the full stabilizer of the last coordinate vector in Spin(n + 1). The forward map is the lower-rank stabilizer inclusion.

@[simp]

theorem CliffordAlgebra.realCliffordSpinEquivLastStabilizer_apply (n : ℕ) [NeZero n] (x : ↥(realCliffordSpinGroupZero n)) : (realCliffordSpinEquivLastStabilizer n) x = (realCliffordSpinStabilizerInclusion n) x

The forward compact Spin stabilizer equivalence is the lower-rank stabilizer inclusion.

@[simp]

theorem CliffordAlgebra.realCliffordSpinEquivLastStabilizer_symm_apply_inclusion (n : ℕ) [NeZero n] (x : ↥(realCliffordSpinGroupZero n)) : (realCliffordSpinEquivLastStabilizer n).symm ((realCliffordSpinStabilizerInclusion n) x) = x

The inverse compact Spin stabilizer equivalence sends an included element back to its lower-rank source.