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

• One entry for the characterization lemmas of elements below idempotents. Label : le-idempotent Tagged Lean lemmas :

• Semigroup.RPreorder.le_idempotent
• Semigroup.LPreorder.le_idempotent
• Semigroup.HPreorder.le_idempotent Content : prove it for R and H, say L holds by a similar argument to R Dependencies : greens-relations

• One entry for the morphism preservation lemmas. Label : 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 Content : prove ≤R and 𝓡, say ≤L and 𝓛 holds by a similar argument. Then, prove ≤𝓙 and 𝓙, then ≤𝓗 and 𝓗, then 𝓓. Dependencies : greens-relations

Idempotent properties (Prop 1.4.1)

theorem Semigroup.RPreorder.le_idempotent {S : Type u_1} [Semigroup S] (x e : S) (h : IsIdempotentElem e) : x ≤𝓡 e ↔ x = e * 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] (x e : S) (h : IsIdempotentElem e) : x ≤𝓛 e ↔ x = x * e

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] (x e : S) (h : IsIdempotentElem e) : x ≤𝓗 e ↔ x = e * x ∧ x = x * e

An element is 𝓗-below an idempotent if and only if it is fixed by both left and right multiplication.

theorem Semigroup.HPreorder.le_idempotent' {S : Type u_1} [Semigroup S] (x e : S) (he : IsIdempotentElem e) : 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.