Idempotent powers in a finite semigroup

Every element of a finite semigroup has an idempotent positive power. This is the basic structural fact behind the equational description of semigroup pseudovarieties: it is what makes a homomorphic image of a member a member, since a preimage of an idempotent need not itself be idempotent, but an idempotent power of a preimage is one and has the same image.

The monoid case is Monoid.exists_pos_pow_isIdempotent. The semigroup case is obtained from it by adjoining an identity: WithOne S is a finite monoid, positive powers of a coerced element are themselves coerced, and WithOne.coe_inj transfers idempotency back.

Main results

• Semigroup.exists_isIdempotentElem: a finite nonempty semigroup contains an idempotent.
• Semigroup.exists_isIdempotentElem_map_eq: a surjective homomorphism onto a semigroup lifts an idempotent to an idempotent — the form the pseudovariety quotient-closure proof consumes.

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 lifts an idempotent to an idempotent: replace a preimage by an idempotent power of it, which the homomorphism still sends to the (idempotent) target.