The compact real Spin unit level as a Euclidean sphere

The positive-definite quadratic form defining the compact real Spin group is the squared Euclidean norm in Euclidean coordinates. This file packages the resulting homeomorphism between the Spin action's unit level and the standard Euclidean unit sphere. The resulting path-connectedness theorem supplies paths between points of the unit level in dimensions at least two.

Main declarations

• CliffordAlgebra.realCliffordUnitLevelAntipode is negation on the compact unit level and is equivariant for the Spin action.
• CliffordAlgebra.realCliffordUnitLevelHomeomorphSubtype identifies the action carrier with the same unit level viewed as a raw quadratic-form subtype.
• CliffordAlgebra.realCliffordUnitLevelHomeomorphSphere identifies the unit level with the Euclidean unit sphere through EuclideanSpace.equiv.
• CliffordAlgebra.pathConnectedSpace_realCliffordUnitLevel_add_two transfers the standard path-connectedness theorem for spheres to the unit level in dimensions at least two.

def CliffordAlgebra.realCliffordUnitLevelAntipode {n : ℕ} (x : ↥(realCliffordUnitLevel n)) : ↥(realCliffordUnitLevel n)

The antipode of a point in the compact real Clifford unit level.

@[simp]

theorem CliffordAlgebra.coe_realCliffordUnitLevelAntipode {n : ℕ} (x : ↥(realCliffordUnitLevel n)) : ↑(realCliffordUnitLevelAntipode x) = -↑x

The compact real Clifford unit-level antipode is negation on the underlying vector.

@[simp]

theorem CliffordAlgebra.realCliffordUnitLevelAntipode_antipode {n : ℕ} (x : ↥(realCliffordUnitLevel n)) : realCliffordUnitLevelAntipode (realCliffordUnitLevelAntipode x) = x

The compact real Clifford unit-level antipode is an involution.

@[simp]

theorem CliffordAlgebra.ne_realCliffordUnitLevelAntipode {n : ℕ} (x : ↥(realCliffordUnitLevel n)) : x ≠ realCliffordUnitLevelAntipode x

A point of the compact real Clifford unit level differs from its antipode.

@[simp]

theorem CliffordAlgebra.smul_realCliffordUnitLevelAntipode {n : ℕ} (g : ↥(realCliffordSpinGroupZero n)) (x : ↥(realCliffordUnitLevel n)) : g • realCliffordUnitLevelAntipode x = realCliffordUnitLevelAntipode (g • x)

The compact Spin action commutes with the unit-level antipode.

noncomputable def CliffordAlgebra.realCliffordUnitLevelHomeomorphSphere (n : ℕ) : ↥(realCliffordUnitLevel n) ≃ₜ ↑(Metric.sphere 0 1)

The compact real Spin unit level is homeomorphic to the Euclidean unit sphere.

def CliffordAlgebra.realCliffordUnitLevelHomeomorphSubtype (n : ℕ) : ↥(realCliffordUnitLevel n) ≃ₜ { x : Fin n → ℝ // (TauCeti.realCliffordForm n 0) x = 1 }

The compact real Spin unit level is the raw quadratic level with its canonical action subtype structure forgotten.

@[simp]

theorem CliffordAlgebra.coe_realCliffordUnitLevelHomeomorphSubtype_apply (n : ℕ) (x : ↥(realCliffordUnitLevel n)) : ↑((realCliffordUnitLevelHomeomorphSubtype n) x) = ↑x

The carrier homeomorphism does not change the underlying vector.

@[simp]

theorem CliffordAlgebra.coe_realCliffordUnitLevelHomeomorphSubtype_symm_apply (n : ℕ) (x : { x : Fin n → ℝ // (TauCeti.realCliffordForm n 0) x = 1 }) : ↑((realCliffordUnitLevelHomeomorphSubtype n).symm x) = ↑x

The inverse carrier homeomorphism does not change the underlying vector.

@[simp]

theorem CliffordAlgebra.coe_realCliffordUnitLevelHomeomorphSphere_apply (n : ℕ) (x : ↥(realCliffordUnitLevel n)) : ↑((realCliffordUnitLevelHomeomorphSphere n) x) = (EuclideanSpace.equiv (Fin n) ℝ).symm ↑x

The forward map of realCliffordUnitLevelHomeomorphSphere is Euclidean coordinate conversion.

@[simp]

theorem CliffordAlgebra.coe_realCliffordUnitLevelHomeomorphSphere_symm_apply (n : ℕ) (u : ↑(Metric.sphere 0 1)) : ↑((realCliffordUnitLevelHomeomorphSphere n).symm u) = (EuclideanSpace.equiv (Fin n) ℝ) ↑u

The inverse map of realCliffordUnitLevelHomeomorphSphere returns function coordinates.

theorem CliffordAlgebra.pathConnectedSpace_realCliffordUnitLevel_add_two (n : ℕ) : PathConnectedSpace ↥(realCliffordUnitLevel (n + 2))

The compact real Spin unit level is path-connected in dimensions at least two.