Topology on Clifford Spin groups

This file uses the canonical subtype topology on a Spin group inside a topological Clifford algebra. The surrounding Clifford algebra has its module topology from TauCeti.Topology.Algebra.CliffordAlgebra.Basic. A special orthogonal group in coordinates has the independently induced topology from TauCeti.Topology.Algebra.QuadraticForm.SpecialOrthogonal.

When 2 is invertible, the vector space has its module topology, and Clifford multiplication is continuous, the Spin action is jointly continuous by the explicit Clifford conjugation formula for spinVectorAction. Under the same hypotheses, this proves continuity of the Spin projection for a quadratic form on a finite coordinate space. In particular, this gives the topological-group bridge for the compact real double cover at signature (n, 0). It makes no smoothness, compactness, connectedness, simple-connectivity, fibration, or universal-cover claim.

Continuity argument

For x : spinGroup Q and a vector v, the public action equation gives

ι Q (spinVectorAction Q x v) = x * ι Q v * star x.

On the Spin group, star x is the inverse of x. The subtype coercion and Clifford star are continuous, so the right-hand side is jointly continuous in x and v. The continuous vector-part map ιInv Q is a left inverse to ι Q; applying it proves continuity of the Spin action.

A map into matrices is continuous exactly when each matrix entry is continuous. The (i, j) entry of the standard matrix of the Spin action is the ith coordinate of the action on Pi.single j 1. The fixed-vector result therefore proves continuity into the independently topologized special orthogonal group.

Main results

• QuadraticMap.Isometry.continuous_spinGroupMap proves continuity of the Spin-group map induced by an isometry of quadratic spaces, and QuadraticMap.IsometryEquiv.continuous_spinGroupEquiv that of the Spin-group equivalence induced by an isometric equivalence.
• QuadraticMap.IsometryEquiv.spinGroupContinuousMulEquiv upgrades the latter to an isomorphism of topological groups.
• QuadraticMap.Isometry.isEmbedding_spinGroupMap restricts an embedding of the induced Clifford map to the corresponding Spin groups.
• CliffordAlgebra.instIsTopologicalGroupSpinGroup equips spinGroup Q with a topological group structure for its canonical subtype topology.
• CliffordAlgebra.continuous_spinVectorAction proves joint continuity of the Spin action when 2 is invertible, the vector space has its module topology, and Clifford multiplication is continuous.
• CliffordAlgebra.continuous_spinVectorAction_apply proves fixed-vector continuity under the same hypotheses.
• CliffordAlgebra.joined_of_coe_eq_prod_mul_ι_mul_prod moves one factor of a Spin element written as a product of vectors along a path in its level set.
• QuadraticForm.isClosed_spinVectorStabilizer proves that every vector stabilizer is closed when the vector space is T1, under the same hypotheses.
• CliffordAlgebra.continuous_spinToSpecialOrthogonal_pi proves continuity of the Spin projection for every quadratic form on a finite coordinate space with its module topology, continuous Clifford multiplication, and 2 invertible.
• CliffordAlgebra.continuous_realCliffordSpinDoubleCoverZero_rightHom specializes this result to the projection field of the packaged compact real double cover.
• CliffordAlgebra.continuous_realCliffordSpinInclusion proves continuity of the lower-rank inclusion used in the compact stabilizer construction.
• CliffordAlgebra.isEmbedding_realCliffordSpinInclusion strengthens this inclusion to a topological embedding.
• CliffordAlgebra.isEmbedding_realCliffordSpinStabilizerInclusion proves that the lower-rank inclusion into the last-vector stabilizer is a topological embedding.
• CliffordAlgebra.isClosed_realCliffordSpinLastStabilizer proves that this stabilizer is closed.
• CliffordAlgebra.continuous_realCliffordSpinStabilizerInclusion proves continuity after restricting the inclusion's codomain to the last-vector stabilizer.
• CliffordAlgebra.realCliffordSpinContinuousMulEquivLastStabilizer identifies the lower-rank Spin group with the full last-vector stabilizer as a topological group.

References

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

theorem QuadraticMap.Isometry.isEmbedding_spinGroupMap {R : Type u} [CommRing R] {V : Type v} {W : Type w} [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] {Q : QuadraticForm R V} {P : QuadraticForm R W} [TopologicalSpace (CliffordAlgebra Q)] [TopologicalSpace (CliffordAlgebra P)] (f : Q →qᵢ P) (hf : Topology.IsEmbedding ⇑(CliffordAlgebra.map f)) : Topology.IsEmbedding ⇑f.spinGroupMap

