Ideals

This file defines Left/Right/Two-sided ideals in magmas as bundled Set-Like structures. We also provide functions that return the minimum ideal containing a set/element in semigroups.

We also give an ideal-based characterization of Green's Relations in semigroups.

We also define typeclasses for simple, zero-simple, and regular semigroups.

Main Definitions

• LeftIdeal - A Set-Like structure for sets closed under left multiplication.

• LeftIdeal.inter - The intersection of two ideals as an ideal.

• LeftIdeal.ofSet - The minimum left ideal containing a set.

• RightIdeal - A Set-Like structure for sets closed under right multiplication.

• RightIdeal.inter - The intersection of two ideals as an ideal.

• RightIdeal.ofSet - The minimum right ideal containing a set.

• Ideal' - A Set-Like structure for sets closed under multiplication.

• Ideal'.inter - The intersection of two ideals as an ideal.

• Ideal'.ofSet - The minimum ideal containing a set.

• SimpleSemigroup - A class that extends Semigroup with a proof that all ideals are empty or full.

• ZeroSimpleSemigroup - A class that entends SemigroupWithZero with a proof that all ideas are empty, full, or the zero ideal.

• JPreorder.toSimpleSemigroup - Given that all elements of a semigroup are 𝓙-preorder related, an instance for SimpleSemigroup

• JPreorder.toZeroSimpleSemigroup - Given that all non-zero elements of a semigroup with zero are 𝓙-preorder related, an instance for ZeroSimpleSemigroup

• isRegularElem is a predicate on elements x in a magma stating that there exists a y such that x * y * x = x.

• RegularSemigroup is a class extending Semigroup with a proof that every element is regular.

Main Theorems

• LeftIdeal.mem - Left Ideals are closed under left multiplication.
• RightIdeal.mem - Right Ideals are closed under right multiplication.
• Ideal'.mul_left_mem - Ideals are closed under left multiplication.
• Ideal'.mul_right_mem - Ideals are closed under right multiplication.
• Ideal'.mem - Ideals are closed under two-sided multiplication.

Let x y be elements of a semigroup S

• LPreorder.iff_in_leftIdeal - x is in the principal Left Ideal of y iff x ≤𝓛 y.

• RPreorder.iff_in_rightIdeal - x is in the principal right ideal of y iff x ≤𝓡 y.

• JPreorder.iff_in_ideal' - x is in the principal Ideal of y iff x ≤𝓙 y.

• LPreorder.le_in_leftIdeal - if x is in a left Ideal and y ≤𝓛 x then y is in the left ideal too.

• RPreorder.le_in_rightIdeal - if x is in a right Ideal and y ≤𝓡 x then y is in that right ideal too.

• JPreorder.le_in_ideal' - if x is in an Ideal and y ≤𝓙 x then y is in that ideal too.

• LPreorder.iff_leftIdeal_subset - The principal left ideal of x is a subset of that of y iff x ≤𝓛 y.

• RPreorder.iff_rightIdeal_subset - The principal right ideal of x is a subset of that of y iff x ≤𝓡 y.

• JPreorder.iff_ideal'_subset - The principal ideal of x is a subset of that of y iff x ≤𝓡 y.

• LEquiv.iff_leftIdeal_eq - The principal left ideal of x is equal to that of y iff x ≤𝓛 y.

• REquiv.iff_rightIdeal_eq - The principal right ideal of x is equal to that of y iff x ≤𝓡 y.

• JEquiv.iff_ideal'_eq - The principal ideal of x is equal to that of y iff x ≤𝓡 y.

• SimpleSemigroup.ideal - Given a SimpleSemigroup instance, all ideals are empty or full.

• ZeroSimpleSemigroup.ideal - Given a ZeroSimpleSemigroup instance, all ideals are empty, full, or the zero ideal.

• JEquiv.ofSimple - Given a SimpleSemigroup instance, all elements are 𝓙-equivalent.

