Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A setoid or Bishop set whose quotient set is a ring. Equivalently, a thin ring groupoid, or in foundations where groupoids are univalent by default, a thin ring pregroupoid.
“Ring setoid” and “Bishop ring” are placeholder names for a concept which may or may not have another name in the mathematics literature.
A ring setoid or Bishop ring is a setoid $(A, \sim)$ with elements $0 \in A$ and $1 \in A$ and functions $\alpha:A \times A \to A$, $\nu:A \to A$, and $\mu:A \times A \to A$, such that
$(A, \sim, 0, \alpha, \nu)$ is a braided groupal setoid
$(A, \sim, 1, \mu)$ is a monoidal setoid
$\mu$ distributes over $\alpha$ up to the equivalence relation: for all elements $a \in A$, $b \in A$, and $c \in A$,
$A$ is commutative or symmetric or braided if additionally for all elements $a \in A$ and $b \in A$, $\mu(a, b) \sim \mu(b, a)$.
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 a ring setoid.
Given any Archimedean ordered field $F$, the set of Cauchy sequences in $F$ is a ring setoid.
Given any Archimedean ordered field $F$, the set of all locators of all elements of $F$ is a ring setoid.
The quotient set of any ring setoid by its equivalence relation is a ring setoid where the equivalence relation is given by equality
More generally, any ring is a ring setoid in which the equivalence relation is given by equality.
A ring setoid homomorphism or Bishop ring homomorphism between two ring setoids $A$ and $B$ is a function $h:A \to B$ such that
$f$ preserves the equivalence relation: for all $a \in A$ and $b \in A$, $a \sim_A b$ implies $f(a) \sim_B f(b)$
$f$ preserves the groupal unit up to equivalence relation: $f(0_A) \sim_B 0_B$
$f$ preserves the groupal product up to equivalence relation: for all $a \in A$ and $b \in A$,
$f$ preserves the groupal inverse up to equivalence relation: for all $a \in A$,
$f$ preserves the monoidal unit up to equivalence relation: $f(1_A) \sim_B 1_B$
$f$ preserves the monoidal product up to equivalence relation: for all $a \in A$ and $b \in A$,
Let $A$ be a ring setoid, and let $A / \sim$ be its quotient set. Then the function $[-]:A \to (A / \sim)$ which takes an element of $A$ to its equivalence class is a ring setoid homomorphism.
Last revised on August 19, 2024 at 14:59:11. See the history of this page for a list of all contributions to it.