The Eilenberg correspondence as a Galois connection

The Eilenberg variety theorem ([Eil76], [Alm95]) sets up an order isomorphism between pseudovarieties of finite monoids and varieties of recognizable languages. This file formalizes the easy, formal half of that correspondence: the two maps varietyToLang and langToVariety form a Galois connection between the two preorders. The hard, content-bearing half — that the connection is in fact an order isomorphism — is the pair of converse inequalities left as the two staged sorrys below.

Main definitions

• Monoid.Pseudovariety is given a Preorder by class inclusion.
• Monoid.Pseudovariety.generated — the smallest pseudovariety containing a class of finite monoids.
• Monoid.LanguageVariety — a (boolean + inverse-homomorphism) variety of recognizable languages.
• Monoid.varietyToLang — the language-side map V ↦ V.langs.
• Monoid.langToVariety — the algebra-side map 𝒱 ↦ generated by the syntactic monoids in 𝒱.

Main results

• Monoid.varietyToLang_monotone / Monoid.langToVariety_monotone — the maps are functors of the thin (preorder) categories; bundled as Monoid.varietyToLangHom / Monoid.langToVarietyHom.
• Monoid.eilenberg_galoisConnection — the adjunction langToVariety ⊣ varietyToLang.
• Monoid.mem_langToVariety_varietyToLang / Monoid.mem_langToVariety_varietyToLang_iff — the monoid-side round-trip (langToVariety ∘ varietyToLang = id on finite monoids), proven.
• Monoid.varietyToLang_langToVariety_le — the language-side round-trip, the deep half of Eilenberg's theorem, currently sorry (see implementation notes).

Implementation notes

LanguageVariety here is the boolean + inverse-homomorphism fragment of an Eilenberg +variety: closure under ⊤, complement, intersection, and inverse homomorphism. The genuine Eilenberg +variety additionally requires closure under left and right residuals u⁻¹L and Lu⁻¹; that axiom is omitted pending a syntacticMonoid_leftQuotient division lemma (TODO). The fragment is already enough to state and prove the Galois connection.

The two preorders are thin categories (CategoryTheory.Preorder.smallCategory); the monotone maps above are the corresponding functors and the Galois connection is their adjunction. The monoid-side round-trip is proven (mem_langToVariety_varietyToLang_iff); refining the Preorders to PartialOrders and discharging the language-side round-trip (varietyToLang_langToVariety_le) would upgrade the adjunction to the Eilenberg order isomorphism (OrderIso). A literal CategoryTheory.Adjunction is obtainable from eilenberg_galoisConnection via mathlib's GaloisConnection.adjunction, kept out of this order-algebra file by design.

Everything lives in a single fixed universe u: alphabets and monoids are all Type u, matching the universe-monomorphic Pseudovariety of Linglib.Core.Algebra.Group.Pseudovariety.

@[implicit_reducible]

instance Monoid.Pseudovariety.instPreorder : Preorder Pseudovariety

Pseudovarieties are preordered by class inclusion of their (total) membership predicates.

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

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

The pseudovariety generated by a class S of finite monoids: the intersection of all pseudovarieties whose finite members include everything in S. Closure under submonoid, quotient, and product is inherited pointwise from the pseudovarieties being intersected.

Equations

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

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

Every finite monoid in S belongs to the pseudovariety it generates.

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

generated S is the least pseudovariety whose finite members include S.

structure Monoid.LanguageVariety : Type (u + 1)

A variety of recognizable languages (boolean + inverse-homomorphism fragment of an Eilenberg +variety): a family of regular languages, over every alphabet α : Type u, closed under the full language, complement, binary intersection, and inverse homomorphism. The residual-closure axiom of a genuine +variety is omitted here (see the module docstring).

• lang {α : Type u} : Language α → Prop

  The languages belonging to the variety, over each alphabet.

• regular {α : Type u} {L : Language α} : self.lang L → L.IsRegular

  Every member is regular.

• univ_mem {α : Type u} : self.lang ⊤

  Closed under the full language.

• compl_mem {α : Type u} {L : Language α} : self.lang L → self.lang Lᶜ

  Closed under complement.

• inf_mem {α : Type u} {L M : Language α} : self.lang L → self.lang M → self.lang (L ⊓ M)

  Closed under binary intersection.

• comap_mem {α β : Type u} {Lb : Language β} (φ : FreeMonoid α →* FreeMonoid β) : self.lang Lb → self.lang {w : List α | φ (FreeMonoid.ofList w) ∈ Lb}

  Closed under inverse homomorphism.

@[implicit_reducible]

instance Monoid.LanguageVariety.instPreorder : Preorder LanguageVariety

Language varieties are preordered by family inclusion.

Equations

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

theorem Monoid.LanguageVariety.le_def {𝒱 𝒲 : LanguageVariety} : 𝒱 ≤ 𝒲 ↔ ∀ (α : Type u) (L : Language α), 𝒱.lang L → 𝒲.lang L

