nLab groupal setoid

Redirected from "abelian groupal setoid".

Context

Algebra

Category theory

Relations

Constructivism, Realizability, Computability

Contents

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,,e,m)(A, \sim, e, m) with a function i:AAi:A \to A such that

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

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

AA is abelian groupal or symmetric groupal or braided groupal if additionally for all elements aAa \in A and bAb \in A, m(a,b)m(b,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 fgf(0)+g(1)=f(1)+g(0)f \sim g \coloneqq f(0) + g(1) = f(1) + g(0), is an abelian groupal setoid.

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

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

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

    (g 1,h)+(g 2,h)(g 1+g 2,h)(g_1, h) + (g_2, h) \sim (g_1 + g_2, h)

    for all g 1,g 2Gg_1, g_2 \in G and hHh \in H and

    (g,h 1)+(g,h 2)(g,h 1+h 2)(g, h_1) + (g, h_2) \sim (g, h_1 + h_2)

    for all gGg \in G and h 1,h 2Hh_1, h_2 \in H, is an abelian groupal setoid whose quotient set is the tensor product of abelian groups GHG \otimes H.

Last revised on July 10, 2024 at 18:38:28. See the history of this page for a list of all contributions to it.