Aperiodic monoids

A monoid is aperiodic when a single power stabilizes every element, x ^ (n + 1) = x ^ n. Schützenberger introduced these monoids as the ones with only trivial subgroups, and they are the algebraic counterpart of the star-free languages.

Main definitions

• Monoid.IsAperiodic: some power stabilizes every element.

Main results

• Monoid.isAperiodic_iff_forall_exists: a finite monoid is aperiodic when the powers of each element stabilize.
• Monoid.IsAperiodic.pow_mul_eq_of_isIdempotentElem: an idempotent power of x absorbs x.
• Monoid.IsAperiodic.of_injective, Monoid.IsAperiodic.of_surjective, Monoid.IsAperiodic.prod: closure under submonoids, quotients and products.

References

• [Sch65]
• [McNP71]
• [Pin]

def Monoid.IsAperiodic (M : Type u_1) [Monoid M] : Prop

A monoid is aperiodic when some power stabilizes every element.

Equations

• Monoid.IsAperiodic M = ∃ (n : ℕ), ∀ (x : M), x ^ (n + 1) = x ^ n

def AddMonoid.IsAperiodic (M : Type u_1) [AddMonoid M] : Prop

Equations

• AddMonoid.IsAperiodic M = ∃ (n : ℕ), ∀ (x : M), (n + 1) • x = n • x

theorem Monoid.IsAperiodic.of_subsingleton {M : Type u_1} [Monoid M] [Subsingleton M] : IsAperiodic M

A subsingleton monoid is aperiodic (take n = 0).

theorem AddMonoid.IsAperiodic.of_subsingleton {M : Type u_1} [AddMonoid M] [Subsingleton M] : IsAperiodic M

theorem Monoid.pow_succ_stabilizes {M : Type u_1} [Monoid M] {x : M} {n : ℕ} (h : x ^ (n + 1) = x ^ n) (m : ℕ) : n ≤ m → x ^ (m + 1) = x ^ m

If x ^ (n + 1) = x ^ n then the power stabilizes at every m ≥ n.

theorem AddMonoid.nsmul_succ_stabilizes {M : Type u_1} [AddMonoid M] {x : M} {n : ℕ} (h : (n + 1) • x = n • x) (m : ℕ) : n ≤ m → (m + 1) • x = m • x

theorem Monoid.isAperiodic_iff_forall_exists {M : Type u_1} [Monoid M] [Finite M] : IsAperiodic M ↔ ∀ (x : M), ∃ (n : ℕ), x ^ (n + 1) = x ^ n

A finite monoid is aperiodic exactly when the powers of each element stabilize.

theorem AddMonoid.isAperiodic_iff_forall_exists {M : Type u_1} [AddMonoid M] [Finite M] : IsAperiodic M ↔ ∀ (x : M), ∃ (n : ℕ), (n + 1) • x = n • x

theorem Monoid.IsAperiodic.pow_mul_eq_of_isIdempotentElem {M : Type u_1} [Monoid M] (h : IsAperiodic M) {x : M} {n : ℕ} (hn : n ≠ 0) (he : IsIdempotentElem (x ^ n)) : x ^ n * x = x ^ n

In an aperiodic monoid, an idempotent positive power of x absorbs x.

theorem Monoid.IsAperiodic.of_surjective {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {f : M →* N} (hf : Function.Surjective ⇑f) (hM : IsAperiodic M) : IsAperiodic N

Aperiodicity passes along a surjective monoid hom, with the same exponent.

theorem AddMonoid.IsAperiodic.of_surjective {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] {f : M →+ N} (hf : Function.Surjective ⇑f) (hM : IsAperiodic M) : IsAperiodic N

theorem Monoid.IsAperiodic.of_injective {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {f : M →* N} (hf : Function.Injective ⇑f) (hN : IsAperiodic N) : IsAperiodic M

Aperiodicity pulls back along an injective monoid hom, with the same exponent.

theorem AddMonoid.IsAperiodic.of_injective {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] {f : M →+ N} (hf : Function.Injective ⇑f) (hN : IsAperiodic N) : IsAperiodic M

theorem Monoid.IsAperiodic.prod {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (hM : IsAperiodic M) (hN : IsAperiodic N) : IsAperiodic (M × N)

A binary product of aperiodic monoids is aperiodic (take the larger exponent).

theorem AddMonoid.IsAperiodic.sum {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] (hM : IsAperiodic M) (hN : IsAperiodic N) : IsAperiodic (M × N)

theorem Monoid.IsAperiodic.of_mulEquiv {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (e : M ≃* N) (hM : IsAperiodic M) : IsAperiodic N

Aperiodicity transports across a monoid isomorphism.

theorem AddMonoid.IsAperiodic.of_addEquiv {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] (e : M ≃+ N) (hM : IsAperiodic M) : IsAperiodic N