Continuity and noncompactness of Spin transvection lifts

The canonical Clifford lift spinTransvection hQ hu huw of an Eichler transvection has carrier 1 + ι Q w * ι Q u. Consequently it varies continuously with the isotropic vector u and its orthogonal parameter w. For fixed u, this continuity descends through the quotient topology on u^⊥ / K ∙ u, making transvectionLiftHom hQ hu a continuous root-subgroup homomorphism.

Over a nontrivially normed field, the Spin root subgroup of u maps continuously onto the Eichler root subgroup of SO(Q), so it is compact exactly when the parameter space u^⊥ / K ∙ u is trivial. For a nonzero isotropic vector this happens exactly when dim V ≤ 2.

Main results

• CliffordAlgebra.continuous_spinTransvection proves continuity for families in both parameters.
• CliffordAlgebra.continuous_transvectionLiftHom proves continuity of the quotient homomorphism.
• CliffordAlgebra.isCompact_range_transvectionLiftHom_iff: the Spin root subgroup is compact exactly when its parameter space is trivial.
• CliffordAlgebra.isCompact_range_transvectionLiftHom_iff_finrank_le_two: for a nonzero isotropic vector, the Spin root subgroup is compact exactly when dim V ≤ 2.

References

• M. Eichler, Quadratische Formen und orthogonale Gruppen, Springer (1952).

theorem CliffordAlgebra.continuous_spinTransvection {K : Type u} [Field K] [TopologicalSpace K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [TopologicalSpace V] [IsModuleTopology K V] {Q : QuadraticForm K V} [ContinuousMul (CliffordAlgebra Q)] {X : Type w} [TopologicalSpace X] (u w : X → V) (hQ : QuadraticMap.Nondegenerate) (hu : ∀ (x : X), Q (u x) = 0) (huw : ∀ (x : X), QuadraticMap.polar (⇑Q) (u x) (w x) = 0) (huc : Continuous u) (hwc : Continuous w) : Continuous fun (x : X) => spinTransvection hQ ⋯ ⋯

Continuously varying isotropic vectors and orthogonal parameters determine continuously varying Spin lifts of Eichler transvections.

theorem CliffordAlgebra.continuous_transvectionLiftHom {K : Type u} [Field K] [TopologicalSpace K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [TopologicalSpace V] [IsModuleTopology K V] {Q : QuadraticForm K V} [ContinuousMul (CliffordAlgebra Q)] {u : V} (hQ : QuadraticMap.Nondegenerate) (hu : Q u = 0) : Continuous ⇑(transvectionLiftHom hQ hu)

The canonical homomorphism from u^⊥ / K ∙ u to the Spin group is continuous.

theorem CliffordAlgebra.isCompact_range_transvectionLiftHom_iff {K : Type u} [NontriviallyNormedField K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} {u : V} (hQ : QuadraticMap.Nondegenerate) (hu : Q u = 0) (hpolar : (QuadraticMap.polarBilin Q) u ≠ 0) : IsCompact (Set.range ⇑(transvectionLiftHom hQ hu)) ↔ Subsingleton (↥((QuadraticMap.polarBilin Q) u).ker ⧸ Submodule.comap ((QuadraticMap.polarBilin Q) u).ker.subtype (K ∙ u))

Compactness of a Spin root subgroup. For a nondegenerate form and an isotropic vector u outside the polar radical, the image of the Spin root-subgroup homomorphism u^⊥ / K ∙ u → Spin(Q) is compact exactly when the parameter space u^⊥ / K ∙ u is trivial.

theorem CliffordAlgebra.isCompact_range_transvectionLiftHom_iff_finrank_le_two {K : Type u} [NontriviallyNormedField K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} {u : V} (hQ : QuadraticMap.Nondegenerate) (hu : Q u = 0) (hu₀ : u ≠ 0) : IsCompact (Set.range ⇑(transvectionLiftHom hQ hu)) ↔ Module.finrank K V ≤ 2

Spin root subgroups are noncompact from dimension three on. For a nonzero isotropic vector u of a nondegenerate quadratic form on a finite-dimensional space, the Spin root subgroup of u is compact exactly when dim V ≤ 2, where it is trivial.