Aperiodic monoids

A monoid is aperiodic (group-free) when some power stabilises every element: ∃ n, ∀ x, x ^ (n + 1) = x ^ n. [Sch65] introduced these as the monoids with only trivial subgroups (his condition γ fⁿ = γ fⁿ⁺¹); they are the algebraic side of the star-free / counter-free / FO[<]-definable languages ([Pin], [McNP71]).

[UPSTREAM]: mathlib has Monoid.IsTorsion but no aperiodicity notion; this is a candidate for Mathlib/Algebra/Group/.

Main results

• Monoid.IsAperiodic.of_subsingleton — subsingleton monoids are aperiodic.
• Monoid.pow_succ_stabilizes — once a stabilising power is reached, all higher powers stabilise too.
• Monoid.IsAperiodic.of_surjective — aperiodicity passes along surjective homs.
• Monoid.IsAperiodic.of_injective — aperiodicity is inherited by submonoids.
• Monoid.IsAperiodic.prod — a product of aperiodic monoids is aperiodic.
• Monoid.IsAperiodic.of_mulEquiv — aperiodicity transports across isomorphisms.

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

A monoid is aperiodic when some uniform power stabilises every element: ∃ n, ∀ x, x ^ (n + 1) = x ^ n. Introduced by [Sch65] as the monoids with only trivial subgroups.

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 stabilises 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.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: the same exponent works for the image.

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 is inherited by submonoids: if f : M →* N is injective and N is aperiodic then so is M (the same exponent works, pulled back through f).

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