My formalization project

1 Green’s Relations

Definition 1 Green’s R-preorder
#

Let \(M\) be a monoid and let \(x,y\in M\). We define \(x \le _{\mathcal R} y\) if there exists \(z\in M\) such that \(x = y\cdot z\). Equivalently, \(x\) lies in the principal right ideal generated by \(y\).

Definition 2 Green’s L-preorder
#

Let \(M\) be a monoid and let \(x,y\in M\). We define \(x \le _{\mathcal L} y\) if there exists \(z\in M\) such that \(x = z\cdot y\). In other words, \(x\) lies in the principal left ideal generated by \(y\).

Definition 3 Green’s J-preorder
#

Let \(M\) be a monoid and let \(x,y\in M\). We define \(x \le _{\mathcal J} y\) if there exist \(u,v\in M\) such that \(x = u\cdot y\cdot v\). Equivalently, \(x\) lies in the two‑sided ideal generated by \(y\).

Definition 4 Green’s H-preorder
#

Let \(M\) be a monoid and let \(x,y\in M\). We define \(x \le _{\mathcal H} y\) if both \(x \le _{\mathcal R} y\) and \(x \le _{\mathcal L} y\) hold, that is, \(x\) is simultaneously in the right and left ideals generated by \(y\). Unwinding the definition, this means there exist elements \(z_1,z_2\in M\) with \(x = y\cdot z_1\) and \(x = z_2\cdot y\).

Lemma 5 \(\le _{\mathcal R}\) is a preorder (reflexive & transitive)
#

The relation \(\le _{\mathcal R}\) on \(M\) is a preorder; in particular:

  • Reflexivity. For every \(x\in M\), \(x \le _{\mathcal R} x\) (witness \(z=1\) since \(x = x\cdot 1\)).

  • Transitivity. If \(x \le _{\mathcal R} y\) and \(y \le _{\mathcal R} z\), pick witnesses \(v,u\in M\) with \(x = yv\) and \(y = zu\); then \(x = z(uv)\), so \(x \le _{\mathcal R} z\).

Lemma 6 \(\le _{\mathcal L}\) is a preorder (reflexive & transitive)
#

The relation \(\le _{\mathcal L}\) on \(M\) is a preorder; in particular:

  • Reflexivity. For every \(x\in M\), \(x \le _{\mathcal L} x\) (witness \(z=1\) since \(1\cdot x = x\)).

  • Transitivity. If \(x \le _{\mathcal L} y\) and \(y \le _{\mathcal L} z\), pick witnesses \(u,v\in M\) with \(x = u y\) and \(y = v z\); then \(x = (uv) z\), so \(x \le _{\mathcal L} z\).

Lemma 7 \(\le _{\mathcal J}\) is a preorder (reflexive & transitive)
#

The relation \(\le _{\mathcal J}\) on \(M\) is a preorder; in particular:

  • Reflexivity. For every \(x\in M\), \(x \le _{\mathcal J} x\) (witness \(u=v=1\) so \(x=1\cdot x\cdot 1\)).

  • Transitivity. If \(x \le _{\mathcal J} y\) and \(y \le _{\mathcal J} z\), pick \(u_1,v_1,u_2,v_2\in M\) with \(x = u_1 y v_1\) and \(y = u_2 z v_2\); then \(x = u_1 (u_2 z v_2) v_1 = (u_1 u_2) z (v_2 v_1)\), so \(x \le _{\mathcal J} z\).

Lemma 8 \(\le _{\mathcal H}\) is a preorder (reflexive & transitive)

The relation \(\le _{\mathcal H}\) on \(M\) is a preorder; in particular:

  • Reflexivity. For every \(x\in M\), \(x \le _{\mathcal H} x\) since \(x \le _{\mathcal R} x\) and \(x \le _{\mathcal L} x\).

  • Transitivity. If \(x \le _{\mathcal H} y\) and \(y \le _{\mathcal H} z\), then \(x \le _{\mathcal R} y \le _{\mathcal R} z\) and \(x \le _{\mathcal L} y \le _{\mathcal L} z\); hence \(x \le _{\mathcal R} z\) and \(x \le _{\mathcal L} z\), so \(x \le _{\mathcal H} z\).

