Definition. Reflection in a nonisotropic vector [lawson2016spin, I.2, (2.12), p. 14] [fcap-0009]
✍️source
reflection
L∃∀N

Let \(F\) be a field of characteristic different from \(2\), let \(Q\) be a quadratic form on an \(F\)-vector space \(V\), and write \[B_Q(x,y)=Q(x+y)-Q(x)-Q(y)\] for its polar form. If \(Q(v)\ne 0\), the reflection with normal vector \(v\) is \[\rho _v(w)=w-\frac {B_Q(v,w)}{Q(v)}v.\] It fixes \(v^\perp \) pointwise, sends \(v\) to \(-v\), and preserves \(Q\). Multiplying \(v\) by a nonzero scalar does not change \(\rho _v\).

Definition. Reflection in a nonisotropic vector [lawson2016spin, I.2, (2.12), p. 14] [fcap-0009]
✍️source
reflection
L∃∀N

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

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.