An embedding of the Clifford-algebra map induced by a quadratic isometry restricts to an embedding of the corresponding Spin groups for their subtype topologies.

theorem QuadraticMap.Isometry.continuous_spinGroupMap {R : Type u_1} [CommRing R] [TopologicalSpace R] {V : Type u} {W : Type v} [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] {Q : QuadraticForm R V} {P : QuadraticForm R W} (f : Q →qᵢ P) : Continuous ⇑f.spinGroupMap

The Spin-group map induced by an isometry of quadratic spaces is continuous for the canonical subtype topologies.

theorem QuadraticMap.IsometryEquiv.continuous_spinGroupEquiv {R : Type u_1} [CommRing R] [TopologicalSpace R] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] {Q : QuadraticForm R V} {P : QuadraticForm R W} (e : IsometryEquiv Q P) : Continuous ⇑e.spinGroupEquiv

The Spin-group equivalence induced by an isometric equivalence of quadratic spaces is continuous for the canonical subtype topologies.

def QuadraticMap.IsometryEquiv.spinGroupContinuousMulEquiv {R : Type u_1} [CommRing R] [TopologicalSpace R] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] {Q : QuadraticForm R V} {P : QuadraticForm R W} (e : IsometryEquiv Q P) : ↥(spinGroup Q) ≃ₜ* ↥(spinGroup P)

The Spin-group equivalence induced by an isometric equivalence of quadratic spaces, as an isomorphism of topological groups for the canonical subtype topologies.

@[simp]

theorem QuadraticMap.IsometryEquiv.coe_spinGroupContinuousMulEquiv {R : Type u_1} [CommRing R] [TopologicalSpace R] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] {Q : QuadraticForm R V} {P : QuadraticForm R W} (e : IsometryEquiv Q P) : ⇑e.spinGroupContinuousMulEquiv = ⇑e.spinGroupEquiv

The topological Spin-group equivalence induced by an isometric equivalence evaluates as the underlying Spin-group equivalence.

@[simp]

theorem QuadraticMap.IsometryEquiv.spinGroupContinuousMulEquiv_symm {R : Type u_1} [CommRing R] [TopologicalSpace R] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] {Q : QuadraticForm R V} {P : QuadraticForm R W} (e : IsometryEquiv Q P) : e.spinGroupContinuousMulEquiv.symm = e.symm.spinGroupContinuousMulEquiv

The inverse of the topological Spin-group equivalence is induced by the inverse isometry.

instance CliffordAlgebra.instIsTopologicalGroupSpinGroup {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) [ContinuousMul (CliffordAlgebra Q)] : IsTopologicalGroup ↥(spinGroup Q)

A Spin group inside a continuously multiplicative Clifford algebra is a topological group for its subtype topology. Multiplication is inherited from the Clifford algebra, while inversion is Clifford star.

theorem CliffordAlgebra.continuous_spinVectorAction {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] [Invertible 2] [TopologicalSpace V] [IsModuleTopology R V] (Q : QuadraticForm R V) [ContinuousMul (CliffordAlgebra Q)] : Continuous fun (p : ↥(spinGroup Q) × V) => (spinVectorAction Q p.1) p.2

The Spin action is jointly continuous in the Spin element and the vector.

theorem CliffordAlgebra.continuous_spinVectorAction_apply {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] [Invertible 2] [TopologicalSpace V] [IsModuleTopology R V] (Q : QuadraticForm R V) [ContinuousMul (CliffordAlgebra Q)] (v : V) : Continuous fun (x : ↥(spinGroup Q)) => (spinVectorAction Q x) v

For a fixed vector, its image under the Spin action depends continuously on the Spin element.

theorem QuadraticForm.isClosed_spinVectorStabilizer {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] [Invertible 2] [TopologicalSpace V] [IsModuleTopology R V] [T1Space V] (Q : QuadraticForm R V) [ContinuousMul (CliffordAlgebra Q)] (v : V) : IsClosed {x : ↥(spinGroup Q) | (CliffordAlgebra.spinVectorAction Q x) v = v}