def Monoid.varietyToLang (V : Pseudovariety) : LanguageVariety

The language-side map: a pseudovariety V goes to the variety of languages whose syntactic monoid lies in V. Well-definedness is exactly the keystone closure theorems of Pseudovariety.langs.

Equations

• Monoid.varietyToLang V = { lang := fun {α : Type ?u.1} (L : Language α) => V.langs L, regular := ⋯, univ_mem := ⋯, compl_mem := ⋯, inf_mem := ⋯, comap_mem := ⋯ }

def Monoid.langToVariety (𝒱 : LanguageVariety) : Pseudovariety

The algebra-side map: a language variety 𝒱 goes to the pseudovariety generated by the syntactic monoids of the languages in 𝒱.

Equations

• Monoid.langToVariety 𝒱 = Monoid.Pseudovariety.generated fun (M : Type ?u.1) (x : Monoid M) => ∃ (α : Type ?u.1) (L : Language α), 𝒱.lang L ∧ Nonempty (M ≃* L.syntacticMonoid)

@[simp]

theorem Monoid.mem_varietyToLang (V : Pseudovariety) {α : Type u} (L : Language α) : (varietyToLang V).lang L ↔ V.langs L

theorem Monoid.eilenberg_galoisConnection : GaloisConnection langToVariety varietyToLang

The Eilenberg Galois connection. langToVariety is left adjoint to varietyToLang: langToVariety 𝒱 ≤ V ↔ 𝒱 ≤ varietyToLang V. This is the formal half of the variety theorem; the content-bearing half is the pair of converse inequalities below.

theorem Monoid.langToVariety_varietyToLang_le (V : Pseudovariety) : langToVariety (varietyToLang V) ≤ V

One free composite from the Galois connection: langToVariety (varietyToLang V) ≤ V.

theorem Monoid.le_varietyToLang_langToVariety (𝒱 : LanguageVariety) : 𝒱 ≤ varietyToLang (langToVariety 𝒱)

The other free composite: 𝒱 ≤ varietyToLang (langToVariety 𝒱).

Functoriality

A preorder is a thin category (CategoryTheory.Preorder.smallCategory) and a functor between thin categories is exactly a monotone map, so the two maps are functors and the Galois connection is the adjunction langToVariety ⊣ varietyToLang. We record functoriality as Monotone and bundle the functors as OrderHoms; both monotonicities are immediate from the Galois connection.

theorem Monoid.langToVariety_monotone : Monotone langToVariety

langToVariety is a functor of the thin category of pseudovarieties (the left adjoint).

theorem Monoid.varietyToLang_monotone : Monotone varietyToLang

varietyToLang is a functor of the thin category of language varieties (the right adjoint).

def Monoid.langToVarietyHom : LanguageVariety →o Pseudovariety

langToVariety bundled as an OrderHom (a functor of thin categories).

Equations

• Monoid.langToVarietyHom = { toFun := Monoid.langToVariety, monotone' := Monoid.langToVariety_monotone }

def Monoid.varietyToLangHom : Pseudovariety →o LanguageVariety

varietyToLang bundled as an OrderHom (a functor of thin categories).

Equations

• Monoid.varietyToLangHom = { toFun := Monoid.varietyToLang, monotone' := Monoid.varietyToLang_monotone }

theorem Monoid.mem_langToVariety_varietyToLang (V : Pseudovariety) {M : Type u} [Monoid M] [Finite M] (hM : V.mem M) : (langToVariety (varietyToLang V)).mem M

Monoid-side round-trip — the "syntactic monoids generate" half of Eilenberg's variety theorem, for finite monoids: every finite M in V lies in langToVariety (varietyToLang V). The finiteness hypothesis is essential — V.mem is a total predicate, so V can hold of infinite monoids that the generated variety excludes (e.g. an infinite semilattice for aperiodicVariety), making the unrestricted V ≤ … false. Each fibre language L_m = φ⁻¹{m} of the surjection φ : FreeMonoid M ↠ M has syntactic monoid a quotient of M (a generator), and ⨅_m syntacticCon (L_m) = ker φ, so M embeds into the finite product of those syntactic monoids.

theorem Monoid.mem_langToVariety_varietyToLang_iff (V : Pseudovariety) {M : Type u} [Monoid M] [Finite M] : (langToVariety (varietyToLang V)).mem M ↔ V.mem M

The monoid-side round-trip as an equivalence on finite monoids: langToVariety (varietyToLang V) and V agree on finite monoids.

theorem Monoid.varietyToLang_langToVariety_le (𝒱 : LanguageVariety) : varietyToLang (langToVariety 𝒱) ≤ 𝒱

Language-side round-trip — the deep half of Eilenberg's variety theorem. TODO: requires (a) the residual closure axiom omitted from LanguageVariety and (b) recognition-by-products / projection-cylinder-language theory (absent from mathlib): every language in varietyToLang (langToVariety 𝒱) is rebuilt from the generators of langToVariety 𝒱 using the closure operations available in 𝒱.