Definition. the distinguished involution of abstract 2T [fgap-0014]
✍️source

    Let \(T\leq \mathbb {H}^{\times }\) be the binary tetrahedral group of Hurwitz units from the binary tetrahedral subgroup of the quaternions, and let \(B\) be the abstract semidirect-product model obtained from the same Hurwitz action. Choose the group isomorphism \[ \rho :B\mathbin {\cong }T \] that compares these two models. Voight identifies \(T\) with the Hurwitz unit group and with \(Q_8\rtimes \mathbb {Z}/3\mathbb {Z}\) in [voight2021quaternion, sec. 11.2.4, p. 168].

    The quaternion \(-1\) belongs to \(T\); it is central, its square is 1, and it is not 1. Define the distinguished central involution of \(B\) by \[ z=\rho ^{-1}(-1). \] Since an isomorphism preserves multiplication and reflects equality, \[ z\in Z(B),\qquad z^2=1,\qquad z\neq 1. \] Thus the abstract group retains the central involution supplied by its quaternionic realization. The element \(z\) is not identified with the quaternion \(-1\); the isomorphism \(\rho \) relates them.

    The same isomorphism transports cardinality. Since the calculation in the twenty-four Hurwitz units gives \(|T|=24\), \[ |B|=|T|=24. \] The corresponding Lean theorem uses Mathlib's Nat.card; its statement is Nat.card BinaryTetrahedral.Abstract = 24.

    The occurrence of \(-1\) among the 24 Hurwitz units is explicit in [voight2021quaternion, sec. 11.2, p. 166].