Help with proving $f^\ast R^\times = \operatorname{Spec}A_f$ where $f\in A$ and $R= \operatorname{Spec} k[x]$

Question

Suppose $\mathcal E$ is the large Zariski site of $k$-algebras for $k$ a (commutative unitary) ring. Let $R=\operatorname{Spec}k[x]$ be the line object of $\mathcal E$. Let $A$ be a $k$-algebra and $f\in A$. Naturally identifying $f\in A$ with $f:\operatorname{Spec}A\to R$, I want to prove $$f^\ast R^\times =\operatorname{Spec}A_f.$$

I think this should be an easy exercise in the internal language, but I feel I don't really know what I'm doing. My idea was to show that both sides have the same "elements".

1. By definition, $f^\ast R^\times =[[a\in \operatorname{Spec} A\mid fa\in R^\times ]].$ I think $a\in \operatorname{Spec} A\mid fa\in R^\times$ translates to an arrow $a: \operatorname{Spec} B\to \operatorname{Spec} A$ such that the composite $$ \operatorname{Spec} B\to \operatorname{Spec} A \to R$$ factors through $R^\times $. Such a composite is an element $af\in B$ which is invertible in $B$.

2. An "element" of $\operatorname{Spec} A_f$ is an arrow $\operatorname{Spec} B\to \operatorname{Spec} A_f$ which is in turn equivalent to an arrow $A_f\to B$. Identifying $A_f\cong A[f^-1]=A[x]/ \left\langle xf-1 \right\rangle $, it looks like an arrow $A_f\to B$ amounts to an element $a\in B$ satisfying $af-1=0$, i,e $af=1$.

It looks like an okay proof, but I don't know if what I wrote makes sense. Also, I don't know how to formally translate $x\in R^\times $ into anything.

Is my proof correct? Is there a better one? How to interpret $x\in R^\times $?

Answer 1

The only things really involving the internal language are:

• The fact $R^\times =[[r\in R\mid \exists s\in R:rs=1]]$ is (the sheafification of the) representable by $\operatorname{Spec} k[x,x^{-1}]$;
• The fact representable generalized elements determine the sheaf semantics.

Combining these two facts reduces us to calculating the pushout, in the category of $k$-algebras, of $k[x,x^{-1}]\leftarrow k[x]\overset{f}{\rightarrow}A$. This pushout is precisely $A_f$, where we are identifying the $k$-algebra arrow $f:k[x]\to A$ and its image of $x\in k[x]$ in $A$. To see this note the universal property of this pushout is the usual universal property of localization - we seek to universally invert $f\in A$. Indeed, a $k$-algebra arrow $k[x,x^{-1}]\to B$ amounts to choosing an invertible element in $B$.