nLab groupal setoid

Idea

A setoid or Bishop set whose quotient set is a group. Equivalently, a locally thin 2-group, or in foundations where 2-categories are locally univalent by default, a locally thin pre-2-group. Also, equivalently, a monoidal setoid in which the monoidal product with any element has an inverse up to equivalence relation.

“Groupal setoid”, “groupal Bishop set”, and “Bishop group” are placeholder names for a concept which may or may not have another name in the mathematics literature.

Definition

Here we assume that setoids or Bishop sets are equipped with an equivalence relation (rather than a pseudo-equivalence relation). A groupal setoid, groupal Bishop set, or Bishop group is a monoidal setoid $(A, \sim, e, m)$ with a function $i:A \to A$ such that

• $i$ preserves the equivalence relation: for all elements $a \in A$ and $b \in A$, if $a \sim b$, then $i(a) \sim i(b)$.

• $i$ satisfies the left and right inverse laws up to the equivalence relation: for all elements $a \in A$, $m(a, i(a)) \sim e$ and $m(i(a), a) \sim e$.

$A$ is abelian groupal or symmetric groupal or braided groupal if additionally for all elements $a \in A$ and $b \in A$, $m(a, b) \sim m(b, a)$.

Examples

• The set $\mathbb{N}^\mathbb{2}$ of functions from the boolean domain $\mathbb{2}$ to the natural numbers $\mathbb{N}$, equipped with the equivalence relation $f \sim g \coloneqq f(0) + g(1) = f(1) + g(0)$, is an abelian groupal setoid.

• Given any Archimedean ordered field $F$, the set of Cauchy sequences in $F$ is an abelian groupal setoid.

• Given any Archimedean ordered field $F$, the set of all locators of all elements of $F$ is an abelian groupal setoid.

• Given two abelian groups $G$ and $H$, the free abelian group $F(G \times H)$ of the product of the carrier sets of $G$ and $H$, equipped with the equivalence relation $\sim$ generated by

  $$(g_1, h) + (g_2, h) \sim (g_1 + g_2, h)$$

  for all $g_1, g_2 \in G$ and $h \in H$ and

  $$(g, h_1) + (g, h_2) \sim (g, h_1 + h_2)$$

  for all $g \in G$ and $h_1, h_2 \in H$, is an abelian groupal setoid whose quotient set is the tensor product of abelian groups $G \otimes H$.

Related concepts

• setoid

• group, abelian group

• monoidal setoid

• ring setoid

• 2-group

• locally thin 2-category