Definite and locally trivial semigroups

A semigroup is definite when each of its idempotents is a right zero, reverse definite when each is a left zero, and locally trivial when every idempotent e satisfies e * s * e = e for every s. In a finite semigroup each condition is equivalent to an equation on all sufficiently long products, which is the form in which these semigroups recognize the definite, reverse definite and generalized definite languages.

Main definitions

• Semigroup.IsDefinite, Semigroup.IsReverseDefinite, Semigroup.IsLocallyTrivial: the three conditions.

Main results

• Semigroup.IsDefinite.of_injective, .of_surjective, .prod and their mirrors: closure under subsemigroups, quotients and products.
• Semigroup.IsDefinite.isRightZero_map, Semigroup.IsReverseDefinite.isLeftZero_map, Semigroup.IsLocallyTrivial.map_mul_map_eq: in a finite semigroup satisfying the condition, every product of at least |S| elements is a right zero, a left zero, respectively absorbs anything placed between two copies of it.
• Semigroup.IsDefinite.of_isRightZero_map and its two mirrors: the converse, for any bound.

Implementation notes

Pin calls definite semigroups righty trivial and reverse definite ones lefty trivial. The long-product characterizations are Propositions XI.4.15–XI.4.17 of Pin's lecture notes.

References

• [Eil76]
• [Pin]

def Semigroup.IsDefinite (S : Type u_3) [Semigroup S] : Prop

A semigroup is definite when every idempotent is a right zero.

Equations

• Semigroup.IsDefinite S = ∀ (e : S), IsIdempotentElem e → IsRightZero e

def Semigroup.IsReverseDefinite (S : Type u_3) [Semigroup S] : Prop

A semigroup is reverse definite when every idempotent is a left zero.

Equations

• Semigroup.IsReverseDefinite S = ∀ (e : S), IsIdempotentElem e → IsLeftZero e

def Semigroup.IsLocallyTrivial (S : Type u_3) [Semigroup S] : Prop

A semigroup is locally trivial when every idempotent e absorbs anything placed between two copies of it, e * s * e = e.

Equations

• Semigroup.IsLocallyTrivial S = ∀ (e : S), IsIdempotentElem e → ∀ (s : S), e * s * e = e

Closure properties

theorem Semigroup.IsDefinite.of_injective {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] {f : S →ₙ* T} (hf : Function.Injective ⇑f) (h : IsDefinite T) : IsDefinite S

theorem Semigroup.IsReverseDefinite.of_injective {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] {f : S →ₙ* T} (hf : Function.Injective ⇑f) (h : IsReverseDefinite T) : IsReverseDefinite S

theorem Semigroup.IsLocallyTrivial.of_injective {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] {f : S →ₙ* T} (hf : Function.Injective ⇑f) (h : IsLocallyTrivial T) : IsLocallyTrivial S

theorem Semigroup.IsDefinite.prod {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] (hS : IsDefinite S) (hT : IsDefinite T) : IsDefinite (S × T)

theorem Semigroup.IsReverseDefinite.prod {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] (hS : IsReverseDefinite S) (hT : IsReverseDefinite T) : IsReverseDefinite (S × T)

theorem Semigroup.IsLocallyTrivial.prod {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] (hS : IsLocallyTrivial S) (hT : IsLocallyTrivial T) : IsLocallyTrivial (S × T)

theorem Semigroup.IsDefinite.of_surjective {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] [Finite S] {f : S →ₙ* T} (hf : Function.Surjective ⇑f) (h : IsDefinite S) : IsDefinite T

theorem Semigroup.IsReverseDefinite.of_surjective {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] [Finite S] {f : S →ₙ* T} (hf : Function.Surjective ⇑f) (h : IsReverseDefinite S) : IsReverseDefinite T

theorem Semigroup.IsLocallyTrivial.of_surjective {S : Type u_1} {T : Type u_2} [Semigroup S] [Semigroup T] [Finite S] {f : S →ₙ* T} (hf : Function.Surjective ⇑f) (h : IsLocallyTrivial S) : IsLocallyTrivial T

Long products

Each condition is equivalent to an equation on all sufficiently long products: S is definite exactly when long products are right zeros, reverse definite when they are left zeros, and locally trivial when they absorb any element placed between two copies. A product is the image of a word under a homomorphism f out of a free semigroup. One direction holds with the bound |S|, by FreeSemigroup.exists_isIdempotentElem_map_eq_mul_mul; the other holds for any bound once f is surjective, because an idempotent is the image of arbitrarily long words.

theorem Semigroup.IsDefinite.of_isRightZero_map {S : Type u_1} [Semigroup S] {α : Type u_3} {f : FreeSemigroup α →ₙ* S} {k : ℕ} (hf : Function.Surjective ⇑f) (h : ∀ (w : FreeSemigroup α), k ≤ w.length → IsRightZero (f w)) : IsDefinite S

A semigroup is definite when, for some bound, every product of at least that many elements is a right zero.

theorem Semigroup.IsReverseDefinite.of_isLeftZero_map {S : Type u_1} [Semigroup S] {α : Type u_3} {f : FreeSemigroup α →ₙ* S} {k : ℕ} (hf : Function.Surjective ⇑f) (h : ∀ (w : FreeSemigroup α), k ≤ w.length → IsLeftZero (f w)) : IsReverseDefinite S

theorem Semigroup.IsLocallyTrivial.of_map_mul_map_eq {S : Type u_1} [Semigroup S] {α : Type u_3} {f : FreeSemigroup α →ₙ* S} {k : ℕ} (hf : Function.Surjective ⇑f) (h : ∀ (w : FreeSemigroup α), k ≤ w.length → ∀ (s : S), f w * s * f w = f w) : IsLocallyTrivial S

theorem Semigroup.IsDefinite.isRightZero_map {S : Type u_1} [Semigroup S] {α : Type u_3} (f : FreeSemigroup α →ₙ* S) {w : FreeSemigroup α} [Finite S] (h : IsDefinite S) (hw : Nat.card S ≤ w.length) : IsRightZero (f w)

In a finite definite semigroup, a product of at least |S| elements is a right zero.

theorem Semigroup.IsReverseDefinite.isLeftZero_map {S : Type u_1} [Semigroup S] {α : Type u_3} (f : FreeSemigroup α →ₙ* S) {w : FreeSemigroup α} [Finite S] (h : IsReverseDefinite S) (hw : Nat.card S ≤ w.length) : IsLeftZero (f w)

In a finite reverse definite semigroup, a product of at least |S| elements is a left zero.

theorem Semigroup.IsLocallyTrivial.map_mul_map_eq {S : Type u_1} [Semigroup S] {α : Type u_3} (f : FreeSemigroup α →ₙ* S) {w : FreeSemigroup α} [Finite S] (h : IsLocallyTrivial S) (hw : Nat.card S ≤ w.length) (s : S) : f w * s * f w = f w

In a finite locally trivial semigroup, a product of at least |S| elements absorbs anything placed between two copies of it.

theorem Semigroup.IsLocallyTrivial.isIdempotentElem_map {S : Type u_1} [Semigroup S] {α : Type u_3} (f : FreeSemigroup α →ₙ* S) {w : FreeSemigroup α} [Finite S] (h : IsLocallyTrivial S) (hw : Nat.card S ≤ w.length) : IsIdempotentElem (f w)