• JPreorder.ofZeroSimple - Given a ZeroSimpleSemigroup instance, all non-zero elements are 𝓙-preorder related.

• RegularSemigroup.regular - Given an instance of RegularSemigroup, for all x there exists a y such that x * y * x = x

Notation

• ⊤, ∅ or {} : Ideal' α refer to the full and empty ideals, respectively.
• Given [MulZeroClass α], ⊥ represents the left/right/two-sided ideal {0}

For p, q : Ideal' α:

• p ∩ q : Ideal α denotes their intersection.
• p ≤ q is notation for (p : Set α) ⊆ (q : Set α)

Implementation Notes

The SetLike implementation is from the template in the docstring of Mathlib.Data.Setlike.Basic.

For an p : Ideal' α and x : α, the notation x ∈ (p : Set S) is perfered over x ∈ p.carrier and this is supported by tagging the mem_carrier lemmas with @[simp].

For principal ideals, use Ideal'.ofSet {x}.

TODO

Prove that ideals are stable under surjective morphisms and inverses of morphisms Prove that a semigroup has at most one minimal ideal

structure LeftIdeal (α : Type u_1) [Mul α] : Type u_1

A Left Ideal is a set X such that ∀ y, ∀ x ∈ X, y * x ∈ X.

• carrier : Set α
• mul_mem_mem {x : α} (hin : x ∈ self.carrier) (y : α) : y * x ∈ self.carrier

instance LeftIdeal.instSetLike {α : Type u_1} [Mul α] : SetLike (LeftIdeal α) α

SetLike instance requires we prove that there is an injection from LeftIdeal → Set. It regesters a coersion to Set and provides various simp lemmas and instances.

Equations

