Basic Properties of Green's Relations

This file proves basic properties about Green's relations and idempotent elements.

We also prove that Green's relations are preserved under morphisms.

Main theorems

Characterizations of elements that are 𝓡-below, 𝓛-below, or 𝓗-below an idempotent:

• Semigroup.RPreorder.le_idempotent - x ≤𝓡 e ↔ x = e * x.
• Semigroup.LPreorder.le_idempotent - x ≤𝓛 e ↔ x = x * e.
• Semigroup.HPreorder.le_idempotent - x ≤𝓗 e ↔ x = e * x ∧ x = x * e.

Green's relations are preserved under semigroup morphisms f:

• Semigroup.RPreorder.hom_pres - x ≤𝓡 y → f x ≤𝓡 f y.
• Semigroup.LPreorder.hom_pres - x ≤𝓛 y → f x ≤𝓛 f y.
• Semigroup.JPreorder.hom_pres - x ≤𝓙 y → f x ≤𝓙 f y.
• Semigroup.HPreorder.hom_pres - x ≤𝓗 y → f x ≤𝓗 f y.
• Semigroup.REquiv.hom_pres - x 𝓡 y → f x 𝓡 f y.
• Semigroup.LEquiv.hom_pres - x 𝓛 y → f x 𝓛 f y.
• Semigroup.JEquiv.hom_pres - x 𝓙 y → f x 𝓙 f y.
• Semigroup.HEquiv.hom_pres - x 𝓗 y → f x 𝓗 f y.
• Semigroup.DEquiv.hom_pres - x 𝓓 y → f x 𝓓 f y.

References

TODO

Blueprint

• Characterization of Elements Below Idempotents Label : lem:le-idempotent Tagged Lean lemmas :

• Semigroup.RPreorder.le_idempotent
• Semigroup.LPreorder.le_idempotent
• Semigroup.HPreorder.le_idempotent Dependencies : def:greens-relations

• Preservation of Green's Relations by Morphisms Label : lem:greens-relations-hom-pres Tagged Lean lemmas :

• Semigroup.RPreorder.hom_pres
• Semigroup.LPreorder.hom_pres
• Semigroup.JPreorder.hom_pres
• Semigroup.HPreorder.hom_pres
• Semigroup.REquiv.hom_pres
• Semigroup.LEquiv.hom_pres
• Semigroup.JEquiv.hom_pres
• Semigroup.HEquiv.hom_pres
• Semigroup.DEquiv.hom_pres Then, prove ≤𝓙 and 𝓙, then ≤𝓗 and 𝓗, then 𝓓. Dependencies : def:greens-relations

Idempotent properties (Prop 1.4.1)

theorem Semigroup.RPreorder.le_idempotent {S : Type u_1} [Semigroup S] {e : S} (h : IsIdempotentElem e) (x : S) : x ≤𝓡 e ↔ e * x = x

An element x is 𝓡-below an idempotent e if and only if x = e * x.

theorem Semigroup.LPreorder.le_idempotent {S : Type u_1} [Semigroup S] {e : S} (h : IsIdempotentElem e) (x : S) : x ≤𝓛 e ↔ x * e = x

An element x is 𝓛-below an idempotent e if and only if x = x * e.

theorem Semigroup.HPreorder.le_idempotent {S : Type u_1} [Semigroup S] {e : S} (he : IsIdempotentElem e) (x : S) : x ≤𝓗 e ↔ e * x * e = x

An element is 𝓗-below an idempotent if and only if it is a sandwich fixed point.

Morphisms

We prove that all of Green's preorders and equivalences are preserved under morphisms. Note that these should quantify over MulHomClass.

theorem Semigroup.RPreorder.hom_pres {S : Type u_2} {T : Type u_3} [Semigroup S] [Semigroup T] {F : Type u_4} [FunLike F S T] [MulHomClass F S T] (f : F) (x y : S) (h : x ≤𝓡 y) : f x ≤𝓡 f y

The 𝓡-preorder is preserved by semigroup morphisms.

theorem Semigroup.LPreorder.hom_pres {S : Type u_2} {T : Type u_3} [Semigroup S] [Semigroup T] {F : Type u_4} [FunLike F S T] [MulHomClass F S T] (f : F) (x y : S) (h : x ≤𝓛 y) : f x ≤𝓛 f y

The 𝓛-preorder is preserved by semigroup morphisms.

theorem Semigroup.JPreorder.hom_pres {S : Type u_2} {T : Type u_3} [Semigroup S] [Semigroup T] {F : Type u_4} [FunLike F S T] [MulHomClass F S T] (f : F) (x y : S) (h : x ≤𝓙 y) : f x ≤𝓙 f y

The 𝓙-preorder is preserved by semigroup morphisms.

theorem Semigroup.HPreorder.hom_pres {S : Type u_2} {T : Type u_3} [Semigroup S] [Semigroup T] {F : Type u_4} [FunLike F S T] [MulHomClass F S T] (f : F) (x y : S) (h : x ≤𝓗 y) : f x ≤𝓗 f y

The 𝓗-preorder is preserved by semigroup morphisms.

theorem Semigroup.REquiv.hom_pres {S : Type u_2} {T : Type u_3} [Semigroup S] [Semigroup T] {F : Type u_4} [FunLike F S T] [MulHomClass F S T] (f : F) (x y : S) (h : x 𝓡 y) : f x 𝓡 f y

The 𝓡 equivalence is preserved by semigroup morphisms.

theorem Semigroup.LEquiv.hom_pres {S : Type u_2} {T : Type u_3} [Semigroup S] [Semigroup T] {F : Type u_4} [FunLike F S T] [MulHomClass F S T] (f : F) (x y : S) (h : x 𝓛 y) : f x 𝓛 f y

The 𝓛 equivalence is preserved by semigroup morphisms.

theorem Semigroup.JEquiv.hom_pres {S : Type u_2} {T : Type u_3} [Semigroup S] [Semigroup T] {F : Type u_4} [FunLike F S T] [MulHomClass F S T] (f : F) (x y : S) (h : x 𝓙 y) : f x 𝓙 f y

The 𝓙 equivalence is preserved by semigroup morphisms.

theorem Semigroup.HEquiv.hom_pres {S : Type u_2} {T : Type u_3} [Semigroup S] [Semigroup T] {F : Type u_4} [FunLike F S T] [MulHomClass F S T] (f : F) (x y : S) (h : x 𝓗 y) : f x 𝓗 f y

The 𝓗 equivalence is preserved by semigroup morphisms.

theorem Semigroup.DEquiv.hom_pres {S : Type u_2} {T : Type u_3} [Semigroup S] [Semigroup T] {F : Type u_4} [FunLike F S T] [MulHomClass F S T] (f : F) (x y : S) (h : x 𝓓 y) : f x 𝓓 f y

The 𝓓 equivalence is preserved by semigroup morphisms.