Eilenberg's variety theorem

This file proves Eilenberg's variety theorem: pseudovarieties of finite monoids correspond bijectively, and order-preservingly, to varieties of languages. A variety of languages assigns to each alphabet a Boolean algebra of regular languages, and these Boolean algebras are closed under quotients by words and under inverse images of monoid homomorphisms between free monoids. A pseudovariety V corresponds to the variety of languages whose syntactic monoid lies in V, and a variety of languages to the pseudovariety generated by the syntactic monoids of its members.

Main definitions

• Monoid.LanguageVariety: a variety of languages.
• Monoid.Pseudovariety.toLanguageVariety: the languages whose syntactic monoid lies in V.
• Monoid.LanguageVariety.toPseudovariety: the pseudovariety generated by the syntactic monoids of the members.

Main results

• Monoid.LanguageVariety.gc_toPseudovariety_toLanguageVariety: the two maps form a Galois connection.
• Monoid.LanguageVariety.setOf_syntacticClass_eq_mem: every fibre of the syntactic morphism of a member is a member.
• Monoid.Pseudovariety.toLanguageVariety_toPseudovariety, Monoid.LanguageVariety.toPseudovariety_toLanguageVariety: the two round trips are identities.
• Monoid.eilenbergOrderIso: the variety theorem as an order isomorphism.

Implementation notes

These are Eilenberg's *-varieties, whose languages are subsets of the free monoid; the +-varieties of the free semigroup are their counterpart for pseudovarieties of semigroups. The proof follows Chapter XIII of [Pin]. For the hard direction, the finite monoids all of whose recognized languages lie in a variety of languages form a pseudovariety containing the syntactic monoids of the members, so the generated pseudovariety recognizes only members. Alphabets range over all of Type u, not only finite types.

References

• [Eil76]
• [Pin]

structure Monoid.LanguageVariety : Type (u + 1)

A variety of languages assigns to each alphabet a Boolean algebra of regular languages, closed under inverse images of homomorphisms between free monoids and under left and right quotients by words.

• lang (α : Type u) : BooleanSubalgebra (Language α)

  The languages of the variety over each alphabet.

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

  Every member is regular.

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

  The inverse image of a member under a homomorphism of free monoids is a member.

• leftQuotient_mem {α : Type u} {L : Language α} (u : List α) : L ∈ self.lang α → L.leftQuotient u ∈ self.lang α

  The left quotient of a member by a word is a member.

• rightQuotient_mem {α : Type u} {L : Language α} (u : List α) : L ∈ self.lang α → L.rightQuotient u ∈ self.lang α

  The right quotient of a member by a word is a member.

@[instance_reducible]

instance Monoid.LanguageVariety.instDFunLikeTypeBooleanSubalgebraLanguage : DFunLike LanguageVariety (Type u) fun (α : Type u) => BooleanSubalgebra (Language α)

Equations

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

theorem Monoid.LanguageVariety.ext {𝒱 𝒲 : LanguageVariety} (h : ∀ (α : Type u) (L : Language α), L ∈ 𝒱 α ↔ L ∈ 𝒲 α) : 𝒱 = 𝒲

theorem Monoid.LanguageVariety.ext_iff {𝒱 𝒲 : LanguageVariety} : 𝒱 = 𝒲 ↔ ∀ (α : Type u) (L : Language α), L ∈ 𝒱 α ↔ L ∈ 𝒲 α

@[instance_reducible]

instance Monoid.LanguageVariety.instPartialOrder : PartialOrder LanguageVariety

Equations

• Monoid.LanguageVariety.instPartialOrder = PartialOrder.lift DFunLike.coe Monoid.LanguageVariety.instPartialOrder._proof_1

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

def Monoid.Pseudovariety.toLanguageVariety (V : Pseudovariety) : LanguageVariety

The variety of languages whose syntactic monoid lies in V.

Equations

• V.toLanguageVariety = { lang := V.toBooleanSubalgebra, isRegular := ⋯, comap_mem := ⋯, leftQuotient_mem := ⋯, rightQuotient_mem := ⋯ }

@[simp]

theorem Monoid.Pseudovariety.mem_toLanguageVariety (V : Pseudovariety) {α : Type u} {L : Language α} : L ∈ V.toLanguageVariety α ↔ V.langs L

def Monoid.LanguageVariety.toPseudovariety (𝒱 : LanguageVariety) : Pseudovariety

The pseudovariety generated by the syntactic monoids of the members of 𝒱.

Equations

• 𝒱.toPseudovariety = Monoid.Pseudovariety.generated fun (M : Type ?u.1) (x : Monoid M) => ∃ (α : Type ?u.1), ∃ L ∈ 𝒱 α, Nonempty (M ≃* L.SyntacticMonoid)

theorem Monoid.LanguageVariety.syntacticMonoid_mem_toPseudovariety (𝒱 : LanguageVariety) {α : Type u} {L : Language α} (h : L ∈ 𝒱 α) : 𝒱.toPseudovariety.mem L.SyntacticMonoid

theorem Monoid.LanguageVariety.gc_toPseudovariety_toLanguageVariety : GaloisConnection toPseudovariety Pseudovariety.toLanguageVariety

theorem Monoid.LanguageVariety.setOf_syntacticClass_eq_mem (𝒱 : LanguageVariety) {α : Type u} {L : Language α} (hL : L ∈ 𝒱 α) (x : L.SyntacticMonoid) : {w : List α | L.syntacticClass w = x} ∈ 𝒱 α

Every fibre of the syntactic morphism of a member is a member, since it is a finite Boolean combination of two-sided quotients of the member.

theorem Monoid.LanguageVariety.toPseudovariety_toLanguageVariety (𝒱 : LanguageVariety) : 𝒱.toPseudovariety.toLanguageVariety = 𝒱

A variety of languages is recovered from the pseudovariety it generates.

theorem Monoid.Pseudovariety.toLanguageVariety_toPseudovariety (V : Pseudovariety) : V.toLanguageVariety.toPseudovariety = V

A member of V embeds in the finite product of the syntactic monoids of its fibre languages, so V is recovered from its variety of languages.

def Monoid.eilenbergOrderIso : Pseudovariety ≃o LanguageVariety

Eilenberg's variety theorem puts pseudovarieties of finite monoids and varieties of languages in order-preserving bijection.

Equations

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