• LeftIdeal.instSetLike = { coe := LeftIdeal.carrier, coe_injective' := ⋯ }

@[simp]

theorem LeftIdeal.mem_carrier {α : Type u_1} [Mul α] {p : LeftIdeal α} {x : α} : x ∈ p.carrier ↔ x ∈ ↑p

theorem LeftIdeal.mem_coe {α : Type u_1} [Mul α] {p : LeftIdeal α} {x : α} : x ∈ ↑p ↔ x ∈ p

theorem LeftIdeal.ext {α : Type u_1} [Mul α] {p q : LeftIdeal α} (h : ∀ (x : α), x ∈ p ↔ x ∈ q) : p = q

This allows us to use the ext tactic

theorem LeftIdeal.ext_iff {α : Type u_1} [Mul α] {p q : LeftIdeal α} : p = q ↔ ∀ (x : α), x ∈ p ↔ x ∈ q

@[simp]

theorem LeftIdeal.mem {α : Type u_1} [Mul α] {x y : α} {p : LeftIdeal α} (hin : x ∈ p) : y * x ∈ p

instance LeftIdeal.instEmptyCollection {α : Type u_1} [Mul α] : EmptyCollection (LeftIdeal α)

Allows for notation ∅ : LeftIdeal α for the empty ideal.

Equations

• LeftIdeal.instEmptyCollection = { emptyCollection := { carrier := ∅, mul_mem_mem := ⋯ } }

@[simp]

theorem LeftIdeal.coe_empty {α : Type u_1} [Mul α] : ↑∅ = ∅

instance LeftIdeal.instTop {α : Type u_1} [Mul α] : Top (LeftIdeal α)

Allows for notation ⊤ : LeftIdeal α for the full ideal.

Equations

• LeftIdeal.instTop = { top := { carrier := Set.univ, mul_mem_mem := ⋯ } }

@[simp]

theorem LeftIdeal.coe_top {α : Type u_1} [Mul α] : ↑⊤ = Set.univ

instance LeftIdeal.instBot {β : Type u_2} [MulZeroClass β] : Bot (LeftIdeal β)

Allows for notation ⊥ : LeftIdeal α for the left ideal {0}.

Equations

• LeftIdeal.instBot = { bot := { carrier := {0}, mul_mem_mem := ⋯ } }

@[simp]

theorem LeftIdeal.coe_bot {β : Type u_2} [MulZeroClass β] : ↑⊥ = {0}

instance LeftIdeal.instInter {α : Type u_1} [Mul α] : Inter (LeftIdeal α)

The intersection of two left ideals is a left ideal.

Equations

• LeftIdeal.instInter = { inter := fun (p q : LeftIdeal α) => { carrier := ↑p ∩ ↑q, mul_mem_mem := ⋯ } }

@[simp]

theorem LeftIdeal.inter_coe {α : Type u_1} [Mul α] {p q : LeftIdeal α} : ↑p ∩ ↑q = ↑p ∩ ↑q

@[simp]

theorem LeftIdeal.univ_mul_self_subset_self {α : Type u_1} [Mul α] (p : LeftIdeal α) : Set.univ * ↑p ⊆ ↑p

If p is a left ideal of α, then α * p ⊆ p.

def LeftIdeal.ofSet {S : Type u_2} [Semigroup S] (s : Set S) : LeftIdeal S

Given a set in a Semigroup, the minimal Left Ideal containing the set.

Equations

• LeftIdeal.ofSet s = { carrier := Set.univ * s ∪ s, mul_mem_mem := ⋯ }

theorem LeftIdeal.ofSet_def {S : Type u_2} [Semigroup S] (p : Set S) : ↑(ofSet p) = Set.univ * p ∪ p

@[simp]

theorem LeftIdeal.mem_ofSet {S : Type u_2} [Semigroup S] (p : Set S) (x : S) : x ∈ ofSet p ↔ x ∈ Set.univ * p ∪ p

theorem LeftIdeal.ofSet_minimal {S : Type u_2} [Semigroup S] {p : LeftIdeal S} {q : Set S} (hin : q ⊆ ↑p) : ofSet q ≤ p

For q : Set S, LeftIdeal.ofSet q is the minimal left ideal containing the set.

structure RightIdeal (α : Type u_1) [Mul α] : Type u_1

A right ideal is a set X such that ∀ y, ∀ x ∈ X, x * y ∈ X.

• carrier : Set α
• mem_mul_mem {x : α} (hin : x ∈ self.carrier) (y : α) : x * y ∈ self.carrier

instance RightIdeal.instSetLike {α : Type u_1} [Mul α] : SetLike (RightIdeal α) α

Equations

• RightIdeal.instSetLike = { coe := RightIdeal.carrier, coe_injective' := ⋯ }

@[simp]

theorem RightIdeal.mem_carrier {α : Type u_1} [Mul α] {p : RightIdeal α} {x : α} : x ∈ p.carrier ↔ x ∈ ↑p

theorem RightIdeal.mem_coe {α : Type u_1} [Mul α] {p : RightIdeal α} {x : α} : x ∈ ↑p ↔ x ∈ p

theorem RightIdeal.ext {α : Type u_1} [Mul α] {p q : RightIdeal α} (h : ∀ (x : α), x ∈ p ↔ x ∈ q) : p = q

theorem RightIdeal.ext_iff {α : Type u_1} [Mul α] {p q : RightIdeal α} : p = q ↔ ∀ (x : α), x ∈ p ↔ x ∈ q

@[simp]

theorem RightIdeal.mem {α : Type u_1} [Mul α] {x y : α} {p : RightIdeal α} (hin : x ∈ p) : x * y ∈ p

instance RightIdeal.instEmptyCollection {α : Type u_1} [Mul α] : EmptyCollection (RightIdeal α)

Equations

• RightIdeal.instEmptyCollection = { emptyCollection := { carrier := ∅, mem_mul_mem := ⋯ } }

@[simp]

theorem RightIdeal.coe_empty {α : Type u_1} [Mul α] : ↑∅ = ∅

instance RightIdeal.instTop {α : Type u_1} [Mul α] : Top (RightIdeal α)

Equations

• RightIdeal.instTop = { top := { carrier := Set.univ, mem_mul_mem := ⋯ } }

@[simp]

theorem RightIdeal.coe_top {α : Type u_1} [Mul α] : ↑⊤ = Set.univ

instance RightIdeal.instBot {β : Type u_2} [MulZeroClass β] : Bot (RightIdeal β)

Equations

• RightIdeal.instBot = { bot := { carrier := {0}, mem_mul_mem := ⋯ } }

@[simp]

theorem RightIdeal.coe_bot {β : Type u_2} [MulZeroClass β] : ↑⊥ = {0}

instance RightIdeal.instInter {α : Type u_1} [Mul α] : Inter (RightIdeal α)

The intersection of right ideals is a right isimpdeal.

Equations

• RightIdeal.instInter = { inter := fun (p q : RightIdeal α) => { carrier := ↑p ∩ ↑q, mem_mul_mem := ⋯ } }

@[simp]

theorem RightIdeal.inter_coe {α : Type u_1} [Mul α] {p q : RightIdeal α} : ↑p ∩ ↑q = ↑p ∩ ↑q

@[simp]

theorem RightIdeal.mul_univ_subset_self {α : Type u_1} [Mul α] (p : RightIdeal α) : ↑p * Set.univ ⊆ ↑p

If p is a right ideal of α, then p * α ⊆ p.

def RightIdeal.ofSet {S : Type u_2} [Semigroup S] (s : Set S) : RightIdeal S

Given a set in a Semigroup, the minimal right ideal containing the set.

Equations

• RightIdeal.ofSet s = { carrier := s * Set.univ ∪ s, mem_mul_mem := ⋯ }

theorem RightIdeal.ofSet_def {S : Type u_2} [Semigroup S] (p : Set S) : ↑(ofSet p) = p * Set.univ ∪ p

@[simp]

theorem RightIdeal.mem_ofSet {S : Type u_2} [Semigroup S] (p : Set S) (x : S) : x ∈ ofSet p ↔ x ∈ p * Set.univ ∪ p

theorem RightIdeal.ofSet_minimal {S : Type u_2} [Semigroup S] {p : RightIdeal S} {q : Set S} (hin : q ⊆ ↑p) : ofSet q ≤ p

For q : Set S, RightIdeal.ofSet q is the minimal right ideal containing the set.

structure Ideal' (α : Type u_1) [Mul α] : Type u_1

An ideal is a set closed under multiplication on both sides.

• carrier : Set α
• mem_mul_mem {x : α} (hin : x ∈ self.carrier) (y : α) : x * y ∈ self.carrier
• mul_mem_mem {x : α} (hin : x ∈ self.carrier) (y : α) : y * x ∈ self.carrier

def Ideal'.toLeftIdeal {α : Type u_1} [Mul α] (p : Ideal' α) : LeftIdeal α

Equations

• p.toLeftIdeal = { carrier := p.carrier, mul_mem_mem := ⋯ }

def Ideal'.toRightIdeal {α : Type u_1} [Mul α] (p : Ideal' α) : RightIdeal α

