Idempotent powers in finite monoids and semigroups

In a finite monoid the powers x, x², x³, … must repeat, so some positive power x^N is idempotent; any two idempotent positive powers of x coincide, so the omega power Monoid.omegaPow x — the unique idempotent in the cyclic subsemigroup ⟨x⟩ — is well defined. The semigroup case follows by adjoining an identity (WithOne).

omegaPow is the substrate for the algebraic characterization of subregular language classes ([Pin]; [Eil76]; [Lam26] §6.2): definite languages are exactly those whose syntactic monoid satisfies s · x^ω = x^ω, reverse-definite ones x^ω · s = x^ω, and so on (Core/Computability/Variety/).

Main results

• Monoid.exists_pos_pow_isIdempotent — existence, by pigeonhole.
• IsIdempotentElem.pow_eq_pow — uniqueness: idempotent positive powers of the same element coincide (no finiteness needed).
• Monoid.omegaPow — the omega power x^ω, canonical by Monoid.omegaPow_unique; IsIdempotentElem.omegaPow_eq, Monoid.omegaPow_pow.
• Semigroup.exists_isIdempotentElem, Semigroup.exists_isIdempotentElem_map_eq — the semigroup transfers consumed by Semigroup/Pseudovariety.lean.

omegaPow is defined by Classical.choose, hence noncomputable; omegaPow_unique makes it independent of the choice.

[UPSTREAM] candidate (Mathlib.Algebra.Group.Idempotent sibling).

Periodicity of powers

theorem IsIdempotentElem.pow_eq_pow {M : Type u_1} [Monoid M] {x : M} {a b : ℕ} (hxa : IsIdempotentElem (x ^ a)) (hxb : IsIdempotentElem (x ^ b)) (ha : a ≠ 0) (hb : b ≠ 0) : x ^ a = x ^ b

Idempotent positive powers of the same element coincide — no finiteness needed: x^a = (x^a)^b = (x^b)^a = x^b. This is what makes the omega power canonical.

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

Pigeonhole on monoid powers: in a finite monoid, the sequence of powers x^1, x^2, x^3, … must repeat — there exist indices i < j with x^i = x^j.

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

Existence of an idempotent power: in a finite monoid M, every element x : M has a positive power x^N that is idempotent. Pigeonhole gives x^i = x^j with i < j; N = j·(j - i) is a positive multiple of the period at least i, so x^N = x^(2N) by pow_period.

The omega power

noncomputable def Monoid.omegaPow {M : Type u_1} [Monoid M] [Finite M] (x : M) : M

The omega power x^ω of an element x in a finite monoid: the idempotent positive power of x (unique by omegaPow_unique), realized via Classical.choose against exists_pos_pow_isIdempotent.

Equations

• Monoid.omegaPow x = x ^ ⋯.choose

noncomputable def Monoid.omegaPowExponent {M : Type u_1} [Monoid M] [Finite M] (x : M) : ℕ

The exponent witnessing omegaPow x (a positive natural number such that x raised to it is idempotent).

Equations

• Monoid.omegaPowExponent x = ⋯.choose

theorem Monoid.omegaPow_eq_pow {M : Type u_1} [Monoid M] [Finite M] (x : M) : omegaPow x = x ^ omegaPowExponent x

theorem Monoid.omegaPowExponent_pos {M : Type u_1} [Monoid M] [Finite M] (x : M) : 0 < omegaPowExponent x

theorem Monoid.omegaPow_isIdempotent {M : Type u_1} [Monoid M] [Finite M] (x : M) : IsIdempotentElem (omegaPow x)

The omega power of x is idempotent.

theorem Monoid.omegaPow_unique {M : Type u_1} [Monoid M] [Finite M] {x : M} {n : ℕ} (hn : n ≠ 0) (hxn : IsIdempotentElem (x ^ n)) : x ^ n = omegaPow x

Any idempotent positive power of x equals omegaPow x: the omega power is canonical, independent of the chosen exponent.

theorem IsIdempotentElem.omegaPow_eq {M : Type u_1} [Monoid M] [Finite M] {x : M} (hx : IsIdempotentElem x) : Monoid.omegaPow x = x

An idempotent element is its own omega power.

@[simp]

theorem Monoid.omegaPow_omegaPow {M : Type u_1} [Monoid M] [Finite M] (x : M) : omegaPow (omegaPow x) = omegaPow x

The omega power is a projection.

theorem Monoid.omegaPow_pow {M : Type u_1} [Monoid M] [Finite M] (x : M) {n : ℕ} (hn : n ≠ 0) : omegaPow x ^ n = omegaPow x

The omega power of x is stable under any positive power: raising omegaPow x to any n ≥ 1 gives omegaPow x back. Direct consequence of idempotence (IsIdempotentElem.pow_eq from mathlib).

@[simp]

theorem Monoid.omegaPow_mul_omegaPow {M : Type u_1} [Monoid M] [Finite M] (x : M) : omegaPow x * omegaPow x = omegaPow x

Multiplying omegaPow x by itself yields omegaPow x — restatement of idempotence in product form.

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