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 with elements and and functions , , and , such that
is a monoidal setoid
distributes over up to the equivalence relation: for all elements , , and ,
is commutative or symmetric or braided if additionally for all elements and , .
The set of functions from the boolean domain to the natural numbers , equipped with the equivalence relation , is a ring setoid.
Given any Archimedean ordered field , the set of Cauchy sequences in is a ring setoid.
Given any Archimedean ordered field , the set of all locators of all elements of 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 and is a function such that
preserves the equivalence relation: for all and , implies
preserves the groupal unit up to equivalence relation:
preserves the groupal product up to equivalence relation: for all and ,
preserves the groupal inverse up to equivalence relation: for all ,
preserves the monoidal unit up to equivalence relation:
preserves the monoidal product up to equivalence relation: for all and ,
Let be a ring setoid, and let be its quotient set. Then the function which takes an element of 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.