First note that a morphism $\operatorname{Spec}(A) \to \mathbb{P}^1$ is just given by an element of the "classical projective space" $\mathbb{P}^1(A) = \{ [a:b] \,|\, \text{$a$ is invertible or $b$ is invertible} \}$, if $A$ is a local ring. The description you gave is valid as well, but since (as you remark) "locally free" is equivalent to "free" over a local ring, it can be simplified further.

The big Zariski topos of $\mathbb{P}^1$ classifies the theory of a "local ring together with a point $[a:b]$". This theory can be explicitly described as follows:

- A sort $R$ together with function symbols, constants, and axioms expressing that $R$ is a local ring.
- A sort $P$ (to be thought of as the set of $[a:b]$ with $a,b:R$ where at least one coordinate is invertible) together with a relation $\langle\cdot,\cdot,\cdot\rangle$ on $R \times R \times P$ and the following axioms:
- $\text{$a$ is invertible} \vee \text{$b$ is invertible} \dashv\vdash_{a,b:R} \exists p:P.\ \langle a,b,p \rangle$
- $\langle a,b,p \rangle \wedge \langle a,b,p' \rangle \vdash_{a,b:R,\, p,p':P} p = p'$
- $\top \vdash_{p:P} \exists a,b:R.\ \langle a,b,p \rangle$
- $\langle a,b,p \rangle \wedge \langle a',b',p \rangle \dashv\vdash_{a,a',b,b':R,\, p:P} \exists s:R.\ \text{$s$ is invertible} \wedge a' = s a \wedge b' = s b$

- A constant of sort $P$.

In a topos $\mathcal{E}$, a model of this theory is given by a local ring $A$ in $\mathcal{E}$ together with a point of the "classical projective space of $A$" as defined above. (Equivalently, by a rank-1 quotient of $A^2$ up to isomorphism of quotients.)

A different theory which the big Zariski topos of $\mathbb{P}^1$ classifies is the theory of a "homogeneous filter $F$ of $\mathbb{Z}[X,Y]$ meeting the irrelevant ideal together with a local ring over the degree-zero part $A := \mathbb{Z}[X,Y][F^{-1}]_0$ which is local over $A$".

For an arbitrary $\mathbb{N}$-graded ring $S$, the big Zariski topos of $\operatorname{Proj}(S)$ classifies the theory of a "homogeneous filter $F$ of $S$ meeting the irrelevant ideal together with a local ring over the degree-zero part $A := S[F^{-1}]_0$ which is local over $A$". (This in turn can be rewritten using the universal property of the degree-zero part of graded localization.) This description follows by combining the description of the little Zariski topos of $\operatorname{Proj}(S)$ (which classifies the theory of a "homogeneous filter $F$ of $S$ meeting the irrelevant ideal") and the description of the big Zariski topos as a topos over the little Zariski topos (which classifies the theory of a "local ring over $\mathcal{O}_S$ which is local over $\mathcal{O}_S$").

Proofs can be found in these note of mine (Section 12.8 and Section 16.1 at the time of writing).

If you care about issues of size, note that all the statements made here are only valid if we define the big Zariski topos of a scheme $X$ using the site consisting of only the locally finitely presented $X$-schemes. (It doesn't matter whether we restrict to affine schemes or not.) If we employ the site consisting of all $X$-schemes, the construction will not be well-defined in ordinary set theory, and if we restrict to those $X$-schemes contained in some universe (either Grothendieck or partial as in the Stacks project), then the resulting topos will have much more points.

3more comments