Cartan--Dieudonné for Lipschitz and Pin actions

Over a field of characteristic other than two, Cartan--Dieudonné and the action of a generating vector show that the Lipschitz action is onto the orthogonal group.

Let g be an orthogonal automorphism fixing a subspace W, and let x be an anisotropic vector orthogonal to W. The generic fixed-subspace correction in the quadratic-form layer uses one or two reflections to make the product fix W ⊔ K ∙ x. Over a separably closed field of characteristic other than two, those reflections lift through the Pin group, so the correcting element lies in the range of pinToOrthogonal.

Main results

• CliffordAlgebra.lipschitzToOrthogonal_surjective: the Lipschitz action is onto for a finite-dimensional nondegenerate quadratic space.
• CliffordAlgebra.exists_mem_range_pinToOrthogonal_mul_eqOn_sup_span_singleton: a Pin-range correction extends a fixed subspace by one orthogonal anisotropic vector.
• CliffordAlgebra.pinToOrthogonal_surjective: over a separably closed field of characteristic other than two, the Pin action is surjective on a finite-dimensional nondegenerate quadratic space.

References

This advances Layer 2's "The double cover" target in TauCetiRoadmap/RepresentationTheory/SpinRepresentations/README.md. See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2.

theorem CliffordAlgebra.lipschitzToOrthogonal_surjective {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : Function.Surjective ⇑(lipschitzToOrthogonal Q)

The Lipschitz action is onto the orthogonal group of a finite-dimensional nondegenerate quadratic space over a field of characteristic other than two.

theorem CliffordAlgebra.exists_mem_range_pinToOrthogonal_mul_eqOn_sup_span_singleton {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [Invertible 2] [IsSepClosed K] (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)) (W : Submodule K V) (hfix : ∀ w ∈ W, ↑g w = w) (x : V) [Invertible (Q x)] (hx : ∀ w ∈ W, QuadraticMap.IsOrtho Q x w) : ∃ r ∈ (pinToOrthogonal Q).range, ∀ y ∈ W ⊔ K ∙ x, ↑(r * g) y = y

Given an orthogonal automorphism that fixes W and an anisotropic vector x orthogonal to W, a Pin-range correction makes the product fix W ⊔ K ∙ x pointwise.

theorem CliffordAlgebra.pinToOrthogonal_surjective_of_isSquare {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hsquare : ∀ (v : V) [inst : Invertible (Q v)], IsSquare (-⅟(Q v))) : Function.Surjective ⇑(pinToOrthogonal Q)

Over a field of characteristic other than two, the twisted-conjugation homomorphism from the Pin group is surjective when every reflection normalization scalar is a square.

theorem CliffordAlgebra.pinToOrthogonal_surjective {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] [IsSepClosed K] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : Function.Surjective ⇑(pinToOrthogonal Q)

The twisted-conjugation homomorphism from the Pin group is surjective for a finite-dimensional nondegenerate quadratic space over a separably closed field of characteristic other than two.