2 Green’s Relations
In a semigroup \(S\), Green’s relations are a set of five equivalence relations that characterize the elements of \(S\) in terms of the principal ideals they generate. These relations are fundamental to the study of semigroups.
First, we define four preorder relations: \(\leq _{\mathcal{R}}\), \(\leq _{\mathcal{L}}\), \(\leq _{\mathcal{J}}\), and \(\leq _{\mathcal{H}}\). Let \(S^1\) be the monoid obtained by adjoining an identity element to \(S\) if it does not already have one. For any two elements \(x, y \in S\):
\(x \leq _{\mathcal{R}} y\) if and only if the principal right ideal generated by \(x\) is a subset of the principal right ideal generated by \(y\) (\(xS^1 \subseteq yS^1\)). In Lean, we use the equivalent definition that there must exist some \(z \in S^1\) such that \(x = yz\).
\(x \leq _{\mathcal{L}} y\) if and only if the principal left ideal generated by \(x\) is a subset of the principal left ideal generated by \(y\) (\(S^1x \subseteq S^1y\)). In Lean, we use the equivalent definition that there must exist some \(z \in S^1\) such that \(x = zy\).
\(x \leq _{\mathcal{J}} y\) if and only if the principal two-sided ideal generated by \(x\) is a subset of the principal two-sided ideal generated by \(y\) (\(S^1xS^1 \subseteq S^1yS^1\)). In Lean, we use the equivalent definition that there must exist some \(u, v \in S^1\) such that \(x = uyv\).
\(x \leq _{\mathcal{H}} y\) if and only if \(x \leq _{\mathcal{R}} y\) and \(x \leq _{\mathcal{L}} y\).
These four relations are preorders (they are reflexive and transitive).
From these preorders, we define the equivalence relations \(\mathcal{R}\), \(\mathcal{L}\), \(\mathcal{J}\), and \(\mathcal{H}\) as the symmetric closures of their corresponding preorders. For example, \(x \mathcal{R} y\) if and only if \(x \leq _{\mathcal{R}} y\) and \(y \leq _{\mathcal{R}} x\). The equivalence classes are denoted by \([x]_{\mathcal{R}}\), \([x]_{\mathcal{L}}\), etc.
Finally, the \(\mathcal{D}\) relation is defined by composing \(\mathcal{R}\) and \(\mathcal{L}\): \(x \mathcal{D} y\) if there exists an element \(z \in S\) such that \(x \mathcal{R} z\) and \(z \mathcal{L} y\). It can be shown that \(\mathcal{D}\) is an equivalence relation and that it can also be defined by composing \(\mathcal{L}\) and \(\mathcal{R}\).
The \(\mathcal{R}\) and \(\mathcal{L}\) relations exhibit compatibility with semigroup multiplication on one side. Specifically, the \(\mathcal{R}\)-preorder is compatible with left multiplication, and the \(\mathcal{L}\)-preorder is compatible with right multiplication. If \(x \leq _{\mathcal{R}} y\), then for any \(z \in S\), we have \(zx \leq _{\mathcal{R}} zy\). This property extends to the equivalence relation \(\mathcal{R}\). If \(x \mathcal{R} y\), then \(zx \mathcal{R} zy\). A similar argument holds for the \(\mathcal{L}\)-preorder and \(\mathcal{L}\)-equivalence, which are compatible with right multiplication. If \(x \leq _{\mathcal{L}} y\), then \(xz \leq _{\mathcal{L}} yz\) for any \(z \in S\).
Let \(x, y, z \in S\). To prove left compatibility for \(\leq _{\mathcal{R}}\), assume \(x \leq _{\mathcal{R}} y\). By definition, there exists \(a \in S^1\) such that \(x = ya\). Multiplying by \(z\) on the left gives \(zx = z(ya) = (zy)a\). This implies \(zx \leq _{\mathcal{R}} zy\). For the equivalence \(x \mathcal{R} y\), we have both \(x \leq _{\mathcal{R}} y\) and \(y \leq _{\mathcal{R}} x\). Applying the result for preorders, we get \(zx \leq _{\mathcal{R}} zy\) and \(zy \leq _{\mathcal{R}} zx\), which means \(zx \mathcal{R} zy\). The proof for \(\leq _{\mathcal{L}}\) and \(\mathcal{L}\) with right multiplication is analogous.
The composition of the relations \(\mathcal{R}\) and \(\mathcal{L}\) is commutative. That is, for any \(x, y \in S\), there exists a \(z\) such that \(x \mathcal{R} z\) and \(z \mathcal{L} y\) if and only if there exists a \(w\) such that \(x \mathcal{L} w\) and \(w \mathcal{R} y\). This can be written as \(\mathcal{R} \circ \mathcal{L} = \mathcal{L} \circ \mathcal{R}\). This property is crucial for proving that the relation \(\mathcal{D} = \mathcal{R} \circ \mathcal{L}\) is symmetric, and therefore an equivalence relation.
Suppose there exists \(z\) with \(x \mathcal{R} z\) and \(z \mathcal{L} y\). From \(x \mathcal{R} z\), we have \(x=za\) and \(z=xb\) for some \(a,b \in S^1\). From \(z \mathcal{L} y\), we have \(z=cy\) and \(y=dz\) for some \(c,d \in S^1\). We need to find an element \(w\) such that \(x \mathcal{L} w\) and \(w \mathcal{R} y\). The Lean proof shows that in the non-trivial case, the element \(dza\) can be used for \(w\). This commutation is essential for establishing that \(\mathcal{D}\) is an equivalence relation, as it directly implies symmetry.
The \(\mathcal{D}\) relation is closed under composition with \(\mathcal{R}\) and \(\mathcal{L}\). If \(x \mathcal{D} y\) and \(y \mathcal{L} z\), then \(x \mathcal{D} z\). Similarly, if \(x \mathcal{D} y\) and \(y \mathcal{R} z\), then \(x \mathcal{D} z\). This property is used to prove the transitivity of \(\mathcal{D}\).
Suppose \(x \mathcal{D} y\) and \(y \mathcal{L} z\). By definition of \(\mathcal{D}\), there exists an element \(w\) such that \(x \mathcal{R} w\) and \(w \mathcal{L} y\). Since \(\mathcal{L}\) is an equivalence relation, from \(w \mathcal{L} y\) and \(y \mathcal{L} z\), we can deduce \(w \mathcal{L} z\). Now we have \(x \mathcal{R} w\) and \(w \mathcal{L} z\), which by definition means \(x \mathcal{D} z\). A similar argument holds for closure under \(\mathcal{R}\). If \(x \mathcal{D} y\) and \(y \mathcal{R} z\), we use the commutation of \(\mathcal{R}\) and \(\mathcal{L}\) (5). \(x \mathcal{D} y\) means there is a \(w\) with \(x \mathcal{L} w\) and \(w \mathcal{R} y\). Since \(\mathcal{R}\) is an equivalence relation, \(w \mathcal{R} y\) and \(y \mathcal{R} z\) implies \(w \mathcal{R} z\). So we have \(x \mathcal{L} w\) and \(w \mathcal{R} z\), which means \(x \mathcal{D} z\).