What does the Zariski topos of $\mathbb{P}^1$ classify? (The word "geometric theory" below is used in the sense of logic / classifying topos.)
We know that the (big) Zariski topos over $\text{Spec}\mathbb{Z}$ classifies the theory of local rings. My question is, what geometric theory does the (big) Zariski topos over $\mathbb{P}^1$ classify?
From algebraic geometry point of view it should classify something like a local rings together with a map to $\mathbb{P}^1$, i.e. something like isomorphism classes of $(A, L, e_0, e_1)$ where $A$ is a local ring, $L$ is an locally free $A$-module of rank 1, and $e_0, e_1\in L$ spans $L$. Is there a good way to describe a geometric / coherent theory of it?
I saw some discussions here but it's mostly about the affine case. I'm curious on what role properness may play here. If possible I'd like to see some description on the geometric theory for a general scheme (or algebraic curve).
(On "locally free $A$-module of rank 1": in this case L must be free, but that uses another result, merely asking for being locally free of rank 1 seems more natural to me.)
 A: 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.
