Green's relations

• Green.L, Green.R — Green's left and right relations on a monoid (a L b ↔ ∃ s t, s * a = b ∧ t * b = a, and dually for R);
• Green.H — their intersection;
• Green.IsAperiodicElem a — the H-class of a is trivial. A finite monoid is aperiodic (has only trivial subgroups) iff all of its elements satisfy this.

References

• [J.A. Green, On the structure of semigroups, Ann. Math. 1951]
• [J.-E. Pin, Mathematical Foundations of Automata Theory, 2022]

Green's L-relation

def LeanPool.KrohnRhodes.Green.L {M : Type u_1} [Monoid M] (a b : M) : Prop

Green's L-relation: a and b generate the same principal left ideal. In a monoid, a L b iff there exist s, t with s * a = b and t * b = a.

Equations

• LeanPool.KrohnRhodes.Green.L a b = ∃ (s : M), ∃ (t : M), s * a = b ∧ t * b = a

Green's R-relation

def LeanPool.KrohnRhodes.Green.R {M : Type u_1} [Monoid M] (a b : M) : Prop

Green's R-relation: a and b generate the same principal right ideal. In a monoid, a R b iff there exist s, t with a * s = b and b * t = a.

Equations

• LeanPool.KrohnRhodes.Green.R a b = ∃ (s : M), ∃ (t : M), a * s = b ∧ b * t = a

Green's H-relation

def LeanPool.KrohnRhodes.Green.H {M : Type u_1} [Monoid M] (a b : M) : Prop

Green's H-relation: intersection of L and R. a H b iff a L b and a R b.

Equations

• LeanPool.KrohnRhodes.Green.H a b = (LeanPool.KrohnRhodes.Green.L a b ∧ LeanPool.KrohnRhodes.Green.R a b)

Aperiodic elements and monoids

def LeanPool.KrohnRhodes.Green.IsAperiodicElem {M : Type u_1} [Monoid M] (a : M) : Prop

An element a is aperiodic if its H-class is trivial (a singleton). Equivalently, a H b → a = b.

Equations

• LeanPool.KrohnRhodes.Green.IsAperiodicElem a = ∀ (b : M), LeanPool.KrohnRhodes.Green.H a b → a = b