Idempotents in finite semigroups

This file proves the basic facts about idempotents in finite monoids and semigroups. In a finite monoid the powers of an element must repeat, so some positive power of every element is idempotent; adjoining an identity transfers this to semigroups, and in particular every nonempty finite semigroup contains an idempotent.

The main result is the factorization of long products: if S is a finite semigroup with n elements, every product s₁ ⋯ sₙ has a prefix s₁ ⋯ sᵢ fixed on the right by an idempotent e, and so lies in S e S.

Main results

• Monoid.exists_pos_pow_isIdempotent: every element of a finite monoid has an idempotent positive power.
• Semigroup.exists_isIdempotentElem: a nonempty finite semigroup contains an idempotent.
• Semigroup.exists_isIdempotentElem_map_eq: a surjective homomorphism of finite semigroups lifts idempotents to idempotents.
• Semigroup.exists_lt_card_isIdempotentElem_mul_eq: among the first |S| terms of a sequence in which each term is a right multiple of the previous one, some term is fixed on the right by an idempotent.
• FreeSemigroup.exists_isIdempotentElem_map_eq_mul_mul: a homomorphism out of the free semigroup sends every word of length at least |S| into S e S for an idempotent e.

Implementation notes

The last two results are Proposition II.6.34 and Corollary II.6.35 of Pin's lecture notes. Products of sequences are expressed through a homomorphism out of FreeSemigroup α, which covers products of arbitrary elements by taking α = S and FreeSemigroup.lift id.

References

• [Pin]
• [Eil76]

Periodicity of powers

Existence of an idempotent power

theorem Monoid.exists_pow_eq_pow_of_finite {M : Type u_1} [Monoid M] [Finite M] (x : M) : ∃ (i : ℕ) (j : ℕ), i < j ∧ x ^ i = x ^ j

In a finite monoid the powers of an element repeat, so x ^ i = x ^ j for some i < j.

theorem Monoid.exists_pos_pow_isIdempotent {M : Type u_1} [Monoid M] [Finite M] (x : M) : ∃ n > 0, IsIdempotentElem (x ^ n)

In a finite monoid every element has an idempotent positive power.

Semigroups: transfer through WithOne

WithOne S is a finite monoid when S is a finite semigroup, positive powers of a coerced element are themselves coerced, and WithOne.coe_inj transfers idempotency back. The payoff is the structural fact behind the equational description of semigroup pseudovarieties: a preimage of an idempotent need not be idempotent, but an idempotent power of a preimage is one and has the same image.

instance WithOne.instFinite {S : Type u_1} [Finite S] : Finite (WithOne S)

WithOne S is Option S, so it inherits finiteness.

@[simp]

theorem WithOne.isIdempotentElem_coe {S : Type u_1} [Semigroup S] {e : S} : IsIdempotentElem ↑e ↔ IsIdempotentElem e

Idempotency is detected by the coercion into WithOne.

theorem WithOne.exists_coe_pow {S : Type u_1} [Semigroup S] (x : S) (n : ℕ) : 0 < n → ∃ (y : S), ↑x ^ n = ↑y

A positive power of a coerced element of WithOne S is itself coerced.

theorem Semigroup.exists_isIdempotentElem {S : Type u_1} [Semigroup S] [Finite S] [Nonempty S] : ∃ (e : S), IsIdempotentElem e

A finite nonempty semigroup contains an idempotent.

theorem Semigroup.exists_isIdempotentElem_map_eq {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] [Finite S] {f : S →ₙ* T} (hf : Function.Surjective ⇑f) {e' : T} (he' : IsIdempotentElem e') : ∃ (e : S), IsIdempotentElem e ∧ f e = e'

A surjective homomorphism of finite semigroups lifts every idempotent to an idempotent, since an idempotent power of a preimage is still sent to it.

Long products

theorem Semigroup.exists_isIdempotentElem_mul_eq {S : Type u_1} [Semigroup S] [Finite S] {p u : S} (h : p * u = p) : ∃ (e : S), IsIdempotentElem e ∧ p * e = p

An element fixed on the right by u is fixed on the right by an idempotent power of u.

theorem Semigroup.exists_lt_card_isIdempotentElem_mul_eq {S : Type u_1} [Semigroup S] [Finite S] [Nonempty S] {p : ℕ → S} (hp : ∀ (k : ℕ), k + 1 < Nat.card S → ∃ (s : S), p (k + 1) = p k * s) : ∃ i < Nat.card S, ∃ (e : S), IsIdempotentElem e ∧ p i * e = p i

Let p be a sequence in a finite nonempty semigroup S in which each of the first |S| terms is a right multiple of the previous one. Then one of these terms is fixed on the right by an idempotent.

theorem FreeSemigroup.exists_le_length_map_eq {α : Type u_1} {S : Type u_2} [Semigroup S] (f : FreeSemigroup α →ₙ* S) {u : FreeSemigroup α} (hu : IsIdempotentElem (f u)) (n : ℕ) : ∃ (v : FreeSemigroup α), n ≤ v.length ∧ f v = f u

An idempotent value of f is attained on words of every length.

theorem FreeSemigroup.exists_isIdempotentElem_map_eq_mul_mul {α : Type u_1} {S : Type u_2} [Semigroup S] (f : FreeSemigroup α →ₙ* S) [Finite S] {w : FreeSemigroup α} (hw : Nat.card S ≤ w.length) : ∃ (x : S) (e : S) (y : S), IsIdempotentElem e ∧ f w = x * e * y

A word of length at least |S| is sent into S e S for an idempotent e.