Equations

• p.toRightIdeal = { carrier := p.carrier, mem_mul_mem := ⋯ }

instance Ideal'.instSetLike {α : Type u_1} [Mul α] : SetLike (Ideal' α) α

Equations

• Ideal'.instSetLike = { coe := Ideal'.carrier, coe_injective' := ⋯ }

@[simp]

theorem Ideal'.mem_carrier {α : Type u_1} [Mul α] {p : Ideal' α} {x : α} : x ∈ p.carrier ↔ x ∈ ↑p

theorem Ideal'.mem_coe {α : Type u_1} [Mul α] {p : Ideal' α} {x : α} : x ∈ ↑p ↔ x ∈ p

theorem Ideal'.ext {α : Type u_1} [Mul α] {p q : Ideal' α} (h : ∀ (x : α), x ∈ p ↔ x ∈ q) : p = q

This allows us to use the ext tactic

theorem Ideal'.ext_iff {α : Type u_1} [Mul α] {p q : Ideal' α} : p = q ↔ ∀ (x : α), x ∈ p ↔ x ∈ q

@[simp]

theorem Ideal'.mem {α : Type u_1} [Mul α] {x z y : α} {p : Ideal' α} (hin : x ∈ p) : z * x * y ∈ p

@[simp]

theorem Ideal'.mul_right_mem {α : Type u_1} [Mul α] {x y : α} {p : Ideal' α} (hin : x ∈ p) : x * y ∈ p

