Advertisement

Inverse semigroups with apartness

  • Alessandra CherubiniEmail author
  • Achille Frigeri
Research Article
  • 7 Downloads

Abstract

The notion of semigroups with apartness has been introduced recently as a constructive counterpart of classical semigroups. On such structures, a constructive analogue of the isomorphism theorem has been proved, and quasiorder relations and related substructures have been studied. In this paper, we extend this approach by introducing inverse semigroups with apartness, a useful tool to describe partial symmetries in sets with apartness. We prove a constructive analogue of the isomorphism theorem for inverse semigroups and provide a characterisation of cocongruences on inverse semigroups.

Keywords

Set with apartness Semigroup with apartness Inverse semigroup with apartness Cocongruence 

1 Introduction

The concept of semigroups with apartness has been introduced in [7, 8] as yet another application of Bishop’s constructive mathematics [1, 2] to algebraic structures [14, 20]. In [3], Bridges and Reeves comment that “modern algebra has proved amenable to a [...] constructive treatment”. The reason for this can be traced back to [15], where Martin-Löf argues that “if programming is understood not as the writing of instructions for this or that computing machine but as the design of methods of computation [...], then it no longer seems possible to distinguish the discipline of programming from constructive mathematics”. These considerations, alongside Howie’s motivation for the study of semigroups (and inverse semigroups) [10], motivate the constructive approach to inverse semigroups which we present in this paper.

In this work, we introduce the concept of inverse semigroups with apartness, and outline some related concepts such as that of symmetric inverse semigroups and their cocongruence pairs. We also provide constructive analogues of some classical theorems for inverse semigroups.

In Sect. 2, we introduce the basic notions of apartness and a set with apartness, as well as that of a d-partial bijection. In Sect. 3, we introduce the concept of an inverse semigroup with apartness. Theorem 2 shows that our definition is well-founded: since inverse semigroups are semigroups of partial one-to-one transformations of a set [18, 21], we prove that the set of d-partial bijections on a set with apartness leads to an inverse semigroup with apartness. Section 4 is devoted to the study of I-cocongruences and their characterization in terms of cocongruence pairs. Lastly, Sect. 5 extends some of the results of [8] by providing an analogue of the Isomorphism Theorem for inverse semigroups with apartness.

In this paper, we do not include any background on constructive mathematics. The interested reader can refer to [4, 5, 6, 20] for a comprehensive introduction. A standard reference for constructive algebra is [14], while for the classical theory of inverse semigroups we refer to [11, 13, 16]. Following [7, 8], we adopt the semantics based on Kripke models with constant domains [12]. Observe that in these models the formula
$$\begin{aligned} \forall x(A\vee B(x))\Rightarrow A\vee \forall x B(x), \end{aligned}$$
where x does not appear in A as a free variable, is deducible; we make use of this property in the proof of Theorem 4.

2 Basic notions

Let X be a set given through an algorithm for constructing its members such that at least one element can be constructed. Such a set is referred to as an inhabited set. Let \(\cong \) be any equivalence relation on X, we call it an equality on X. For a given equality, we will require that all properties P are extensional, in the sense that for all \(x_1,x_2\in X\), \(x_1\cong x_2\) implies that \(P(x_1)\) and \(P(x_2)\) are equivalent. An apartness relation on X is a binary relation \(\ncong \) on X satisfying the following properties:
$$\begin{aligned} \lnot (x\ncong x); \end{aligned}$$
(irreflexivity)
$$\begin{aligned} x\ncong y \Rightarrow y\ncong x; \end{aligned}$$
(symmetry)
$$\begin{aligned} x\ncong z \Rightarrow (x\ncong y \vee y\ncong z). \end{aligned}$$
(cotransitivity)
An apartness is tight if
$$\begin{aligned} \lnot (x\ncong y)\Rightarrow x\cong y \end{aligned}$$
(tightness)
while we say that \(\cong \) and \(\ncong \) are relatively decidable if
$$\begin{aligned} x\cong y\vee x\ncong y. \end{aligned}$$
(decidability)

Definition 1

Let X be a set, \(\cong \) an equality on X and \(\ncong \) an apartness relation on X. Then the tuple \((X,\cong ,\ncong )\) is a set with apartness.

Remark 1

By extensionality, in a set with apartness \((X,\cong ,\ncong )\) we have \(x\ncong y\) and \(y\cong z\) imply \(x\ncong z\). Notice that in [20] apartness is named “pre-apartness”, while the term “apartness” is used to refer to what is called a tight apartness here. Also observe that by extensionality, tightness implies \(\lnot (x\ncong y)\Leftrightarrow x\cong y\).

Let \((S,\cong _S,\ncong _S),\ (T,\cong _T,\ncong _T)\) be two sets with apartness. The cartesian product \(S\times T\) is a set with apartness with respect to the equality and apartness defined respectively by
$$\begin{aligned} \begin{array}{l} (s_1,t_1)\cong (s_2,t_2) {\mathop {\Longleftrightarrow }\limits ^{\text { def}}}s_1\cong _S s_2 \wedge t_1\cong _T t_2,\\ (s_1,t_1)\ncong (s_2,t_2) {\mathop {\Longleftrightarrow }\limits ^{\text { def}}}s_1\ncong _S s_2 \vee t_1\ncong _T t_2, \end{array} \end{aligned}$$
where \(s_1,s_2\in S\) and \(t_1,t_2\in T\).

Definition 2

Let \((S,\cong _S,\ncong _S),\ (T,\cong _T,\ncong _T)\) be two sets with apartness and \(f:S\rightarrow T\) a map from S to T. Extensionality guarantees that f is well-defined, i.e., for all \(x,y\in S\), \(x\cong _S y\) implies \(f(x)\cong _T f(y)\). The map f is:
  • onto if for each \(y\in T\), there is \(x\in S\) such that \(f(x)\cong _T y\),

  • one-to-one if for all \(x,y\in S\), \(f(x)\cong _T f(y)\) implies \(x\cong _S y\),

  • bijective if it is onto and one-to-one,

  • injective if for all \(x,y\in S\), \(x\ncong _S y\) implies \(f(x)\ncong _T f(y)\),

  • strongly extensional if for all \(x,y\in S\), \(f(x)\ncong _T f(y)\) implies \(x\ncong _S y\),

  • an apartness bijection if it is injective, bijective and strongly extensional (see [7]).

In the sequel, we will always deal with sets with apartness and, for brevity, a set with apartness \((X,\cong ,\ncong )\) will be denoted simply by X.

By \(\rhd \) we denote the relation between elements and subsets of X defined by
$$\begin{aligned} x\rhd Y {\mathop {\Longleftrightarrow }\limits ^{\text { def}}}\forall y\in Y\ (x\ncong y). \end{aligned}$$
The complement of Y in X is the subset
$$\begin{aligned} {\sim }Y{\mathop {=}\limits ^{\text { def}}}\{x\in X\mid x\rhd Y\}. \end{aligned}$$
A subset Y of a set X is detachable (or a d-subset) in X if
$$\begin{aligned} \forall x\in X\ (x\in Y\vee x\rhd Y), \end{aligned}$$
i.e.,
$$\begin{aligned} \forall x\in X\ (x\in Y\vee x\in {\sim } Y). \end{aligned}$$
Let Y and Z be two subsets of a set X, then \(Y\cong Z\) means that for each \(y\in Y\) there exists \(z\in Z\) such that \(y\cong z\) and for each \(z\in Z\) there exists \(y\in Y\) such that \(z\cong y\).

Definition 3

A partial apartness bijection on S is an apartness bijection from X to Y, where X and Y are subsets of S. As usual, the sets X and Y are called respectively the domain and the image of f and denoted by \({{\,\mathrm{Dom}\,}}(f)\) and \({{\,\mathrm{Im}\,}}(f)\). A d-partial bijection on S is a partial apartness bijection whose domain and codomain are d-subsets of S. We denote by \(I^S\) the set of all d-partial bijections on S.

On \(I^S\) we define an equality \(\cong \) as usual: \(f\cong g\) if and only if \({{\,\mathrm{Dom}\,}}(f)\cong {{\,\mathrm{Dom}\,}}(g)\) and for all \(x\in {{\,\mathrm{Dom}\,}}(f)\), \(f(x)\cong g(x)\). We define \(\ncong \) by
$$\begin{aligned} f\ncong g {\mathop {\Longleftrightarrow }\limits ^{\text { def}}}&\exists x (x\in {{\,\mathrm{Dom}\,}}(f) \wedge x\in {\sim } {{\,\mathrm{Dom}\,}}(g)) \vee \\&\exists x (x\in {\sim } {{\,\mathrm{Dom}\,}}(f)\wedge x\in {{\,\mathrm{Dom}\,}}(g))\vee \\&\exists x (x\in {{\,\mathrm{Dom}\,}}(f) \wedge x\in {{\,\mathrm{Dom}\,}}(g) \wedge f(x)\ncong g(x)). \end{aligned}$$

Example 1

