The languages of a pseudovariety

This file defines the languages of a pseudovariety: for a pseudovariety V of finite monoids, the languages whose syntactic monoid lies in V, and for a pseudovariety of finite semigroups, the languages whose syntactic semigroup lies in V. Over each alphabet these languages form a Boolean algebra closed under quotients and inverse homomorphisms of free monoids, respectively free semigroups. These are Eilenberg's *-varieties and +-varieties of languages.

Main definitions

• Monoid.Pseudovariety.langs, Semigroup.Pseudovariety.langs: the languages of a pseudovariety.
• Monoid.Pseudovariety.toBooleanSubalgebra: the languages of V over an alphabet, as a Boolean subalgebra.

Main results

• Monoid.Pseudovariety.langs_of_recognizes, Semigroup.Pseudovariety.langs_of_recognizes: a language recognized by a member of V lies in V.langs.
• langs_leftQuotient, langs_rightQuotient, langs_comap on both sides: closure under quotients and inverse homomorphisms.

Implementation notes

A free semigroup has no erasing homomorphisms, so the semigroup side is closed only under inverse images of homomorphisms between free semigroups.

References

• [Eil76]
• [Pin]

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

The languages of a pseudovariety V are those whose syntactic monoid lies in V.

Equations

• V.langs L = V.mem L.SyntacticMonoid

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

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

theorem Monoid.Pseudovariety.langs_of_syntacticCon_le {V : Pseudovariety} {α : Type u} {L M : Language α} (h : V.langs L) (hle : L.syntacticCon ≤ M.syntacticCon) : V.langs M

The languages of V are upward closed in the order of syntactic congruences.

theorem Monoid.Pseudovariety.langs_of_recognizes (V : Pseudovariety) {α : Type u} {L : Language α} {N : Type u} [Monoid N] (hN : V.mem N) {η : FreeMonoid α →* N} (h : Language.Recognizes η L) : V.langs L

A language recognized by a member of V lies in V.langs.

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

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

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

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

theorem Monoid.Pseudovariety.langs_bot (V : Pseudovariety) {α : Type u} : 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}

The languages of V are closed under inverse homomorphisms of free monoids.

theorem Monoid.Pseudovariety.langs_leftQuotient {V : Pseudovariety} {α : Type u} {L : Language α} (h : V.langs L) (u : List α) : V.langs (L.leftQuotient u)

theorem Monoid.Pseudovariety.langs_rightQuotient {V : Pseudovariety} {α : Type u} {L : Language α} (h : V.langs L) (u : List α) : V.langs (L.rightQuotient u)

def Monoid.Pseudovariety.toBooleanSubalgebra (V : Pseudovariety) (α : Type u) : BooleanSubalgebra (Language α)

The languages of V over α, as a Boolean subalgebra of Language α.

Equations

• V.toBooleanSubalgebra α = { carrier := {L : Language α | V.langs L}, supClosed' := ⋯, infClosed' := ⋯, compl_mem' := ⋯, bot_mem' := ⋯ }

@[simp]

theorem Monoid.Pseudovariety.mem_toBooleanSubalgebra {V : Pseudovariety} {α : Type u} {L : Language α} : L ∈ V.toBooleanSubalgebra α ↔ V.langs L

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

The languages of a pseudovariety V are those whose syntactic semigroup lies in V.

Equations

• V.langs L = V.mem L.SyntacticSemigroup

theorem Semigroup.Pseudovariety.langs_isRegular (V : Pseudovariety) {α : Type u} {L : Language α} (h : V.langs L) : L.IsRegular

theorem Semigroup.Pseudovariety.langs_iff (V : Pseudovariety) {α : Type u} {L : Language α} : V.langs L ↔ L.IsRegular ∧ V.mem L.SyntacticSemigroup

theorem Semigroup.Pseudovariety.langs_of_syntacticSemigroupCon_le {V : Pseudovariety} {α : Type u} {L M : Language α} (h : V.langs L) (hle : L.syntacticSemigroupCon ≤ M.syntacticSemigroupCon) : V.langs M

The languages of V are upward closed in the order of syntactic congruences.

theorem Semigroup.Pseudovariety.langs_of_recognizes (V : Pseudovariety) {α : Type u} {L : Language α} {T : Type u} [Semigroup T] (hT : V.mem T) {η : FreeSemigroup α →ₙ* T} (h : Language.RecognizesSemigroup η L) : V.langs L

A language recognized by a member of V lies in V.langs.

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

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

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

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

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

theorem Semigroup.Pseudovariety.langs_comap (V : Pseudovariety) {α β : Type u} {Lb : Language β} (h : V.langs Lb) (φ : FreeSemigroup α →ₙ* FreeSemigroup β) : V.langs {w : List α | ∃ (u : FreeSemigroup α), FreeMonoid.toList (FreeSemigroup.toFreeMonoid u) = w ∧ FreeMonoid.toList (FreeSemigroup.toFreeMonoid (φ u)) ∈ Lb}

The languages of V are closed under inverse homomorphisms of free semigroups. A free semigroup has no erasing homomorphisms, which is the difference from the monoid case.

theorem Semigroup.Pseudovariety.langs_leftQuotient {V : Pseudovariety} {α : Type u} {L : Language α} (h : V.langs L) (u : List α) : V.langs (L.leftQuotient u)

theorem Semigroup.Pseudovariety.langs_rightQuotient {V : Pseudovariety} {α : Type u} {L : Language α} (h : V.langs L) (u : List α) : V.langs (L.rightQuotient u)