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 local ring.
“local ring setoid” and “Bishop local ring” are placeholder names for a concept which may or may not have another name in the mathematics literature.
Let $R$ be a ring setoid. An element $a \in R$ is invertible if there exists an element $b \in R$ such that $a \cdot b \sim 1$.
A local ring setoid or Bishop local ring is a ring setoid (usually also assumed commutative) such that:
$0 \sim 1$ is false
whenever $a + b \sim 1$, $a$ or $b$ is invertible.
Here are a few equivalent ways to phrase the combined condition:
Whenever a (finite) sum is equivalent to $1$, at least one of the summands is invertible.
Whenever a sum is invertible, at least one of the summands is invertible.
Whenever a sum of products is invertible, for at least one of the summands, all of its multiplicands are invertible. (This is not entirely trivial in the noncommutative case, but it's still correct.)
The invertible elements form an anti-ideal:
In the context of excluded middle, every weak local ring setoid? is a local ring setoid. Thus, the following is equivalent to the above definitions in classical mathematics:
Given any Archimedean ordered field $F$, the set of Cauchy sequences in $F$ is a local ring setoid.
Given any Archimedean ordered field $F$, the set of all locators of all elements of $F$ is a local ring setoid.
Last revised on August 19, 2024 at 14:52:46. See the history of this page for a list of all contributions to it.