The order of the Fano collineation group #
The collineation group TotD.fanoGroup of the Fano plane (the stabilizer of its seven lines in
Equiv.Perm (Fin 7)) has order 168. The map g ↦ (g 0, g 1, g 3) is a bijection onto the triples
of non-collinear points. It is injective because a collineation fixing three non-collinear points
fixes every point (each remaining point is the third point of a line through two fixed ones). It is
surjective because, reading the points as the nonzero vectors of F₂³, the linear map sending
e₁, e₂, e₃ to a given triple maps lines to lines; this is checked by decide over the 168
triples, never over all of Equiv.Perm (Fin 7).
Main results #
TotD.fanoGroup_card: Nat.card fanoGroup = 168
References #
- C. Marín, When Separation Fails, a Canon Appears: One counting identity behind separation,
synchronization, and symmetry-breaking in permutation groups, formalized in Lean 4 (Part I),
Zenodo (2026), doi:10.5281/zenodo.21419285,
fano-order.
The collineation group of the Fano plane has order 168: g ↦ (g 0, g 1, g 3) is a bijection
onto the triples of non-collinear points (7 · 6 · 4).