1.1 Equivalences from Preorders

To obtain equivalence relations from a preorder we take its symmetric closure. Given any preorder \(p\), we define an equivalence relation by declaring two elements equivalent exactly when both \(p\, x\, y\) and \(p\, y\, x\) hold. This construction works uniformly for all preorders and, in particular, produces Green’s equivalence relations from Green’s preorders.

Definition 9 Equivalence of a preorder
#

Let \(\alpha \) be a type and let \(p : \alpha \to \alpha \to \mathrm{Prop}\) be a preorder. For \(x,y : \alpha \) we define \(\mathrm{EquivOfLE}\, p\, x\, y\) to hold when both \(p\, x\, y\) and \(p\, y\, x\) hold. In other words, \(\mathrm{EquivOfLE}\, p\) is the symmetric closure of the relation \(p\).

Lemma 10 EquivOfLE is an equivalence relation
#

If \(p\) is a preorder on \(\alpha \) then \(\mathrm{EquivOfLE}\, p\) is an equivalence relation.

Proof

We verify the three properties of an equivalence relation. For reflexivity, if \(p\) is a preorder then it is reflexive, so for every \(x\) we have both \(p\, x\, x\) and \(p\, x\, x\); hence \(\mathrm{EquivOfLE}\, p\, x\, x\) holds. Symmetry is immediate: if \(\mathrm{EquivOfLE}\, p\, x\, y\) holds, meaning \(p\, x\, y\) and \(p\, y\, x\), then the pair \(p\, y\, x\) and \(p\, x\, y\) shows \(\mathrm{EquivOfLE}\, p\, y\, x\). For transitivity, suppose \(\mathrm{EquivOfLE}\, p\, x\, y\) and \(\mathrm{EquivOfLE}\, p\, y\, z\). Then we have \(p\, x\, y\) and \(p\, y\, z\); by transitivity of the preorder \(p\) we obtain \(p\, x\, z\). Similarly from \(p\, z\, y\) and \(p\, y\, x\) we deduce \(p\, z\, x\). Thus \(\mathrm{EquivOfLE}\, p\, x\, z\) holds, completing the proof.

1.2 Green’s Equivalences (\(\mathcal R, \mathcal L, \mathcal J, \mathcal H\))

Definition 11 Right equivalence
#

Let \(M\) be a monoid. For \(x,y \in M\) we define \(x \, \mathcal R\, y\) to hold if both \(x \le _{\mathcal R} y\) and \(y \le _{\mathcal R} x\) hold. In other words, two elements are right equivalent when they lie in the principal right ideals generated by each other.

Lemma 12 Right equivalence is an equivalence relation
#

The relation \(\mathcal R\) defined in Definition 11 is an equivalence relation on \(M\).

Definition 13 Left equivalence
#

For \(x,y\in M\) we define \(x \, \mathcal L\, y\) to hold when both \(x \le _{\mathcal L} y\) and \(y \le _{\mathcal L} x\) hold. This expresses that \(x\) and \(y\) generate the same principal left ideals.

Lemma 14 Left equivalence is an equivalence relation
#

The relation \(\mathcal L\) defined in Definition 13 is an equivalence relation on \(M\).

Definition 15 J equivalence
#

For \(x,y\in M\) we define \(x \, \mathcal J\, y\) to hold when both \(x \le _{\mathcal J} y\) and \(y \le _{\mathcal J} x\) hold, i.e., each lies in the two‑sided ideal generated by the other.

Lemma 16 J equivalence is an equivalence relation
#

The relation \(\mathcal J\) defined in Definition 15 is an equivalence relation on \(M\).

Definition 17 H equivalence
#

For \(x,y\in M\) we define \(x \, \mathcal H\, y\) to hold when both \(x \le _{\mathcal H} y\) and \(y \le _{\mathcal H} x\) hold. This captures when two elements are simultaneously right and left equivalent.

Lemma 18 H equivalence is an equivalence relation
#

The relation \(\mathcal H\) defined in Definition 17 is an equivalence relation on \(M\).

