[6, 13747] A₂¹ no finite basis
[6, 13747] is the monoid A₂¹, obtained from A₂ by adjoining an identity, one of the four semigroups of order six without a finite identity basis.
Cayley table
| · | 1 | 2 | 3 | 4 | 5 | 6 |
|---|---|---|---|---|---|---|
| 1 | 1 | 1 | 1 | 1 | 1 | 1 |
| 2 | 1 | 1 | 1 | 2 | 2 | 3 |
| 3 | 1 | 2 | 3 | 2 | 3 | 3 |
| 4 | 1 | 1 | 1 | 4 | 4 | 6 |
| 5 | 1 | 2 | 3 | 4 | 5 | 6 |
| 6 | 1 | 4 | 6 | 4 | 6 | 6 |
The product of the row element and the column element, numbered as in Smallsemi. Blue: idempotents on the diagonal; grey: the zero.
Structure
- Smallsemi
- SmallSemigroup(6, 13747)
- Idempotents
- 1, 3, 4, 5, 6
- Zero
- 1
- Identity
- 5
- Nilpotent
- no
- Commutative
- no
- Regular
- yes
- Group
- no
- 𝒥-classes
- 3
- Rank
- 3, generated by {2, 5, 6}
- Self-dual
- yes: anti-isomorphic to itself
No finite identity basis
For every n, the identity
X y X′ y X ≈ X y X′ y X y X′ y X, with X = x₁⋯xₙ and X′ its reverse
holds in A₂¹. No derivation step with an identity in fewer variables changes the left side at all. A finite set of identities uses boundedly many variables, so it misses one of these identities and is not a basis.
Argument: A. N. Trahtman (1987); M. V. Sapir (1988). That L, B₂¹, A₂ᵍ and A₂¹ are the only semigroups of order six without a finite basis was shown by Lee, Li and Zhang (2012). See the four nonfinitely based semigroups.
Lean proof
Endpoint theorem: SemigroupBasis.Examples.A2One.s6_13747_nonfinitelyBased
theorem s6_13747_nonfinitelyBased : NonfinitelyBased catalogueTable.semigroup
- Size
- Checking this class alone compiles 14 Lean files with 11,338 lines: the endpoint theorem and everything it imports, the shared library included. Of these, 10,502 lines are used by the proof of this class and of no other.
- Census
- SemiBase.Census.S6_13747 checks that the theorem is about the table of this class and concludes Classified; SemiBase.Catalogue.Order6.S6_13747 is the table, with the elements numbered 0 to 5.
Varieties
[6, 13747] generates a variety without a finite basis, so not one of the 505 varieties of this census. It lies in none of them: no finitely based semigroup of order six generates a variety that contains it, as evaluating their bases in this table shows.