Idempotent powers in finite monoids (omegaPow) #
In any finite monoid M, the powers x, x², x³, … of an element x
must eventually repeat: pigeonhole on the infinite indexing of a finite
set forces some x^i = x^j with i < j. From this it follows that
some positive power x^N is idempotent (x^N * x^N = x^N). The
canonical such power is the omega power x^ω, the unique idempotent
in the cyclic subsemigroup ⟨x⟩.
This file lands the basic substrate:
Monoid.exists_pow_eq_pow_of_finite— pigeonhole.Monoid.exists_pos_pow_isIdempotent— idempotent power exists.Monoid.omegaPow x— the noncomputable choice of one such power.- Basic lemmas:
omegaPow_isIdempotent,omegaPow_pow,omegaPow_mul_omegaPow.
omegaPow is the substrate for the algebraic characterization of
subregular language classes (@cite{pin-mfa}; @cite{eilenberg-1976};
@cite{lambert-2026} §6.2): definite languages are exactly those whose
syntactic monoid satisfies s · x^ω = x^ω, reverse-definite by
x^ω · y = x^ω, and so on. Until this file is in place, the algebraic
characterizations are stuck at finite-k forms that don't generalize
cleanly across the hierarchy.
Mathlib promotion #
This file is structured to be promotable to mathlib as a sibling of
Mathlib.Algebra.Group.Idempotent. The construction depends only on
Monoid M, Finite M, and IsIdempotentElem — no automata-theory
content. The choice of noncomputable def over a decidability-aware
Fintype-based search is the simplest one for the algebraic theorems;
a computable variant would be a natural follow-up.
Implementation note #
The omegaPow definition uses Classical.choose against
exists_pos_pow_isIdempotent, so it is noncomputable. For the
algebraic theorems this is fine — omegaPow x is determined up to
equality, not up to computation.
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.
Existence of an idempotent power: in a finite monoid M,
every element x : M has a positive power x^N that is idempotent
(x^N * x^N = x^N).
Construction: pigeonhole gives i < j with x^i = x^j. Set the
period p = j - i > 0 and pick N = j · p. Then N is positive, is
a multiple of p, and satisfies N ≥ j > i — so the periodicity
lemma pow_period (x^N = x^(N + m·p) for any m) instantiated at
m = j gives x^N = x^(N + j·p) = x^(2N).
The omega power x^ω of an element x in a finite monoid:
the choice of one positive power of x that is idempotent. Such a
power exists by exists_pos_pow_isIdempotent. The choice is via
Classical.choose, hence noncomputable; the algebraic content of
omegaPow x (its idempotence and stability under further powers) is
captured by the lemmas below.
Equations
- Monoid.omegaPow x = x ^ ⋯.choose
Instances For
The exponent witnessing omegaPow x (a positive natural number
such that x raised to it is idempotent).
Equations
- Monoid.omegaPowExponent x = ⋯.choose
Instances For
The omega power of x is idempotent.
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).