The transition monoid of a DFA

The transition monoid of an automaton is the monoid of state-transformations induced by input words — foundational algebraic automata theory (syntactic monoid, Schützenberger's theorem, Eilenberg variety theory), currently absent from mathlib.

A word w acts on a state s of M : DFA α σ by s ↦ M.evalFrom s w. Reading u then v (evalFrom_of_append) makes this a right action — an anti-homomorphism into Function.End σ — so as a MonoidHom its target is the opposite monoid (Function.End σ)ᵐᵒᵖ.

• DFA.transitionHom M : FreeMonoid α →* (Function.End σ)ᵐᵒᵖ — the transition action.
• DFA.transitionMonoid M : Submonoid (Function.End σ)ᵐᵒᵖ — its range, the transition monoid.
• DFA.transitionMonoidEquiv M — the first iso theorem: (Con.ker M.transitionHom).Quotient ≃* the transition monoid.
• Finite (Function.End σ) / Finite M.transitionMonoid instances (these do not auto-synthesize from Finite σ, so we register them here once).

def DFA.transitionHom {α : Type u} {σ : Type v} (M : DFA α σ) : FreeMonoid α →* (Function.End σ)ᵐᵒᵖ

The transition action of M: word w sends state s to M.evalFrom s w.

Equations

• M.transitionHom = { toFun := fun (w : FreeMonoid α) => MulOpposite.op fun (s : σ) => M.evalFrom s (FreeMonoid.toList w), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem DFA.unop_transitionHom_apply {α : Type u} {σ : Type v} (M : DFA α σ) (w : FreeMonoid α) (s : σ) : MulOpposite.unop (M.transitionHom w) s = M.evalFrom s (FreeMonoid.toList w)

theorem DFA.transitionHom_eq_iff {α : Type u} {σ : Type v} (M : DFA α σ) {u v : FreeMonoid α} : M.transitionHom u = M.transitionHom v ↔ ∀ (s : σ), M.evalFrom s (FreeMonoid.toList u) = M.evalFrom s (FreeMonoid.toList v)

Two words induce the same transition iff evalFrom agrees from every state.

def DFA.transitionMonoid {α : Type u} {σ : Type v} (M : DFA α σ) : Submonoid (Function.End σ)ᵐᵒᵖ

The transition monoid of M: the range of its transition action.

Equations

• M.transitionMonoid = MonoidHom.mrange M.transitionHom

noncomputable def DFA.transitionMonoidEquiv {α : Type u} {σ : Type v} (M : DFA α σ) : (Con.ker M.transitionHom).Quotient ≃* ↥M.transitionMonoid

First isomorphism theorem: the transition monoid as a quotient of FreeMonoid α.

Equations

• M.transitionMonoidEquiv = Con.quotientKerEquivRange M.transitionHom

instance DFA.Function.End.instFinite {σ : Type v} [Finite σ] : Finite (Function.End σ)

Function.End σ is finite when σ is (not found automatically through the def).

instance DFA.instFiniteEndMop {σ : Type v} [Finite σ] : Finite (Function.End σ)ᵐᵒᵖ

(Function.End σ)ᵐᵒᵖ is finite when σ is (likewise not found automatically).

instance DFA.transitionMonoid.instFinite {α : Type u} {σ : Type v} (M : DFA α σ) [Finite σ] : Finite ↥M.transitionMonoid