Pseudovarieties of finite monoids

A pseudovariety of finite monoids ([Eil76], [Alm95]) is a class of finite monoids closed under taking submonoids, quotients (homomorphic images), and finite direct products (the empty product being the trivial monoid). Pseudovarieties are the algebraic side of the Eilenberg correspondence: the recognizable-language classes closed under the boolean / quotient / inverse-homomorphism operations are exactly {L | L.syntacticMonoid ∈ V} for V a pseudovariety.

Main definitions

• Monoid.Pseudovariety — a class of finite monoids closed under submonoid, quotient, product.
• Monoid.aperiodicVariety — the pseudovariety A of aperiodic monoids (the star-free side).

Implementation notes

mem is a total predicate over Type u monoids (no [Finite] binder), mirroring Monoid.IsAperiodic; the finiteness restriction characteristic of a pseudovariety lives on the closure-field hypotheses, where it is used. This lets V.mem M be stated before a Finite M instance is in scope (as in the language-side operator Pseudovariety.langs, where finiteness is recovered from regularity).

Like mathlib's MorphismProperty, a Pseudovariety is relative to a fixed universe u (structure fields cannot be universe-polymorphic); concrete pseudovarieties such as aperiodicVariety are universe-polymorphic defs producing one Pseudovariety.{u} per u, so nothing is lost in use.

structure Monoid.Pseudovariety : Type (u + 1)

A pseudovariety of finite monoids: a class closed under submonoids, quotients, and finite products. Submonoid/quotient closure is phrased via injective/surjective monoid homomorphisms (the divisor form), which is what the closure proofs and the syntactic-monoid arguments consume.

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

  The monoids belonging to the pseudovariety.

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

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

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

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

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

  Closed under binary products.

• memUnit : self.mem PUnit

  Contains the trivial monoid (the empty product).

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

Closed under isomorphism (a special case of quot).

def Monoid.aperiodicVariety : Pseudovariety

The pseudovariety of aperiodic monoids A — the algebraic counterpart of the star-free languages ([Sch65]). The four closure obligations are the corresponding Monoid.IsAperiodic lemmas.

Equations

• Monoid.aperiodicVariety = { mem := fun (M : Type ?u.1) [Monoid M] => Monoid.IsAperiodic M, sub := ⋯, quot := ⋯, prod := ⋯, memUnit := Monoid.aperiodicVariety._proof_1 }

@[simp]

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