The Location Theorem

This file proves the Location Theorem, which states that the following conditions are equivalent for x y : S where S is a semigroup:

1. x * y ∈ ⟦x⟧𝓡 ∩ ⟦y⟧𝓛
2. ⟦x⟧𝓡 ∩ ⟦y⟧𝓛 contains an idempotent element.

If the semigroup is finite, these conditions are equivalent to 3. x * y 𝓓 x (Alternatively, x * y 𝓓 y) and x 𝓓 y

Additionally, we prove that the 𝓗-class of an idempotent element is a group, and we define this as a subgroup of the underlying semigroup.

Main Definitions

• HEquiv.subgroup_of_idempotent - Given an idempotent element e : S, the 𝓗-class of e as a subgroup of S

• HEquiv.group_of_idempotent - Given an idempotent element e : S, the H-class of e as a group on the subtype {x : S // x ∈ ⟦e⟧𝓗}

Main Theorems

• DEquiv.mul_in_inter_iff_equiv - For x y : S where S is a finite semigroup, x * y is in ⟦x⟧𝓡 ∩ ⟦y⟧𝓛 iff x 𝓓 y 𝓓 x * y. This proves the equivalence of statements 1 and 3 abolve.

• mul_in_inter_iff_exists_idempotent - For x y : S, x * y is in ⟦x⟧𝓡 ∩ ⟦y⟧𝓛 iff there exists an idempotent element in ⟦x⟧𝓡 ∩ ⟦y⟧𝓛. This proves the equivalence of statments 1 and 2 above.

• DEquiv.maximal_subgroups_equiv - Two maximal subgroups of a 𝓓-class are isomorphic.

• HEquiv.hClass_of_subgroup - Every maximal subgroup is the 𝓗-class of an idempotent element.

Refrences

TODO

Blueprint

Location Theorem Lablel : lem:location-theorem Lean lemmas to tag:

• Semigroup.DEquiv.mul_in_inter_iff_equiv
• Semigroup.mul_in_inter_iff_exists_idempotent Dependencies:
• lem:d-j-theorem
• lem:j-strengthening
• lem:greens-lemma
• lem:le-idempotent

H-class of Idempotent is a Maximal Subgroup label : lem:hclass-subgroup Lean Lemmas to tag:

• Semigroup.HEquiv.subgroup_of_idempotent
• Semigroup.HEquiv.group_of_idempotent
• Semigroup.HEquiv.hClass_of_subgroup Dependencies:
• lem:location-theorem
• def:maximal-subgroup

Two Maximal Subgroups of a D-Class are Isomorphic Label: lem:maximal-subgroups-isomorphic lean lemmas to tag:

• Semigroup.DEquiv.maximal_subgroups_equiv dependencies:
• lem:hclass-subgroup

TODO

Should We prove the finite condition or just leave it talking about J equivalence?

theorem Semigroup.DEquiv.mul_in_inter_iff_equiv {S : Type u_1} [Semigroup S] (x y : S) [Finite S] : x * y ∈ ⟦x⟧𝓡 ∩ ⟦y⟧𝓛 ↔ x 𝓓 y ∧ x * y 𝓓 x

In Finite semigroups, x * y is in the intersection of the 𝓡-class of x and the 𝓛-class of y iff x, y, and x * y are 𝓓-Equivalent.

theorem Semigroup.mul_in_inter_iff_exists_idempotent {S : Type u_1} [Semigroup S] (x y : S) : x * y ∈ ⟦x⟧𝓡 ∩ ⟦y⟧𝓛 ↔ ∃ (e : S), IsIdempotentElem e ∧ e ∈ ⟦y⟧𝓡 ∩ ⟦x⟧𝓛

x * y is 𝓡-equivalent to x and 𝓛-equivalent to y iff there exists an idempotent element in the intersection of the 𝓡-class of y and the 𝓛-class of x.

theorem Semigroup.HEquiv.mul_closed_of_idempotent {S : Type u_1} [Semigroup S] {e x y : S} (he : IsIdempotentElem e) (hx : x ∈ ⟦e⟧𝓗) (hy : y ∈ ⟦e⟧𝓗) : x * y ∈ ⟦e⟧𝓗

Idempotent-containing 𝓗-classes are closed under multiplication.

theorem Semigroup.HEquiv.idempotent_mul {S : Type u_1} [Semigroup S] {e : S} (he : IsIdempotentElem e) {x : S} (hx : x ∈ ⟦e⟧𝓗) : e * x = x

For all elements in the 𝓗-class of an idempotent, that idempotent acts as a left identity.

theorem Semigroup.HEquiv.mul_idempotent {S : Type u_1} [Semigroup S] {e : S} (he : IsIdempotentElem e) {x : S} (hx : x ∈ ⟦e⟧𝓗) : x * e = x

For all elements in the 𝓗-class of an idempotent, that idempotent acts as a right identity.

theorem Semigroup.HEquiv.idempotent_eq {S : Type u_1} [Semigroup S] {e x : S} (hh : x 𝓗 e) (he : IsIdempotentElem e) (hx : IsIdempotentElem x) : e = x

All idempotent elements in an 𝓗 class are equal.

theorem Semigroup.HEquiv.exists_inverse_of_idempotent {S : Type u_1} [Semigroup S] {e x : S} (he : IsIdempotentElem e) (hh : x ∈ ⟦e⟧𝓗) : ∃ (y : S), y 𝓗 e ∧ x * y = e ∧ y * x = e

The 𝓗-class of an idempotent element is closed under inverses.

noncomputable def Semigroup.HEquiv.subgroup_of_idempotent {S : Type u_1} [Semigroup S] {e : S} (he : IsIdempotentElem e) : Subgroup S

The 𝓗-class of an idempotent element as a subgroup of the semigroup.

Equations

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

@[simp]

theorem Semigroup.HEquiv.subgroup_of_idempotent_carrier_def {S : Type u_1} [Semigroup S] {e : S} (he : IsIdempotentElem e) : (subgroup_of_idempotent he).carrier = ⟦e⟧𝓗

noncomputable instance Semigroup.HEquiv.group_of_idempotent {S : Type u_1} [Semigroup S] {e : S} (he : IsIdempotentElem e) : Group ↥(subgroup_of_idempotent he)

The 𝓗-class of a semigroup as a Group on the subtype {x : S // x ∈ ⟦e⟧𝓗}

Equations

• Semigroup.HEquiv.group_of_idempotent he = inferInstance

noncomputable instance Semigroup.HEquiv.group_of_idempotent' {S : Type u_1} [Semigroup S] {e : S} (he : IsIdempotentElem e) : Group { x : S // x ∈ ⟦e⟧𝓗 }

The 𝓗-class of a semigroup as a Group on the subtype {x : S // x ∈ ⟦e⟧𝓗}

Equations

• Semigroup.HEquiv.group_of_idempotent' he = Semigroup.HEquiv.group_of_idempotent he

theorem Semigroup.HEquiv.idempotent_in_subgroup {S : Type u_1} [Semigroup S] {x y : S} (h₁ : x 𝓗 y) (h₂ : x * y 𝓗 x) : ∃ (e : S), e 𝓗 x ∧ IsIdempotentElem e

If there exists an x, y in an 𝓗 class such that x * y remains in the 𝓗-class, then that 𝓗 class contains an idempotent.

theorem Semigroup.DEquiv.idempotent_in_rClass {S : Type u_1} [Semigroup S] {e x : S} (he : IsIdempotentElem e) (hx : x 𝓓 e) : ∃ f ∈ ⟦x⟧𝓡, IsIdempotentElem f

If a 𝓓-class contains an idempotent, it contains at least one idempotent in each 𝓡-class.

theorem Semigroup.DEquiv.idempotent_in_lClass {S : Type u_1} [Semigroup S] {e x : S} (he : IsIdempotentElem e) (hx : x 𝓓 e) : ∃ f ∈ ⟦x⟧𝓛, IsIdempotentElem f

If a 𝓓-class contains an idempotent, it contains at least one idempotent in each 𝓛-class.

theorem Semigroup.HEquiv.ofSubgroup {S : Type u_1} [Semigroup S] {x y : S} {H : Subgroup S} (hx : x ∈ H) (hy : y ∈ H) : x 𝓗 y

All elements within a subgroup are 𝓗-related.

theorem Semigroup.HEquiv.hClass_of_subgroup {S : Type u_1} [Semigroup S] {H : Subgroup S} (hH : H.isMaximal) : ∃ (e : S), IsIdempotentElem e ∧ H.carrier = ⟦e⟧𝓗

A maximal subgroup is the 𝓗-class of an idempotent.

theorem Semigroup.DEquiv.bij_on_hClass {S : Type u_1} [Semigroup S] {e f s t : S} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (hr : e 𝓡 s) (hl : s 𝓛 f) (ht : t * s = f) : Set.BijOn (fun (x : S) => t * x * s) ⟦e⟧𝓗 ⟦f⟧𝓗

Let e f : S be idempotent elements. Let e 𝓓 f such that we have a s with e 𝓡 s and s 𝓛 f. Let t be the witness of f ≤𝓛 s such that t * s = f. Then, the map x ↦ t * x * s is a bijection from the 𝓗-class of e to the 𝓗-class of f.

theorem Semigroup.DEquiv.bij_on_hClass_map_mul {S : Type u_1} [Semigroup S] {e f s t x y : S} : IsIdempotentElem e → ∀ (hf : IsIdempotentElem f) (hr : e 𝓡 s) (hl : s 𝓛 f) (ht : t * s = f), x 𝓗 e → ∀ (hy : y 𝓗 e), (fun (x : S) => t * x * s) x * (fun (x : S) => t * x * s) y = (fun (x : S) => t * x * s) (x * y)

Let e f : S be idempotent elements. Let e 𝓓 f such that we have a s with e 𝓡 s and s 𝓛 f. Let t be the witness of f ≤𝓛 s such that t * s = f. let u be the witness of e ≤𝓡 s such that s * u = e. Then, the map x ↦ t * x * s is a bijection which preserves multiplication (like a morphism).

noncomputable def Semigroup.DEquiv.hClass_equiv' {S : Type u_1} [Semigroup S] {e f s t : S} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (hr : e 𝓡 s) (hl : s 𝓛 f) (ht : t * s = f) : ↥(HEquiv.subgroup_of_idempotent he) ≃* ↥(HEquiv.subgroup_of_idempotent hf)

For idempotents e, f, with e 𝓓 f such that e 𝓡 s and s 𝓛 f such that t * s = f, the isomorphism between ⟦e⟧𝓗 and ⟦f⟧𝓗

Equations

• Semigroup.DEquiv.hClass_equiv' he hf hr hl ht = (Semigroup.HEquiv.subgroup_of_idempotent he).hom_of_bijOn (Semigroup.HEquiv.subgroup_of_idempotent hf) (fun (x : S) => t * x * s) ⋯ ⋯

theorem Semigroup.DEquiv.hClass_equiv {S : Type u_1} [Semigroup S] {e f : S} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (hd : e 𝓓 f) : Nonempty (↥(HEquiv.subgroup_of_idempotent he) ≃* ↥(HEquiv.subgroup_of_idempotent hf))

For idempotents e, f, if e 𝓓 f, then ⟦e⟧𝓗 and ⟦f⟧𝓗 are isomorphic subgroups.

theorem Semigroup.DEquiv.maximal_subgroups_equiv {S : Type u_1} [Semigroup S] {x y : S} {H K : Subgroup S} (hH : H.isMaximal) (hK : K.isMaximal) (hx : x ∈ H) (hy : y ∈ K) (hd : x 𝓓 y) : Nonempty (↥H ≃* ↥K)

Two maximal subgroups of a 𝓓-class are isomorphic.

theorem Semigroup.isRegularElem_of_idempotent {S : Type u_2} [Semigroup S] {e : S} (he : IsIdempotentElem e) : isRegularElem e

theorem Semigroup.mulOpposite_rEquiv_of_lEquiv {S : Type u_2} [Semigroup S] {e x : S} (h : e 𝓛 x) : MulOpposite.op e 𝓡 MulOpposite.op x

In MulOpposite S, 𝓡 for op-images matches 𝓛 in S.

theorem Semigroup.exists_idempotent_r_of_isRegularElem {S : Type u_2} [Semigroup S] {x : S} (hx : isRegularElem x) : ∃ (e : S), IsIdempotentElem e ∧ e 𝓡 x

If x is regular then ⟦x⟧𝓡 contains an idempotent (x * y for a witness x * y * x = x).

theorem Semigroup.exists_idempotent_l_of_isRegularElem {S : Type u_2} [Semigroup S] {x : S} (hx : isRegularElem x) : ∃ (e : S), IsIdempotentElem e ∧ e 𝓛 x

If x is regular then ⟦x⟧𝓛 contains an idempotent (y * x for a witness x * y * x = x).

theorem Semigroup.isRegularElem_of_exists_idempotent_r {S : Type u_2} [Semigroup S] {x : S} (h : ∃ (e : S), IsIdempotentElem e ∧ e 𝓡 x) : isRegularElem x

If the 𝓡-class of x contains an idempotent, then x is regular.

theorem Semigroup.isRegularElem_of_exists_idempotent_l {S : Type u_2} [Semigroup S] {x : S} (h : ∃ (e : S), IsIdempotentElem e ∧ e 𝓛 x) : isRegularElem x

If the 𝓛-class of x contains an idempotent, then x is regular.

theorem Semigroup.isRegularElem_of_rEquiv {S : Type u_2} [Semigroup S] {x y : S} (h : x 𝓡 y) (hx : isRegularElem x) : isRegularElem y

theorem Semigroup.isRegularElem_of_lEquiv {S : Type u_2} [Semigroup S] {x y : S} (h : x 𝓛 y) (hx : isRegularElem x) : isRegularElem y

theorem Semigroup.isRegularElem_of_dEquiv {S : Type u_2} [Semigroup S] {x y : S} (hd : x 𝓓 y) (hx : isRegularElem x) : isRegularElem y

Regularity propagates within a 𝓓-class.

def Semigroup.DEquiv.regularClass {S : Type u_2} [Semigroup S] (d : S) : Prop

Equations

• Semigroup.DEquiv.regularClass d = ∀ (x : S), x 𝓓 d → Semigroup.isRegularElem x

def Semigroup.DEquiv.hasIdempotent {S : Type u_2} [Semigroup S] (d : S) : Prop

Equations

• Semigroup.DEquiv.hasIdempotent d = ∃ (e : S), e 𝓓 d ∧ IsIdempotentElem e

theorem Semigroup.DEquiv.regularClass_iff_exists_regular {S : Type u_2} [Semigroup S] (d : S) : regularClass d ↔ ∃ (x : S), x 𝓓 d ∧ isRegularElem x

(i) ↔ (ii) There is at least one regular element 𝓓-related to d.

theorem Semigroup.DEquiv.regularClass_iff_forall_rClass_idem {S : Type u_2} [Semigroup S] (d : S) : regularClass d ↔ ∀ (x : S), x 𝓓 d → ∃ (e : S), IsIdempotentElem e ∧ e 𝓡 x

(i) ↔ (iii) Each 𝓡-class that meets the class contains an idempotent.

theorem Semigroup.DEquiv.regularClass_iff_forall_lClass_idem {S : Type u_2} [Semigroup S] (d : S) : regularClass d ↔ ∀ (x : S), x 𝓓 d → ∃ (e : S), IsIdempotentElem e ∧ e 𝓛 x

(i) ↔ (iv) Each 𝓛-class that meets the class contains an idempotent.

theorem Semigroup.DEquiv.regularClass_iff_hasIdempotent {S : Type u_2} [Semigroup S] (d : S) : regularClass d ↔ hasIdempotent d

theorem Semigroup.DEquiv.forall_rClass_idem_iff_hasIdempotent {S : Type u_2} [Semigroup S] (d : S) : (∀ (x : S), x 𝓓 d → ∃ (e : S), IsIdempotentElem e ∧ e 𝓡 x) ↔ hasIdempotent d

(iii) ↔ (v) (each 𝓡-class has an idempotent vs. some idempotent in the class).

theorem Semigroup.DEquiv.forall_lClass_idem_iff_hasIdempotent {S : Type u_2} [Semigroup S] (d : S) : (∀ (x : S), x 𝓓 d → ∃ (e : S), IsIdempotentElem e ∧ e 𝓛 x) ↔ hasIdempotent d

(iv) ↔ (v)

theorem Semigroup.DEquiv.hasIdempotent_iff_exists_regular {S : Type u_2} [Semigroup S] (d : S) : hasIdempotent d ↔ ∃ (x : S), x 𝓓 d ∧ isRegularElem x

(v) ↔ (ii)

theorem Semigroup.DEquiv.hasIdempotent_iff_pair_product_in_class {S : Type u_2} [Semigroup S] [Finite S] (d : S) : hasIdempotent d ↔ ∃ (x : S) (y : S), x 𝓓 d ∧ y 𝓓 d ∧ x * y 𝓓 d

(v) ↔ (vi) for finite semigroups: there exist x, y in the class with x * y still in the class

theorem Semigroup.DEquiv.regular_d_class_tfae {S : Type u_2} [Semigroup S] [Finite S] (d : S) : [regularClass d, ∃ (x : S), x 𝓓 d ∧ isRegularElem x, ∀ (x : S), x 𝓓 d → ∃ (e : S), IsIdempotentElem e ∧ e 𝓡 x, ∀ (x : S), x 𝓓 d → ∃ (e : S), IsIdempotentElem e ∧ e 𝓛 x, hasIdempotent d, ∃ (x : S) (y : S), x 𝓓 d ∧ y 𝓓 d ∧ x * y 𝓓 d].TFAE