Observe that in general the apartness on \(I^S\) is neither tight nor decidable w.r.t. \(\cong \). Indeed, let S be the set \(\{0,1,2,3\}\), let \(\cong \) be the standard equality on S, i.e.\(\cong {\mathop {=}\limits ^{\text { def}}}\{(0,0),(1,1),(2,2),(3,3)\}\) and let \(\ncong \) be the apartness defined by \(\ncong {\mathop {=}\limits ^{\text { def}}}\{(0,1),(1,2),(2,3),(3,0),(1,0),(2,1),(3,2),(0,3)\}\). Then let \(i,g:S\rightarrow S\) be respectively the identity map on S and the map defined by \(g(0){\mathop {=}\limits ^{\text { def}}}3\), \(g(1){\mathop {=}\limits ^{\text { def}}}2\), \(g(2){\mathop {=}\limits ^{\text { def}}}1\) and \(g(3){\mathop {=}\limits ^{\text { def}}}0\). The maps i and g are d-partial bijections and neither \(i\cong g\) nor \(i\ncong g\). Then the relation \(\ncong \) on \(I^S\) is not empty (as, for example, the identity map on the set \(\{0,2\}\) and the identity map on S are apart) but \(\ncong \) is neither tight nor decidable w.r.t. \(\cong \).

The following result is straightforward:

Theorem 1

Let \((S,\cong ,\ncong )\) be a set with apartness. Then \((I^S,\cong ,\ncong )\) is a set with apartness.

3 Inverse semigroups with apartness

Definition 4

An I-semigroup with apartness is an inhabited set with apartness \((S,\cong ,\ncong )\) equipped with an associative, strongly extensional binary operation on S, denoted by “\(\cdot \)”, and with a strongly extensional unary operation on S denoted by “\(^{-1}\)” such that \(\forall x\in S (x\cdot x^{-1}\cdot x\cong x)\) and \((x^{-1})^{-1} \cong x\). In other words, an I-semigroup with apartness is a tuple \((S,\cong ,\ncong ,\cdot ,^{-1})\) where
  1. 1.

    \((S,\cong ,\ncong )\) is an inhabited set with apartness,

     
  2. 2.
    \(\cdot \)” is a binary operation on S such that:
    1. (a)

      \(x\cdot (y\cdot z)\cong (x\cdot y)\cdot z\) for all \(x,y,z\in S\),

       
    2. (b)

      for all \(x,y,z\in S\), \(x\cdot y\ncong z\cdot v\) implies \(x\ncong z\) or \(y\ncong v\),

       
     
  3. 3.
    \(^{-1}\)” is a unary operation such that:
    1. (a)

      \((x^{-1})^{-1}\cong x\) for all \(x\in S\),

       
    2. (b)

      for all \(x,y\in S\), \(x^{-1}\ncong y^{-1}\) implies \(x\ncong y\),

       
     
  4. 4.

    \(x\cdot x^{-1}\cdot x\cong x\) for all \(x\in S\).

     

As usual, we will write xy instead of \(x\cdot y\).

Remark 2

Since we assumed that all properties we are dealing with are extensional, we immediately derive that \(\cdot \) and \(^{-1}\) are well defined, i.e., \(x\cong z\wedge y\cong v\) implies \(xy\cong zv\) for all \(x,y,z,v\in S\), and \(x\cong y\) implies \(x^{-1}\cong y^{-1}\) for all \(x,y\in S\). Moreover, by extensionality and 3(a), we also derive that for all \(x,y\in S\), \(x\ncong y\) implies \(x^{-1}\ncong y^{-1}\). Then, in the definition of an I-semigroup with apartness, condition 3(b) can be written as
  1. 3(b’)

    \(x^{-1}\ncong y^{-1} \Leftrightarrow x\ncong y\) for all \(x,y\in S\).

     
Moreover, condition 3(a) implies that \(x^{-1}xx^{-1}\cong x^{-1}\) for all \(x\in S\). Lastly, 3(a) and extensionality of \(^{-1}\) give that for all \(x,y\in S\)
$$\begin{aligned} x^{-1}\cong y^{-1}\Leftrightarrow x\cong y. \end{aligned}$$
(1)

Definition 5

An inverse semigroup with apartness is an I-semigroup with apartness \((S,\cong ,\ncong ,\cdot ,^{-1})\) such that
  1. 5.

    \(xx^{-1}yy^{-1}\cong yy^{-1}xx^{-1}\) for all \(x,y\in S\).

     

Remark 3

Observe that property 5. implies that \((xy)^{-1}\cong y^{-1}x^{-1}\).

An idempotent of S is an element \(e\in S\) such that \(ee\cong e\); we denote the set of the idempotents of S by E(S).

Proposition 1

Let S be an inverse semigroup with apartness. Then \(e\cong ee^{-1}\) and \(ef\cong fe\) for each \(e,f\in E(S)\).

Proof

The proof is the same of the classical case and can be found in [11, Theorem 5.1.1, \((1)\Rightarrow (2)\)]. \(\square \)

Proposition 2

A semigroup with apartness \((S,\cong ,\ncong ,\cdot )\) is an inverse semigroup if and only if the relation \(\iota {\mathop {=}\limits ^{\text { def}}}\{(x,y)\in S\times S\mid x\cong xyx \wedge y\cong yxy\}\) is a strongly extensional function from S to S.

Proof

Let \((S,\cong ,\ncong ,\cdot ,^{-1})\) be an inverse semigroup with apartness. Then for each \(x\in S\), \((x,x^{-1})\in \iota \). Now we show that \(y\cong x^{-1}\) for each \((x,y)\in \iota \). From \(xx^{-1}x\cong xyx\cong x\) we get \(xx^{-1}xy\cong xy\) and \(xyxx^{-1}\cong xx^{-1}\), and since xy and \(xx^{-1}\) are idempotents, it follows \(xy\cong xx^{-1}\). Similarly we get \(yx\cong x^{-1}x\). Then \(y\cong yxy\cong x^{-1}xy\cong x^{-1}xx^{-1}\cong x^{-1}\). Thus, \(\iota \) is the function \(^{-1}\), and since \(^{-1}\) is strongly extensional by definition, so is \(\iota \).

Conversely, assume that S is a semigroup with apartness such that \(\iota \) is a strongly extensional function from S to S. For \((x,y)\in \iota \), put \(x^{-1}\cong \iota (x)\). Then it is immediate that \((x^{-1})^{-1}\cong x\). Moreover, let \(e,f\in E(S)\): it is easy to verify that the element \(z{\mathop {=}\limits ^{\text { def}}}f(ef)^{-1}e\) belongs to E(S). In addition, \((ef)z(ef)\cong (ef)\) and \(z(ef)z \cong z\). Then, since \(z^3\cong z\), both (zz) and (zef) are in \(\iota \), so \(z\cong ef\). Whence \(fz\cong z\cong fef\) and \(ze\cong z\cong efe\), i.e., \(ef\cong _S fef \cong efe\). Similarly, we can get \(fe\cong efe \cong fef\). So, \(ef\cong fe\) for all \(e,f\in E(S)\). Moreover, \(\iota \) is strongly extensional by definition, whence S is an inverse semigroup with apartness. \(\square \)

Remark 4

The relation \(\iota \) defined above is a strongly extensional function from S to S if and only if S is equipped with a strongly extensional unary operation f such that for all \(x,x'\in X\) it holds that \(xf(x)x\cong x\), \(f(x)xf(x)\cong f(x)\), and \((xx'x\cong x \wedge x'xx'\cong x')\) implies \(x'\cong f(x)\).

Theorem 2

Let \((S,\cong ,\ncong )\) be a set with apartness. Then \((I^S,\cong ,\ncong ,\circ ,^{-1})\) is an inverse semigroup with apartness, where “\(\circ \)” is the usual product of relations and “\(^{-1}\)” denotes the inverse relation.

Proof

