The equation of the multitier reverse definite languages

A monoid is multitier reverse definite when it is aperiodic and every idempotent e satisfies e x e = e x. Over a finite alphabet, a language is multitier reverse definite exactly when its syntactic monoid is. This is Lambert's (62), whose monoid side is Pin's theorem as reported by Almeida: the monoids generated by the reverse definite semigroups are those satisfying x^ω y x = x^ω y, equivalently the aperiodic monoids satisfying e x e = e x, equivalently those satisfying x y₁ x y₂ ⋯ x yₙ x = x y₁ x y₂ ⋯ x yₙ for some n.

Main definitions

• Monoid.IsMultitierReverseDefinite, Monoid.multitierReverseDefiniteVariety: the aperiodic monoids whose idempotents satisfy e x e = e x.

Main results

• Monoid.isMultitierReverseDefinite_iff: in a finite monoid this is the equation x^ω y x = x^ω y.
• Monoid.IsMultitierReverseDefinite.prod_map_mul_mul_eq: the equation x y₁ x y₂ ⋯ x yₙ x = x y₁ x y₂ ⋯ x yₙ for n the size of the monoid.
• Language.isBTK_of_forall_take_filter_eq: a language decided by the length-k prefixes of the tier projections of a word is multitier reverse definite with window k.
• Language.exists_isBTK_iff: Lambert's (62).

Implementation notes

The equations of Lambert and Almeida use the omega power x^ω; isMultitierReverseDefinite_iff states the first through idempotent powers instead. Almeida leaves the proof of Pin's theorem as an exercise. The proof here goes through words: once a letter has occurred n times, where n is the size of the syntactic monoid, further occurrences leave the syntactic class unchanged, so the class of a word is determined by its first n occurrences of each letter, and these are read off the tier projections up to length n times the size of the alphabet.

References

• [Lam26]
• [Alm94]

def Monoid.IsMultitierReverseDefinite (M : Type u_1) [Monoid M] : Prop

A monoid is multitier reverse definite when it is aperiodic and every idempotent e satisfies e * x * e = e * x for every x.

Equations

• Monoid.IsMultitierReverseDefinite M = (Monoid.IsAperiodic M ∧ ∀ (e : M), IsIdempotentElem e → ∀ (x : M), e * x * e = e * x)

theorem Monoid.IsMultitierReverseDefinite.of_injective {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {f : M →* N} (hf : Function.Injective ⇑f) (h : IsMultitierReverseDefinite N) : IsMultitierReverseDefinite M

theorem Monoid.IsMultitierReverseDefinite.of_surjective {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] [Finite M] {f : M →* N} (hf : Function.Surjective ⇑f) (h : IsMultitierReverseDefinite M) : IsMultitierReverseDefinite N

theorem Monoid.IsMultitierReverseDefinite.prod {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (hM : IsMultitierReverseDefinite M) (hN : IsMultitierReverseDefinite N) : IsMultitierReverseDefinite (M × N)

theorem Monoid.IsMultitierReverseDefinite.of_subsingleton {M : Type u_1} [Monoid M] [Subsingleton M] : IsMultitierReverseDefinite M

theorem Monoid.IsMultitierReverseDefinite.mul_eq_of_mul_mul_eq {M : Type u_1} [Monoid M] (h : IsMultitierReverseDefinite M) {e x z : M} (he : IsIdempotentElem e) (hz : e * x * z = e) : e * x = e

An idempotent e absorbs every x from which it can be recovered, e * x * z = e, since in the local monoid at e the element e * x has the right inverse e * z and aperiodicity makes it the identity e.

theorem Monoid.IsMultitierReverseDefinite.prod_map_mul_mul_eq {M : Type u_1} [Monoid M] [Finite M] (h : IsMultitierReverseDefinite M) (x : M) {ys : List M} (hys : Nat.card M ≤ ys.length) : (List.map (fun (x_1 : M) => x * x_1) ys).prod * x = (List.map (fun (x_1 : M) => x * x_1) ys).prod

In a finite multitier reverse definite monoid, a product of at least |M| factors x * yᵢ absorbs a further x. Two of its first |M| + 1 prefix products coincide, so a prefix a satisfies a * u = a for a segment u beginning with x, and the idempotent power of u absorbs x.

theorem Monoid.isMultitierReverseDefinite_iff {M : Type u_1} [Monoid M] [Finite M] : IsMultitierReverseDefinite M ↔ ∀ (x y : M) (n : ℕ), n ≠ 0 → IsIdempotentElem (x ^ n) → x ^ n * y * x = x ^ n * y

A finite monoid is multitier reverse definite exactly when it satisfies Lambert's equation x^ω y x = x^ω y, stated through the idempotent powers of x.

def Monoid.multitierReverseDefiniteVariety : Pseudovariety

The pseudovariety of finite multitier reverse definite monoids.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Monoid.mem_multitierReverseDefiniteVariety {M : Type u} [Monoid M] : multitierReverseDefiniteVariety.mem M ↔ Finite M ∧ IsMultitierReverseDefinite M

Multitier reverse definite languages satisfy the equation

theorem Language.IsReverseDefinite.isMultitierReverseDefinite_syntacticMonoid {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : L.IsReverseDefinite k) : Monoid.IsMultitierReverseDefinite L.SyntacticMonoid

Over a finite alphabet, the syntactic monoid of a reverse definite language is multitier reverse definite.

theorem Language.IsBTK.mem_multitierReverseDefiniteVariety {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : IsBTK k L) : Monoid.multitierReverseDefiniteVariety.langs L

Over a finite alphabet, a multitier reverse definite language lies in the variety of the multitier reverse definite monoids.

Languages satisfying the equation are multitier reverse definite

theorem Language.isBTK_of_forall_take_filter_eq {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : ∀ (w w' : List α), (∀ (T : α → Bool), List.take k (List.filter T w) = List.take k (List.filter T w')) → (w ∈ L ↔ w' ∈ L)) : IsBTK k L

Over a finite alphabet, a language decided by the length-k prefixes of the tier projections of a word is multitier reverse definite with window k, as a finite union of intersections of tier-based reverse definite languages.

theorem Language.isBTK_of_mem_multitierReverseDefiniteVariety {α : Type u_1} {L : Language α} [Fintype α] (h : Monoid.multitierReverseDefiniteVariety.langs L) : IsBTK (Fintype.card α * Nat.card L.SyntacticMonoid) L

Over a finite alphabet, a language whose syntactic monoid is multitier reverse definite is multitier reverse definite, with window the size of the alphabet times that of the monoid. This is the converse of IsBTK.mem_multitierReverseDefiniteVariety.

theorem Language.exists_isBTK_iff {α : Type u_1} {L : Language α} [Fintype α] : (∃ (k : ℕ), IsBTK k L) ↔ Monoid.multitierReverseDefiniteVariety.langs L

Over a finite alphabet, a language is multitier reverse definite exactly when its syntactic monoid is, which is Lambert's (62).