Continuity of the Lipschitz action

The Lipschitz group of a finite-dimensional quadratic space acts continuously on the space by twisted Clifford conjugation. Consequently its vector representation into the orthogonal group is continuous for the canonical topologies: the subgroup topology on the Lipschitz group inside the units of the Clifford algebra, and the subgroup topology on the orthogonal group inside the linear automorphism group.

Joint continuity holds over a commutative base ring when the quadratic space carries its module topology and multiplication in the Clifford algebra is continuous. Over a topological field, the representation is continuous when the quadratic space is finite-dimensional and carries its module topology.

Main results

• CliffordAlgebra.continuous_lipschitzVectorAction: the action is jointly continuous in the Lipschitz element and the vector.
• CliffordAlgebra.instContinuousSMulLipschitzGroup: the standard Lipschitz-group action is a continuous scalar action.
• CliffordAlgebra.continuous_lipschitzVectorAction_apply: the image of a fixed vector varies continuously with the Lipschitz element.
• CliffordAlgebra.continuous_lipschitzVectorAction_toLinearMap: the underlying endomorphism varies continuously.
• CliffordAlgebra.continuous_lipschitzVectorAction_linearEquiv: the automorphism-valued action varies continuously.
• CliffordAlgebra.continuous_lipschitzToOrthogonal: the vector representation is continuous.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.

theorem CliffordAlgebra.continuous_lipschitzVectorAction {R : Type u_1} {V : Type u_2} [CommRing R] [TopologicalSpace R] [Invertible 2] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsModuleTopology R V] (Q : QuadraticForm R V) [ContinuousMul (CliffordAlgebra Q)] : Continuous fun (p : ↥(lipschitzGroup Q) × V) => (lipschitzVectorAction Q p.1) p.2

The action of the Lipschitz group on its quadratic space is jointly continuous.

instance CliffordAlgebra.instContinuousSMulLipschitzGroup {R : Type u_1} {V : Type u_2} [CommRing R] [TopologicalSpace R] [Invertible 2] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsModuleTopology R V] (Q : QuadraticForm R V) [ContinuousMul (CliffordAlgebra Q)] : ContinuousSMul (↥(lipschitzGroup Q)) V

The standard action of the Lipschitz group on its quadratic space is continuous.

theorem CliffordAlgebra.continuous_lipschitzVectorAction_apply {R : Type u_1} {V : Type u_2} [CommRing R] [TopologicalSpace R] [Invertible 2] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsModuleTopology R V] (Q : QuadraticForm R V) [ContinuousMul (CliffordAlgebra Q)] (v : V) : Continuous fun (x : ↥(lipschitzGroup Q)) => (lipschitzVectorAction Q x) v

For a fixed vector, its image under a Lipschitz element varies continuously.

theorem CliffordAlgebra.instIsTopologicalRing_tauCeti {K : Type u_1} [Field K] [TopologicalSpace K] [IsTopologicalSemiring K] : IsTopologicalRing K

theorem CliffordAlgebra.continuous_lipschitzVectorAction_toLinearMap {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalSemiring K] [Invertible 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [TopologicalSpace V] [IsModuleTopology K V] (Q : QuadraticForm K V) : Continuous fun (x : ↥(lipschitzGroup Q)) => ↑(lipschitzVectorAction Q x)

The underlying endomorphism of the Lipschitz action varies continuously.

theorem CliffordAlgebra.continuous_lipschitzVectorAction_linearEquiv {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalSemiring K] [Invertible 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [TopologicalSpace V] [IsModuleTopology K V] (Q : QuadraticForm K V) : Continuous fun (x : ↥(lipschitzGroup Q)) => lipschitzVectorAction Q x

The linear-automorphism-valued Lipschitz action varies continuously.

theorem CliffordAlgebra.continuous_lipschitzToOrthogonal {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalSemiring K] [Invertible 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [TopologicalSpace V] [IsModuleTopology K V] (Q : QuadraticForm K V) : Continuous ⇑(lipschitzToOrthogonal Q)

The twisted-conjugation homomorphism from the Lipschitz group to the orthogonal group is continuous for the canonical subgroup topologies.