By Theorem 1, \((I^S,\cong ,\ncong )\) is a set with apartness. So, we start proving that for each \(f\in I^S\), the relation \(f^{-1}\) is a d-partial bijection from \({{\,\mathrm{Im}\,}}(f)\) to \({{\,\mathrm{Dom}\,}}(f)\), i.e., \(f^{-1}\in I^S\). Let \(f:X\rightarrow Y\) be a d-partial bijection, then \(f^{-1}\) is defined as
$$\begin{aligned} f^{-1}{\mathop {=}\limits ^{\text { def}}}\{(y,x)\mid f(x)\cong y\}\subseteq Y\times X. \end{aligned}$$
Let \(y\in Y\), then, as f is onto, there exists \(x\in X\) such that \(f(x)\cong y\), and so \((y,x)\in f^{-1}\). Let \(y,y'\in Y\) be such that \(y\cong y'\), and suppose \((y,x),(y',x')\in f^{-1}\). Then \(f(x)\cong y\), \(f(x')\cong y'\) and, by extensionality, \(f(x)\cong f(x')\). Since f is one-to-one, we have \(x\cong x'\), i.e., \((y,x)\cong (y',x')\). Hence, we have proved that \(f^{-1}\) is an extensional function from Y to X and we can write \(f^{-1}(y)\cong x\) instead of \((y,x)\in f^{-1}\). Now let \(x\in X\); clearly \(f(x)\in Y\) and \((f(x),x)\in f^{-1}\), so \(f^{-1}\) is onto.

Now, suppose \(f^{-1}(y)\cong f^{-1}(y')\), and let \(x,x'\in X\) be such that \(x\cong f^{-1}(y)\) and \(x'\cong f^{-1}(y')\). Then \((y,x),(y',x')\in f^{-1}\), so \(f(x)\cong y\) and \(f(x')\cong y'\). By extensionality we have \(x\cong x'\), then \(f(x)\cong f(x')\) and \(y\cong y'\), so \(f^{-1}\) is one-to-one. Now, suppose \(f^{-1}(y)\ncong f^{-1}(y')\) and, as above, let \(x,x'\in X\) be such that \(x\cong f^{-1}(y)\) and \(x'\cong f^{-1}(y')\) from which \(f(x)\cong y\) and \(f(x')\cong y'\). By extensionality, we have \(x\ncong x'\) and, since f is injective, it follows \(f(x)\ncong f(x')\) and then \(y\ncong y'\), so \(f^{-1}\) is strongly extensional. Finally, suppose \(y\ncong y'\) and, as usual, let \(x,x'\in X\) be such that \(x\cong f^{-1}(y)\), \(x'\cong f^{-1}(y')\), \(f(x)\cong y\) and \(f(x')\cong y'\). By extensionality, we have \(f(x)\ncong f(x')\), and since f is strongly extensional it follows \(x\ncong x'\) and then \(f^{-1}(y)\ncong f^{-1}(y')\), so \(f^{-1}\) is injective. Thus we have proved that \(f^{-1}\in I^S\).

Now, let \(f:X\rightarrow Y\) and \(g:U\rightarrow V\) be two d-partial bijections in \(I^S\). The product \(f\circ g\) is the usual product of relations, hence \((x,y)\in f\circ g\) if and only if there is \(z\in Y\cap U\) such that \(z\cong f(x)\) and \(y\cong g(z)\). Then
$$\begin{aligned} {{\,\mathrm{Dom}\,}}(f\circ g){\mathop {=}\limits ^{\text { def}}}\{x\in X\mid f(x)\in U\} \end{aligned}$$
and
$$\begin{aligned} {{\,\mathrm{Im}\,}}(f\circ g){\mathop {=}\limits ^{\text { def}}}\{y\in V\mid g^{-1}(y)\in Y\}. \end{aligned}$$
Having in mind that the intersection of d-subsets is again a d-subset, it is easy to observe that \({{\,\mathrm{Dom}\,}}(f\circ g)\) and \({{\,\mathrm{Im}\,}}(f\circ g)\) are also d-subsets. The fact that \(f\circ g\) belongs to \(I^S\) follows from a direct calculation similar to that we have performed for the inverse. The fact that the composition is associative directly follows by definition, so we only have to check that composition is strongly extensional.
Let \(f,g,h,k\in I^S\) and assume that \(f\circ g\ncong h\circ k\). By definition we have that
$$\begin{aligned}&\exists x \bigl (x\in {{\,\mathrm{Dom}\,}}(f\circ g) \wedge x\rhd {{\,\mathrm{Dom}\,}}(h\wedge k)\bigr ) \vee {}\\&\exists x \bigl (x\rhd {{\,\mathrm{Dom}\,}}(f\circ g)\wedge x\in {{\,\mathrm{Dom}\,}}(h\circ k)\bigr )\vee {} \\&\exists x \bigl (x\in {{\,\mathrm{Dom}\,}}(f\circ g) \wedge x\in {{\,\mathrm{Dom}\,}}(h\circ k) \wedge (f\circ g)(x)\ncong _S (h\circ k)(x)\bigr ). \end{aligned}$$
So, suppose \(x\in S\) is such that \(x\in {{\,\mathrm{Dom}\,}}(f\circ g) \wedge x\rhd {{\,\mathrm{Dom}\,}}(h\circ k)\). Then \(x\in {{\,\mathrm{Dom}\,}}(f)\), \(f(x)\in {{\,\mathrm{Dom}\,}}(g)\) and for all \(y\in S\), if \(y\in {{\,\mathrm{Dom}\,}}(h)\) and \(f(y)\in {{\,\mathrm{Dom}\,}}(k)\), then \(x\ncong y\). Since \({{\,\mathrm{Dom}\,}}(h)\) is a d-subset, it follows that \(x\in {{\,\mathrm{Dom}\,}}(h)\) or \(x\rhd {{\,\mathrm{Dom}\,}}(h)\). If \(x\rhd {{\,\mathrm{Dom}\,}}(h)\), since we have supposed \(x\in {{\,\mathrm{Dom}\,}}(f)\), we obtain \(f\ncong h\), so suppose \(x\in {{\,\mathrm{Dom}\,}}(h)\). Since also \({{\,\mathrm{Dom}\,}}(k)\) is a d-subset, it follows that \(f(x)\in {{\,\mathrm{Dom}\,}}(k)\) or \(f(x)\rhd {{\,\mathrm{Dom}\,}}(k)\). If \(f(x)\rhd {{\,\mathrm{Dom}\,}}(k)\), since we have supposed \(f(x)\in {{\,\mathrm{Dom}\,}}(g)\), we obtain \(g\ncong k\), so suppose \(f(x)\in {{\,\mathrm{Dom}\,}}(k)\). This last case implies \(x\in {{\,\mathrm{Dom}\,}}(h\circ k)\) and \(x\rhd {{\,\mathrm{Dom}\,}}(h\circ k)\), which gives a contradiction. The case in which there exists \(x\in S\) such that \(x\rhd {{\,\mathrm{Dom}\,}}(f\circ g)\wedge x\in {{\,\mathrm{Dom}\,}}(h\circ k)\) works analogously, so let us consider the case in which there exists \(x\in S\) such that \(x\in {{\,\mathrm{Dom}\,}}(f\circ g)\), \(x\in {{\,\mathrm{Dom}\,}}(h\circ w)\) and \(g(f(x))\ncong k(h(x))\). Then \(x\in {{\,\mathrm{Dom}\,}}(f)\), \(x\in {{\,\mathrm{Dom}\,}}(h)\) and \(f(x)\in {{\,\mathrm{Dom}\,}}(g)\). Since \({{\,\mathrm{Dom}\,}}(k)\) is a d-subset, hence either \(f(x)\rhd {{\,\mathrm{Dom}\,}}(k)\) or \(f(x)\in {{\,\mathrm{Dom}\,}}(k)\). In the former case we get \(g\ncong k\). In the latter, let us consider the element \(k(f(x))\in S\). Then, by cotransitivity, from \(g(f(x))\ncong k(h(x))\) it follows \(g(f(x))\ncong k(f(x))\), and then \(g\ncong k\), or \(k(f(x))\ncong k(h(x))\), and then \(f\ncong h\).

Now, let us consider inversion. The map \(^{-1}:I^S\rightarrow I^S\) sending each f in its inverse \(f^{-1}\) is clearly an unary strongly extensional operation on \(I^S\) and \((f^{-1})^{-1}\cong f\) for each \(f\in I^S\). Moreover, it is straightforward to prove that \(f^{-1}\circ f\) is the identity function on \({{\,\mathrm{Dom}\,}}(f^{-1})\) and that \(f\circ f^{-1}\) is the identity function on \({{\,\mathrm{Dom}\,}}(f)\), and hence \(f\circ f^{-1}\circ f\cong f\) for each \(f\in I^S\). Lastly, for all \(f,g\in I^S\), the function \((f\circ f^{-1})\circ (g\circ g^{-1})\) is the identity function on \({{\,\mathrm{Dom}\,}}(f)\cap {{\,\mathrm{Dom}\,}}(g)\), while \((g\circ g^{-1})\circ (f\circ f^{-1})\) is the identity function on \({{\,\mathrm{Dom}\,}}(g)\cap {{\,\mathrm{Dom}\,}}(f)\), and so \((f\circ f^{-1})\circ (g\circ g^{-1})\cong (g\circ g^{-1})\circ (f\circ f^{-1})\). \(\square \)

Definition 6

Let \((S,\cong ,\ncong )\) be a set with apartness. The semigroup
$$\begin{aligned} (I^S,\cong ,\ncong ,\circ ,^{-1}) \end{aligned}$$
is called the symmetric inverse semigroup with apartness on S.

Lemma 1

Let \((S,\cong ,\ncong ,\cdot ,^{-1})\) be an inverse semigroup with apartness. Then:
  1. 1.

    \(Se\cong Sf \Rightarrow e\cong f\) and \(eS\cong fS \Rightarrow e\cong f\) for all \(e,f\in E(S)\);

     
  2. 2.

    \((Se\cap Sf)\cong S(ef)\) and \((eS\cap fS)\cong (ef)S\) for all \(e,f\in E(S)\);

     
  3. 3.

    \(S(aa^{-1})\cong Sa^{-1}\), \(S(a^{-1}a)\cong Sa\), \((aa^{-1})S\cong aS\) and \((a^{-1}a)S\cong a^{-1}S\) for all \(a\in S\).

     

Proof

The proof is analogous to the classical case ( [11], Lemma 5.1.6). \(\square \)

Proposition 3

Let \((S,\cong ,\ncong ,\cdot ,^{-1})\) be an inverse semigroup with apartness and suppose that \(e\cong f\) or \(e\ncong f\) for all \(e,f\in E(S)\), i.e., \(\cong \) and \(\ncong \) are relatively decidable in E(S). Then, for each \(a\in S\), the sets Sa, aS, \(Sa^{-1}\) and \(a^{-1}S\) are detachable.

Proof

First observe that \(x\in Sa\) if and only if \(xa^{-1}a\cong x\). Indeed, suppose \(x\in Sa\), i.e., \(x\cong sa\) for some \(s\in S\). Since \(sa\cong saa^{-1}a\), we have immediately \(x\cong xa^{-1}a\). Conversely, it is obvious that if \(x\cong xa^{-1}a\), then \(x\in Sa\). Now we can prove that Sa is a d-subset. Let \(x\in S\): as \(x^{-1}x\) and \(a^{-1}a\) are idempotents, then \(x^{-1}x\cong x^{-1}xa^{-1}a\) or \(x^{-1}x\ncong x^{-1}xa^{-1}a\). By extensionality, the former condition implies \(xx^{-1}x\cong xx^{-1}xa^{-1}a\), i.e., \(x\cong xa^{-1}a\), and then \(x\in Sa\). Now suppose that \(x^{-1}x\ncong x^{-1}xa^{-1}a\). By cotransitivity w.r.t. the product, we get \(x^{-1}\ncong x^{-1}\) or \(x\ncong xa^{-1}a\), and, by irreflexivity, it follows \(x\ncong xa^{-1}a\). So, let \(y\in Sa\), by the cotransitivity of apartness we get \(x\ncong y\) or \(y\ncong xa^{-1}a\). In the last case, since \(y\in Sa\), we have \(y\cong ya^{-1}a\), and then, by extensionality, \(ya^{-1}a\ncong xa^{-1}a\), so, by cotransitivity, \(y\ncong x\), and hence \(x\rhd Sa\). Thus we have proved that Sa is a d-subset, and similarly we obtain the same result for aS, \(Sa^{-1}\) and \(a^{-1}S\). \(\square \)

Definition 7

Let S and T be semigroups with apartness. A map \(f :S \rightarrow T\) is a homomorphism if \(f(xy) \cong f(x)f(y)\). A strongly extensional homomorphism (se-homomorphism for short) is an apartness embedding if it is one-one and injective. An se-homomorphism is an apartness isomorphism if it is an apartness bijection.

Definition 8

Let \((S,\cong _S,\ncong _S),\ (T,\cong _T,\ncong _T)\) be two semigroups with apartness. The semigroup \((S,\cong _S,\ncong _S)\) is se-embeddable in \((T,\cong _T,\ncong _T)\) if there exists an apartness embedding \(\varphi :S\rightarrow T\).

Theorem 3

Let \((S,\cong ,\ncong ,\cdot ,^{-1})\) be an inverse semigroup with apartness and suppose that \(e\cong f\) or \(e\ncong f\) for all \(e,f\in E(S)\), i.e., \(\cong \) and \(\ncong \) are relatively decidable in E(S). Then S is se-embeddable in the symmetric inverse semigroup with apartness \((I^S,\cong ,\ncong ,\circ ,^{-1})\) on the set \((S,\cong ,\ncong )\).

Proof

For each \(a\in S\), let \(\rho _a\) be the map with \({{\,\mathrm{Dom}\,}}(\rho _a){\mathop {=}\limits ^{\text { def}}}Sa^{-1}\) defined by \(\rho _a(x){\mathop {=}\limits ^{\text { def}}}xa\). Clearly \({{\,\mathrm{Im}\,}}(\rho _a)\cong Sa\) and so, by Proposition 3, the domain and the image of \(\rho _a\) are d-subsets. Obviously, the map \(\rho _a\) is extensional. It is onto, since \(sa\cong \rho _a (saa^{-1})\) for each \(s\in S\). Now let \(x,y \in Sa^{-1}\), by definition \(x\cong sa^{-1}\) and \(y\cong ta^{-1}\) for some \(s,t\in S\). If \(\rho _a(x)\cong \rho _a(y)\), i.e., \((sa^{-1})a \cong (ta^{-1})a\), by extensionality we have \(sa^{-1}aa^{-1} \cong ta^{-1}aa^{-1}\), whence \(x\cong sa^{-1}\cong ta^{-1}\cong y\), as so \(\rho _a\) is one-to-one. If \(x\ncong y\), we have \(sa^{-1} \ncong ta^{-1}\) and then \(sa^{-1}aa^{-1} \ncong ta^{-1}aa^{-1}\). Then \(xaa^{-1} \ncong yaa^{-1}\) and, by extensionality w.r.t. the product, \(xa \ncong ya\), or equivalently \(\rho _a(x)\ncong \rho _a(y)\), and thus \(\rho _a\) is injective. The fact that \(\rho _a\) is strongly extensional follows directly from the fact that the product in S is strongly extensional. Therefore \(\rho _a\) is a d-partial bijection on S.

Let \(\varphi :S\rightarrow I^S\) be the map defined by \(\varphi (a){\mathop {=}\limits ^{\text { def}}}\rho _a\) for each \(a\in S\). Then, as in the classical case, \(\varphi \) is one-to-one. Indeed, assume that \(\varphi (a)\cong \varphi (b)\), then \({{\,\mathrm{Dom}\,}}(\rho _a)\cong {{\,\mathrm{Dom}\,}}(\rho _b)\) and so, by property 3 of Lemma 1, we get \(S(aa^{-1})\cong S(bb^{-1})\). Hence, by property 1. of Lemma 1, we obtain \(aa^{-1}\cong _S bb^{-1}\), and then \(a\cong aa^{-1}a\cong \rho _a(aa^{-1})\cong \rho _b(aa^{-1})\cong \rho _b(bb^{-1})\cong b\).

Now, we show that \(\varphi \) is strongly extensional. Assume that \(\varphi (a)\ncong \varphi (b)\). Since \({{\,\mathrm{Dom}\,}}(\rho _b)\) is a d-subset of S, then \(a^{-1}\in {{\,\mathrm{Dom}\,}}(\rho _b)\vee a^{-1}\rhd {{\,\mathrm{Dom}\,}}(\rho _b)\), and analogously \(b^{-1}\in {{\,\mathrm{Dom}\,}}(\rho _a)\vee b^{-1}\rhd {{\,\mathrm{Dom}\,}}(\rho _a)\).

If \(a^{-1}\rhd {{\,\mathrm{Dom}\,}}(\rho _b)\) then, since \(b^{-1}\in {{\,\mathrm{Dom}\,}}(\rho _b)\), we get \(a^{-1}\ncong _S b^{-1}\). Analogously, if \(b^{-1}\rhd {{\,\mathrm{Dom}\,}}(\rho _a)\) then, since \(a^{-1}\in {{\,\mathrm{Dom}\,}}(\rho _a)\), we get \(a^{-1}\ncong _S b^{-1}\). In both cases, from the strong extensionality of inversion, we get \(a\ncong _S b\). Then assume \(a^{-1}\in {{\,\mathrm{Dom}\,}}(\rho _b)\) and \(b^{-1}\in {{\,\mathrm{Dom}\,}}(\rho _a)\). Hence \({{\,\mathrm{Dom}\,}}(\rho _b)\cong Sb^{-1}\cong Sa^{-1}\cong {{\,\mathrm{Dom}\,}}(\rho _a)\). Since \(\varphi (a)\ncong \varphi (b)\), we get that there is \(x\in {{\,\mathrm{Dom}\,}}(\rho _a)\cong {{\,\mathrm{Dom}\,}}(\rho _b)\) such that \(\rho _a(x)\ncong _S \rho _b(x)\), i.e., \( x\cdot a\ncong _S x\cdot b\), and, by strong extensionality, it follows \(a\ncong _S b\). So, we have proved that \(\varphi \) is a d-partial bijection.

It is routine to prove that \(\rho _a\circ \rho _b\cong \rho _{a\cdot b}\) and \((\rho _a)^{-1}\cong \rho _{a^{-1}}\), so \(\varphi \) is an se-embedding, as required. \(\square \)

Notice that Theorem 3 is stated under the assumption that \(\cong \) and \(\ncong \) are relatively decidable on the set of idempotents. In general, an inverse semigroup with apartness \((S,\cong ,\ncong ,\cdot ,^{-1})\) cannot be embedded into the symmetric inverse semigroup with apartness \((I^S,\cong ,\ncong ,\circ ,^{-1})\), as the next example shows.

Example 2

Let \(S{\mathop {=}\limits ^{\text { def}}}\{0,1,2\}\) be the semilattice with the following multiplication table.Let \(\cong \) be the standard equality, i.e., \(\cong {\mathop {=}\limits ^{\text { def}}}\{(0,0),(1,1),(2,2)\}\), and let \(\ncong \) be the relation \(\{(0,1),(1,0),(1,2),(2,1)\}\). It is easy to prove that \((S,\cong ,\ncong ,\cdot ,^{-1})\) is an inverse semigroup with apartness. The d-subsets of S are \(\emptyset \), \(\{1\}\), \(\{0,2\}\) and S. Then the d-partial bijections on S are: the identity maps on \(\emptyset \), \(\{1\}\), \(\{0,2\}\) and S, denoted respectively by \(i_\emptyset \), \(i_{\{1\}}\), \(i_{\{0,2\}}\) and \(i_S\), the map \(f:\ \{0,2\}\rightarrow \{0,2\}\) defined by \(f(0){\mathop {=}\limits ^{\text { def}}}2\) and \(f(2){\mathop {=}\limits ^{\text { def}}}0\), and the map \(g:\ S\rightarrow S\) defined by \(g(0){\mathop {=}\limits ^{\text { def}}}2\), \(g(1){\mathop {=}\limits ^{\text { def}}}1\) and \(g(2){\mathop {=}\limits ^{\text { def}}}0\). The composition table for \(I^S\) isThe relation \(\cong \) on \(I^S\) is the standard equality, while \(\ncong \) is the standard inequality. As \(E(S)=S\), then the image of any se-homomorphism from S to \(I^S\) is contained in the set \(E(I^S){\mathop {=}\limits ^{\text { def}}}\{i_\emptyset , i_{\{1\}},i_{\{0,2\}},i_S\}\). Then there are only two one-to-one homomorphisms from S to \(I^S\), namely the map \(\rho \) defined by \(\rho (0){\mathop {=}\limits ^{\text { def}}}i_\emptyset \), \(\rho (1){\mathop {=}\limits ^{\text { def}}}i_{\{0,2\}}\) and \(\rho (2){\mathop {=}\limits ^{\text { def}}}i_S\), and the map \(\sigma \) defined by \(\sigma (0){\mathop {=}\limits ^{\text { def}}}i_\emptyset \), \(\sigma (1){\mathop {=}\limits ^{\text { def}}}i_{\{1\}}\) and \(\sigma (2){\mathop {=}\limits ^{\text { def}}}i_S\). Nevertheless, neither \(\rho \) nor \(\sigma \) is injective as \(i_\emptyset \ncong i_S\) but \(\lnot (0\ncong 2)\). Hence, S is not se-embeddable in \(I^S\), since the apartness on S is not compatible with the apartness on the set \(I^S\).

4 I-cocongruences

Congruences play a central role in many of the structure theorems of semigroups, so it is quite natural to study their constructive counterparts. Cocongruences are introduced in [7], where the prefix “co” suggests that they cooperate with classical equivalences in order to contemplate the presence of the apartness relation. Cocongruences are then defined as follows.

Definition 9

A binary relation \(\kappa \) on a semigroup with apartness S is a cocongruence if
  1. 1.

    it is consistent with respect to the apartness, i.e., \(\kappa \subseteq \ncong \),

     
  2. 2.

    it is cotransitive, i.e., \((x,y)\in \kappa \) implies \((x,z)\in \kappa \) or \((z,y)\in \kappa \),

     
  3. 3.

    it is symmetric, i.e., \((x,y)\in \kappa \) implies \((y,x)\in \kappa \),

     
  4. 4.

    it is cocompatible w.r.t. the semigroup multiplication, i.e., \((ax,by)\in \kappa \) implies \((a,b)\in \kappa \) or \((x,y)\in \kappa \).

     

Lemma 2

Let \(\kappa \) be a consistent and cotransitive binary relation on a semigroup with apartness S. Then \(\kappa \) is cocompatible w.r.t. the semigroup multiplication if and only if for all \(a,b,c\in S\)
  1. 4’.

    \((ac,bc)\in \kappa \) implies \((a,b)\in \kappa \) and \((ca,cb)\in \kappa \) implies \((a,b)\in \kappa \) .

     

Proof

Let \(\kappa \) be cocompatible w.r.t. the multiplication of S, and \(a,b,c\in S\). Then \((ac,bc)\in \kappa \) implies either \((a,b)\in \kappa \) or \((c,c)\in \kappa \). As \(\kappa \) is consistent, then \(\lnot ((c,c)\in \kappa )\), and then actually \((a,b)\in \kappa \). The case \((ca,cb)\in \kappa \) is identical.

Now, let \(\kappa \) be a consistent and cotransitive binary relation that satisfies condition 4’.

Let \(a,b,x,y\in S\) be such that \((ax,by)\in \kappa \). By cotransitivity, it follows either \((ax,ay)\in \kappa \) or \((ay,by)\in \kappa \), and, by condition 4’, either \((x,y)\in \kappa \) or \((a,b)\in \kappa \), as required. \(\square \)

In the case of inverse semigroups with apartness, we have to add the cocompatibility with respect to the inversion.

Definition 10

A binary relation \(\kappa \) on an inverse semigroup with apartness \((S,\cong ,\ncong ,\cdot ,^{-1})\) is an I-cocongruence if it is a cocongruence on \((S,\cong ,\ncong ,\cdot )\) and it is cocompatible w.r.t. the inversion, i.e., \((a^{-1},b^{-1})\in \kappa \) implies \((a,b)\in \kappa \) for all \(a,b\in S\).

Proposition 4

Let \(\kappa \) be an I-cocongruence on an inverse semigroup with apartness S. Then for all \(a,b\in S\),
$$\begin{aligned}&(a^{-1},b^{-1})\in \kappa \text { if and only if } (a,b)\in \kappa , \end{aligned}$$
(2)
$$\begin{aligned}&(a^{-1},b^{-1})\rhd \kappa \text { if and only if } (a,b)\rhd \kappa . \end{aligned}$$
(3)

Proof

Property (2) follows directly from the cocompatibility with respect to the inversion and condition 3(a) of Definition 4. To prove property (3), let \((a,b)\rhd \kappa \) and let \((c,d)\in \kappa \). Then also \((c^{-1},d^{-1})\in \kappa \), and so \((a,b)\ncong (c^{-1},d^{-1})\). Thus either \(a\ncong c^{-1}\) or \(b\ncong d^{-1}\). From condition 3(b’) of Definition 4, it follows either \(a^{-1}\ncong c\) or \(b^{-1}\ncong d\), thus \((a^{-1},b^{-1})\ncong (c,d)\) and then \((a^{-1},b^{-1})\rhd \kappa \). The other part of the implication follows in the same way. \(\square \)

Following a common notation, for an I-cocongruence \(\kappa \) on S and for \(a\in S\) we denote by \(\kappa (a)\) the set of all \(b\in S\) such that \((a,b)\in \kappa \).

Definition 11

An I-cocongruence \(\kappa \) is called conormal if for all \(a\in S\) and for all \(e,f\in E(S)\), \((a^{-1}ea,a^{-1}fa)\in \kappa \) implies \((e,f)\in \kappa \).

Strictly related to I-cocongruences, we can define some special substructure of inverse semigroups.

Definition 12

A subset M of an inverse semigroup S is an inverse antisubsemigroup if
  1. 1.

    \(xy\in M\) implies \(x\in M\vee y\in M\),

     
  2. 2.

    \(x^{-1}\in M\) implies \(x\in M\).

     
We say that an inverse antisubsemigroup M is
  1. 1.

    cofull if \(e\rhd M\) for all \(e\in E(S)\);

     
  2. 2.

    coself-conjugate if \(x^{-1}ax\in M\) implies \(a\in M\) for all \(a,x\in S\);

     
  3. 3.

    conormal if it is cofull and coself-conjugate.

     

In [21], Wagner proved that every congruence on an inverse semigroup is completely determined by its idempotent classes. The advances made in [9, 17, 19] lead to a general result describing the congruences on an inverse semigroup, see [13, Theorem 2, p. 135]: for an inverse semigroup S, there exists a bijection between the set of congruences on S and the set of congruence pairs (namely, a pair consisting of a normal subsemigroup and a normal congruence satisfying some special conditions) on S. Along the same line, we want to give a characterization of I-cocongruences on an inverse semigroup with apartness in terms of “cocongruence pairs”.

Definition 13

A cocongruence pair\((M,\kappa )\) on an inverse semigroup with apartness S consists of a conormal inverse antisubsemigroup M and a conormal I-cocongruence \(\kappa \) on E(S) such that
  1. 1.

    \(ae\in M \vee (e,a^{-1}a)\in \kappa \) for all \(a\in M\) and for all \(e\in E(S)\);

     
  2. 2.

    \((aa^{-1},a^{-1}a)\in \kappa \) implies \(a\in M\) for all \(a\in S\).

     

Definition 14

Let \(\kappa \) be an I-cocongruence on an inverse semigroup with apartness S. The cokernel of \(\kappa \) is defined as
$$\begin{aligned} {{\,\mathrm{coker}\,}}(\kappa ){\mathop {=}\limits ^{\text { def}}}\bigcap _{e\in E(S)}\kappa (e), \end{aligned}$$
while the trace of \(\kappa \) is the restriction of \(\kappa \) to E(S), i.e.,
$$\begin{aligned} {{\,\mathrm{tr}\,}}(\kappa ){\mathop {=}\limits ^{\text { def}}}\kappa _{\big |(E(S)\times E(S))}. \end{aligned}$$

Theorem 4

Let S be an inverse semigroup with apartness and let \(\kappa \) be an I-cocongruence on S. Let \(M{\mathop {=}\limits ^{\text { def}}}{{\,\mathrm{coker}\,}}(\kappa )\) and \(\nu {\mathop {=}\limits ^{\text { def}}}{{\,\mathrm{tr}\,}}(\kappa )\). Then \((M,\nu )\) is a cocongruence pair.

Proof

Obviously \(\nu \) is a conormal I-cocongruence on E(S). Let us prove that M is an inverse antisubsemigroup of S. Let \(xy\in M\), then for all \(e,f\in E(S)\) we have \(xy\in \kappa (ef)\), i.e., \((xy,ef)\in \kappa \). By the cocompatibility w.r.t. the product, it follows that \((x,e)\in \kappa \vee (y,f)\in \kappa \). From Kripke semantics, this entails that either \((x,e)\in \kappa \) for each \(e\in E(S)\), and so \(x\in M\), or \((y,f)\in \kappa \) for all \(f\in E(S)\), and so \(y\in M\). Now suppose \(x^{-1}\in M\). Then \((x^{-1},e)\in \kappa \) for all \(e\in E(S)\) and, since \(e\cong e^{-1}\) and \(\kappa \) is cocompatible w.r.t. the inversion, we have \((x,e)\in \kappa \), and so \(x\in M\). We now prove that M is cofull. Let \(e\in E(S)\) and \(x\in M\). Then \(x\in \kappa (e)\), i.e., \((x,e)\in \kappa \). As \(\kappa \) is consistent, this implies \(x\ncong e\), and then, for the generality of \(x\in S\), we get \(e\rhd M\). Now, to prove that M is coself-conjugate, let \(x^{-1}ax\in M\). We have that for all \(e\in E(S)\), the element \(x^{-1}ex\) belongs to E(S), and then \((x^{-1}ax,x^{-1}ex)\in \kappa \). Property 4’ of Lemma 2 implies \((a,e)\in \kappa \), i.e., for the generality of \(e\in E(S)\), that \(a\in M\). So M is a conormal inverse antisubsemigroup of S.

Lastly, we prove that \((M,\nu )\) is a cocongruence pair. Let \(a\in M\), \(e,f\in E(S)\). As M is the cokernel of \(\kappa \), by definition we have \((a,f)\in \kappa \). Considering the element \(ae\in S\), by cotransitivity of \(\kappa \), we get either \((a,ae)\in \kappa \) or \((ae,f)\in \kappa \). In the former case, we also have \((aa^{-1}a,ae)\in \kappa \), and by Lemma 2, property 4’, we obtain \((a^{-1}a,e)\in \kappa \) and then \((a^{-1}a,e)\in \nu \). Thus, by the symmetry of \(\nu \), we have \((e,a^{-1}a)\in \nu \). In the latter case, we have \(ae\in \kappa (f)\) and, for the generality of f, it follows that \(ae\in M\). Now, suppose \((aa^{-1},a^{-1}a)\in \nu \). Then, for each \(e\in E(S)\), we get \((aa^{-1},e)\cong (aa^{-1},ee^{-1})\in \nu \subseteq \kappa \) or \((e,a^{-1}a)\cong (e^{-1}e,a^{-1}a)\in \nu \subseteq \kappa \), then, by the cocompatibility of \(\kappa \) w.r.t. the product and inversion and symmetry, we have \((a,e)\in \kappa \). \(\square \)

Before proving that Theorem 4 can be in some sense inverted, we need a technical lemma.

Lemma 3

Let S be an inverse semigroup with apartness, \((M,\nu )\) a cocongruence pair on S, \(a,b\in S\) and \(e\in E(S)\). Then
  1. 1.

    if \(ab\in M\), then \(aeb\in M\) or \((e,a^{-1}a)\in \nu \);

     
  2. 2.

    if \(aeb\in M\), then \(ab\in M\).

     

Proof

Assume \(ab\in M\), since \((M,\nu )\) is a cocongruence pair and \(b^{-1}eb\in E(S)\), we have \(ab(b^{-1}eb)\in M\) or \((b^{-1}eb,(ab)^{-1}ab)\in \nu \). In the former case we have \(ab(b^{-1}eb)\cong ae(bb^{-1})b\cong aeb\in M\); in the latter case, by property 4’ of Lemma 2, we have \((e,a^{-1}a)\in \nu \), and then the first claim is proved.

Now let \(aeb\in M\). Then \(aeb\cong aebb^{-1}b\cong abb^{-1}eb\in M\). From the definition of inverse antisubsemigroup it follows \(ab\in M\) or \(b^{-1}eb\in M\). The second case gives a contradiction, as M is cofull, and then also the second statement is proved. \(\square \)

We are now able to prove that each cocongruence pair implicitly defines a (minimal) I-cocongruence on an inverse semigroup with apartness.

Theorem 5

Let \((M,\nu )\) be a cocongruence pair on an inverse semigroup with apartness S. Define the relation \(\kappa _{(M,\nu )}\) on S in the following way:
$$\begin{aligned} \begin{aligned} \kappa _{(M,\nu )}{\mathop {=}\limits ^{\text { def}}}&\{(a,b)\in S\times S\mid ab^{-1}\in M \vee a^{-1}b\in M \vee \\&(a^{-1}a,b^{-1}b)\in \nu \vee (aa^{-1},bb^{-1})\in \nu \vee \\&(a^{-1}fa,b^{-1}fb)\in \nu \vee (afa^{-1},bfb^{-1})\in \nu \text { for some }f\in E(S)\}. \end{aligned} \end{aligned}$$
Then \(\kappa _{(M,\nu )}\) is the smallest I-cocongruence on S having M as its cokernel and \(\nu \) as its trace.

Proof

Let \((M,\nu )\) be a cocongruence pair. The relation \(\kappa _{(M,\nu )}\) is consistent because \(\nu \) is consistent and M is cofull. It is symmetric because \(\nu \) is symmetric and M is an inverse antisubsemigroup. We now prove that \(\kappa _{(M,\nu )}\) is also cotransitive. Let \(x,y\in S\) such that \((x,y)\in \kappa _{(M,\nu )}\) and let \(z\in S\). Note that \(z^{-1}z\in E(S)\). If \(xy^{-1}\in M\), then from Lemma 3 we have \(xz^{-1}zy^{-1}\in M\) or \((z^{-1}z,x^{-1}x)\in \nu \). In the former case, from the definition of inverse antisubsemigroup, we have either \(xz^{-1}\in M\) or \(zy^{-1}\in M\), and then either \((x,z)\in \kappa _{(M,\nu )}\) or \((z,y)\in \kappa _{(M,\nu )}\). In the latter case, it follows directly from the definition of \(\kappa _{(M,\nu )}\) that \((z,x)\in \kappa _{(M,\nu )}\), and by symmetry, also \((x,z)\in \kappa _{(M,\nu )}\). The case \(x^{-1}y\in M\) is identical, so consider the case \((x^{-1}x,y^{-1}y)\in \nu \). By cotransitivity of \(\nu \), we have either \((x^{-1}x,z^{-1}z)\in \nu \) or \((z^{-1}z,y^{-1}y)\in \nu \), and then directly from the definition of \(\kappa _{(M,\nu )}\), it follows that either \((x,z)\in \kappa _{(M,\nu )}\) or \((z,y)\in \kappa _{(M,\nu )}\). The case \((xx^{-1},yy^{-1})\in \nu \) is clearly identical, so consider the case \((x^{-1}fx,y^{-1}fy)\in \nu \) for some \(f\in E(S)\). Again, by cotransitivity of \(\nu \), we have either \((x^{-1}fx,z^{-1}fz)\in \nu \) or \((z^{-1}fz,y^{-1}fy)\in \nu \), and then directly from the definition of \(\kappa _{(M,\nu )}\), it follows that either \((x,z)\in \kappa _{(M,\nu )}\) or \((z,y)\in \kappa _{(M,\nu )}\). The case \((xfx^{-1},yfy^{-1})\in \nu \) for some \(f\in E(S)\) is identical, so we have proved that \(\kappa _{(M,\nu )}\) is cotransitive.

Now we prove that \(\kappa _{(M,\nu )}\) is cocompatible w.r.t. the product showing that it satisfies condition 4’ of Lemma 2. Let \(a,b,c\in S\). First suppose \((ac,bc)\in \kappa _{(M,\nu )}\). If \(ac(bc)^{-1}\cong acc^{-1}b^{-1}\in M\), then, as \(cc^{-1}\in E(S)\), by Lemma 3 it follows \(ab^{-1}\in M\) and so \((a,b)\in \kappa _{(M,\nu )}\). If \((ac)^{-1}bc\cong c^{-1}a^{-1}bc\in M\), then, as M is coself-conjugate, it follows \(a^{-1}b\in M\) and so \((a,b)\in \kappa _{(M,\nu )}\). If \(((ac)^{-1}ac,(bc)^{-1}bc)\cong (c^{-1}a^{-1}ac,c^{-1}b^{-1}bc)\in \nu \), then, by conormality of \(\nu \), it follows \((a^{-1}a,b^{-1}b)\) and so \((a,b)\in \kappa _{(M,\nu )}\). If \((ac(ac)^{-1},bc(bc)^{-1})\cong (acc^{-1}a^{-1},bcc^{-1}b^{-1})\in \nu \), then, as \(cc^{-1}\in E(S)\), it follows directly by definition that \((a,b)\in \kappa _{(M,\nu )}\).

The cases \(((ac)^{-1}fac,(bc)^{-1}fbc)\in \nu \) and \((acf(ac)^{-1},bcf(bc)^{-1})\in \nu \) with \(f\in E(S)\) are identical to the two previous cases. Analogously we can prove that \((ca,cb)\in \kappa _{(M,\nu )}\) implies \((a,b)\in \kappa _{(M,\nu )}\). Lastly, the fact that \(\kappa _{(M,\nu )}\) is also cocompatible w.r.t. the inversion directly follows by definition, and then \(\kappa _{(M,\nu )}\) is actually a I-cocongruence on S.

We now prove that the cokernel and the trace of \(\kappa _{(M,\nu )}\) are M and \(\nu \), respectively. Let \(a\in M\), and \(e\in E(S)\). Then, as \((M,\nu )\) is a cocongruence pair, we get either \(ae\cong ae^{-1}\in M\) or \((e,a^{-1}a)\cong (e^{-1}e,a^{-1}a)\in \nu \) and in both cases \((a,e)\in \kappa _{(M,\nu )}\), and so \(a\in {{\,\mathrm{coker}\,}}(\kappa _{(M,\nu )})\). Conversely, let \(a\in {{\,\mathrm{coker}\,}}(\kappa _{(M,\nu )})\). Then, for all \(e\in E(S)\) it is \((a,e)\in \kappa _{(M,\nu )}\), and in particular \((a,a^{-1}a)\in \kappa _{(M,\nu )}\).

Observe that \({\lnot }((a^{-1}a,a^{-1}aa^{-1}a)\in \nu )\) as \((a^{-1}a,a^{-1}aa^{-1}a)\in \nu \) would entail \((a^{-1}a,a^{-1}a)\in \nu \), and, since \(\nu \) is consistent, this is a contradiction.

Then one of the following five cases holds. If \(aa^{-1}a \in M\), then \(a\in M\). If \(a^{-1}a^{-1}a \in M\), then, as Mis coself-conjugate, we have \(a^{-1} \in M\) and again \(a\in M\).

If \((a^{-1}a,aa^{-1}aa^{-1})\in \nu \), then \((a^{-1}a,aa^{-1})\in \nu \), and, by definition of cocongruence pair, we have \(a\in M\). If \((a^{-1}fa,a^{-1}afa^{-1}a)\in \nu \) for some \(f\in E(S)\), then it follows also \((a^{-1}fa,fa^{-1}af)\in \nu \). Let us consider the element \(faa^{-1}f\in E(S)\). By the cotransitivity of \(\nu \) we have either \((a^{-1}fa,faa^{-1}f)\in \nu \) or \((faa^{-1}f,fa^{-1}af)\in \nu \). In the former case we have \((a^{-1}fa,faa^{-1}f)\cong (a^{-1}f(a^{-1}f)^{-1},(a^{-1}f)^{-1}a^{-1}f)\in \nu \), and then, as \((M,\nu )\) is a cocongruence pair, it follows \(a^{-1}f\in M\) and, remembering that by definition \(f\rhd M\), also \(a^{-1}\in M\) and \(a\in M\). In the latter case we obtain \((f^{-1}aa^{-1}f,f^{-1}a^{-1}af)\in \nu \), and by conormality of \(\nu \), we have \((aa^{-1},a^{-1}a)\in \nu \) and then \(a\in M\). Thus we have proved that \({{\,\mathrm{coker}\,}}(\kappa _{(M,\nu )})\cong M\).

Now let \(e,f\in E(S)\) such that \((e,f) \in \nu \). Then \((ee^{-1},ff^{-1}) \in \nu \), and so \((e,f) \in {{\,\mathrm{tr}\,}}(\kappa _{(M,\nu )})\). So, let \((e,f) \in {{\,\mathrm{tr}\,}}(\kappa _{(M,\nu )})\). In particular we have \((e,f) \in \kappa _{(M,\nu )}\). As \(e^{-1}f\) and \(ef^{-1}\) are both idempotents and M is cofull, we only have to consider the following four cases. Let \((e^{-1}e,f^{-1}f) \in \nu \) or \((ee^{-1},ff^{-1}) \in \nu \), then both cases give \((e,f) \in \nu \), as required. If \((e^{-1}ge,f^{-1}gf) \in \nu \) for some \(g\in E(S)\), then \((geg^{-1},gfg^{-1}) \in \nu \) and, by conormality of \(\nu \), again we have \((e,f) \in \nu \). The case \((ege^{-1},fgf^{-1}) \in \nu \) for some \(g\in E(S)\) is identical to the previous one. Thus we have proved that \({{\,\mathrm{tr}\,}}(\kappa _{(M,\nu )})\cong \nu \).

Finally, we prove that \(\kappa _{(M,\nu )}\) is the smallest I-cocongruence on S having M and \(\nu \) as its cokernel and its trace, respectively. Let \(\tau \) be a cocongruence on S such that \({{\,\mathrm{coker}\,}}(\tau )\cong M\) and \({{\,\mathrm{tr}\,}}(\tau )\cong \nu \), and \((a,b)\in \kappa _{(M,\nu )}\). If \(ab^{-1}\in M\), then \((ab^{-1},aa^{-1})\in \tau \), as M is the cokernel of \(\tau \) and \(aa^{-1}\in E(S)\). As \(\tau \) is an I-cocongruence, from condition 4’ of Lemma 2, we have \((b^{-1},a^{-1})\in \tau \), and then \((a,b)\in \tau \). The case \(a^{-1}b\in M\) is analogous, as it entails \((a^{-1}b,a^{-1}a)\in \tau \) and then \((a,b)\in \tau \). If \((a^{-1}a,b^{-1}b)\in \nu \cong {{\,\mathrm{tr}\,}}(\tau )\), then \((a^{-1}a,b^{-1}b)\in \tau \). Let us consider the element \(a^{-1}b\in S\), by cotransitivity of \(\tau \) we have either \((a^{-1}a,a^{-1}b)\in \tau \) or \((a^{-1}b,b^{-1}b)\in \tau \) and in any case, from condition 4’ of Lemma 2, we have \((a,b)\in \tau \). The case \((aa^{-1},bb^{-1})\in \nu \) is identical to the previous one, when one consider the element \(ba^{-1}\in S\). The last two cases, namely if \((a^{-1}fa,b^{-1}fb)\in \nu \) or \((afa^{-1},bfb^{-1})\in \nu \) for some \(f\in E(S)\), are identical to the two previous case, when one consider the element \(a^{-1}fb\in S\) or \(bfa^{-1}\in S\), respectively. Thus, we have proved that \(\kappa _{(M,\nu )}\subseteq \tau \). \(\square \)

Lastly, we can show how I-cocongruences are related to congruences in an inverse semigroup.

Definition 15

([7,  p. 409]) Let \(\alpha \) and \(\beta \) be two relations defined on the set with apartness S. Then \(\alpha \) is associated to \(\beta \) if
$$\begin{aligned} (x, y)\in \alpha \wedge (y, z) \in \beta \text { implies } (x, z) \in \alpha . \end{aligned}$$

Theorem 6

([7, Theorem 2.3, pp. 409–410; Theorem 3.2, p. 412]) Let \(\kappa \) be a cocongruence on a semigroup with apartness S. The relation
$$\begin{aligned} {\sim } \kappa {\mathop {=}\limits ^{\text { def}}}\{(x, y)\in S\times S\mid (x, y)\rhd \kappa \} \end{aligned}$$
is a congruence on S and \(\kappa \) is associated to \({\sim }\kappa \).

This result naturally extends to inverse semigroups with apartness.

Corollary 1

Let \(\kappa \) be an I-cocongruence on an inverse semigroup with apartness S. The relation \({\sim } \kappa \) is a congruence on S and \(\kappa \) is associated with \({\sim } \kappa \).

Proof

We only need to prove that \({\sim }\kappa \) is compatible w.r.t. the inversion. This follows from [11, Theorem 5.1.4, formula (5.1.2)]. More explicitly, we can observe that if \((a,b)\in {\sim }\kappa \), then \((a,b)\rhd \kappa \). By property 3 of Proposition 4, this implies also \((a^{-1},b^{-1})\rhd \kappa \), thus \((a^{-1},b^{-1})\in {\sim }\kappa \). \(\square \)

5 The isomorphism theorem

In [7], the authors have introduced the concept of a strongly extensional homomorphism between semigroups with apartness and proved that the quotient set induced by a cocongruence of a semigroup with apartness inherits the same structure (see [7], Theorems 2.4 and 3.3). This naturally leads to the Apartness Isomorphism Theorem for semigroups [7, Theorem 3.5].

We show that this result can be easily extended to the case of inverse semigroups with apartness.

Definition 16

Let S be a semigroup with apartness and \(\kappa \) a cocongruence. The relation \({\sim }\kappa \) is a congruence such that \(\kappa \) is associated with \({\sim }\kappa \). The quotient set\(S/{\sim }\kappa \) is defined by
$$\begin{aligned} S/{\sim }\kappa {\mathop {=}\limits ^{\text { def}}}\{[a]_{{\sim }\kappa }\mid a\in S\}, \end{aligned}$$
where \([a]_{{\sim }\kappa }\) is the usual \({\sim }\kappa \) class of the element a.

Theorem 7

(Corollary of [7, Theorem 2.4, Theorem 3.3]) Let \((S,\cong ,\ncong ,\cdot ,^{-1})\) be an inverse semigroup with apartness, and let \(\kappa \) be an I-cocongruence. Define the structure \((S/{\sim }\kappa ,\cong ,\ncong ,\cdot ,^{-1})\) by
$$\begin{aligned} \begin{aligned}&[a]_{{\sim }\kappa }\cong [b]_{{\sim }\kappa } {\mathop {\Longleftrightarrow }\limits ^{\text { def}}}(a,b)\rhd \kappa ,\\&[a]_{{\sim }\kappa }\ncong [b]_{{\sim }\kappa } {\mathop {\Longleftrightarrow }\limits ^{\text { def}}}(a,b)\in \kappa ,\\&[a]_{{\sim }\kappa }\cdot [b]_{{\sim }\kappa } {\mathop {=}\limits ^{\text { def}}}[a\cdot b]_{{\sim }\kappa },\\&[a]_{{\sim }\kappa }^{-1} {\mathop {=}\limits ^{\text { def}}}[a^{-1}]_{{\sim }\kappa }. \end{aligned} \end{aligned}$$
Then \((S/{\sim }\kappa ,\cong ,\ncong ,\cdot ,^{-1})\) is well-defined and it is an inverse semigroup with apartness. Moreover, the natural projection \(\pi :S\rightarrow S/{\sim }\kappa \) defined by \(\pi (x){\mathop {=}\limits ^{\text { def}}}[x]_{{\sim }\kappa }\) is an onto se-homomorphism.

Proof

The theorem in [7] is stated for semigroups with apartness, so we only need to prove that properties 3(a), 3(b) and 4. of Definition 4 and property 5. of Definition 5 are satisfied, and this immediately follows by a direct calculation. \(\square \)

Definition 17

Let \((S,\cong _S,\ncong _S,\cdot )\) and \((T,\cong _T,\ncong _T,\cdot )\) be two semigroups with apartness and \(f :S \rightarrow T\) an se-homomorphism. The relations\(\ker (f)\) and \({{\,\mathrm{coker}\,}}(f)\) on S are defined as by
$$\begin{aligned} \begin{array}{l} \ker (f){\mathop {=}\limits ^{\text { def}}}\{(x,y)\in S\times S\mid f(x)\cong _T f(y)\},\\ {{\,\mathrm{coker}\,}}(f){\mathop {=}\limits ^{\text { def}}}\{(x,y)\in S\times S\mid f(x)\ncong _T f(y)\}. \end{array} \end{aligned}$$

Now we can finally state the Apartness Isomorphism Theorem for inverse semigroups with apartness.

Theorem 8

(Corollary of [7, Theorem 2.5, Theorem 3.4]) Let \(f :S \rightarrow T\) be an se-homomorphism between inverse semigroups with apartness. Then \({{\,\mathrm{coker}\,}}(f)\) is an I-cocongruence associated with the congruence \(\ker (f)\subseteq {\sim }{{\,\mathrm{coker}\,}}(f)\). Moreover, \((S/\ker (f),\cong ,\ncong ,\cdot )\) is an inverse semigroup with apartness and the map \(\Theta :S/\ker (f)\rightarrow T\) defined by \(\Theta ([x]_{\ker (f)}){\mathop {=}\limits ^{\text { def}}}f(x)\) is an se-embedding such that \(f \cong \Theta \circ \pi \), where \(\pi \) is the natural projection. Lastly, if f is onto, then \(\Theta \) is an apartness isomorphism.

Proof

Theorem 3.4 in [7] is stated for semigroups with apartness, so we only have to check the properties involving inversion. First, observe that we cannot apply Theorem 7 to prove that \(S/\ker (f)\) is an inverse semigroup with apartness, since in general \(\ker (f)\) differs from \({\sim }{{\,\mathrm{coker}\,}}(f)\). Nevertheless, it is routine to prove properties 3(a), 3(b) and 4. of Definition 4 and property 5. of Definition 5, and then that \(S/\ker (f)\) is actually an inverse semigroup with apartness. So, we only have to prove that the \({{\,\mathrm{coker}\,}}(f)\) is cocompatible w.r.t. the inversion and that \(\ker (f)\) is compatible w.r.t. the inversion. Indeed, \(f(a^{-1})\cong _T f(a^{-1}aa^{-1})\cong _T f(a^{-1})f(a)f(a^{-1})\), and then immediately follows \(f(a)^{-1}\cong _T f(a^{-1})\). Now we can prove that \({{\,\mathrm{coker}\,}}(f)\) is an I-cocongruence. Let \(a,b\in S\) be such that \((a^{-1},b^{-1})\in {{\,\mathrm{coker}\,}}(f)\). Then, by definition, we get \(f(a^{-1})\ncong _T f(b^{-1})\) and, by the above observation, \(f(a)^{-1}\ncong _T f(b)^{-1}\). As T is an inverse semigroup with apartness, from condition 3(b) of Definition 4, it follows \(f(a)\ncong _T f(b)\), and then \((a,b)\in {{\,\mathrm{coker}\,}}(f)\). Now, let \(a,b\in S\) be such that \((a^{-1},b^{-1})\in \ker (f)\). By definition, we have \(f(a^{-1})\cong _T f(b^{-1})\), and then, again by the above observation, \(f(a)^{-1}\cong _T f(b)^{-1}\). From the implication (1) of Remark 2, it follows \(f(a)\cong _T f(b)\), and then \((a,b)\in \ker (f)\), as required. \(\square \)

6 Conclusion

Inverse semigroups can be seen as algebraic structures between semigroups and groups and have been proposed as a natural tool in several applications. Since a constructive approach for both groups and semigroups has been considered and constructive mathematics has relevance in applications, it is timely to consider a constructive approach to inverse semigroups as well.

Stating a constructive counterpart of Wagner–Preston Theorem has proved to be more difficult, as we are able to only do so under conditions of relative decidability of equality and apartness on the set of idempotents. However, as noticed in [8], Green’s relations are fundamental tools in the classical structure theory of semigroups but their definitions involve existential quantification which is in general problematic in constructive mathematics. In the classical inverse semigroup theory, Green’s relations can be defined avoiding the existential quantification but still including the equality of idempotents. So, the condition on idempotents could be useful to introduce a good theory of Green’s relations in this framework.

Notes

Acknowledgements

The authors acknowledge the research cooperation project among Department of Mathematics of Politecnico di Milano, Faculty of Science of the University of Novi Sad, and the Department of Mathematics and Computer Science of the University of Maribor. In this framework, Professor Crvenković gave a talk on semigroups with apartness which drew our attention to constructive algebra. The authors thank the referee for constructive comments and recommendations which helped to improve the readability and quality of the paper.

References

  1. 1.
    Bishop, E.A.: Foundations of Constructive Analysis. McGraw-Hill, New York (1967)zbMATHGoogle Scholar
  2. 2.
    Bishop, E.A., Bridges, D.S.: Constructive Analysis, Grundlehren der mathematischen Wissenschaften, vol. 279. Springer, Berlin (1985)Google Scholar
  3. 3.
    Bridges, D.S., Reeves, S.: Constructive mathematics in theory and programming practice. Philosophia Mathematica 7(3), 65–104 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Bridges, D.S., Richman, F.: Varieties of Constructive Mathematics. London Mathematical Society Lecture Notes, vol. 97. Cambridge University Press, Cambridge (1987)CrossRefzbMATHGoogle Scholar
  5. 5.
    Bridges, D.S., Vîţă, L.S.: Techniques in Constructive Analysis. Universitext. Springer, Berlin (2006)zbMATHGoogle Scholar
  6. 6.
    Bridges, D.S., Vîţă, L.S.: Apartness and Uniformity: A Constructive Development. CiE series on theory and applications of computability. Springer, Berlin (2011)CrossRefzbMATHGoogle Scholar
  7. 7.
    Crvenković, S., Mitrović, M., Romano, D.: Semigroups with apartness. Math. Log. Q. 59(6), 407–414 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Crvenković, S., Mitrović, M., Romano, D.: Basic notions of (constructive) semigroups with apartness. Semigroup Forum 92(3), 659–674 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Green, D.G.: The lattice of congruences on an inverse semigroup. Pac. J. Math. 57(1), 141–152 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Howie, J.M.: Why study semigroups? Math. Chron. 16, 1–14 (1987)MathSciNetzbMATHGoogle Scholar
  11. 11.
    Howie, J.M.: Fundamentals of Semigroup Theory. Clarendon Press, Oxford (1995)zbMATHGoogle Scholar
  12. 12.
    Kripke, S.: Semantical analysis of modal logic I, Normal modal propositional calculi. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 9(5–6), 67–96 (1963)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Lawson, M.V.: Inverse Semigroups: The Theory of Partial Symmetries. World Scientific, Singapore (1999)zbMATHGoogle Scholar
  14. 14.
    Mines, R., Richman, F., Ruitenburg, W.: A Course of Constructive Algebra. Universitext. Springer, New York (1988)CrossRefzbMATHGoogle Scholar
  15. 15.
    Martin-Löf, Per: Constructive mathematics and computer programming. Philos. Trans. R. Soc. Lond. A 312, 501–518 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Petrich, M.: Inverse Semigroups. Wiley, New York (1984)zbMATHGoogle Scholar
  17. 17.
    Petrich, M., Reilly, N.R.: A network of congruences on an inverse semigroup. Trans. Am. Math. Soc. 270, 309–325 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Preston, G.B.: Inverse semi-groups. J. Lond. Math. Soc. 29(4), 396–403 (1954)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Scheiblich, H.E.: Kernels of inverse semigroup homomorphisms. J. Aust. Math. Soc. 18(3), 289–292 (1974)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Troelstra, A., van Dalen, D.: Constructivism in Mathematics. An Introduction. Volume II, Studies in Logic and the Foundations of Mathematics, vol. 123. North-Holland, Amsterdam (1988)zbMATHGoogle Scholar
  21. 21.
    Wagner, V.V.: The theory of generalized heaps and generalized groups. Matematicheskii Sbornik. Novaya Seriya 32(3), 545–632 (1953). (in Russian)MathSciNetGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2019

Authors and Affiliations

  1. 1.Dipartimento di MatematicaPolitecnico di MilanoMilanItaly

Personalised recommendations