Thread by @gro_tsen

I gave this a bit more thought: here are some interesting examples to have in mind (here, ring objects in some topos of sheaves): ⤵️

https://twitter.com/gro_tsen/status/1347548409532731394

‣ The ring of Dedekind reals, which is represented by the sheaf of continuous ℝ-valued functions, in the topos of sheaves on many reasonable topological spaces (such as ℝ itself), satisfies ③ ∀x.(x=0⇔¬∃y.(x·y=1)) but fails ② ∀x.(¬(x=0)⇔∃y.(x·y=1)) (so fails ① too).

Indeed, x is invertible iff the continuous ℝ-valued function is everywhere ≠0, but it satisfies ¬(x=0) iff the function does not vanish on any nontrivial open set (so ② fails for a function vanishing somewhere but not on any nontrivial open set); …

… on the other hand, x satisfies ¬∃y.(x·y=1) iff x is not ≠0 on any nontrivial open set, and this is clearly the same as being identically 0 (so ③ holds).

‣ The forgetful functor from rings to sets, seen as a sheaf of rings on the opposite category to rings (=affine schemes) with the Zariski topology, satisfies ② ∀x.(¬(x=0)⇔∃y.(x·y=1)) but fails ③ ∀x.(x=0⇔¬∃y.(x·y=1)).

Indeed, x, seen as en element of some ring R, satisfies ¬(x=0) when the only ring homomorphism R→R′ taking x to 0 is for R′ being the zero ring, which means exactly that x is invertible (so ② holds); …

… but x satisfies ¬∃y.(x·y=1) when the only ring homomorphism R→R′ taking x to an invertible is for R′ being the zero ring, which exactly means that x is nilpotent (so ③ fails for any nonzero nilpotent x).

‣ Now if we modify this last example to take the “reduced ring” functor instead (taking a ring R to the quotient R/Nil(R) by the nilradical), this is still a sheaf for the Zariski topology, and now it satisfies ② and ③, …

… but it fails ①, because for, say, x=2∈ℤ, we cannot find a covering by a ring ℤ→R′ in which 2 vanishes and one in which 2 is invertible.

Together, these examples show that each of ② and ③ fails to imply the other and that the two, even when taken together, still fail to imply ①. I don't have any examples of rings satisfying ④ but failing ② and ③, but ④ isn't super interesting, really.

I'm more or less convinced, now, that the “best” definition of a “field” is to demand x#x′ :⇔ ∃y.((x−x′)·y=1) to be a tight apartness, or equivalently, both ③ and being a local ring.

https://twitter.com/gro_tsen/status/1347617503837614081