Remark. Real spinor-norm images and the low-rank boundary [fcap-002F]
✍️source

Let \(Q\) be a positive-dimensional finite-dimensional nondegenerate real quadratic form. Distinguish the orthogonal norm \(\nu _Q^O\) on \(O(Q)\) from its restriction \(\nu _Q\) to \(SO(Q)\). Since \(\mathbb R^{\times }/(\mathbb R^\times )^2=\{[1],[-1]\}\), their images and the Spin image are: \[\begin {array}{c|c|c|c} \text {case}&\operatorname {im}\nu _Q^O& \operatorname {im}\nu _Q&\text {Spin image}\\ \hline \text {positive definite}&\{[1]\}&\{[1]\}&SO(Q)\\ \text {negative definite}&\{[1],[-1]\}&\{[1]\}&SO(Q)\\ \text {indefinite}&\{[1],[-1]\}&\{[1],[-1]\}&\ker \nu _Q \end {array}\] For a positive form, every reflected value is a square, so the orthogonal norm is trivial CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_posDef. For a negative form, the orthogonal norm is the determinant square class and is therefore trivial on \(SO(Q)\) CliffordAlgebra.orthogonalSpinorNorm_eq_orthogonalDetSquareClass_of_negDef CliffordAlgebra.spinorNorm_eq_one_of_negDef. In the indefinite case, one positive and one negative reflection give a determinant-one element of norm \([-1]\), so \(\nu _Q\) is onto CliffordAlgebra.spinorNorm_surjective_of_indefinite. Thus the final kernel has index two. The Spin-image column follows from Theorem [fcap-0023]; the table does not identify this kernel with a topological component.

Rank zero is separate: \(SO(Q)\) is trivial, and the image/kernel theorem uses its subsingleton branch rather than the positive-dimensional scalar row. In rank one, \(SO(Q)\) and its spinor norm are trivial. For any nonzero \(v\), the image of \(\nu _Q^O\) is generated by \([Q(v)]\), and it is trivial exactly when \(Q(v)\) is a square CliffordAlgebra.spinorNorm_eq_one_of_finrank_le_one CliffordAlgebra.orthogonalSpinorNorm_range_eq_zpowers_of_finrank_eq_one CliffordAlgebra.orthogonalSpinorNorm_eq_one_iff_isSquare_apply_of_finrank_eq_one. An indefinite real form has rank at least two. Degenerate or semidefinite PGA forms lie outside every row of this nondegenerate table.

Remark. Real spinor-norm images and the low-rank boundary [fcap-002F]
✍️source

From reflection generation to Pin and Spin [fcap-000U]

Lemma. Fixed-subspace correction by reflections [cartan1981theory, Section 10, pp. 10--12] [fcap-000V]

Proof.

Lemma. Pin-range refinement of the correction [cartan1981theory, Section 10, pp. 10--12]; [lawson2016spin, I.2, (2.26) and Theorem 2.9, pp. 18--19] [fcap-0018]

exists_mem_range_pinToOrthogonal_mul_eqOn_sup_span_singleton
L∃∀N

Theorem. Cartan--Dieudonne generation [lawson2016spin, I.2, Theorem 2.7, p. 17] [fcap-000W]

subgroup_eq_top_of_reflection_mem
L∃∀N

Proof.

Theorem. Surjectivity of the Pin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-000X]

pinToOrthogonal_surjective_of_isSquare pinToOrthogonal_surjective
L∃∀N

Example. A planar rotation as two reflections [lawson2016spin, I.2, (2.24)--(2.26), p. 18] [fcap-000Y]

Lemma. Determinant parity detects the even lift [lawson2016spin, I.2, Theorems 2.7 and 2.9, pp. 17--19] [fcap-001A]

det_reflection mem_even_of_det_pinToOrthogonal_eq_one
L∃∀N

Proof.

Theorem. Surjectivity of the Spin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-001B]

spinToSpecialOrthogonal_surjective_of_isSquare spinToSpecialOrthogonal_surjective
L∃∀N

Proposition. The reverse norm descends through the Lipschitz action [fcap-002D]

Theorem. The Spin image is the spinor-norm kernel [fcap-0023]

range_spinToSpecialOrthogonal_eq_ker_spinorNorm
L∃∀N

Proof.

Theorem. Spinor norms commute with extension of scalars [fcap-003N]

Proof.

Proposition. Spin lifts over a quadratic extension [fcap-003O]

Proof.

Proposition. Eichler transvections have additive Spin lifts [fcap-002M]

Example. A null-frame Spin transvection and a radical shear [fcap-002N]

Example. A mixed-sign isometry has no norm-one Spin lift [fcap-002E]

Remark. Real spinor-norm images and the low-rank boundary [fcap-002F]
✍️source

Theorem. Spin acts transitively on a positive quadratic sphere [fcap-0024]

exists_spinVectorAction_eq_of_posDef
L∃∀N

Proof.

Lemma. The real Spin kernel is the scalar pair [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40] [fcap-001C]

zmodTwoMulEquivKerSpinToSpecialOrthogonal
L∃∀N

Theorem. The algebraic Spin extension [meinrenken2013clifford, Definition 3.2, pp. 51--52] [fcap-001D]

spinDoubleCoverOfSurjective spinDoubleCover
L∃∀N

Lemma. The real Pin kernel is the scalar pair [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40] [fcap-001E]

zmodTwoMulEquivKerPinToOrthogonal
L∃∀N

Theorem. The algebraic Pin extension [meinrenken2013clifford, Definition 3.2, pp. 51--52] [fcap-001F]

pinDoubleCoverOfSurjective pinDoubleCover
L∃∀N

Proposition. Isometries transport the Spin vector action [fcap-0029]

spinGroupMap_spinVectorAction
L∃∀N

Remark. Algebraic extension versus topological cover [fcap-000Z]

Proposition. The compact real Spin projection is a two-sheeted cover [fcap-0039]

Proposition. The compact Spin cover is universal from dimension three [fcap-003A]

Theorem. The Spin image is the spinor-norm kernel [fcap-0023]

range_spinToSpecialOrthogonal_eq_ker_spinorNorm
L∃∀N

Proof.