@[simp]

theorem Ideal'.mul_left_mem {α : Type u_1} [Mul α] {x y : α} {p : Ideal' α} (hin : x ∈ p) : y * x ∈ p

instance Ideal'.instEmptyCollection {α : Type u_1} [Mul α] : EmptyCollection (Ideal' α)

Equations

• Ideal'.instEmptyCollection = { emptyCollection := { carrier := ∅, mem_mul_mem := ⋯, mul_mem_mem := ⋯ } }

@[simp]

theorem Ideal'.coe_empty {α : Type u_1} [Mul α] : ↑∅ = ∅

@[simp]

theorem Ideal'.not_in_empty {α : Type u_1} [Mul α] (x : α) : x ∉ ∅

instance Ideal'.instTop {α : Type u_1} [Mul α] : Top (Ideal' α)

Equations

• Ideal'.instTop = { top := { carrier := Set.univ, mem_mul_mem := ⋯, mul_mem_mem := ⋯ } }

@[simp]

theorem Ideal'.coe_top {α : Type u_1} [Mul α] : ↑⊤ = Set.univ

@[simp]

theorem Ideal'.in_top {α : Type u_1} [Mul α] (x : α) : x ∈ ⊤

instance Ideal'.instBot {β : Type u_2} [MulZeroClass β] : Bot (Ideal' β)

Equations

• Ideal'.instBot = { bot := { carrier := {0}, mem_mul_mem := ⋯, mul_mem_mem := ⋯ } }

@[simp]

theorem Ideal'.coe_bot {β : Type u_2} [MulZeroClass β] : ↑⊥ = {0}

theorem Ideal'.eq_zero_iff_in_bot {β : Type u_2} [MulZeroClass β] (x : β) : x = 0 ↔ x ∈ ⊥

instance Ideal'.instInter {α : Type u_1} [Mul α] : Inter (Ideal' α)

The intersection of two ideals is an ideal.

Equations

• Ideal'.instInter = { inter := fun (p q : Ideal' α) => { carrier := ↑p ∩ ↑q, mem_mul_mem := ⋯, mul_mem_mem := ⋯ } }

@[simp]

theorem Ideal'.inter_coe {α : Type u_1} [Mul α] {p q : Ideal' α} : ↑p ∩ ↑q = ↑p ∩ ↑q

def Ideal'.ofSet {S : Type u_2} [Semigroup S] (s : Set S) : Ideal' S

Given a set in a Semigroup, the minimal ideal containing the set.

Equations

• Ideal'.ofSet s = { carrier := ↑(LeftIdeal.ofSet s) ∪ ↑(RightIdeal.ofSet s) ∪ Set.univ * s * Set.univ ∪ s, mem_mul_mem := ⋯, mul_mem_mem := ⋯ }

theorem Ideal'.ofSet_def {S : Type u_2} [Semigroup S] (p : Set S) : ↑(ofSet p) = ↑(LeftIdeal.ofSet p) ∪ ↑(RightIdeal.ofSet p) ∪ Set.univ * p * Set.univ ∪ p

@[simp]

theorem Ideal'.mem_ofSet {S : Type u_2} [Semigroup S] (s : Set S) (x : S) : x ∈ ofSet s ↔ x ∈ ↑(LeftIdeal.ofSet s) ∪ ↑(RightIdeal.ofSet s) ∪ Set.univ * s * Set.univ ∪ s

