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

The exterior action constructed above stops before several classical consequences in representation theory. Over a split field, irreducibility and the decomposition into two half-spin modules require further hypotheses and arguments; Meinrenken proves these results after establishing that the Clifford action is an isomorphism. The currently open TauCeti half-spin work is therefore not represented by a Lean marker here.

The generic mathematics of differentiating a smooth Lie-group homomorphism is developed in § [fcap-001Q]. What remains missing for the Spin cover is more specific: compatible Lie-group structures on TauCeti's abstract \(\operatorname {Spin}(V)\) and \(SO(V)\), followed by the identification of their specialized differential with the algebraic quadratic action above. The open TauCeti PR linked in Remark [fcap-001W] proposes only the generic Lie functor.

Highest weights, triality, and the Bott-periodic real table also belong to later layers. Kostant supplies the differential in the classical complex setting, and Lawson--Michelsohn treat the real Pin and Spin groups. None of these horizons follows merely from the algebraic restrictions \(\operatorname {spinRep}\) and \(\operatorname {pinRep}\).

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

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

Reference. Clifford algebras and lie theory [meinrenken2013clifford]

Reference. Clifford algebra analogue of the Hopf--Koszul--Samelson theorem [kostant1997clifford]

Polarization and the exterior spinor model [fcap-001G]

Definition. Polarization data and its carrier [chevalley1954algebraic, II.2.1--II.2.2, pp. 42--44] [fcap-001H]

SpinPolarizationData
L∃∀N

Definition. Creation, contraction, and the line operator [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57] [fcap-001I]

wedge contract lineOperator
L∃∀N

Lemma. The polarized Clifford relation [meinrenken2013clifford, Section 3.2.1, pp. 54--55] [fcap-001J]

contract_wedge cliffordOperator_sq
L∃∀N

Theorem. The exterior Clifford action [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57] [fcap-001K]

spinAction
L∃∀N

Theorem. Creation and contraction generate all endomorphisms [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60] [fcap-001L]

creation_contraction_adjoin_eq_top spinAction_surjective
L∃∀N

Definition. The Spin and Pin representations [meinrenken2013clifford, Section 3.2.1, pp. 55--56] [fcap-001M]

spinRep pinRep
L∃∀N

Lemma. The restricted actions are the Clifford action [meinrenken2013clifford, Section 3.2.1, pp. 55--56] [fcap-001N]

spinRep_apply pinRep_apply
L∃∀N

Example. The rank-one polarized model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, p. 59] [fcap-001P]

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

Differentiating smooth group homomorphisms [fcap-001Q]

Definition. The differential of a smooth homomorphism [liu2016lie, Section 2.1, p. 9] [fcap-001R]

Lemma. The differential preserves the Lie bracket [liu2016lie, Section 2.1, p. 9] [fcap-001S]

Theorem. The Lie functor [liu2016lie, Section 2.2, p. 10] [fcap-001T]

Theorem. Naturality of the exponential [liu2016lie, Section 2.4, pp. 12--13] [fcap-001U]

Proof.

Example. Differentiating a matrix representation [liu2016lie, Sections 2.1 and 2.4, pp. 9, 12] [fcap-001V]

Remark. Why explicit smoothness changes the roadmap [liu2016lie, Sections 2.1--2.4 and 2.8, pp. 9--13, 19--20]; [isaev2018theory, Section 3.1.2, pp. 106--107] [fcap-001W]

Remark. Why explicit smoothness changes the roadmap [liu2016lie, Sections 2.1--2.4 and 2.8, pp. 9--13, 19--20]; [isaev2018theory, Section 3.1.2, pp. 106--107] [fcap-001W]