Remark. concrete and abstract factor models [fgap-000D]
Remark. concrete and abstract factor models [fgap-000D]
The subgroups \(Q,C\leq \mathbb {H}^{\times }\) are concrete: their elements are quaternions, and the Hurwitz action is quaternion conjugation. The abstract groups \[ Q_8,\qquad \mathbb {Z}/3\mathbb {Z} \] remember the same group structures without remembering their quaternion coordinates.
Matching names and cardinalities does not identify these models. We need explicit isomorphisms \[ Q_8\mathbin {\cong }Q,\qquad \mathbb {Z}/3\mathbb {Z}\mathbin {\cong }C. \] The action must then be transported through these isomorphisms and proved equivariant. This keeps later abstract calculations connected to the quaternion realization that supplied them.
In Lean, QuaternionGroup at parameter \(2\) models the abstract
quaternion factor, and Multiplicative applied to ZMod at
modulus \(3\) models the abstract cyclic factor. The
concrete subgroups remain the main computational model. Explicit isomorphisms
recover the abstract interface from that model, and equivariance connects the
transported action to quaternion conjugation. Formalization therefore keeps
these bridges as results rather than treating them as definitions.