nLab field setoid

Idea

A setoid or Bishop set whose quotient set is a field.

“Field setoid” and “Bishop field” are placeholder names for a concept which may or may not have another name in the mathematics literature.

Definition

Let $R$ be a commutative 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 field setoid or Bishop field is a commutative ring setoid $F$ in which for every element $a \in F$, $a$ is invertible if and only if $a \sim 0$ is false.

Constructive notions

Similarly to the case for fields, there are different notions for field setoids in constructive mathematics. These include

• discrete field setoids

• Heyting field setoids

• weak Heyting field setoids

• Kock field setoids

Definition

A discrete field setoid is a commutative ring setoid $F$ in which for every element $a \in F$, either $a \sim 0$ or $a$ is invertible.

Definition

A weak Heyting field setoid is a commutative ring setoid $F$ in which for every element $a \in F$, $a$ is not invertible if and only if $a \sim 0$.

Definition

A Heyting field setoid is a weak Heyting field setoid which is also a local ring setoid.

Examples

• Given any Archimedean ordered field $F$, the set of Cauchy sequences in $F$ is a field setoid. In constructive mathematics, the set of Cauchy sequences in $F$ is only a Heyting field setoid.

• Given any Archimedean ordered field $F$, the set of all locators of all elements of $F$ is a field setoid. In constructive mathematics, the set of all locators of all elements of $F$ is only a Heyting field setoid.

Related concepts

• setoid, Bishop set

• field

• ring setoid

• local ring setoid

• ordered field setoid