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

2016
H. Blaine Lawson, Marie-Louise Michelsohn

@book{lawson2016spin,
 title = {Spin Geometry (Pms-38)},
 author = {Lawson, H. Blaine and Michelsohn, Marie-Louise},
 date = {2016},
 volume = {38},
 publisher = {{Princeton university press}}
}

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

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

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

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

subgroup_eq_top_of_reflection_mem
L∃∀N

Proof.

Comments on [weber2013lie] [uts-0005]

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.

Example. Four real Clifford base entries [lawson2016spin, I.4, Theorem 4.3 and Tables I--II, pp. 27--29] [fcap-0015]

realCliffordOneZeroEquivProd realCliffordZeroOneEquivComplex realCliffordZeroTwoEquivQuaternion realCliffordOneOneEquivMatrix
L∃∀N

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]

Remark. Horizons beyond the exterior model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60]; [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]; [lawson2016spin, I.2, pp. 13--19] [fcap-0017]

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.

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

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

Convention. Real signature and Clifford signs [chevalley1954algebraic, II.2.9, pp. 65--66] [fcap-0011]

realCliffordForm realCliffordForm_apply
L∃∀N

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

reflection
L∃∀N

Definition. Spin group [lawson2016spin] [spin-0002]

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. Surjectivity of the Pin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-000X]

pinToOrthogonal_surjective_of_isSquare pinToOrthogonal_surjective
L∃∀N

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

Theorem. The hyperbolic matrix recurrence [lawson2016spin, I.4, Theorem 4.1, (4.3), pp. 25--26] [fcap-0013]

hyperbolicEquivTensor realCliffordBottEquiv_ι
L∃∀N

Definition. The hyperbolic plane [lawson2016spin, I.4, Theorem 4.1 and (4.3), pp. 25--26] [fcap-0012]

realCliffordForm_one_one_apply realBottSplitIsometry
L∃∀N

Theorem. The signature-switch recurrence [lawson2016spin, I.4, Theorem 4.1 and (4.1), pp. 25--26] [fcap-001X]

realCliffordSignatureSwitchRecurrenceEquiv
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.

Remark. What the recurrence does not classify [fcap-0016]

Remark. Why algebraic periodicity is a separate branch [chevalley1954algebraic, II.2.1, II.2.5, and II.2.9, pp. 42--46, 65--66]; [lawson2016spin, I.4, Theorems 4.1 and 4.3, pp. 25--29] [fcap-001Y]