Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorEgbertRijke
    • CommentTimeJan 8th 2021

    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 RR such that

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

    for all xRx\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)¬isinvertible(x)(x=0)\Leftrightarrow\neg\mathsf{isinvertible}(x)

    for all xRx\in R. This condition implies that the predicate x=0x=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 (x0)isinvertible(x)(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.

    • CommentRowNumber2.
    • CommentAuthorUlrik
    • CommentTimeJan 8th 2021

    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?

  1. 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.)