# Proving $\operatorname{Spec} k[x]$ is internally a ring of fractions in the internal language of the Zariski topos

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:

1. Why does this finish the proof? Don't we need to show $a:k[x]\to S$ is an isomorphism?
2. 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?
• Maybe I misunderstood everything, but how is $\operatorname{Spec} k[x]$ a ring object? Are you considering some Hopf algebra structure on $k[x]$? – Najib Idrissi Sep 26 '16 at 14:33
• @NajibIdrissi I think the coring structure $k[x]\to k[x]\otimes k[x]$ gives a ring structure, no? – Arrow Sep 26 '16 at 14:37
• Well it gives it a monoid object structure, true (note that you need a bialgebra, not just a coring, and it's not obvious that there's only one such structure), in fact an abelian group object structure since it's a cocommutative Hopf algebra (assuming you're considering the standard one given by $\Delta(x) = x \otimes 1 + 1 \otimes x$). But I don't see how it becomes a ring object... Maybe I'm missing something. – Najib Idrissi Sep 26 '16 at 15:23
• @Najib The comultiplication is given by $x \mapsto x \otimes x$ and the coaddition is given by $x \mapsto x \otimes 1 + 1 \otimes x$. However, I believe that it's simpler to not directly think about $\operatorname{Spec}(k[x])$, but about the represented functor $\mathrm{Hom}(\cdot, \operatorname{Spec}(k[x]))$. Arrow has provided an explicit description of that functor; you see that it factors over the category of rings. – Ingo Blechschmidt Sep 26 '16 at 21:04

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.