The Spin double cover as a group extension

For a positive-dimensional finite nondegenerate quadratic space over a field in which 2 is invertible, the kernel equivalence from Spin.Kernel and any proof that the action is surjective package the Spin double cover as a GroupExtension; in particular, the action is surjective over a separably closed field.

Main definitions and results

• CliffordAlgebra.spinDoubleCoverOfSurjective packages any surjective Spin action as a group extension.
• CliffordAlgebra.spinDoubleCover packages 1 → ZMod 2 → Spin(Q) → SO(Q) → 1 as a group extension.
• CliffordAlgebra.spinDoubleCoverOfSurjective_inl_ofAdd_one and CliffordAlgebra.spinDoubleCoverOfSurjective_rightHom characterize the generic extension.
• CliffordAlgebra.spinDoubleCover_inl_ofAdd_one and CliffordAlgebra.spinDoubleCover_rightHom characterize the separably closed case.

References

This supplies the Spin short exact sequence over a separably closed field; the Pin/O(V) sequence and the general-field spinor-norm version are not covered here. See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2.

noncomputable def CliffordAlgebra.spinDoubleCoverOfSurjective {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Nontrivial V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hsurj : Function.Surjective ⇑(spinToSpecialOrthogonal Q)) : GroupExtension (Multiplicative (ZMod 2)) ↥(spinGroup Q) ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)

A surjective Spin action on a positive-dimensional nondegenerate quadratic space over a field in which 2 is invertible is the group extension 1 → ZMod 2 → Spin(Q) → SO(Q) → 1.

@[simp]

theorem CliffordAlgebra.spinDoubleCoverOfSurjective_inl_ofAdd_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Nontrivial V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hsurj : Function.Surjective ⇑(spinToSpecialOrthogonal Q)) : (spinDoubleCoverOfSurjective Q hQ hsurj).inl (Multiplicative.ofAdd 1) = spinGroup.negOne Q ⋯

The inclusion in a Spin double cover built from a surjectivity proof sends the generator to the scalar -1.

@[simp]

theorem CliffordAlgebra.spinDoubleCoverOfSurjective_rightHom {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Nontrivial V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hsurj : Function.Surjective ⇑(spinToSpecialOrthogonal Q)) : (spinDoubleCoverOfSurjective Q hQ hsurj).rightHom = spinToSpecialOrthogonal Q

The projection in a Spin double cover built from a surjectivity proof is the Spin action.

noncomputable def CliffordAlgebra.spinDoubleCover {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Nontrivial V] [FiniteDimensional K V] [Invertible 2] [IsSepClosed K] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : GroupExtension (Multiplicative (ZMod 2)) ↥(spinGroup Q) ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)

For a positive-dimensional nondegenerate quadratic space over a separably closed field in which 2 is invertible, the Spin action is the group extension 1 → ZMod 2 → Spin(Q) → SO(Q) → 1.

theorem CliffordAlgebra.spinDoubleCover_def {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Nontrivial V] [FiniteDimensional K V] [Invertible 2] [IsSepClosed K] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : spinDoubleCover Q hQ = spinDoubleCoverOfSurjective Q hQ ⋯

The separably closed Spin double cover is the generic construction applied to canonical surjectivity.

@[simp]

theorem CliffordAlgebra.spinDoubleCover_inl_ofAdd_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Nontrivial V] [FiniteDimensional K V] [Invertible 2] [IsSepClosed K] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : (spinDoubleCover Q hQ).inl (Multiplicative.ofAdd 1) = spinGroup.negOne Q ⋯

The inclusion in the separably closed Spin double cover sends the generator to the scalar -1.

@[simp]

theorem CliffordAlgebra.spinDoubleCover_rightHom {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Nontrivial V] [FiniteDimensional K V] [Invertible 2] [IsSepClosed K] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : (spinDoubleCover Q hQ).rightHom = spinToSpecialOrthogonal Q

The projection in the separably closed Spin double cover is the Spin action.