Finite Semigroups and Green's Relations

This file proves lemmas about Green's relations in finite semigroups.

Main theorems

All the following lemmas assume S is a finite semigroup.

• Semigroup.dEquiv_iff_jEquiv - x 𝓓 y ↔ x 𝓙 y.
• Semigroup.REquiv.of_rPreorder_and_jEquiv - If x 𝓙 y and x ≤𝓡 y, then x 𝓡 y.
• Semigroup.LEquiv.of_lPreorder_and_jEquiv - If x 𝓙 y and x ≤𝓛 y, then x 𝓛 y.
• Semigroup.HEquiv.of_eq_sandwich - If x = u * x * v, then x 𝓗 u * x ∧ x 𝓗 x * v.

References

TODO

Blueprint

• Equivalence of 𝓓 and 𝓙 in Finite Semigroups Label : lem:d-j-theorem Lean lemmas to tag :

  • Semigroup.JEquiv.to_dEquiv
  • Semigroup.dEquiv_iff_jEquiv Dependencies : lem:exists-pow-sandwich, def:greens-relations

• J-Equivalence Strengthening Preorders Label : lem:j-strengthening Lean lemmas to tag :

  • Semigroup.REquiv.of_rPreorder_and_jEquiv
  • Semigroup.LEquiv.of_lPreorder_and_jEquiv Dependencies : lem:exists-pow-sandwich, def:greens-relations

• H-Equivalence from Sandwiching Label : lem:h-of-sandwich Lean lemmas to tag :

  • Semigroup.HEquiv.of_eq_sandwich Dependencies : lem:j-strengthening, lem:exists-pow-sandwich, def:greens-relations

The D-J Theorem for Finite Semigroups

instance WithOne.finite {S : Type u_1} [Finite S] : Finite (WithOne S)

If S is finite, then WithOne S is also finite.

@[simp]

theorem Semigroup.JEquiv.to_dEquiv {S : Type u_1} [Semigroup S] [Finite S] {x y : S} (hj : x 𝓙 y) : x 𝓓 y

In finite semigroups, 𝓙-equivalence implies 𝓓-equivalence.

theorem Semigroup.dEquiv_iff_jEquiv {S : Type u_1} [Semigroup S] [Finite S] {x y : S} : x 𝓓 y ↔ x 𝓙 y

In finite semigroups, the 𝓓-relation equals the 𝓙-relation.

Properties relating J, L, and R (Proposition 1.4.2 and 1.4.4)

This section shows how 𝓙-equivalence "strengthens" 𝓡 and 𝓛 preorders to equivalences in finite semigroups.

theorem Semigroup.REquiv.of_jEquiv_mul_right {S : Type u_1} [Semigroup S] [Finite S] {x y : S} (hj : x 𝓙 x * y) : x 𝓡 x * y

In finite semigroups, 𝓙-equivalence with a right product gives 𝓡-equivalence.

theorem Semigroup.LEquiv.of_jEquiv_mul_left {S : Type u_1} [Semigroup S] [Finite S] {x y : S} (hj : x 𝓙 y * x) : x 𝓛 y * x

In finite semigroups, 𝓙-equivalence with a left product gives 𝓛-equivalence.

theorem Semigroup.REquiv.of_rPreorder_and_jEquiv {S : Type u_1} [Semigroup S] [Finite S] {x y : S} (hr : x ≤𝓡 y) (hj : x 𝓙 y) : x 𝓡 y

In finite semigroups, 𝓙-equivalence strengthens the 𝓡-preorder to 𝓡-equivalence.

theorem Semigroup.LEquiv.of_lPreorder_and_jEquiv {S : Type u_1} [Semigroup S] [Finite S] {x y : S} (hl : x ≤𝓛 y) (hj : x 𝓙 y) : x 𝓛 y

In finite semigroups, 𝓙-equivalence strengthens the 𝓛-preorder to 𝓛-equivalence.

Theorems about 𝓗

theorem Semigroup.HEquiv.of_eq_sandwich {S : Type u_1} [Semigroup S] [Finite S] {x u v : S} (h : u * x * v = x) : x 𝓗 u * x ∧ x 𝓗 x * v

In finite semigroups, an element sandwiched between two factors is 𝓗-related to its left and right partial products.