syntactic monoid

Stream: new members

[Carlos Silva]

Hello. I defined the syntactic monoid in lean. I did this without asking about it, so I hope I am not just repeating what has already been done. If this is mostly good, can I get write access to a branch? My github name is carlosa95silva.

A transition monoid is the monoid created by the action of an alphabet on an automaton. The syntactic monoid is monoid corresponding to the minimal automaton. I also defined the syntactic congruence and saturated relations.

I don't know how to split this up. I could put the syntactic and transition monoids in the computability folder, but the syntactic congruence is a congruence and might belong elsewhere. Thank you for any advice.

import computability.DFA
import group_theory.subgroup.basic
import group_theory.congruence

section t_section

universes u v
variables (A : Type u) (σ : Type v)

/--Each letter of the alphabet induces a function on the states.-/
def transition_function (X : DFA A σ) : A → (function.End σ):= λ(a : A),λ(s : σ), X.eval_from s [a]

def transition_morphism (X : DFA A σ) := free_monoid.lift (transition_function A σ X)

/--The transition monoid is the range of the transition_morphism. -/
def transition_monoid (X : DFA A σ) := monoid_hom.mrange(transition_morphism A σ X)

theorem transition_monoid_elements (X : DFA A σ) : (transition_monoid A σ X).carrier =
  { f | ∃ (w : list A), f = (transition_morphism A σ X) w } :=
begin
  refine set.ext _,
  intro f,
  split,
  { intro hf,
    cases hf,
    exact Exists.intro hf_w (eq.symm hf_h)},
  intro hf,
  cases hf,
  exact Exists.intro hf_w (eq.symm hf_h),
end

end t_section

universes u v
variables {X : Type u} {Y : Type v}

def syntactic_congruence [G : semigroup X] (S : set X) : X → X → Prop :=
λ(a1 : X),λ(a2 : X), ∀ (x y : X), (x*a1*y ∈ S) ↔ (x*a2*y ∈ S)

theorem syntactic.equivalence [G : semigroup X] (S : set X) : equivalence (syntactic_congruence S) :=
begin
  unfold syntactic_congruence equivalence,
  repeat {split},
  { unfold reflexive,
    intros a1 x y,
    apply iff.rfl},
  { unfold symmetric,
    intros a1 a2,
    introv h1,
    exact iff.symm(h1 x y)},
  { unfold transitive,
    intros a1 a2 a3,
    introv h1 h2,
    exact iff.trans (h1 x y) (h2 x y)}
end

def syntactic_setoid [G : semigroup X] (S : set X) : setoid X := ⟨syntactic_congruence S, syntactic.equivalence S⟩

theorem syntactic.mul [G : semigroup X] (S : set X) : ∀ (w x y z : X),
(syntactic_setoid S).rel w x → (syntactic_setoid S).rel y z → (syntactic_setoid S).rel (w * y) (x * z) :=
begin
  intros a1 a2 a3 a4,
  unfold syntactic_setoid syntactic_congruence,
  intros h1 h2 x y,
  specialize h1 x (a3*y),
  specialize h2 (x*a2) y,
  simp only [mul_assoc] at *,
  exact iff.trans h1 h2,
end

def syntactic_con [G : semigroup X] (S : set X) : con X := ⟨syntactic_setoid S, syntactic.mul S⟩

def syntactic_monoid [M : monoid X] (S : set X) := (syntactic_con S).quotient

def saturated (r : X → X → Prop) (L : set X) : Prop := ∀ (x y : X), (x ∈ L ∧ r x y) → y ∈ L

/--The syntactic congruence of L in a monoid X saturates L. -/
theorem syntactic.sat [M : monoid X] (L : set X) : saturated (syntactic_con L).r L :=
begin
  unfold saturated,
  introv h,
  cases h with hS hr,
  simp only [con.rel_eq_coe] at hr,
  unfold syntactic_con syntactic_setoid syntactic_congruence at hr,
  simp only [propext con.rel_mk] at hr,
  specialize hr 1 1,
  simp only [mul_one, one_mul] at hr,
  apply hr.1 hS,
end

/--Let L be a subset of a monoid X. Any congruence K that saturates L is finer than the syntactic congruence.-/
theorem syntactic.finest [M : monoid X] (L : set X) (K : con X) (hK: saturated K L) : K ≤ syntactic_con L :=
begin
  intros x y hkxy a b,
  have h1 : K (a*x*b) (a*y*b) :=
  begin
    repeat {apply K.mul},
    repeat {apply K.refl},
    exact hkxy,
  end,
  have h2 : K  (a*y*b) (a*x*b) := con.symm K h1,
  unfold saturated at hK,
  have hK2 : ∀ (x y : X), x ∈ L ∧ K x y → y ∈ L := by exact hK,
  specialize hK (a*x*b) (a*y*b),
  specialize hK2 (a*y*b) (a*x*b),
  simp only [h1, h2, and_true] at hK hK2,
  refine ⟨hK, hK2⟩,
end

[Yaël Dillies]

Looks pretty good! This does not duplicate anybody's work as far as I'm aware.

[Eric Wieser]

Some quick feedback would be to try to move arguments before the colons