1.3 Basic Preorder Properties

Lemma 19 Multiplication decreases for \(\le _{\mathcal R},\le _{\mathcal L},\le _{\mathcal J}\)

For all \(M\) a monoid and \(x,y,u,v\in M\), the following hold:

  • \(\mathbf{(R)}\) \(x\cdot y \le _{\mathcal R} x\).

  • \(\mathbf{(L)}\) \(y\cdot x \le _{\mathcal L} x\).

  • \(\mathbf{(J)}\) \(u\cdot x\cdot v \le _{\mathcal J} x\).

Proof
  • (R) By definition of \(\le _{\mathcal R}\), we need \(u\) with \(x\cdot u = x\cdot y\). Take \(u:=y\).

  • (L) By definition of \(\le _{\mathcal L}\), we need \(u\) with \(u\cdot x = y\cdot x\). Take \(u:=y\).

  • (J) By definition of \(\le _{\mathcal J}\), we need \(s,t\) with \(s\cdot x\cdot t = u\cdot x\cdot v\). Take \(s:=u\), \(t:=v\).

Lemma 20 Cancellation for \(\le _{\mathcal J},\le _{\mathcal R},\le _{\mathcal L}\)

Let \(M\) be a monoid and \(x,y,z\in M\).

  • \(\mathbf{(J\text{-}L)}\) If \(x \le _{\mathcal J} y\cdot z\), then \(x \le _{\mathcal J} z\).

  • \(\mathbf{(J\text{-}R)}\) If \(x \le _{\mathcal J} y\cdot z\), then \(x \le _{\mathcal J} y\).

  • \(\mathbf{(R\text{-}R)}\) If \(x \le _{\mathcal R} y\cdot z\), then \(x \le _{\mathcal R} y\).

  • \(\mathbf{(L\text{-}L)}\) If \(x \le _{\mathcal L} y\cdot z\), then \(x \le _{\mathcal L} z\).

