Pseudovarieties of finite monoids and semigroups

This file defines pseudovarieties of finite monoids and of finite semigroups. A pseudovariety is a class of finite monoids, or of finite semigroups, closed under submonoids or subsemigroups, quotients and finite direct products, the empty product being the trivial one. Pseudovarieties are the algebraic side of Eilenberg's variety theorem, which matches the monoid ones with the varieties of regular languages and the semigroup ones with the varieties of languages of nonempty words.

Main definitions

• Monoid.Pseudovariety, Semigroup.Pseudovariety: classes of finite monoids, respectively semigroups, closed under substructures, quotients and products.
• Monoid.Pseudovariety.generated: the least pseudovariety containing a class of finite monoids.
• Monoid.aperiodicVariety: the pseudovariety of finite aperiodic monoids.
• Semigroup.definiteVariety, Semigroup.reverseDefiniteVariety, Semigroup.locallyTrivialVariety: the pseudovarieties D, K and LI.

Main results

• Monoid.Pseudovariety.pi_mem: closure under finite dependent products.
• Monoid.Pseudovariety.mem_quotient_of_le, mem_quotient_ker, mem_quotient_inf and their semigroup counterparts: closure properties of quotients by congruences.
• The pseudovarieties of finite monoids form a complete lattice, with infimum the intersection.

Implementation notes

mem is a total predicate on Type u monoids or semigroups that implies finiteness (finite_of_mem), so the order on pseudovarieties is inclusion of classes of finite structures and is antisymmetric. The structures live in a fixed universe u, like mathlib's MorphismProperty; concrete pseudovarieties are universe-polymorphic definitions. The semigroup pseudovarieties D, K and LI have no monoid counterpart, since their conditions at the idempotent 1 force triviality; the pseudovariety N of nilpotent semigroups is the intersection of D and K and is not bundled.

References

• [Eil76]
• [Pin]

structure Monoid.Pseudovariety : Type (u + 1)

A pseudovariety of finite monoids is a class of finite monoids closed under submonoids, quotients and finite products, with closure phrased through injective and surjective homomorphisms.

• mem (M : Type u) [Monoid M] : Prop

  The monoids belonging to the pseudovariety.

• finite_of_mem {M : Type u} [Monoid M] : self.mem M → Finite M

  Every member is finite.

• sub {M N : Type u} [Monoid M] [Monoid N] {f : M →* N} : Function.Injective ⇑f → self.mem N → self.mem M

  The domain of an injective homomorphism into a member is a member.

• quot {M N : Type u} [Monoid M] [Monoid N] {f : M →* N} : Function.Surjective ⇑f → self.mem M → self.mem N

  The codomain of a surjective homomorphism from a member is a member.

• prod {M N : Type u} [Monoid M] [Monoid N] : self.mem M → self.mem N → self.mem (M × N)

  The product of two members is a member.

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

  The trivial monoid is a member.

theorem Monoid.Pseudovariety.ext {V W : Pseudovariety} (h : ∀ (M : Type u) [inst : Monoid M], V.mem M ↔ W.mem M) : V = W

theorem Monoid.Pseudovariety.ext_iff {V W : Pseudovariety} : V = W ↔ ∀ (M : Type u) [inst : Monoid M], V.mem M ↔ W.mem M

@[instance_reducible]

instance Monoid.Pseudovariety.instPartialOrder : PartialOrder Pseudovariety

Equations

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

theorem Monoid.Pseudovariety.le_def {V W : Pseudovariety} : V ≤ W ↔ ∀ (M : Type u) [inst : Monoid M], V.mem M → W.mem M

theorem Monoid.Pseudovariety.mem_of_mulEquiv (V : Pseudovariety) {M N : Type u} [Monoid M] [Monoid N] (e : M ≃* N) (h : V.mem M) : V.mem N

theorem Monoid.Pseudovariety.mem_of_isSubquotient (V : Pseudovariety) {M N : Type u} [Monoid M] [Monoid N] (h : IsSubquotient M N) (hN : V.mem N) : V.mem M

A subquotient of a member is a member.

Quotients by congruences

theorem Monoid.Pseudovariety.mem_quotient_of_le (V : Pseudovariety) {M : Type u} [Monoid M] {c d : Con M} (h : c ≤ d) (hc : V.mem c.Quotient) : V.mem d.Quotient

Membership of a quotient descends along a coarsening of congruences.

theorem Monoid.Pseudovariety.mem_quotient_ker (V : Pseudovariety) {M N : Type u} [Monoid M] [Monoid N] (f : M →* N) (h : V.mem N) : V.mem (Con.ker f).Quotient

The quotient by the kernel of a homomorphism into a member is a member.

