## Stream: new members

### Topic: syntactic monoid

#### Carlos Silva (Dec 19 2021 at 00:36):

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 (Dec 19 2021 at 01:05):

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

#### Eric Wieser (Dec 19 2021 at 08:42):

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

Last updated: Dec 20 2023 at 11:08 UTC