Identity bases of the semigroups of order six
A census of the 15,973 semigroups of order six, counted up to isomorphism and anti-isomorphism. All of them except four have a finite identity basis, and every case is proved in Lean: an explicit basis for each of the 15,969 finitely based semigroups, for most of which only the existence of a finite basis was known before, and a proof for the other four that no finite basis exists.
Explore
- Browse all 15,973 semigroups and filter them by structure, basis and proof.
- Varieties: the 505 varieties the semigroups generate, as a list or as an interactive graph of their inclusions.
- No finite basis: L, B₂¹, A₂ᵍ and A₂¹, and why no finite set of identities suffices.
- A random semigroup.
Worth a look
- [6, 3842] C₈, the semigroup C₈ of Lee and Zhang: finitely based, two table entries away from the nonfinitely based L.
- [6, 12824]: the largest proof, 333,599 lines of Lean that the proof of no other class uses.
- [6, 2582]: the longest certified basis, 3,513 identities, which reduce to 3.
- V[2771]: the variety whose shortest known basis is longest, with 31 identities.
- V[239]: the variety with the most generators, 2,335 semigroups of order six.
How short are the bases?
The finitely based semigroups by the number of identities in their shortest known basis.
On each page
For each semigroup: the Cayley table and its structure; the shortest known basis and the basis certified in Lean; the Lean theorem, linked to its line, and the size of its proof; the variety it generates, with the varieties directly above and below and the other semigroups that generate it; and the tables that differ from it in one or two entries. About says what is proved in Lean and what is not.