The transition monoid of a DFA

Each word induces a transformation of the states of a DFA, and reading one word after another composes these transformations. The monoid they generate is the transition monoid, the basic algebraic invariant of an automaton [Pin].

Main definitions

• DFA.transitionHom: the monoid homomorphism sending a word to the transformation it induces
• DFA.transitionMonoid: the transition monoid, the range of DFA.transitionHom
• DFA.transitionMonoidEquiv: the transition monoid as a quotient of FreeMonoid α

Implementation notes

A word w acts on a state s by s ↦ M.evalFrom s w, and evalFrom_of_append makes this a right action, written q · u in the literature. Since Function.End composes on the left, that is an anti-homomorphism, so the target of DFA.transitionHom is the opposite monoid (Function.End σ)ᵐᵒᵖ.

[Pin] takes automata to be partial, so its transition monoid sits in the monoid of partial transformations. DFA has a total step, so the transformations here are total and the target is Function.End σ.

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

M.transitionHom w is the transformation of states induced by the word 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)

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

M.transitionMonoid is the monoid of transformations of the states of M induced by words.

Equations

• M.transitionMonoid = MonoidHom.mrange M.transitionHom

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

M.transitionMonoidEquiv presents the transition monoid as a quotient of FreeMonoid α, by the first isomorphism theorem.

Equations

• M.transitionMonoidEquiv = Con.quotientKerEquivRange M.transitionHom

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