theorem Monoid.Pseudovariety.mem_quotient_inf (V : Pseudovariety) {M : Type u} [Monoid M] {c d : Con M} (hc : V.mem c.Quotient) (hd : V.mem d.Quotient) : V.mem (c ⊓ d).Quotient

The quotient by the meet of two congruences is a member when both quotients are.

Finite products

theorem Monoid.Pseudovariety.pi_mem (V : Pseudovariety) {ι : Type u} [Finite ι] {f : ι → Type u} [(i : ι) → Monoid (f i)] (h : ∀ (i : ι), V.mem (f i)) : V.mem ((i : ι) → f i)

A pseudovariety is closed under finite dependent products.

The lattice of pseudovarieties

@[instance_reducible]

instance Monoid.Pseudovariety.instInfSet : InfSet Pseudovariety

Equations

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

theorem Monoid.Pseudovariety.mem_sInf {s : Set Pseudovariety} {M : Type u} [Monoid M] : (sInf s).mem M ↔ Finite M ∧ ∀ V ∈ s, V.mem M

@[instance_reducible]

instance Monoid.Pseudovariety.instCompleteLattice : CompleteLattice Pseudovariety

Equations

• Monoid.Pseudovariety.instCompleteLattice = completeLatticeOfInf Monoid.Pseudovariety Monoid.Pseudovariety.instCompleteLattice._proof_1

def Monoid.Pseudovariety.generated (S : (M : Type u) → [Monoid M] → Prop) : Pseudovariety

The pseudovariety generated by a class of monoids is the least pseudovariety containing its finite members.

Equations

• Monoid.Pseudovariety.generated S = sInf {V : Monoid.Pseudovariety | ∀ (N : Type ?u.1) [inst : Monoid N] [Finite N], S N → V.mem N}

theorem Monoid.Pseudovariety.subset_generated {S : (M : Type u) → [Monoid M] → Prop} {M : Type u} [Monoid M] [Finite M] (h : S M) : (generated S).mem M

theorem Monoid.Pseudovariety.generated_le {S : (M : Type u) → [Monoid M] → Prop} {V : Pseudovariety} (h : ∀ (N : Type u) [inst : Monoid N] [Finite N], S N → V.mem N) : generated S ≤ V

def Monoid.aperiodicVariety : Pseudovariety

The pseudovariety of finite aperiodic monoids, the algebraic counterpart of the star-free languages.

Equations

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

@[simp]

theorem Monoid.mem_aperiodicVariety {M : Type u} [Monoid M] : aperiodicVariety.mem M ↔ Finite M ∧ IsAperiodic M

structure Semigroup.Pseudovariety : Type (u + 1)

A pseudovariety of finite semigroups is a class of finite semigroups closed under subsemigroups, quotients and finite products, with closure phrased through injective and surjective MulHoms.

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

  The semigroups belonging to the pseudovariety.

• finite_of_mem {S : Type u} [Semigroup S] : self.mem S → Finite S

  Every member is finite.

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

  The domain of an injective homomorphism into a member is a member.

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

  The codomain of a surjective homomorphism from a member is a member.

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

  The product of two members is a member.

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

  The trivial semigroup is a member.

theorem Semigroup.Pseudovariety.ext {V W : Pseudovariety} (h : ∀ (S : Type u) [inst : Semigroup S], V.mem S ↔ W.mem S) : V = W

theorem Semigroup.Pseudovariety.ext_iff {V W : Pseudovariety} : V = W ↔ ∀ (S : Type u) [inst : Semigroup S], V.mem S ↔ W.mem S

@[instance_reducible]

instance Semigroup.Pseudovariety.instPartialOrder : PartialOrder Pseudovariety

Equations

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

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

theorem Semigroup.Pseudovariety.mem_quotient_of_le (V : Pseudovariety) {S : Type u} [Semigroup S] {c d : Con S} (h : c ≤ d) (hc : V.mem c.Quotient) : V.mem d.Quotient

Membership of a quotient descends along a coarsening of congruences.

theorem Semigroup.Pseudovariety.mem_quotient_ker (V : Pseudovariety) {S T : Type u} [Semigroup S] [Semigroup T] (f : S →ₙ* T) (h : V.mem T) : V.mem (Con.ker f).Quotient

The quotient by the kernel of a homomorphism into a member is a member.

theorem Semigroup.Pseudovariety.mem_quotient_inf (V : Pseudovariety) {S : Type u} [Semigroup S] {c d : Con S} (hc : V.mem c.Quotient) (hd : V.mem d.Quotient) : V.mem (c ⊓ d).Quotient

The quotient by the meet of two congruences is a member when both quotients are.

The bundled pseudovarieties

def Semigroup.definiteVariety : Pseudovariety

The pseudovariety D of definite semigroups.

Equations

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

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 ↔ Finite S ∧ IsDefinite S

@[simp]

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

@[simp]

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