Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorEgbertRijke
   • CommentTimeJan 8th 2021
   • PermaLink
   Author: EgbertRijke
   Format: MarkdownItexThe [entry for constructive fields](https://ncatlab.org/nlab/show/field#constructive) contains a discussion about different options to define a field constructively, but the most obvious definitions is not among the options. One could simply say that a constructive field is a commutative ring $R$ such that $(x\neq 0)\Leftrightarrow\mathsf{isinvertible}(x)$. for all $x\in R$. Strangely, in several of the definitions on the nlab page it is proposed to replace this condition, but it is never said why this is necessary. On the other hand, the definition of a residue field is included. Here the condition is $(x=0)\Leftrightarrow\neg\mathsf{isinvertible}(x)$ for all $x\in R$. This condition implies that the predicate $x=0$ is double-negation stable, which seems to reduce the applicability of the definition more than the more natural condition which seems to be dismissed. So I was wondering why the condition $(x\neq 0)\Leftrightarrow\mathsf{isinvertible}(x)$ is not considered as an option for a definition of constructive field. Perhaps there is something obviously wrong with it, that I'm missing.

   The entry for constructive fields contains a discussion about different options to define a field constructively, but the most obvious definitions is not among the options. One could simply say that a constructive field is a commutative ring $R$ such that

   $(x\neq 0)\Leftrightarrow\mathsf{isinvertible}(x)$.

   for all $x\in R$. Strangely, in several of the definitions on the nlab page it is proposed to replace this condition, but it is never said why this is necessary.

   On the other hand, the definition of a residue field is included. Here the condition is

   $(x=0)\Leftrightarrow\neg\mathsf{isinvertible}(x)$

   for all $x\in R$. This condition implies that the predicate $x=0$ is double-negation stable, which seems to reduce the applicability of the definition more than the more natural condition which seems to be dismissed.

   So I was wondering why the condition $(x\neq 0)\Leftrightarrow\mathsf{isinvertible}(x)$ is not considered as an option for a definition of constructive field. Perhaps there is something obviously wrong with it, that I’m missing.

2. • CommentRowNumber2.
   • CommentAuthorUlrik
   • CommentTimeJan 8th 2021
   • PermaLink
   Author: Ulrik
   Format: MarkdownItexWell, a main example we want is the real numbers, which form a Heyting field, whose apartness is not the denial inequality. The condition you write is like MRR87's denial field, but without the requirement that the denial inequality be tight (so = not nec. stable), and without the requirement that (0) be a prime ideal. What's a good example of such a field with non-stable equality?

   Well, a main example we want is the real numbers, which form a Heyting field, whose apartness is not the denial inequality. The condition you write is like MRR87’s denial field, but without the requirement that the denial inequality be tight (so = not nec. stable), and without the requirement that (0) be a prime ideal. What’s a good example of such a field with non-stable equality?

3. • CommentRowNumber3.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeApr 12th 2022
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexOne such example is the affine line, the canonical ring object in the big Zariski topos of a scheme. (Granted, technically, it's not a ring but a sheaf of rings.)

   One such example is the affine line, the canonical ring object in the big Zariski topos of a scheme. (Granted, technically, it’s not a ring but a sheaf of rings.)