theorem Ideal'.ofSet_minimal {S : Type u_2} [Semigroup S] {p : Ideal' S} {q : Set S} (hin : q ⊆ ↑p) : ofSet q ≤ p

For q : Set S, Ideal'.ofSet q is the minimal ideal containing the set.

Ideal characterization of Greens Relations

theorem Semigroup.LPreorder.iff_in_leftIdeal {S : Type u_1} [Semigroup S] (x y : S) : x ∈ LeftIdeal.ofSet {y} ↔ x ≤𝓛 y

x is in the principal left ideal of y iff x ≤𝓛 y.

theorem Semigroup.LPreorder.le_in_leftIdeal {S : Type u_1} [Semigroup S] {x y : S} {i : LeftIdeal S} (hx : x ∈ i) (hy : y ≤𝓛 x) : y ∈ i

For x ∈ i : LeftIdeal S, if y ≤𝓛 x then y ∈ i.

theorem Semigroup.LPreorder.iff_leftIdeal_subset {S : Type u_1} [Semigroup S] (x y : S) : LeftIdeal.ofSet {x} ≤ LeftIdeal.ofSet {y} ↔ x ≤𝓛 y

The principal left ideal of x is a subset of that of y iff x ≤𝓛 y

theorem Semigroup.LEquiv.iff_leftIdeal_eq {S : Type u_1} [Semigroup S] (x y : S) : LeftIdeal.ofSet {x} = LeftIdeal.ofSet {y} ↔ x 𝓛 y

The principal left ideal of x is a equal to that of y iff x 𝓛 y.

theorem Semigroup.RPreorder.iff_in_rightIdeal {S : Type u_1} [Semigroup S] (x y : S) : x ∈ RightIdeal.ofSet {y} ↔ x ≤𝓡 y

x is in the principal right ideal of y iff x ≤𝓡 y.

theorem Semigroup.RPreorder.le_in_rightIdeal {S : Type u_1} [Semigroup S] {x y : S} {i : RightIdeal S} (hx : x ∈ i) (hy : y ≤𝓡 x) : y ∈ i

For x ∈ i : RightIdeal S, if y ≤𝓡 x then y ∈ i.

theorem Semigroup.RPreorder.iff_rightIdeal_subset {S : Type u_1} [Semigroup S] (x y : S) : RightIdeal.ofSet {x} ≤ RightIdeal.ofSet {y} ↔ x ≤𝓡 y

The principal right ideal of x is a subset of that of y iff x ≤𝓡 y

theorem Semigroup.REquiv.iff_rightIdeal_eq {S : Type u_1} [Semigroup S] (x y : S) : RightIdeal.ofSet {x} = RightIdeal.ofSet {y} ↔ x 𝓡 y

The principal right ideal of x is a equal to that of y iff x 𝓡 y.

theorem Semigroup.JPreorder.iff_in_ideal' {S : Type u_1} [Semigroup S] (x y : S) : x ∈ Ideal'.ofSet {y} ↔ x ≤𝓙 y

x is in the principal ideal of y iff x ≤𝓙 y.

theorem Semigroup.JPreorder.le_in_ideal' {S : Type u_1} [Semigroup S] {x y : S} {i : Ideal' S} (hx : x ∈ i) (hy : y ≤𝓙 x) : y ∈ i

For x ∈ i : Ideal' S, if y ≤𝓙 x then y ∈ i.

theorem Semigroup.JPreorder.iff_ideal'_subset {S : Type u_1} [Semigroup S] (x y : S) : Ideal'.ofSet {x} ≤ Ideal'.ofSet {y} ↔ x ≤𝓙 y

The principal ideal of x is a subset of that of y iff x ≤𝓙 y

