Let $\mathcal E$ be a Grothendieck topos and $R$ be a ring object in it. Say $R$ is internally a ring of fractions if $\neg (a=0)\implies a$ is invertible.
I'm trying to prove that in the opposite category of commutative $k$-algebras for $k$ a (commutative unitary) ring, taken with the Zariski topology, the canonical line object $R=\operatorname{Spec}k[x]$ is a ring of fractions. I would like to do this using the internal language, but I'm kind of stuck at the very beginning.
Since $$\mathsf{Hom}(\operatorname{Spec}S,R)\cong \mathsf{Hom}(k[x],S)\cong \mathsf{Hom}(1,US)\cong S$$ it kind of looks like I'm supposed to prove that $S$ is literally a field, which makes no sense. I don't see where I can use the locality of the internal language to restrict to the cover $S_a,S_{1-a}$.
So how can I complete this proof?
Added. This paper by Kock contains as proposition 2.2 a proof of a stronger claim. The author seems to say $\neg(a=0)$ means that given our $a:\operatorname{Spec}S\to R$, if $a\circ b:\operatorname{Spec}T\to R$ is trivial, i.e $b\circ a:k[X]\to T$ is zero, then $T$ is zero. But then, given $a$, just take $b$ to be the natural projection $S\to S/(aX)$. Conclude $S/(aX)$ must be zero, which means $aX$ must be invertible in $S$.
Two things confuse me now:
- Why does this finish the proof? Don't we need to show $a:k[x]\to S$ is an isomorphism?
- I originally wanted to just use the table on pages 7,8 of these notes by Ingo Blechschmidt, and there $U\models\neg \varphi \implies \psi$ is said to mean that for every open $V\subset U$, if $V\models \phi \implies \psi$ then $V=\emptyset$. However, the rings $S,S/(x)$ don't seem to have anything to do with opens of $R$. Can someone explain how to write the proof actually using the internal language, as presented in the table?
The answers to questions 1 and 2 are very much related.
The table in the notes you cited gives the Kripke–Joyal semantics of the small Zariski topos. This is the category of set-valued sheaves on $\operatorname{Spec}(k)$. In its internal language the statement "$\neg(a = 0) \Rightarrow \text{$a$ is invertible}$" does not hold in general.
You are working with the big Zariski topos, described in Section 13 of the notes. This is the category of sheaves on the Grothendieck site $\mathrm{Alg}(k)^\mathrm{op}$ (or rather its full subcategory consisting only of the finitely presented $k$-algebras). The Kripke–Joyal semantics of this topos is very similar to the semantics of the small topos, but with the crucial difference that the clauses for implication and universal quantification refer to arbitrary algebras over the base ring (instead of only localizations of it). A table giving all the rules of the Kripke–Joyal semantics of the big Zariski topos is recorded at the nLab.
To answer your first question, just translate the internal formula "$\forall a{:} \mathbb{A}^1. \neg(a = 0) \Rightarrow \text{$a$ is invertible}$" using the Kripke–Joyal semantics (noting that the value of the structure sheaf $\mathbb{A}^1$ at stage $S$ is precisely $S$, as you explained) to see for yourself that Kock's proof gives what you want.
You also wonder whether a purely internal proof is possible, i.e. a proof which doesn't use the Kripke–Joyal semantics to first translate the internal formula to an external one and then verify the external one. You have to specify which axioms you want to allow yourself for this. If you just allow the axioms for a ring or even a local ring, then you won't succeed, since the statement is false for arbitrary local rings. You need to allow some ingredient particular to the Zariski topos. In fact, I see the statement itself as such a particularity and would include it as an axiom to prove other internal statements.