Idempotent Elements in Finite Semigroups

This file defines properties related to idempotent elements in finite semigroups and monoids.

Main theorems

Let S be a finite semigroup and x : S

• Semigroup.exists_idempotent_pow - ∃ (m : ℕ+), IsIdempotentElem (x ^ m)
• Monoid.exists_idempotent_pow - ∃ (n : ℕ), IsIdempotentElem (x ^ n) ∧ n ≠ 0 in finite monoids.
• Monoid.exists_pow_sandwich_eq_self - If a = x * a * y, then ∃ n₁ n₂ : ℕ, n₁ ≠ 0 ∧ n₂ ≠ 0 ∧ x ^ n₁ * a = a ∧ a * y ^ n₂ = a.

Implementation notes

Monoid.exists_idempotent_pow is useful when reasoning about elements in monoids, when the theorem is needed in terms of ℕ powers greater than 0 rather than ℕ+ powers.

Blueprint

• One blueprint entry for Semigroup.exists_idempotent_pow and Semigroup.pow_idempotent_unique. Label : exists-unique-idempotent-pow Tagged Lean lemmas :

• Semigroup.exists_repeating_pow
• Semigroup.pow_idempotent_unique
• Semigroup.exists_idempotent_pow Dependencies: None

• One entry for Monoid.exists_pow_sandwich_eq_self. Label : exists-pow-sandwhich Tagged Lean lemmas :

• Monoid.exists_pow_sandwich_eq_self Dependencies: exists-unique-idempotent-pow

theorem Semigroup.pow_succ_eq {S : Type u_1} [Semigroup S] {x : S} (n : ℕ+) (h_idem : IsIdempotentElem x) : x ^ n = x

Idempotent elements are stable under positive powers.

theorem Semigroup.exists_repeating_pow {S : Type u_1} [Semigroup S] [Finite S] (x : S) : ∃ (m : ℕ+) (n : ℕ+), x ^ m * x ^ n = x ^ m

In a finite semigroup, powers of any element eventually repeat.

theorem Semigroup.pow_idempotent_unique {S : Type u_1} [Semigroup S] {x : S} {m n : ℕ+} (hm : IsIdempotentElem (x ^ m)) (hn : IsIdempotentElem (x ^ n)) : x ^ m = x ^ n

If two powers of an element are both idempotent, then they are equal.

theorem Semigroup.exists_idempotent_pow {S : Type u_1} [Semigroup S] [Finite S] (x : S) : ∃ (m : ℕ+), IsIdempotentElem (x ^ m)

In a finite semigroup, every element has an idempotent power.

theorem Monoid.pow_succ_eq {M : Type u_1} [Monoid M] {x : M} {n : ℕ} (h_idem : IsIdempotentElem x) : x ^ (n + 1) = x

Idempotent elements are stable under positive powers in monoids.

theorem Monoid.exists_idempotent_pow {M : Type u_1} [Monoid M] [Finite M] (x : M) : ∃ (n : ℕ), IsIdempotentElem (x ^ n) ∧ n ≠ 0

Every element in a finite monoid has a nonzero idempotent power.

theorem Monoid.exists_pow_sandwich_eq_self {M : Type u_1} [Monoid M] [Finite M] {x a y : M} (h : a = x * a * y) : ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ ≠ 0 ∧ n₂ ≠ 0 ∧ x ^ n₁ * a = a ∧ a * y ^ n₂ = a

In finite monoids, elements satisfying a sandwich property have powers that left-cancel and right-cancel the sandwich factors.