Proof
  • (J–L) From \(x \le _{\mathcal J} y z\), pick \(u,v\) with \(u\cdot (y z)\cdot v = x\). By associativity, \((u y)\cdot z\cdot v = x\). Set \(u':=u y\), \(v':=v\). Then \(x \le _{\mathcal J} z\).

  • (J–R) From \(x \le _{\mathcal J} y z\), pick \(u,v\) with \(u\cdot (y z)\cdot v = x\). By associativity, \(u\cdot y\cdot (z v) = x\). Set \(u':=u\), \(v':=z v\). Then \(x \le _{\mathcal J} y\).

  • (R–R) From \(x \le _{\mathcal R} y z\), pick \(u\) with \((y z)\cdot u = x\). By associativity, \(y\cdot (z u) = x\). Set \(u':=z u\). Then \(x \le _{\mathcal R} y\).

  • (L–L) From \(x \le _{\mathcal L} y z\), pick \(u\) with \(u\cdot (y z) = x\). By associativity, \((u y)\cdot z = x\). Set \(u':=u y\). Then \(x \le _{\mathcal L} z\).

Lemma 21 Idempotent characterizations for \(\le _{\mathcal R}\) and \(\le _{\mathcal L}\)

Let \(M\) be a monoid and let \(e\in M\) be idempotent \((e\cdot e = e)\). For any \(x\in M\),

\[ \text{\bf (R)}\quad x \le _{\mathcal R} e \; \Longleftrightarrow \; e\cdot x = x, \qquad \text{\bf (L)}\quad x \le _{\mathcal L} e \; \Longleftrightarrow \; x\cdot e = x. \]
Proof

Assume \(e^2=e\).

  • (R) (\(\Rightarrow \)) If \(x \le _{\mathcal R} e\), pick \(t\) with \(e\cdot t = x\). Then \(e\cdot x = e\cdot (e\cdot t) = (e\cdot e)\cdot t = e\cdot t = x\). (\(\Leftarrow \)) If \(e\cdot x = x\), take \(t:=x\); then \(e\cdot t = x\), so \(x \le _{\mathcal R} e\).

  • (L) (\(\Rightarrow \)) If \(x \le _{\mathcal L} e\), pick \(t\) with \(t\cdot e = x\). Then \(x\cdot e = (t\cdot e)\cdot e = t\cdot (e\cdot e) = t\cdot e = x\). (\(\Leftarrow \)) If \(x\cdot e = x\), take \(t:=x\); then \(t\cdot e = x\), so \(x \le _{\mathcal L} e\).

1.4 R–L multiplicative compatibility

Lemma 22 Left multiplication: compatibility with \(\le _{\mathcal R}\) and \(\mathcal R\)-equivalence

For all \(x,y,z\in M\):

  • (Preorder) If \(x \le _{\mathcal R} y\), then \(z\cdot x \le _{\mathcal R} z\cdot y\).

  • (Equivalence) If \(x \, \mathcal R\, y\), then \(z\cdot x \, \mathcal R\, z\cdot y\).

Proof
  • (Preorder) From \(x \le _{\mathcal R} y\) pick \(u\) with \(y\cdot u = x\). Then \((z\cdot y)\cdot u = z\cdot (y\cdot u) = z\cdot x\) by associativity, hence \(z\cdot x \le _{\mathcal R} z\cdot y\).

  • (Equivalence) If \(x \, \mathcal R\, y\), then \(x \le _{\mathcal R} y\) and \(y \le _{\mathcal R} x\). Apply the preorder case to both inclusions to get \(z\cdot x \le _{\mathcal R} z\cdot y\) and \(z\cdot y \le _{\mathcal R} z\cdot x\), whence \(z\cdot x \, \mathcal R\, z\cdot y\).

Lemma 23 Right multiplication: compatibility with \(\le _{\mathcal L}\) and \(\mathcal L\)-equivalence

For all \(x,y,z\in M\):

  • (Preorder) If \(x \le _{\mathcal L} y\), then \(x\cdot z \le _{\mathcal L} y\cdot z\).

  • (Equivalence) If \(x \, \mathcal L\, y\), then \(x\cdot z \, \mathcal L\, y\cdot z\).

Proof
  • (Preorder) From \(x \le _{\mathcal L} y\) pick \(u\) with \(u\cdot y = x\). Then \(u\cdot (y\cdot z) = (u\cdot y)\cdot z = x\cdot z\) by associativity, hence \(x\cdot z \le _{\mathcal L} y\cdot z\).

  • (Equivalence) If \(x \, \mathcal L\, y\), then \(x \le _{\mathcal L} y\) and \(y \le _{\mathcal L} x\). Apply the preorder case to both inclusions to get \(x\cdot z \le _{\mathcal L} y\cdot z\) and \(y\cdot z \le _{\mathcal L} x\cdot z\), hence \(x\cdot z \, \mathcal L\, y\cdot z\).

1.5 R–L commutativity

Lemma 24 Commutativity of \(\le _{\mathcal L}\) and \(\le _{\mathcal R}\)

For any \(x,y \in M\), there exists an element \(z\) with \(x \le _{\mathcal L} z\) and \(z \le _{\mathcal R} y\) if and only if there exists an element \(w\) with \(x \le _{\mathcal R} w\) and \(w \le _{\mathcal L} y\).

Proof

First suppose there exists \(z\in M\) such that \(x \le _{\mathcal L} z\) and \(z \le _{\mathcal R} y\). Unwinding the definitions, there are witnesses \(u\) and \(v\) with \(u\cdot z = x\) and \(y\cdot v = z\). Taking \(w = u\cdot y\) we have

\[ w \le _{\mathcal L} y \quad \text{since}\quad w = u\cdot y \]

and

\[ x = u\cdot z = u\cdot (y\cdot v) = (u\cdot y)\cdot v = w\cdot v, \]

so \(x \le _{\mathcal R} w\). Conversely, suppose there exists \(w\in M\) with \(x \le _{\mathcal R} w\) and \(w \le _{\mathcal L} y\). Then there are witnesses \(v\) and \(u\) with \(w\cdot v = x\) and \(u\cdot y = w\). Let \(z = y\cdot v\). We compute

\[ z \le _{\mathcal R} y \quad \text{because}\quad y\cdot v = z, \]

and

\[ x = w\cdot v = (u\cdot y)\cdot v = u\cdot (y\cdot v) = u\cdot z, \]

showing \(x \le _{\mathcal L} z\). This establishes the equivalence.

Lemma 25 Commutativity of right and left equivalence

For any \(x,y \in M\), there exists \(z\in M\) such that \(x \, \mathcal L\, z\) and \(z \, \mathcal R\, y\) if and only if there exists \(w\in M\) such that \(x \, \mathcal R\, w\) and \(w \, \mathcal L\, y\).

Proof

Suppose there exists \(z\) with \(x \, \mathcal L\, z\) and \(z \, \mathcal R\, y\). Write this as \(x \le _{\mathcal L} z \land z \le _{\mathcal L} x\) and \(z \le _{\mathcal R} y \land y \le _{\mathcal R} z\). From the left and right preorder conditions we have witnesses \(u_1,u_2,v_1,v_2\) satisfying

\[ u_1\cdot z = x,\qquad z\cdot u_2 = x,\qquad y\cdot v_1 = z,\qquad z\cdot v_2 = y. \]

Set \(w = u_1\cdot y\). Then using the first pair of equations we have

\[ w \le _{\mathcal L} y \quad \text{since}\quad w = u_1\cdot y, \]

and from the remaining equations we compute

\[ x = u_1\cdot z = u_1\cdot (y\cdot v_1) = (u_1\cdot y)\cdot v_1 = w\cdot v_1, \]

so \(x \le _{\mathcal R} w\). Moreover, by applying Lemma ?? to the equivalence \(z \, \mathcal R\, y\) we deduce \(u_1\cdot z\) is \(\mathcal R\)-equivalent to \(u_1\cdot y\). Since \(u_1\cdot z = x\), this shows \(x \, \mathcal R\, w\). Combined with the previous observation that \(w\) and \(y\) are \(\mathcal L\)-equivalent, we obtain the right-to-left implication.

Conversely, assume there exists \(w\) such that \(x \, \mathcal R\, w\) and \(w \, \mathcal L\, y\). This means \(x \le _{\mathcal R} w\) and \(w \le _{\mathcal R} x\), and \(w \le _{\mathcal L} y\) and \(y \le _{\mathcal L} w\). Pick witnesses \(v_1,v_2,u_1,u_2\) with

\[ w\cdot v_1 = x,\qquad x\cdot v_2 = w,\qquad u_1\cdot y = w,\qquad y\cdot u_2 = w. \]

Let \(z = y\cdot v_1\). Then \(z\) and \(y\) are \(\mathcal R\)-equivalent because both \(y \le _{\mathcal R} z\) and \(z \le _{\mathcal R} y\) hold via the witnesses above. Using Lemma ?? applied to the \(\mathcal L\)-equivalence \(w \, \mathcal L\, y\), we have \(x\cdot u_1\) is \(\mathcal L\)-equivalent to \(w\cdot u_1 = u_1\cdot y\). Since \(x\cdot u_1 = (w\cdot v_1)\cdot u_1\) and \(z = y\cdot v_1\), a straightforward computation shows \(x \le _{\mathcal L} z\) and \(z \le _{\mathcal L} x\). Hence \(x \, \mathcal L\, z\) and \(z \, \mathcal R\, y\), completing the proof.

1.6 The D-equivalence

Definition 26 D-equivalence
#

Let \(M\) be a monoid. For \(x,y\in M\) we say \(x \, \mathcal D\, y\) holds if there exists \(z\in M\) such that \(x \, \mathcal R\, z\) and \(z \, \mathcal L\, y\). Equivalently, there is a chain \(x \, \mathcal R\, z\) and \(z \, \mathcal L\, y\).

Lemma 27 D-equivalence symmetry

For all \(x,y\in M\),

\[ x \, \mathcal D\, y \; \Longleftrightarrow \; (\exists z,\; x \, \mathcal R\, z \land z \, \mathcal L\, y) \; \Longleftrightarrow \; (\exists w,\; y \, \mathcal R\, w \land w \, \mathcal L\, x), \]

and in particular \(x \, \mathcal D\, y \Rightarrow y \, \mathcal D\, x\).

Proof
  • The first equivalence is just Definition 26 unfolded.

  • The second equivalence uses the commutation of \(\mathcal R\)- and \(\mathcal L\)-equivalences: any chain \(x \, \mathcal R\, z \, \mathcal L\, y\) can be rotated to a chain \(y \, \mathcal R\, w \, \mathcal L\, x\) (Lemma rEquiv_lEquiv_comm).

  • Taking \(x,y\) swapped in the second characterization yields the symmetry \(x \, \mathcal D\, y \Rightarrow y \, \mathcal D\, x\).

Lemma 28 Closure under \(\mathcal L\)- and \(\mathcal R\)-equivalence

Let \(x,y,z\in M\).

  • If \(x \, \mathcal D\, y\) and \(y \, \mathcal L\, z\), then \(x \, \mathcal D\, z\).

  • If \(x \, \mathcal D\, y\) and \(y \, \mathcal R\, z\), then \(x \, \mathcal D\, z\). (by duality from the previous bullet, using symmetry)

Proof
  • Write \(x \, \mathcal D\, y\) as \(x \, \mathcal R\, u\) and \(u \, \mathcal L\, y\) for some \(u\). If \(y \, \mathcal L\, z\), then by transitivity of \(\mathcal L\)-equivalence, \(u \, \mathcal L\, z\). Hence \(x \, \mathcal R\, u \, \mathcal L\, z\), i.e. \(x \, \mathcal D\, z\).

  • For the \(\mathcal R\)-closure: from \(x \, \mathcal D\, y\) get \(y \, \mathcal D\, x\) by symmetry (Lemma 27); combine with \(y \, \mathcal R\, z\) and apply the previous bullet in the dual form to obtain \(y \, \mathcal D\, z\), then symmetrize back to \(x \, \mathcal D\, z\).

Lemma 29 Transitivity of \(\mathcal D\)
#

If \(x \, \mathcal D\, y\) and \(y \, \mathcal D\, z\) then \(x \, \mathcal D\, z\).

Proof

Choose witnesses \(x \, \mathcal R\, u \, \mathcal L\, y\) and \(y \, \mathcal R\, v \, \mathcal L\, z\). Apply the \(\mathcal R\)-closure to get \(x \, \mathcal D\, v\), then the \(\mathcal L\)-closure to conclude \(x \, \mathcal D\, z\).

Lemma 30 \(\mathcal D\) is an equivalence relation
#

The relation \(\mathcal D\) on \(M\) is reflexive, symmetric, and transitive.

Proof
  • Reflexive: take \(z:=x\) and use reflexivity of \(\mathcal R\) and \(\mathcal L\).

  • Symmetric: Lemma 27.

  • Transitive: Lemma 29.

1.7 Equivalence classes

Green’s equivalence relations partition a monoid into subsets called equivalence classes. Concretely, given an element \(a\in M\), the \(\mathcal R\)-class of \(a\) is the set of all \(x\) such that \(x \, \mathcal R\, a\). Similarly for \(\mathcal L, \mathcal J, \mathcal H\) and \(\mathcal D\).

Definition 31 Right class
#

For \(a\in M\) we define \(\mathrm{RClass}(a)\) to be the set \(\{ x\in M \mid x \, \mathcal R\, a\} \).

Definition 32 Left class
#

For \(a\in M\) we define \(\mathrm{LClass}(a)\) to be the set \(\{ x\in M \mid x \, \mathcal L\, a\} \).

Definition 33 J class
#

For \(a\in M\) we define \(\mathrm{JClass}(a)\) to be the set \(\{ x\in M \mid x \, \mathcal J\, a\} \).

Definition 34 H class
#

For \(a\in M\) we define \(\mathrm{HClass}(a)\) to be the set \(\{ x\in M \mid x \, \mathcal H\, a\} \).

Definition 35 D class
#

For \(a\in M\) we define \(\mathrm{DClass}(a)\) to be the set \(\{ x\in M \mid x \, \mathcal D\, a\} \).