Convention. Quadratic-form sign [lawson2016spin, I.1, (1.3)--(1.4), p. 8] [fcap-0008]
✍️source

Lawson and Michelsohn write \[v^2=-q(v)1, \qquad vw+wv=-2q(v,w),\] where \(2q(v,w)=q(v+w)-q(v)-q(w)\). Mathlib and TauCeti instead use a quadratic form \(Q\) with \[\iota (v)^2=Q(v)1.\] The conventions agree after setting \(Q=-q\). The orthogonal group and its reflections are unchanged by this global sign reversal. A vector with \(q(v)=1\) therefore has \(Q(v)=-1\) in the convention used below. Mathlib's generator-square rule CliffordAlgebra.ι_sq_scalar uses this \(Q\)-convention.

Convention. Quadratic-form sign [lawson2016spin, I.1, (1.3)--(1.4), p. 8] [fcap-0008]
✍️source

Reference. Spin geometry (pms-38) [lawson2016spin]

Reflections and square-normalized Clifford lifts [fcap-0007]

Convention. Quadratic-form sign [lawson2016spin, I.1, (1.3)--(1.4), p. 8] [fcap-0008]
✍️source

Definition. Reflection in a nonisotropic vector [lawson2016spin, I.2, (2.12), p. 14] [fcap-0009]

reflection
L∃∀N

Lemma. Twisted Clifford conjugation is a reflection [lawson2016spin, I.2, Proposition 2.2 and (2.8), p. 13; (2.11)--(2.12), p. 14] [fcap-000A]

Proof.

Lemma. Square-normalized Pin lift [lawson2016spin, I.2, Definition 2.3 and (2.26), pp. 14, 18] [fcap-000B]

reflection_mem_range_pinToOrthogonal_of_isSquare
L∃∀N

Theorem. Paired reflections have a product-square Spin lift [lawson2016spin, I.2, (2.24)--(2.26), p. 18] [fcap-000C]

reflection_mul_reflection_mem_range_spinToOrthogonal_of_isSquare
L∃∀N

Proof.

Example. A Euclidean unit normal [lawson2016spin, I.2, (2.12), p. 14; (2.24)--(2.26), p. 18] [fcap-000D]

Remark. From individual lifts to generation [lawson2016spin, I.2, Proposition 2.2, Definition 2.3, and (2.24)--(2.26), pp. 13--18] [fcap-000E]

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

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

exists_mem_subgroup_mul_eqOn_sup_span_singleton_of_reflection_mem
L∃∀N

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

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

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