Lifting reflections to the Pin and Spin groups

When the inverse negative norm of a vector is a square, the vector can be rescaled to have norm -1. It therefore defines an element of the Pin group whose twisted-conjugation action is the reflection in the original vector. A pair of reflections needs only that the product of the inverse norms be a square: rescaling one vector then gives a unitary even product and hence a lift to the Spin group. Over a separably closed field, the required square conditions hold automatically. When the quadratic form is nondegenerate, the same lifts show that the Spin group linearly spans the even Clifford algebra, provided 2 is nonzero.

Main results

• CliffordAlgebra.reflection_mem_range_pinToOrthogonal_of_isSquare: a reflection lifts through the Pin action when its normalization scalar is a square.
• CliffordAlgebra.reflection_mul_reflection_mem_range_spinToOrthogonal_of_isSquare: a product of two reflections lifts through the Spin action when the product of its normalization scalars is a square. The version without the suffix is a separably closed-field corollary.
• CliffordAlgebra.span_spinGroup_eq_even_of_span_anisotropic: the Spin group spans the even Clifford algebra when anisotropic vectors span and pairs admit the required square normalization.
• CliffordAlgebra.span_spinGroup_eq_even_of_isSquare: the nondegenerate, characteristic-not-two corollary.
• CliffordAlgebra.span_spinGroup_eq_even: the separably closed-field corollary, for a nondegenerate form in characteristic different from two.

References

This supplies the reflection-lift prerequisite for Layer 2's double-cover target and the Spin-group spanning prerequisite for Layer 4's irreducibility target in TauCetiRoadmap/RepresentationTheory/SpinRepresentations/README.md. See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2.

theorem CliffordAlgebra.reflection_mem_range_pinToOrthogonal_of_isSquare {K : Type u} {V : Type v} [CommRing K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [Invertible 2] (v : V) [Invertible (Q v)] (hv : IsSquare (-⅟(Q v))) : TauCeti.QuadraticMap.reflectionOrthogonal Q v ∈ (pinToOrthogonal Q).range

If the required normalization scalar is a square, the reflection in v lifts through the Pin action.

theorem CliffordAlgebra.reflection_mul_reflection_mem_range_spinToOrthogonal_of_isSquare {K : Type u} {V : Type v} [CommRing K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [Invertible 2] (v w : V) [Invertible (Q v)] [Invertible (Q w)] (h : IsSquare (⅟(Q v) * ⅟(Q w))) : TauCeti.QuadraticMap.reflectionOrthogonal Q v * TauCeti.QuadraticMap.reflectionOrthogonal Q w ∈ (spinToOrthogonal Q).range

If the product of the required normalization scalars is a square, the product of the reflections in v and w lifts through the Spin action.

theorem CliffordAlgebra.reflection_mem_range_pinToOrthogonal {K : Type u} {V : Type v} [Field K] [IsSepClosed K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (v : V) [Invertible (Q v)] : TauCeti.QuadraticMap.reflectionOrthogonal Q v ∈ (pinToOrthogonal Q).range

Over a separably closed field, every reflection in a vector of invertible norm lifts to the Pin group.

theorem CliffordAlgebra.reflection_mul_reflection_mem_range_spinToOrthogonal {K : Type u} {V : Type v} [Field K] [IsSepClosed K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (v w : V) [Invertible (Q v)] [Invertible (Q w)] : TauCeti.QuadraticMap.reflectionOrthogonal Q v * TauCeti.QuadraticMap.reflectionOrthogonal Q w ∈ (spinToOrthogonal Q).range

Over a separably closed field, every product of two reflections in vectors of invertible norm lifts to the Spin group.

Linear generation of the even Clifford algebra

theorem CliffordAlgebra.span_spinGroup_eq_even_of_span_anisotropic {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hspan : Submodule.span K {v : V | Q v ≠ 0} = ⊤) (hsq : ∀ (v w : V), Q v ≠ 0 → Q w ≠ 0 → IsSquare ((Q v)⁻¹ * (Q w)⁻¹)) : Submodule.span K ↑(spinGroup Q) = Subalgebra.toSubmodule (even Q)

The Spin group linearly spans the even Clifford algebra when anisotropic vectors span and every pair of them admits the square normalization needed to lift it to the Spin group.

theorem CliffordAlgebra.span_spinGroup_eq_even_of_isSquare {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [NeZero 2] (hQ : QuadraticMap.Nondegenerate) (hsq : ∀ (v w : V), Q v ≠ 0 → Q w ≠ 0 → IsSquare ((Q v)⁻¹ * (Q w)⁻¹)) : Submodule.span K ↑(spinGroup Q) = Subalgebra.toSubmodule (even Q)

The Spin group linearly spans the even Clifford algebra when every pair of anisotropic vectors admits the square normalization, the form is nondegenerate, and 2 is nonzero.

theorem CliffordAlgebra.span_spinGroup_eq_even {K : Type u} {V : Type v} [Field K] [IsSepClosed K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [NeZero 2] (hQ : QuadraticMap.Nondegenerate) : Submodule.span K ↑(spinGroup Q) = Subalgebra.toSubmodule (even Q)

The Spin group linearly spans the even Clifford algebra for a nondegenerate quadratic form over a separably closed field of characteristic different from two.