Classifying Space of "Valuation Ringed Spaces over a Topos"

Question

The classifying topos for local rings is the big Zariski topos of $\text{Spec}(\mathbb{Z})$. Call this topos $T$. Geometric maps of topoi from a topos $T'$ to $T$ are in correspondence with sheaves of rings on $T'$ which are locally local rings. This is related to how $\text{Spec} : \text{Ring} \rightarrow \text{Loc}$ from rings to locally ringed spaces is adjoint, while if we replace $\text{Loc}$ with ringed spaces, it is not an adjunction.

I wonder if there is a similar situation for $\text{Spa}$ and some classifying topos involving valuation rings. That is, I want some topos $T_{val}$ such that maps of a topos $T'$ into $T_{val}$ are in correspondence with sheaves of rings on $T'$ which are locally certain valuation rings.

Answer 1

Since the axioms describing what a valuation ring can be put as what's called geometric sequents [*], by the fundamental theorem on classifying toposes, there is a topos $T_{val}$ with precisely the universal property you're asking for. (See for instance Section 2.1.2 and more specifically Theorem 2.1.8 in Olivia Caramello's book Theories, Sites, Toposes.)

But then there is the additional question whether we can recognize this topos as one of the toposes commonly used in algebraic geometry, just as we can recognize the classifying topos of local rings as the big Zariski topos of $\operatorname{Spec}(\mathbb{Z})$.

As far as I know, this question is open. The answer linked to by Robert in the comments gives some indication that $T_{val}$ might coincide with the big rh topos of $\operatorname{Spec}(\mathbb{Z})$, but just that $T_{val}$ and the big rh topos have the same topos-theoretic points, as set out in the linked answer, doesn't yet mean that the toposes are equivalent.

You could also ask the analogous question for algebraically closed valuation rings. In this case again a classifying topos exists, by the same abstract nonsense, and conditional on some representability conjecture it coincides with the big ph topos of $\operatorname{Spec}(\mathbb{Z})$ (see Proposition 21.18 in these notes of mine).

---

[*] A geometric sequent is a logical formula of the form $\forall \cdots \forall. (\cdots) \Rightarrow (\cdots)$ where in the two bracketed subformulas the connectives $\Rightarrow$ $\neg$ $\forall$ may not occur. For instance the field axiom "$\forall x : R. x = 0 \vee (\exists y : R. xy = 1)$" can be put as a geometric sequent (just imagine an invisible "$\top \Rightarrow$"), but the (classically but not intuitionistically) equivalent axiom "$\forall x : R. \neg(\exists y : R. xy = 1) \Rightarrow x = 0$" cannot.