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]
✍️source

Lawson and Michelsohn supply the twisted-adjoint reflection formula, the definitions of Pin and Spin, the description by products of normalized vectors, and the square-root obstruction to normalization. The square-witness statements in Lemma [fcap-000B] and Theorem [fcap-000C] isolate the precise algebraic hypotheses under which one or two reflections lift.

An individual lift does not by itself show that all orthogonal transformations lift. That global conclusion requires finite dimension, nondegeneracy, and the Cartan--Dieudonne factorization developed next.

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]
✍️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]

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]
✍️source

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]

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