The subgroup of a Spin group fixing a vector is closed when the vector space is T1.

theorem CliffordAlgebra.continuous_spinToSpecialOrthogonal_pi {R : Type u} [CommRing R] [TopologicalSpace R] [Invertible 2] {n : Type v} [Fintype n] (Q : QuadraticForm R (n → R)) [IsModuleTopology R (n → R)] [ContinuousMul (CliffordAlgebra Q)] : Continuous ⇑(spinToSpecialOrthogonal Q)

The Spin action of a quadratic form on a finite coordinate space is continuous as a map to the special orthogonal group with its standard coordinate topology.

theorem CliffordAlgebra.joined_of_coe_eq_prod_mul_ι_mul_prod {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsModuleTopology R V] {Q : QuadraticForm R V} [ContinuousMul (CliffordAlgebra Q)] {l₁ l₂ : List V} {b b' : V} (hl : Even (l₁.length + l₂.length + 1)) (hQ : (List.map (⇑Q) l₁).prod * Q b * (List.map (⇑Q) l₂).prod = 1) (h : JoinedIn {v : V | Q v = Q b} b b') {x y : ↥(spinGroup Q)} (hx : ↑x = (List.map (⇑(ι Q)) l₁).prod * (ι Q) b * (List.map (⇑(ι Q)) l₂).prod) (hy : ↑y = (List.map (⇑(ι Q)) l₁).prod * (ι Q) b' * (List.map (⇑(ι Q)) l₂).prod) : Joined x y

Moving one factor of a product of vectors. Let a Spin element be a product P₁ * ι b * P₂ of vectors whose norms multiply to one, with P₁ and P₂ products of vectors. Moving the factor b to b' along a path inside its level set {v | Q v = Q b} keeps the product in the Spin group, and so joins the element to P₁ * ι b' * P₂.

theorem CliffordAlgebra.continuous_realCliffordSpinDoubleCoverZero_rightHom (n : ℕ) [NeZero n] : Continuous ⇑(realCliffordSpinDoubleCoverZero n).rightHom

The projection field of the compact real Spin double cover is continuous.

theorem CliffordAlgebra.isEmbedding_realCliffordSpinInclusion (n : ℕ) : Topology.IsEmbedding ⇑(realCliffordSpinInclusion n)

The canonical inclusion Spin(n) → Spin(n + 1) is a topological embedding for every n.

theorem CliffordAlgebra.continuous_realCliffordSpinInclusion (n : ℕ) : Continuous ⇑(realCliffordSpinInclusion n)

The lower-rank inclusion Spin(n) → Spin(n + 1) is continuous for the canonical real Clifford-algebra subtype topologies.

theorem CliffordAlgebra.isClosed_realCliffordSpinLastStabilizer (n : ℕ) : IsClosed ↑(realCliffordSpinLastStabilizer n)

The subgroup of Spin(n + 1) fixing the last coordinate vector is closed.

theorem CliffordAlgebra.isEmbedding_realCliffordSpinStabilizerInclusion (n : ℕ) : Topology.IsEmbedding ⇑(realCliffordSpinStabilizerInclusion n)

The canonical inclusion Spin(n) → Spin(n + 1), restricted to the last-vector stabilizer, is a topological embedding.

theorem CliffordAlgebra.continuous_realCliffordSpinStabilizerInclusion (n : ℕ) : Continuous ⇑(realCliffordSpinStabilizerInclusion n)

The canonical inclusion Spin(n) → Spin(n + 1) is continuous after restricting its codomain to the last-vector stabilizer.

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

For positive n, the lower-rank compact Spin group is isomorphic as a topological group to the full last-vector stabilizer in Spin(n + 1).

@[simp]

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

The forward map of the topological stabilizer equivalence is the canonical lower-rank Spin inclusion into the stabilizer.

@[simp]

theorem CliffordAlgebra.realCliffordSpinContinuousMulEquivLastStabilizer_toMulEquiv (n : ℕ) [NeZero n] : ↑(realCliffordSpinContinuousMulEquivLastStabilizer n) = realCliffordSpinEquivLastStabilizer n

The multiplicative equivalence underlying the topological stabilizer equivalence is the canonical algebraic stabilizer equivalence.

@[simp]

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

The inverse topological stabilizer equivalence sends an included element back to the original lower-rank Spin element.