theorem Semigroup.JEquiv.ideal'_eq {S : Type u_1} [Semigroup S] (x y : S) : Ideal'.ofSet {x} = Ideal'.ofSet {y} ↔ x 𝓙 y

The principal ideal of x is a equal to that of y iff x 𝓙 y.

Simple Semigroups

class SimpleSemigroup (S : Type u_1) extends Semigroup S : Type u_1

A semigroup is simple if its only ideals are ⊥ and ∅

• mul : S → S → S
• mul_assoc (a b c : S) : a * b * c = a * (b * c)
• ideal_eq (I : Ideal' S) : I = ∅ ∨ I = ⊤

@[simp]

theorem SimpleSemigroup.ideal {S : Type u_1} [inst : SimpleSemigroup S] (I : Ideal' S) : I = ∅ ∨ I = ⊤

class ZeroSimpleSemigroup (S : Type u_2) extends SemigroupWithZero S : Type u_2

• mul : S → S → S
• mul_assoc (a b c : S) : a * b * c = a * (b * c)
• zero : S
• zero_mul (a : S) : 0 * a = 0
• mul_zero (a : S) : a * 0 = 0
• ideal_eq (I : Ideal' S) : I = ∅ ∨ I = ⊤ ∨ I = ⊥

@[simp]

theorem ZeroSimpleSemigroup.ideal {S : Type u_1} [inst : ZeroSimpleSemigroup S] (I : Ideal' S) : I = ∅ ∨ I = ⊤ ∨ I = ⊥

theorem Semigroup.JPreorder.ofSimple {S : Type u_1} [SimpleSemigroup S] (x y : S) : x ≤𝓙 y

In a simple semigroup, all elements are J-preorder related

theorem Semigroup.JEquiv.ofSimple {S : Type u_1} [SimpleSemigroup S] (x y : S) : x 𝓙 y

In a simple semigroup, all elements are 𝓙 related

instance Semigroup.JPreorder.toSimpleSemigroup {S : Type u_1} [Semigroup S] (h : ∀ (x y : S), x ≤𝓙 y) : SimpleSemigroup S

If all elements of a semigroup are J-preorder related, then it is a simple semigroup.

Equations

• Semigroup.JPreorder.toSimpleSemigroup h = { toSemigroup := inst✝, ideal_eq := ⋯ }

theorem Semigroup.JPreorder.ofZeroSimple {S : Type u_1} [ZeroSimpleSemigroup S] (x y : S) (hy : y ≠ 0) : x ≤𝓙 y

All non-zero elements of a zero-simple-semigroup are J-preorder related.

instance Semigroup.JPreorder.toZeroSimpleSemigroup {S : Type u_1} [SemigroupWithZero S] (h : ∀ (x y : S), y ≠ 0 → x ≤𝓙 y) : ZeroSimpleSemigroup S

If all non-zero elements of a semigroup with zero are J-preorder related, then it is a zero-simple semigroup.

Equations

• Semigroup.JPreorder.toZeroSimpleSemigroup h = { toSemigroupWithZero := inst✝, ideal_eq := ⋯ }

Regular Semigroups

See Semigroup.DEquiv.regular_d_class_tfae and regularClass_iff_* / hasIdempotent_iff_* in MyProject/Green/Location.lean (Proposition 1.9).

def Semigroup.isRegularElem {α : Type u_2} [Mul α] (x : α) : Prop

A element x of a magma is regular iff ∃ y, x * y * x = x.

Equations

• Semigroup.isRegularElem x = ∃ (y : α), x * y * x = x

class Semigroup.RegularSemigroup (S : Type u_2) extends Semigroup S : Type u_2

In a regular semigroup, every element is regular.

• mul : S → S → S
• mul_assoc (a b c : S) : a * b * c = a * (b * c)
• isRegular (x : S) : isRegularElem x

@[simp]

theorem Semigroup.RegularSemigroup.regular {S : Type u_1} [inst : RegularSemigroup S] (x : S) : ∃ (y : S), x * y * x = x