Continuity of the Spin and Pin inclusions

The Pin group inherits the subtype topology from the Clifford algebra with its module topology. Its inclusion into the Lipschitz group is continuous for the subgroup topology inside the units of the Clifford algebra. Both unit coordinates are continuous: the forward coordinate is the subtype coercion, and the inverse coordinate is Clifford star. This inclusion allows continuity of the Lipschitz representation to restrict to Pin and Spin. The Spin inclusion into Pin is continuous for their Clifford-algebra subtype topologies.

References

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

theorem TauCeti.CliffordAlgebra.continuous_spinToPin {R : Type u_1} {V : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) : Continuous ⇑(CliffordAlgebra.spinToPin Q)

The Spin inclusion into the Pin group is continuous for their canonical Clifford-algebra subtype topologies.

theorem TauCeti.CliffordAlgebra.continuous_pinToLipschitz {R : Type u_1} {V : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) : Continuous ⇑(CliffordAlgebra.pinToLipschitz Q)

The Pin inclusion into the Lipschitz group is continuous for the canonical Clifford-algebra and unit-group topologies.