Topology on Clifford algebras

This file gives a Clifford algebra its module topology, making it a topological additive group. Over a topological ring, multiplication is continuous when the Clifford algebra is a finite module. The topology is Hausdorff when the base ring is Hausdorff with continuous addition and multiplication, and the Clifford algebra is free. Clifford reverse, involution, and star are continuous without these additional assumptions.

The topology is intrinsic: it depends only on the module structure of the Clifford algebra together with the topology on the base ring, and does not use a basis, Pin or Spin groups, or their actions. A basis appears only in the proof that the topology is Hausdorff.

Main results

• CliffordAlgebra.instTopologicalSpaceCliffordAlgebra installs the module topology.
• CliffordAlgebra.instIsTopologicalAddGroupCliffordAlgebra makes addition continuous.
• CliffordAlgebra.continuous_ι proves continuity of the canonical generator when the vector module has its module topology.
• CliffordAlgebra.continuous_algHom_apply proves continuity of a Clifford representation evaluated at a fixed module element.
• CliffordAlgebra.continuous_ιInv proves continuity of the vector-part map under the same topology assumption when 2 is invertible.
• QuadraticMap.Isometry.continuous_cliffordAlgebraMap proves continuity of maps induced by quadratic isometries.
• CliffordAlgebra.instIsTopologicalRingCliffordAlgebra makes multiplication continuous.
• CliffordAlgebra.instT2SpaceCliffordAlgebra proves the topology is Hausdorff.
• CliffordAlgebra.instLocallyCompactSpaceCliffordAlgebra proves the topology is locally compact for a finite-dimensional space over a locally compact field in which 2 is invertible.
• CliffordAlgebra.instSigmaCompactSpaceCliffordAlgebra proves the topology is σ-compact under the same hypotheses with σ-compact in place of locally compact.
• CliffordAlgebra.isClosedEmbedding_algebraMap identifies the scalar field as a closed subspace over a Hausdorff topological field in which 2 is invertible.
• CliffordAlgebra.continuous_reverse and CliffordAlgebra.continuous_involute prove continuity of the two canonical Clifford involutions.
• CliffordAlgebra.instContinuousStarCliffordAlgebra packages continuity of Clifford star.

@[instance_reducible]

instance CliffordAlgebra.instTopologicalSpaceCliffordAlgebra {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) : TopologicalSpace (CliffordAlgebra Q)

The canonical topology on a Clifford algebra is its module topology.

theorem CliffordAlgebra.continuous_ι {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsModuleTopology R V] (Q : QuadraticForm R V) : Continuous ⇑(ι Q)

The canonical generator into a Clifford algebra is continuous for the module topologies.

theorem CliffordAlgebra.continuous_algHom_apply {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] {S : Type u_1} {W : Type u_2} [CommRing S] [Algebra R S] [AddCommGroup W] [Module S W] [Module R W] [IsScalarTower R S W] [TopologicalSpace W] [ContinuousAdd W] [ContinuousSMul R W] {Q : QuadraticForm R V} (ρ : CliffordAlgebra Q →ₐ[R] Module.End S W) (w : W) : Continuous fun (a : CliffordAlgebra Q) => (ρ a) w

A Clifford representation evaluated at a fixed module element is continuous for the canonical module topology on the Clifford algebra.

theorem CliffordAlgebra.continuous_ιInv {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) : Continuous ⇑(ιInv Q)

The vector-part projection from a Clifford algebra is continuous for the module topologies.

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

The Clifford-algebra map induced by an isometry of quadratic spaces is continuous for the canonical module topologies.

theorem CliffordAlgebra.continuous_reverse {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) : Continuous ⇑reverse

Clifford reversal is continuous for the module topology.

theorem CliffordAlgebra.continuous_involute {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) : Continuous ⇑involute

The Clifford grade involution is continuous for the module topology.

instance CliffordAlgebra.instContinuousStarCliffordAlgebra {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) : ContinuousStar (CliffordAlgebra Q)

Clifford star is continuous for the module topology.

instance CliffordAlgebra.instIsTopologicalAddGroupCliffordAlgebra {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) : IsTopologicalAddGroup (CliffordAlgebra Q)

A Clifford algebra is a topological additive group for its module topology.

instance CliffordAlgebra.instT2SpaceCliffordAlgebra {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] [IsTopologicalSemiring R] [T2Space R] (Q : QuadraticForm R V) [Module.Free R (CliffordAlgebra Q)] : T2Space (CliffordAlgebra Q)

The module topology on a free Clifford algebra over a Hausdorff ring with continuous addition and multiplication is Hausdorff.

instance CliffordAlgebra.instIsTopologicalRingCliffordAlgebra {R : Type u} [CommRing R] [TopologicalSpace R] {V : Type v} [AddCommGroup V] [Module R V] [IsTopologicalRing R] (Q : QuadraticForm R V) [Module.Finite R (CliffordAlgebra Q)] : IsTopologicalRing (CliffordAlgebra Q)

A Clifford algebra that is finite as a module is a topological ring for its module topology.

instance CliffordAlgebra.instLocallyCompactSpaceCliffordAlgebra {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalSemiring K] [LocallyCompactSpace K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) : LocallyCompactSpace (CliffordAlgebra Q)

The Clifford algebra of a finite-dimensional space over a locally compact field in which 2 is invertible is locally compact for its module topology, being finite-dimensional.

instance CliffordAlgebra.instSigmaCompactSpaceCliffordAlgebra {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalSemiring K] [SigmaCompactSpace K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) : SigmaCompactSpace (CliffordAlgebra Q)

The Clifford algebra of a finite-dimensional space over a σ-compact field in which 2 is invertible is σ-compact for its module topology, being finite-dimensional.

theorem CliffordAlgebra.isClosedEmbedding_algebraMap {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [Invertible 2] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) : Topology.IsClosedEmbedding ⇑(algebraMap K (CliffordAlgebra Q))

The scalar inclusion in a Clifford algebra is a closed embedding for its module topology.