Groups: LMFDB finite-group label (small-group identification)

[CBirkbeck]

Goal

Provide the LMFDB group label N.i — order N and the GAP small-group id i — i.e. a canonical identification of a finite group up to isomorphism.

What already exists

• mathlib: finite group theory, Fintype.card, isomorphism (MulEquiv), and named small groups (DihedralGroup, QuaternionGroup, CyclicGroup/ZMod, Equiv.Perm/alternatingGroup). There is no small-groups catalogue / canonical labelling.

What's missing

• A decidable up-to-isomorphism identifier for small finite groups matching the GAP/LMFDB N.i numbering (at least for small N), or a mapping from mathlib's named families to their labels.

Test cases

• C_2 = 2.1, C_2² = 4.2, S_3 = 6.1, Q_8 = 8.4, D_4 = 8.3.

LMFDB targets

• group.label
• group.order
• group.isomorphism

New area, not yet in the Verso blueprint — links go to the LMFDB knowls.