The language-side operator of a pseudovariety

The forward half of the Eilenberg correspondence: for a pseudovariety V of finite monoids, V.langs collects the regular languages whose syntactic monoid lies in V. The keystone is that V.langs is a variety of languages — closed under the boolean operations and inverse homomorphism — for any V. Each closure proof is the syntactic-monoid argument already used for star-free languages (Language.IsStarFree, the V = aperiodicVariety instance), generalized by replacing Monoid.IsAperiodic with V.mem and the aperiodic closure lemmas with the closure fields of V.

Main definitions

• Monoid.Pseudovariety.langs — the languages whose syntactic monoid lies in V.

Main results

• Monoid.Pseudovariety.langs_of_recognizes — a language recognized by a finite monoid in V is in V.langs (the engine).
• langs_compl / langs_inf / langs_sup / langs_univ / langs_bot — boolean closure.
• langs_comap — closure under inverse homomorphism.

def Monoid.Pseudovariety.langs (V : Pseudovariety) {α : Type u} (L : Language α) : Prop

The languages over α whose (necessarily finite) syntactic monoid lies in V — the language-side operator of the Eilenberg correspondence.

Equations

• V.langs L = (L.IsRegular ∧ V.mem L.syntacticMonoid)

theorem Monoid.Pseudovariety.langs_def (V : Pseudovariety) {α : Type u} {L : Language α} : V.langs L ↔ L.IsRegular ∧ V.mem L.syntacticMonoid

theorem Monoid.Pseudovariety.langs_of_recognizes (V : Pseudovariety) {α : Type u} {L : Language α} {N : Type u} [Monoid N] [Finite N] (hN : V.mem N) (η : FreeMonoid α →* N) (P : Set N) (hL : ∀ (w : List α), w ∈ L ↔ η (FreeMonoid.ofList w) ∈ P) : V.langs L

Engine. A language recognized by a finite monoid in V lies in V.langs: the syntactic monoid is a quotient of a submonoid of the recognizer, hence in V. Generalizes Language.IsStarFree.of_recognizes.

theorem Monoid.Pseudovariety.langs_compl (V : Pseudovariety) {α : Type u} {L : Language α} (h : V.langs L) : V.langs Lᶜ

Closure under complement — immediate from complement-invariance of the syntactic monoid.

theorem Monoid.Pseudovariety.langs_inf (V : Pseudovariety) {α : Type u} {L M : Language α} (hL : V.langs L) (hM : V.langs M) : V.langs (L ⊓ M)

Closure under intersection — the syntactic monoid of L ⊓ M is a quotient of a submonoid of L.syntacticMonoid × M.syntacticMonoid, which is in V by prod/sub/quot.

theorem Monoid.Pseudovariety.langs_sup (V : Pseudovariety) {α : Type u} {L M : Language α} (hL : V.langs L) (hM : V.langs M) : V.langs (L ⊔ M)

Closure under union — by De Morgan, L ⊔ M = (Lᶜ ⊓ Mᶜ)ᶜ.

theorem Monoid.Pseudovariety.langs_univ (V : Pseudovariety) {α : Type u} : V.langs ⊤

The full language is in V.langs — recognized by the trivial monoid, which is in every pseudovariety (memUnit).

theorem Monoid.Pseudovariety.langs_bot (V : Pseudovariety) {α : Type u} : V.langs ⊥

The empty language is in V.langs — ⊥ = ⊤ᶜ.

theorem Monoid.Pseudovariety.langs_comap (V : Pseudovariety) {α β : Type u} {Lb : Language β} (h : V.langs Lb) (φ : FreeMonoid α →* FreeMonoid β) : V.langs {w : List α | φ (FreeMonoid.ofList w) ∈ Lb}

Closure under inverse homomorphism. If Lb over β is in V.langs and φ : FreeMonoid α →* FreeMonoid β is any monoid hom, the preimage language is in V.langs. The recognizer is Lb.toSyntacticMonoid.comp φ into the finite Lb.syntacticMonoid ∈ V. Generalizes Language.IsStarFree.comap.