Pseudovarieties of finite semigroups

A pseudovariety of finite semigroups ([Eil76]) is a class of finite semigroups closed under subsemigroups, quotients, and finite direct products. It is the semigroup-side counterpart of Monoid.Pseudovariety, and the two are not interchangeable: the classes D, K and LI below are semigroup varieties that collapse over monoids, since applying their defining condition to the idempotent 1 forces triviality.

The conditions are stated on idempotents, as Eilenberg states them: D is Se = e ([Eil76] VIII.4.1) and LI is eSe = e (VIII.5.1), with K the left-right dual of D. Quotient closure is where the semigroup case departs from the monoid one — a preimage of an idempotent need not be idempotent — and is discharged by Semigroup.exists_isIdempotentElem_map_eq.

Main definitions

• Semigroup.Pseudovariety: a class of finite semigroups closed under subsemigroup, quotient, product.
• Semigroup.IsDefinite, IsReverseDefinite, IsLocallyTrivial: the defining conditions of D, K, LI.
• Semigroup.definiteVariety, reverseDefiniteVariety, locallyTrivialVariety: the bundled pseudovarieties.

Implementation notes

mem is a total predicate over Type u semigroups, mirroring Monoid.Pseudovariety; the finiteness characteristic of a pseudovariety lives on the closure-field hypotheses. The variety N of nilpotent semigroups is the intersection of D and K and is not bundled here.

structure Semigroup.Pseudovariety : Type (u + 1)

A pseudovariety of finite semigroups: a class closed under subsemigroups, quotients, and finite products. Closure is phrased via injective/surjective MulHoms (the divisor form).

• mem (S : Type u) [Semigroup S] : Prop

  The semigroups belonging to the pseudovariety.

• sub {S T : Type u} [Semigroup S] [Semigroup T] [Finite S] [Finite T] {f : S →ₙ* T} : Function.Injective ⇑f → self.mem T → self.mem S

  Closed under subsemigroups: an injective homomorphism into a member has member domain.

• quot {S T : Type u} [Semigroup S] [Semigroup T] [Finite S] [Finite T] {f : S →ₙ* T} : Function.Surjective ⇑f → self.mem S → self.mem T

  Closed under quotients: a surjective homomorphism from a member has member codomain.

• prod {S T : Type u} [Semigroup S] [Semigroup T] [Finite S] [Finite T] : self.mem S → self.mem T → self.mem (S × T)

  Closed under binary products.

• memUnit : self.mem PUnit.{u + 1}

  Contains the trivial semigroup (the empty product).

theorem Semigroup.Pseudovariety.mem_of_mulEquiv (V : Pseudovariety) {S T : Type u} [Semigroup S] [Semigroup T] [Finite S] [Finite T] (e : S ≃* T) (h : V.mem S) : V.mem T

Closed under isomorphism (a special case of quot).

The conditions defining D, K and LI

def Semigroup.IsDefinite (S : Type u_3) [Semigroup S] : Prop

A finite semigroup is definite when every idempotent absorbs on the left: Se = e ([Eil76] VIII.4.1).

Equations

• Semigroup.IsDefinite S = ∀ (e : S), IsIdempotentElem e → ∀ (s : S), s * e = e

def Semigroup.IsReverseDefinite (S : Type u_3) [Semigroup S] : Prop

A finite semigroup is reverse definite when every idempotent absorbs on the right — the left-right dual of IsDefinite.

Equations

• Semigroup.IsReverseDefinite S = ∀ (e : S), IsIdempotentElem e → ∀ (s : S), e * s = e

def Semigroup.IsLocallyTrivial (S : Type u_3) [Semigroup S] : Prop

A finite semigroup is locally trivial when every idempotent absorbs on both sides at once: eSe = e ([Eil76] VIII.5.1). This is the condition behind the generalized definite languages.

Equations

• Semigroup.IsLocallyTrivial S = ∀ (e : S), IsIdempotentElem e → ∀ (s : S), e * s * e = e

Closure properties

theorem Semigroup.IsDefinite.of_injective {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] {f : S →ₙ* T} (hf : Function.Injective ⇑f) (h : IsDefinite T) : IsDefinite S

theorem Semigroup.IsReverseDefinite.of_injective {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] {f : S →ₙ* T} (hf : Function.Injective ⇑f) (h : IsReverseDefinite T) : IsReverseDefinite S

theorem Semigroup.IsLocallyTrivial.of_injective {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] {f : S →ₙ* T} (hf : Function.Injective ⇑f) (h : IsLocallyTrivial T) : IsLocallyTrivial S

theorem Semigroup.IsDefinite.prod {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] (hS : IsDefinite S) (hT : IsDefinite T) : IsDefinite (S × T)

theorem Semigroup.IsReverseDefinite.prod {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] (hS : IsReverseDefinite S) (hT : IsReverseDefinite T) : IsReverseDefinite (S × T)

theorem Semigroup.IsLocallyTrivial.prod {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] (hS : IsLocallyTrivial S) (hT : IsLocallyTrivial T) : IsLocallyTrivial (S × T)

theorem Semigroup.IsDefinite.subsingleton {M : Type u_3} [Monoid M] (h : IsDefinite M) : Subsingleton M

D collapses over monoids: a definite monoid is trivial, since the condition applied to the idempotent 1 gives s = s * 1 = 1. This is why D, K and LI are semigroup varieties.

theorem Semigroup.IsDefinite.isLocallyTrivial {S : Type u_1} [Semigroup S] (h : IsDefinite S) : IsLocallyTrivial S

A definite semigroup is locally trivial: apply Se = e at the element e * s.

theorem Semigroup.IsReverseDefinite.isLocallyTrivial {S : Type u_1} [Semigroup S] (h : IsReverseDefinite S) : IsLocallyTrivial S

A reverse definite semigroup is locally trivial: apply eS = e twice.

theorem Semigroup.IsDefinite.of_surjective {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] [Finite S] {f : S →ₙ* T} (hf : Function.Surjective ⇑f) (h : IsDefinite S) : IsDefinite T

theorem Semigroup.IsReverseDefinite.of_surjective {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] [Finite S] {f : S →ₙ* T} (hf : Function.Surjective ⇑f) (h : IsReverseDefinite S) : IsReverseDefinite T

theorem Semigroup.IsLocallyTrivial.of_surjective {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] [Finite S] {f : S →ₙ* T} (hf : Function.Surjective ⇑f) (h : IsLocallyTrivial S) : IsLocallyTrivial T

The bundled pseudovarieties

def Semigroup.definiteVariety : Pseudovariety

The pseudovariety D of definite semigroups.

Equations

• Semigroup.definiteVariety = { mem := fun (S : Type ?u.1) [Semigroup S] => Semigroup.IsDefinite S, sub := ⋯, quot := ⋯, prod := ⋯, memUnit := Semigroup.definiteVariety._proof_1 }

def Semigroup.reverseDefiniteVariety : Pseudovariety

The pseudovariety K of reverse definite semigroups.

Equations

• One or more equations did not get rendered due to their size.

def Semigroup.locallyTrivialVariety : Pseudovariety

The pseudovariety LI of locally trivial semigroups.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Semigroup.mem_definiteVariety {S : Type u} [Semigroup S] : definiteVariety.mem S ↔ IsDefinite S

@[simp]

theorem Semigroup.mem_reverseDefiniteVariety {S : Type u} [Semigroup S] : reverseDefiniteVariety.mem S ↔ IsReverseDefinite S

@[simp]

theorem Semigroup.mem_locallyTrivialVariety {S : Type u} [Semigroup S] : locallyTrivialVariety.mem S ↔ IsLocallyTrivial S