######  Lemma 5.17.

For $X:\mathsf{LRDL}_{\ell+1}^{op}$ an essentially small qcqs-scheme there
exists a small scheme $Y:\mathsf{QcQsSch}_{\ell}$ with
$X\cong\mathsf{lift}(Y)$.

###### Proof.

This follows from Proposition 3.20 and the fact that the functor
$\mathsf{lift}$ preserves colimits. ∎

######  Remark 5.18.

Note that we did not require _mere_ existence of an essentially small scheme
in Lemma 5.17. This is because the $\Sigma$-type of
$Y:\mathsf{QcQsSch}_{\ell}$ with an isomorphism $X\cong\mathsf{lift}(Y)$ is a
proposition, since locally ringed lattices form a univalent category by
Proposition 3.7 and $\mathsf{lift}$ is fully faithful. In other words, Lemma
5.17 allows us to _choose_ an isomorphic small scheme for each essentially
small scheme. This choice can even be made functorial by invoking the chosen
isomorphisms, giving us a _functor_ from essentially small to small
schemes.303030This is basically the trick used in the proof of [Uni13, Lemma
9.4.5]. This functor appears implicitly in the proof of Theorem 5.22.

######  Proposition 5.19.

The functor
$\lvert\\_\rvert:\mathsf{FunnQcQsSch}_{\ell}\to\mathsf{QcQsSch}_{\ell+1}$ is
fully faithful.

###### Proof.

Let $X,Y$ be functorial qcqs-schemes. Any
$\pi:\mathsf{LRDL}_{\ell+1}^{op}\big{(}\lvert X\rvert,\lvert Y\rvert\big{)}$
is locally a morphism of small affine schemes in the following sense: There
merely exist compatible affine compact open covers
$U_{1},...,U_{n}:{X}\Rightarrow{\mathcal{L}}$ with
$\llbracket\,{U_{i}}\,\rrbracket\cong\mathsf{Sp}(A_{i})$ and
$V_{1},...,V_{m}:{Y}\Rightarrow{\mathcal{L}}$ with
$\llbracket\,{V_{j}}\,\rrbracket\cong\mathsf{Sp}(B_{j})$, where the $A_{i}$
and $B_{j}$ are small rings. Compatibility means that for each $U_{i}$ exists
a $V_{j}$ such that $U_{i}\leq\pi^{*}(V_{j})$ and the “restriction”
$\pi\\!\\!\restriction_{U_{i}}:\mathsf{LRDL}_{\ell+1}^{op}\big{(}\lvert
X\rvert\\!\\!\restriction_{U_{i}},\lvert
Y\rvert\\!\\!\restriction_{V_{j}}\\!\\!\big{)}$ is induced by a ring morphism
$\varphi_{ij}:\mathsf{Hom}(B_{j},A_{i})$. This means that
$\mathsf{lift}(\varphi_{ij})$ agrees with
$\pi^{\sharp}\\!\\!\restriction_{U_{i}}:\mathsf{Hom}\big{(}\mathcal{O}(\llbracket\,{V_{j}}\,\rrbracket),\mathcal{O}(\llbracket\,{U_{i}}\,\rrbracket)\big{)}$,
modulo the canonical
$\mathcal{O}(\llbracket\,{V_{j}}\,\rrbracket)\cong\mathsf{lift}(B_{j})$ and
$\mathcal{O}(\llbracket\,{U_{i}}\,\rrbracket)\cong\mathsf{lift}(A_{i})$ given
by Proposition 4.6, and that by applying $\mathsf{Spec}$ to this morphism we
recover $\pi\\!\\!\restriction_{U_{i}}$. Note that such $\varphi_{ij}$ exist
since $\mathsf{lift}$ is fully faithful.

The morphism $\varphi_{ij}$ induces a natural transformation
$\alpha_{i}:{\llbracket\,{U_{i}}\,\rrbracket}\Rightarrow{{\llbracket\,{V_{j}}\,\rrbracket}\Rightarrow{Y}}$,
which we can glue to an $\alpha:{X}\Rightarrow{Y}$ by Lemma 4.24. Cumbersome
computations show that, modulo the equivalence $\lvert
X\rvert\\!\\!\restriction_{U_{i}}\cong\lvert\llbracket\,{U_{i}}\,\rrbracket\rvert$
of Lemma 5.13, $\lvert\alpha_{i}\rvert$ is just $(\\_\wedge
V_{j})\circ\pi\\!\\!\restriction_{U_{i}}:\mathsf{LRDL}_{\ell+1}^{op}\big{(}\lvert
X\rvert\\!\\!\restriction_{U_{i}},\lvert Y\rvert\big{)}$, as both maps are
induced by $\varphi_{ij}$. In other words, the following diagram commutes

${{\lvert X\rvert\\!\\!\restriction_{U_{i}}}}$${{\lvert
Y\rvert\\!\\!\restriction_{V_{j}}}}$${{\lvert
Y\rvert}}$${{\mathsf{Spec}\big{(}\mathsf{lift}(A_{i})\big{)}}}$${{\mathsf{Spec}\big{(}\mathsf{lift}(B_{j})\big{)}}}$${{\lvert\llbracket\,{U_{i}}\,\rrbracket\rvert}}$${{\lvert\llbracket\,{V_{j}}\,\rrbracket\rvert}}$${{\lvert
Y\rvert}}$$\scriptstyle{\pi\leavevmode\nobreak\
\\!\\!\restriction_{U_{i}}}$$\scriptstyle{\mathbin{\text{\rotatebox[origin={c}]{90.0}{$\scriptstyle\simeq$}}}}$$\scriptstyle{\\_\wedge
V_{j}}$$\scriptstyle{\mathbin{\text{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\simeq$}}}}$$\scriptstyle{\mathsf{Spec}(\mathsf{lift}(\varphi_{ij}))}$$\scriptstyle{\mathbin{\text{\rotatebox[origin={c}]{90.0}{$\scriptstyle\simeq$}}}}$$\scriptstyle{\mathbin{\text{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\simeq$}}}}$$\scriptstyle{\lvert\alpha_{i}\rvert}$

This shows that $\alpha$ is the unique natural transformation such that
$\lvert\alpha\rvert=\pi$. ∎

###  5.3 Comparison theorem

Morally, the functor of points and the geometric realization functor give us
an equivalence of the two notions of qcqs-scheme. However, in our setting they
only form a relative coadjunction.

######  Proposition 5.20.

$\lvert\\_\rvert\dashv_{\mathsf{lift}}h$.

###### Proof.

Let $X:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$ and
$Y:\mathsf{LRDL}_{\ell}^{op}$. We give a bijection

$\displaystyle\\_^{\flat}:\mathsf{LRDL}_{\ell+1}^{op}\big{(}\lvert
X\rvert,\mathsf{lift}(Y)\big{)}\leavevmode\nobreak\ \cong\leavevmode\nobreak\
\big{(}{X}\Rightarrow{h_{Y}}\big{)}$

For the left to right direction, let
$\pi:\mathsf{LRDL}_{\ell+1}^{op}\big{(}\lvert X\rvert,\mathsf{lift}(Y)\big{)}$
be a morphism of (big) locally ringed lattices. For a $R$-valued point
$\alpha:{\mathsf{Sp}(R)}\Rightarrow{X}$ we take its geometric realization and
compose with $\pi$ to get
$|\alpha|\circ\pi:\mathsf{LRDL}_{\ell+1}^{op}\big{(}\lvert\mathsf{Sp}(R)\rvert,\mathsf{lift}(Y)\big{)}$.
By Lemma 5.12 and the properties of $\mathsf{lift}$, we get a chain of
equivalences

$\displaystyle\mathsf{LRDL}_{\ell+1}^{op}\big{(}\lvert\mathsf{Sp}(R)\rvert,\mathsf{lift}(Y)\big{)}\leavevmode\nobreak\
$ $\displaystyle\cong\leavevmode\nobreak\
\mathsf{LRDL}_{\ell+1}^{op}\big{(}\mathsf{Spec}(\mathsf{lift}(R)),\mathsf{lift}(Y)\big{)}$
$\displaystyle\cong\leavevmode\nobreak\
\mathsf{LRDL}_{\ell}^{op}\big{(}\mathsf{Spec}(R),Y\big{)}$

Applying these equivalences to $|\alpha|\circ\pi$ gives the desired morphism
$\pi^{\flat}(\alpha):h_{Y}(R)$. This is immediately seen to be natural in $R$,
i.e. define the required natural transformation.

Now, let $\alpha:{X}\Rightarrow{h_{Y}}$ be a natural transformation. We need
to define a morphism of locally ringed lattices
$\pi:\equiv(\pi^{*},\pi^{\sharp}):\mathsf{LRDL}_{\ell+1}^{op}\big{(}\lvert
X\rvert,\mathsf{lift}(Y)\big{)}$. Let $u:L_{Y}$, this defines a natural
transformation

$\displaystyle\theta_{u}:{h_{Y}}\Rightarrow{\mathcal{L}}$
$\displaystyle\theta_{u}(\rho^{*},\rho^{\sharp})\leavevmode\nobreak\
:\equiv\leavevmode\nobreak\ \rho^{*}(u)$

We can then set
$\pi^{*}(u):\equiv\theta_{u}\circ\alpha:{X}\Rightarrow{\mathcal{L}}$. We now
need to provide a morphism of rings
$\pi^{\sharp}:\mathcal{O}_{Y}(u)\to\big{(}{\llbracket\,{\pi^{*}(u)}\,\rrbracket}\Rightarrow{\mathbb{A}^{1}}\big{)}$.
So let us fix $s:\mathcal{O}_{Y}(u)$ and $x:X(A)$ such that
$\theta_{u}(\alpha(x))\equiv\alpha(x)^{*}(u)=D(1)$. This means that we have a
morphism

$\displaystyle\alpha(x)^{\sharp}:\mathcal{O}_{Y}(u)\to\mathcal{O}_{A}(D(1))\quad(=A)$

which, modulo the above identification, lets us define
$\pi^{\sharp}(s)(x):\equiv\alpha(x)^{\sharp}(s)$. We omit the proof that this
is a ring homomorphism natural in $A$. In order to check that $\pi$ is a
morphism of locally ringed lattices, let $u:L_{Y}$ and $s:\mathcal{O}_{Y}(u)$.
We need give an equality of natural transformations
${X}\Rightarrow{\mathcal{L}}$, so let $x:X(R)$ be given such that
$\alpha(x)^{*}(u)=D(f_{1},...,f_{n})$. We get

$\displaystyle\pi^{*}\big{(}\mathcal{D}_{u}(s)\big{)}(x)\leavevmode\nobreak\ $
$\displaystyle=\leavevmode\nobreak\
\alpha(x)^{*}\big{(}\mathcal{D}_{u}(s)\big{)}$
$\displaystyle=\leavevmode\nobreak\
\mathcal{D}_{\alpha(x)^{*}(u)}(\alpha(x)^{\sharp}(s))$
$\displaystyle=\leavevmode\nobreak\
{\textstyle\bigvee_{i=1}^{n}}\mathcal{D}_{D(f_{i})}(\alpha(x)^{\sharp}(s)\\!\\!\restriction_{D(f_{i})})$
$\displaystyle=\leavevmode\nobreak\
{\textstyle\bigvee_{i=1}^{n}}\psi_{f_{i}}\big{(}D(\alpha(x_{i})^{\sharp}(s))\big{)}$
$\displaystyle=\leavevmode\nobreak\
\mathcal{D}_{\pi^{*}(u)}(\pi^{\sharp}(s))(x)$

where $x_{i}:X(R[\nicefrac{{1}}{{f_{i}}}])$ is the canonical restriction and
$\psi_{f_{i}}$ is given by Lemma 2.4. We omit the proof that this is inverse
to $\\_^{\flat}$. ∎

######  Corollary 5.21.

For a functorial qcqs-scheme $X$ and $Y:\mathsf{LRDL}_{\ell}^{op}$, the map

$\displaystyle\\_^{\flat}:\mathsf{LRDL}_{\ell+1}^{op}\big{(}\lvert
X\rvert,\mathsf{lift}(Y)\big{)}\to\big{(}{X}\Rightarrow{h_{Y}}\big{)}$

given in the proof of Proposition 5.20, maps isomorphisms of ringed lattices
to natural isomorphisms.

###### Proof.

Let $\pi:\mathsf{LRDL}_{\ell+1}^{op}\big{(}\lvert
X\rvert,\mathsf{lift}(Y)\big{)}$ be an isomorphism of locally ringed lattices
and $R:\mathsf{CommRing}_{\ell}$. Since $\lvert\\_\rvert$ is fully faithful on
functorial qcqs-schemes by Proposition 5.19, the map

$\displaystyle\lvert\\_\rvert\circ\pi:\big{(}{\mathsf{Sp}(R)}\Rightarrow{X}\big{)}\to\mathsf{LRDL}_{\ell+1}^{op}\big{(}\lvert\mathsf{Sp}(R)\rvert,\mathsf{lift}(Y)\big{)}$

is a bijection. ∎

######  Theorem 5.22.

We have an adjoint equivalence of categories between functorial and
geometrical qcqs-schemes.

###### Proof.

Since locally ringed lattices and $\mathbb{Z}$-functors form univalent
categories (Proposition 3.7 and [Uni13, Thm. 9.2.5]), it suffices by [Uni13,
Lemma 9.4.7] to show that
$h_{(\\_)}:\mathsf{QcQsSch}_{\ell}\to\mathsf{FunQcQsSch}_{\ell}$ is fully
faithful and essentially surjective. Fully faithfulness was already proved in
Proposition 5.6. Let $X$ be a functorial qcqs-scheme. Looking at the proof of
Corollary 5.14, we can see that $\lvert X\rvert$ is an essentially small
scheme. By Lemma 5.17, we can thus assume the existence of a
$Y:\mathsf{QcQsSch}_{\ell}$ with an isomorphism $\lvert
X\rvert\cong\mathsf{lift}(Y)$. Using Corollary 5.21 this gives us the desired
natural isomorphism $X\cong h_{Y}$. ∎

######  Remark 5.23.

We want to conclude this section with a comparison of our approach with the
presentation in [DG80]. Demazure and Gabriel assume two Grothendieck universes
and define $\mathbb{Z}$-functors to map small rings to big sets. To model this
situation in our setting, assume cumulative universes
$\mathsf{Type}_{\ell}:\mathsf{Type}_{\ell+1}$ and define $\mathbb{Z}$-functors
to be functors $\mathsf{CommRing}_{\ell}\to\mathsf{Set}_{\ell+1}$. The
spectrum $\mathsf{Sp}(A):\equiv\mathsf{Hom}(A,\\_)$ can then even be defined
for big $A:\mathsf{CommRing}_{\ell+1}$. Note however, that this $\mathsf{Sp}$
is only fully faithful when restricted to $\mathsf{CommRing}_{\ell}^{op}$.
This caveat and the fact that universes are simply not cumulative in Cubical
Agda, led the formalization [ZH24] to deviate from [DG80]. We decided to
follow the formalization here, as one of the main objectives was to develop a
univalent and constructive theory of schemes that can be formalized in e.g.
Cubical Agda.

The advantage of the approach of [DG80] is that it allows one to avoid
relative coadjunctions. The “big spectrum functor” $\mathsf{Sp}$ is right
adjoint to $\mathcal{O}$. Similarly, we can define define the functor of
points

$\displaystyle
h_{X}:\equiv\mathsf{LRDL}^{op}_{\ell+1}\big{(}\mathsf{Spec}(\\_),X\big{)}\leavevmode\nobreak\
:\leavevmode\nobreak\ \mathsf{CommRing}_{\ell}\to\mathsf{Set}_{\ell+1}$

for any big $X:\mathsf{LRDL}_{\ell+1}$ and we get an adjunction
$\lvert\\_\rvert\dashv h$. We can then show that this becomes an adjoint
equivalence when restricted to functorial qcqs-schemes and essentially small
qcqs-schemes. In this setting, one can show the existence of the geometric
realization functor $\lvert\\_\rvert$ using purely categorical methods, which
further simplifies the proof. Note that the category of functors
$\mathsf{CommRing}_{\ell}\to\mathsf{Set}_{\ell+1}$ and
$\mathsf{LRDL}^{op}_{\ell+1}$ have colimits over diagrams in
$\mathsf{Type}_{\ell+1}$.313131Showing the completeness of $\mathsf{LRDL}$ is
straightforward, perhaps even more so than the cocompleteness of locally
ringed spaces. Everything, including the support, is computed point-wise. We
can define $\lvert\\_\rvert$ to be the _left Kan-extension_ of the restricted
$\mathsf{Spec}:\mathsf{CommRing}_{\ell}^{op}\to\mathsf{LRDL}^{op}_{\ell+1}$
along the restricted $\mathsf{Sp}$, i.e. the Yoneda embedding. By a standard
result, it is the unique functor (up to unique natural isomorphism) extending
the restricted $\mathsf{Spec}$ that is cocontinuous and left-adjoint to
$h$.323232See e.g. section 1.3 of [Vez10].

In our predicative, constructive setting we do not expect to be able to show
the existence of the Kan extension by general methods, as
$\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$ does not have colimits in
$\mathsf{Type}_{\ell+1}$. Nevertheless, it is still possible to prove the
comparison theorem using the explicit point-free description of
$\lvert\\_\rvert$ as shown in this paper. Univalence allows us two view
$\lvert\\_\rvert$ as a sort of adjoint inverse to $h$ on (functorial) qcqs-
schemes even with a mismatch of universe levels present. For a functorial
qcqs-scheme $X$, $\lvert X\rvert$ has a cover by small affine schemes, and as
sketched in Remark 5.18, we can choose a small scheme for $\lvert X\rvert$ in
a functorial way. In other words the adjoint inverse to $h$ is
$\lvert\\_\rvert$ composed with the functor choosing a small scheme for an
essentially small scheme.

##  6 Schemes of finite presentation

For the statement and proof of the comparison theorem we required three
universes
$\mathsf{Type}_{\ell}\hookrightarrow\mathsf{Type}_{\ell+1}\hookrightarrow\mathsf{Type}_{\ell+2}$
(the last one being the universe in which $\mathsf{LRDL}_{\ell+1}$ lives). The
comparison theorem presented in the previous section is predicative in that it
does not require resizing assumptions. From a truly predicative point of view,
however, having to work in $\mathsf{Type}_{\ell+1}$ for a considerable part of
the proof in order to prove the equivalence for schemes in
$\mathsf{Type}_{\ell}$ feels somewhat unsatisfactorily ad hoc.333333Perhaps
worse still, in a certain sense the types of algebraic structures like groups
and rings depend on the universe. This can be shown already in a rather
minimal type theory. The special case of groups is discussed in [BCDE22]. We
thus want to outline a more “parsimonious” approach that requires only one
universe, in which a specified but arbitrary ring $R$ is assumed and an
ambient universe where e.g. the category of rings (that $R$ belongs to) lives.
The caveat of this approach is that we can only describe schemes of finite
presentation over $R$, a subclass of qcqs-schemes. However, these schemes
still include many motivating examples in algebraic geometry that come from
studying roots of polynomials. Blechschmidt considers the “parsimonious site”
of affine schemes that are locally of finite presentation over some base
scheme $S$, which can be constructed without size issues [Ble21, Sec. 15]. In
the special case where $S=\mathsf{Spec}(R)$ is the affine scheme corresponding
to our fixed ring $R$, one can define schemes of finite presentation over $R$
in a purely functorial way [Ble21, Sec. 16.5].343434These are the external
counterpart for Blechschmidt’s notion of “finitely presented synthetic scheme”
[Ble21, Def. 19.49]. The key algebraic notion is that of a finitely presented
algebra.

######  Definition 6.1.

We say that an $R$-algebra $A$ is _finitely presented_ if there merely exist
polynomials $p_{1},...,p_{m}:R[x_{1},...,x_{n}]$ together with an isomorphism
$A\cong\nicefrac{{R[x_{1},...,x_{n}]}}{{\langle p_{1},...,p_{m}\rangle}}$ of
$R$-algebras. A ring morphism $\mathsf{Hom}(R,A)$ is _of finite presentation_
if it makes $A$ into a finitely presented $R$-algebra. For a ring $R$, the
category $R\text{-}\mathsf{Alg}_{fp}$ has objects pairs of positive integers
$n,m:\mathbb{N}$ together with a list of polynomials $p_{1},...,p_{m}$ with
$p_{i}:R[x_{1},...,x_{n}]$. Such an object $(p_{1},...,p_{m})_{n,m}$
represents the finitely presented algebra
$\nicefrac{{R[x_{1},...,x_{n}]}}{{\langle p_{1},...,p_{m}\rangle}}$.
Accordingly, arrows are $R$-algebra morphisms, i.e.

$\displaystyle R\text{-}\mathsf{Alg}_{fp}$
$\displaystyle\big{(}(p_{1},...,p_{m})_{n,m},(q_{1},...,q_{l})_{k,m}\big{)}$
$\displaystyle:\equiv\mathsf{Hom}_{R}\big{(}\nicefrac{{R[x_{1},...,x_{n}]}}{{\langle
p_{1},...,p_{m}\rangle}},\nicefrac{{R[x_{1},...,x_{k}]}}{{\langle
q_{1},...,q_{l}\rangle}}\big{)}$

This way, we can present the category of finitely presented $R$-algebras as a
small category living in the same universe as $R$.353535Note that this
category is not univalent. However, this does not affect any of the following
results. One could of course consider the Rezk completion [Uni13, Sec. 9.8],
but since we only consider functors from $R\text{-}\mathsf{Alg}_{fp}$ to
univalent categories, these will always factor through the Rezk completion.

######  Example 6.2.

For a ring $R$ and $f:R$ the localization $R[\nicefrac{{1}}{{f}}]$ is a
finitely presented $R$-algebra, as
$R[\nicefrac{{1}}{{f}}]\cong\nicefrac{{R[x]}}{{\langle fx-1\rangle}}$.

######  Lemma 6.3.

If $A$ and $B$ are two finitely presented $R$-algebras, the tensor product
$A\otimes_{R}B$ is finitely presented.

######  Lemma 6.4.

Let $A,B,C$ be rings and $\varphi:\mathsf{Hom}(A,B)$ and
$\psi:\mathsf{Hom}(B,C)$ be morphisms of rings. Then the following hold:

  1. 1.

If $\varphi$ and $\psi$ are of finite presentation, then $\psi\circ\varphi$ is
of finite presentation.

  2. 2.

If $\varphi$ and $\psi\circ\varphi$ are of finite presentation, then $\psi$ is
of finite presentation.

###### Proof.

[Sta18, Tag 00F4] ∎

Defining schemes of finite presentation using locally ringed lattices can be
done analogously to the standard classical setting. By a qcqs-scheme over $R$
we mean a $X:\mathsf{QcQsSch}$ together with a morphism
$\pi_{X}:\mathsf{LRDL}^{op}\big{(}X,\mathsf{Spec}(R)\big{)}$, and we will
simply call them $R$-schemes. A morphism of $R$-schemes is a morphism in the
slice category $\nicefrac{{\mathsf{LRDL}^{op}}}{{\mathsf{Spec}(R)}}$. For a
$R$-scheme $X$ we may regard the structure sheaf as taking values in
$R$-algebras, i.e. $\mathcal{O}_{X}:L_{X}^{op}\to R\text{-}\mathsf{Alg}$.

######  Definition 6.5.

A morphism between two qcqs-schemes $\pi:X\to Y$ is said to be _of finite
presentation_ if there are compatible affine covers $u_{1},\dots,u_{n}$ of
$L_{X}$ and $w_{1},\dots,w_{m}$ of $L_{Y}$ such that for every $u_{i}$ and
$w_{j}$ with $u_{i}\leq\pi^{*}(w_{j})$ the ring morphism
$\pi^{\sharp}\\!\\!\restriction_{u_{i}}:\mathcal{O}_{Y}(w_{j})\to\mathcal{O}_{X}(u_{i})$
is of finite presentation. A qcqs-scheme $X$ over $R$, is said to be of
_finite presentation_ if its morphism $X\to\mathsf{Spec}(R)$ is of finite
presentation.

Using Lemma 6.4 and some standard computations for morphisms of schemes, one
can prove the following two lemmas.

######  Lemma 6.6.

A $R$-scheme $X$ is of finite presentation if and only if there is a an affine
cover $u_{1},...,u_{n}:L_{X}$, such that $\mathcal{O}_{X}(u_{i})$ is a
finitely presented $R$-algebra for all $i$ in $1,...,n$.

######  Lemma 6.7.

Let $X$ and $Y$ be two $R$-schemes of finite presentation, then any morphism
of $R$-schemes $X\to Y$ is of finite presentation.

Note that even if $X$ is an $R$-scheme of finite presentation, the global
sections $\mathcal{O}_{X}(1)$ need not be a finitely presented
$R$-algebra.363636See e.g. [Vak00] for a concrete counterexample. We still get
the following:

######  Proposition 6.8.

Let $\Gamma:\nicefrac{{\mathsf{LRDL}^{op}}}{{\mathsf{Spec}(R)}}\to
R\text{-}\mathsf{Alg}^{op}$ be the global sections functor,
$\mathsf{Spec}:R\text{-}\mathsf{Alg}_{fp}^{op}\to\nicefrac{{\mathsf{LRDL}^{op}}}{{\mathsf{Spec}(R)}}$
be the restriction of the usual spectrum functor to finitely presented
algebras and $\mathcal{U}:R\text{-}\mathsf{Alg}_{fp}\to R\text{-}\mathsf{Alg}$
be the forgetful functor. Then we have a relative coadjunction
$\Gamma\dashv_{\,\mathcal{U}}\mathsf{Spec}$ whose relative counit is an
isomorphism.

Now for the functorial definition of schemes of finite presentation. These
will be _finitely presented $R$-functors_
$R\text{-}\mathsf{Alg}_{fp}\to\mathsf{Set}$, i.e. presheaves on
$R\text{-}\mathsf{Alg}_{fp}^{op}$. The main difference to the situation of
general qcqs-schemes is that this presheaf category is locally small.
Important presheaves, like $\mathbb{A}^{1}$ and $\mathcal{L}$ are defined in
the obvious way (by precomposition with the forgetful functor to rings).
However, functions ${X}\Rightarrow{\mathbb{A}^{1}}$ and compact opens
${X}\Rightarrow{\mathcal{L}}$ of $X:R\text{-}\mathsf{Alg}_{fp}\to\mathsf{Set}$
are now small types. Note that ${X}\Rightarrow{\mathbb{A}^{1}}$ carries an
$R$-algebra structure but does not have to be finitely presented. Similar to
the locally ringed lattice case we get a relative coadjunction with respect to
the forgetful functor $\mathcal{U}:R\text{-}\mathsf{Alg}_{fp}\to
R\text{-}\mathsf{Alg}$.

######  Proposition 6.9.

Let
$\mathsf{Sp}:R\text{-}\mathsf{Alg}_{fp}^{op}\hookrightarrow\mathsf{Fun}\big{(}R\text{-}\mathsf{Alg}_{fp},\mathsf{Set}\big{)}$
denote the Yoneda embedding and
$\mathcal{O}:\mathsf{Fun}\big{(}R\text{-}\mathsf{Alg}_{fp},\mathsf{Set}\big{)}\to
R\text{-}\mathsf{Alg}^{op}$ the global functions functor. Then we have a
relative coadjunction $\mathcal{O}\dashv_{\,\mathcal{U}}\mathsf{Sp}$ whose
relative counit is an isomorphism.

The Zariski coverage on $R\text{-}\mathsf{Alg}_{fp}^{op}$ is defined just as
for $\mathsf{CommRing}^{op}$. Note that this crucially relies on the fact that
by Example 6.2 localizations $R[\nicefrac{{1}}{{f}}]$ and by Lemma 6.3 tensor
products are finitely presented. The proof of subcanonicity carries over to
finitely presented algebras. Compact opens are defined just as for
$\mathbb{Z}$-functors, leading to a functorial definition of $R$-schemes of
finite presentation.

######  Definition 6.10.

We say that $X:R\text{-}\mathsf{Alg}_{fp}\to\mathsf{Set}$ is a _functorial
$R$-scheme of finite presentation_ if it is local and merely has a cover
$U_{1},...,U_{n}:{X}\Rightarrow{\mathcal{L}}$ with
$\llbracket\,{U_{i}}\,\rrbracket\cong\mathsf{Sp}(A_{i})$ for some finitely
presented $R$-algebra $A_{i}$.373737Note that when working with a non-
univalent definition of $R\text{-}\mathsf{Alg}_{fp}$, a truncation is needed
to define the property of “being an affine $R$-scheme of finite presentation”,
i.e. the property of being a representable, see [Uni13, Thm. 9.5.9],

To show that the two definitions of $R$-schemes of finite presentation are
equivalent, we proceed as for qcqs-schemes, but we do not have to be as
careful about universe levels. The functor of points

$\displaystyle
h_{(\\_)}:\equiv\nicefrac{{\mathsf{LRDL}^{op}}}{{\mathsf{Spec}(R)}}\big{(}\mathsf{Spec}(\\_),X\big{)}\leavevmode\nobreak\
:\leavevmode\nobreak\
\nicefrac{{\mathsf{LRDL}^{op}}}{{\mathsf{Spec}(R)}}\to\mathsf{Fun}\big{(}R\text{-}\mathsf{Alg}_{fp},\mathsf{Set}\big{)}$

is defined just as for $\mathbb{Z}$-functors. The realization functor
$\lvert\\_\rvert$ can be defined directly following Definition 5.7 and using
the fact that an object of
$\nicefrac{{\mathsf{LRDL}^{op}}}{{\mathsf{Spec}(R)}}$ is the same as a locally
ringed lattice whose structure sheaf is a sheaf of $R$-algebras.
Alternatively, one can take $\lvert\\_\rvert$ to be the left Kan extension of
$\mathsf{Spec}$ along $\mathsf{Sp}$. Using the small definition of
$R\text{-}\mathsf{Alg}_{fp}$, this Kan extension can be shown to exist
predicatively, as it can be computed pointwise [Rie17, Thm. 6.3.7].

Moreover, we get a regular adjunction $\lvert\\_\rvert\dashv h$. We can show
that $h$ sends $R$-schemes of finite presentation to functorial $R$-schemes of
finite presentation, using Lemma 6.6. Similarly, $\lvert\\_\rvert$ sends
functorial $R$-schemes of finite presentation to $R$-schemes of finite
presentation and we do not have to consider “essentially small schemes” or the
like. When restricted to (functorial) $R$-schemes of finite presentation, the
two adjoints become fully faithful, inducing an equivalence of categories as
illustrated in the diagram below:

${{R\text{-}\mathsf{FunSch}_{fp}}}$${{R\text{-}\mathsf{Sch}_{fp}}}$${{\mathsf{Fun}\big{(}R\text{-}\mathsf{Alg}_{fp},\mathsf{Set}\big{)}}}$${{\nicefrac{{\mathsf{LRDL}^{op}}}{{\mathsf{Spec}(R)}}}}$${{R\text{-}\mathsf{Alg}_{fp}^{op}}}$$\scriptstyle{\mathsf{Spec}}$$\scriptstyle{\mathsf{Sp}}$$\scriptstyle{\lvert\\_\rvert}$$\scriptstyle{h_{(\\_)}}$$\scriptstyle{\Large\simeq}$$\scriptstyle{\dashv}$

##  7 Conclusion

In this paper we gave two point-free definitions of qcqs-schemes, namely as
locally ringed lattices and as $\mathbb{Z}$-functors, and proved the two
notions equivalent. We worked constructively in HoTT/UF using univalence and
higher inductive types. Due to size issues inherent in the functor of points
approach, we had to work across several universes, but we did stay predicative
in the sense that we did not require any form of propositional resizing. In
the last section, we described how one can then define schemes of finite
presentation over an arbitrary base ring and prove a similar equivalence
result, but with less universes.

Even though univalence did play a crucial role in the proof of the main
comparison theorem, many of the results in this paper should be of interest
for the program of constructive algebraic geometry in general. With the
constructive definition (or rather the definitions) of scheme pinned down,
there are plenty of directions in which constructive algebraic geometry could
be developed. We do not want to engage in speculation about which parts of
this vast field can be constructivized. We want to stress, however, that
because of the computational content of constructive proofs, it would be
particularly interesting to see whether a constructive development can be
leveraged for computational problems in algebraic geometry. The relation to
synthetic algebraic geometry needs also to be explored. Especially in view of
the recent use of HoTT/UF for this internal approach by Cherubini, Coquand and
Hutzler [CCH23], one might hope that a comparison with our external approach
can lead to fruitful insights.383838For an overview of the many (sub-) topics
currently investigated in this fascinating young research program see
https://github.com/felixwellen/synthetic-zariski Finally, it is worth noting
that the fundamental notions of constructive scheme theory, as presented in
this paper, allow for a concise and pleasant presentation. Hopefully, this
will serve an inspiration to further the development of constructive algebraic
geometry, with or without univalence.

The other main objective was of course to give an account of basic scheme
theory that can be formalized in a proof assistant like Cubical Agda. While
the paper can be used as a general blueprint for a formalization of the
comparison theorem, the same cannot be said for some of the individual proofs
and definitions given in the paper. Extending the formalization of functorial
qcqs-schemes in [ZH24] to include all results of Section 4 should be more or
less directly feasible. A formalization of qcqs-schemes as locally ringed
lattices, however, should be regarded as a substantial formalization project,
even with the structure sheaf of an affine scheme already formalized in
[ZM23]. This is because we did not work with an exact definition of the
structure sheaf and instead relied heavily on canonical isomorphisms. The case
that this common practice generally creates an obstacle towards formalization
was put forward rather convincingly by Buzzard [Buz24]. In view of the results
of [ZM23], one might hope that in this particular instance univalence could be
of help, but as indicated in the paper, careful and clever rephrasing of many
of the results and constructions might be required. Ultimately, it appears
necessary to prove a lot of results on locally ringed lattices in terms of
sheaves obtained by Kan extensions, before even being able to describe affine
schemes as locally ringed lattices. Formalizing the proof of the univalent
constructive comparison theorem will certainly hold many surprises. All in
all, such a formalization would figure as a major milestone in formal
univalent set-level mathematics.

## References

  * [ACMZ21] Carlo Angiuli, Evan Cavallo, Anders Mörtberg, and Max Zeuner.  Internalizing representation independence with univalence.  Proc. ACM Program. Lang., 5(POPL), January 2021.  doi:10.1145/3434293.
  * [AL19] Benedikt Ahrens and Peter LeFanu Lumsdaine.  Displayed Categories.  Logical Methods in Computer Science, Volume 15, Issue 1, March 2019.  URL: https://lmcs.episciences.org/5252, doi:10.23638/LMCS-15(1:20)2019.
  * [AM69] Michael Francis Atiyah and Ian Grant MacDonald.  Introduction to Commutative Algebra.  Addison-Wesley-Longman, 1969.
  * [BCDE22] Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó.  The Burali-Forti argument in HoTT/UF with applications to the type of groups in a universe.  Agda formalization available at https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.BuraliForti.html, 2022\.
  * [Ble21] Ingo Blechschmidt.  Using the internal language of toposes in algebraic geometry, 2021.  arXiv:2111.03685.
  * [Buz24] Kevin Buzzard.  Grothendieck’s use of equality, 2024.  URL: https://arxiv.org/abs/2405.10387, arXiv:2405.10387.
  * [CCH23] Felix Cherubini, Thierry Coquand, and Matthias Hutzler.  A foundation for synthetic algebraic geometry, 2023.  arXiv:2307.00073.
  * [CD13] Thierry Coquand and Nils Anders Danielsson.  Isomorphism is equality.  Indagationes Mathematicae, 24(4):1105–1120, 2013.  In memory of N.G. (Dick) de Bruijn (1918–2012).  URL: https://www.sciencedirect.com/science/article/pii/S0019357713000694, doi:https://doi.org/10.1016/j.indag.2013.09.002.
  * [CL03] Thierry Coquand and Henri Lombardi.  Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative rings.  In Commutative ring theory and applications, volume 231 of Lecture Notes in Pure and Applied Mathematic, pages 477–499. Dekker, New-York, 2003.  doi:10.1201/9780203910627.
  * [CLS07] Thierry Coquand, Henri Lombardi, and Peter Schuster.  The projective spectrum as a distributive lattice.  Cahiers de Topologie et Géométrie différentielle catégoriques, 48(3):220–228, 2007.  URL: http://www.numdam.org/item/CTGDC_2007__48_3_220_0/.
  * [CLS09] Thierry Coquand, Henri Lombardi, and Peter Schuster.  Spectral schemes as ringed lattices.  Annals of Mathematics and Artificial Intelligence, 56(3):339–360, 2009.  doi:10.1007/s10472-009-9160-7.
  * [DG71] Jean Dieudonné and Alexandre Grothendieck.  Éléments de géométrie algébrique, volume 166\.  Springer Berlin Heidelberg New York, 1971.
  * [DG80] Michel Demazure and Peter Gabriel.  Introduction to algebraic geometry and algebraic groups.  Elsevier, 1980.
  * [EH06] David Eisenbud and Joe Harris.  The geometry of schemes, volume 197.  Springer Science & Business Media, 2006.
  * [En83] Luis Español.  Le spectre d’un anneau dans l’algèbre constructive et applications à la dimension.  Cahiers de Topologie et Géométrie Différentielle Catégoriques, 24(2):133–144, 1983.  URL: http://www.numdam.org/item/CTGDC_1983__24_2_133_0/.
  * [Esc22] Martín Hötzel Escardó.  Introduction to Univalent Foundations of Mathematics with Agda, 2022\.  URL: https://arxiv.org/abs/1911.00580, arXiv:1911.00580.
  * [GG74] Alexandre Grothendieck and Federico Gaeta.  Introduction to Functorial Algebraic Geometry: After a Summer Course.  State University of New York at Buffalo, Department of Mathematics, 1974\.  https://ncatlab.org/nlab/files/GrothendieckIntrodFunctorialGeometryI1973.pdf.
  * [Hak72] Monique Hakim.  Topos annelés et schémas relatifs.  Springer-Verlag, Berlin, 1972.
  * [Har13] Robin Hartshorne.  Algebraic geometry, volume 52.  Springer Science & Business Media, 2013.
  * [Jan87] Jens Carsten Jantzen.  Representations of algebraic groups.  Academic Press, Boston, 1987.  earlier preprint available at https://archive.mpim-bonn.mpg.de/id/eprint/607/1/preprint_1985_9.pdf.
  * [Joh82] Peter T. Johnstone.  Stone spaces, volume 3.  Cambridge university press, 1982.
  * [Joh02] Peter T Johnstone.  Sketches of an Elephant: A Topos Theory Compendium: Volume 2, volume 2.  Oxford University Press, 2002.
  * [Joy76] André Joyal.  Les théoremes de chevalley-tarski et remarques sur l’algèbre constructive.  Cahiers Topologie Géom. Différentielle, 16:256–258, 1976\.
  * [Koc76] Anders Kock.  Universal projective geometry via topos theory.  J. Pure Appl. Algebra, 9:1–24, 1976.  doi:10.1016/0022-4049(76)90002-5.
  * [Mad13] David Madore.  Comment définir efficacement ce qu’est un schéma.  David Madore’s WebLog, 2013.  http://www.madore.org/~david/weblog/d.2013-09-21.2160.definition-schema.html.
  * [ML75] Per Martin-Löf.  An Intuitionistic Theory of Types: Predicative Part.  In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium ’73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73–118. North-Holland, 1975.  doi:10.1016/S0049-237X(08)71945-1.
  * [ML13] Saunders Mac Lane.  Categories for the working mathematician, volume 5.  Springer Science & Business Media, 2013.
  * [MLM12] Saunders Mac Lane and Ieke Moerdijk.  Sheaves in geometry and logic: A first introduction to topos theory.  Springer Science & Business Media, 2012.
  * [Mum99] David Mumford.  The red book of varieties and schemes: includes the Michigan lectures (1974) on curves and their Jacobians, volume 1358.  Springer Science & Business Media, 1999.
  * [nLa24a] nLab authors.  coverage.  https://ncatlab.org/nlab/show/coverage, May 2024.  Revision 42.
  * [nLa24b] nLab authors.  relative adjoint functor.  https://ncatlab.org/nlab/show/relative+adjoint+functor, May 2024\.  Revision 17.
  * [NW08] Marc Nieper-Wißkirchen.  Algebraische geometrie.  unpublished lecture notes, 2008.
  * [Rie17] Emily Riehl.  Category Theory in Context.  Courier Dover Publications, 2017.
  * [Sch03] Peter Michael Schuster.  Spectra and sheaves in formal topology, 2003.  Habilitationsschrift, Universität München.
  * [Sch06] Peter Schuster.  Formal zariski topology: Positivity and points.  Annals of Pure and Applied Logic, 137(1):317–359, 2006.  URL: https://www.sciencedirect.com/science/article/pii/S016800720500076X, doi:https://doi.org/10.1016/j.apal.2005.05.026.
  * [Sch08] Peter Schuster.  The zariski spectrum as a formal geometry.  Theoretical Computer Science, 405(1):101–115, 2008.  Computational Structures for Modelling Space, Time and Causality.  URL: https://www.sciencedirect.com/science/article/pii/S0304397508004507, doi:https://doi.org/10.1016/j.tcs.2008.06.030.
  * [Sta18] The Stacks Project Authors.  Stacks Project.  https://stacks.math.columbia.edu, 2018.
  * [Sto38] Marshall Harvey Stone.  Topological representations of distributive lattices and brouwerian logics.  Časopis pro pěstování matematiky a fysiky, 67(1):1–25, 1938.
  * [Uni13] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  * [Vak00] Ravi Vakil.  An example of a nice variety whose ring of global sections is not finitely generated.  Unpublished note available online at https://math.stanford.edu/~vakil/files/nonfg.pdf, 2000.
  * [Vak24] Ravi Vakil.  The Rising Sea: Foundations of Algebraic Geometry.  Preprint, 2024.  URL: http://math.stanford.edu/~vakil/216blog/FOAGfeb2124public.pdf.
  * [vBB21] Johannes Schipp von Branitz and Ulrik Buchholtz.  Using Displayed Univalent Graphs to Formalize Higher Groups in Univalent Foundations.  unpublished draft available online at https://ulrikbuchholtz.dk/durgs.pdf, 2021.
  * [Vez10] Alberto Vezzani.  On the geometry over the fiel with one element.  Master’s thesis, Università degli Studi di Milano, 2010.  Available at https://www.math.univ-paris13.fr/~vezzani/Files/Research/tesi_vezzani.pdf.
  * [Voe11] Vladimir Voevodsky.  Resizing rules – their use and semantic justification. slides from a talk at types, bergen, 11 september, 2011.  URL: https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2011_Bergen.pdf.
  * [Voe15] Vladimir Voevodsky.  An experimental library of formalized mathematics based on the univalent foundations.  Mathematical Structures in Computer Science, 25(5):1278–1294, 2015\.  doi:10.1017/S0960129514000577.
  * [ZH24] Max Zeuner and Matthias Hutzler.  The Functor of Points Approach to Schemes in Cubical Agda.  https://arxiv.org/abs/2403.13088, 2024.  arXiv:2403.13088.
  * [ZM23] Max Zeuner and Anders Mörtberg.  A Univalent Formalization of Constructive Affine Schemes.  In Delia Kesner and Pierre-Marie Pédrot, editors, 28th International Conference on Types for Proofs and Programs (TYPES 2022), volume 269 of Leibniz International Proceedings in Informatics (LIPIcs), pages 14:1–14:24, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.  URL: https://drops.dagstuhl.de/opus/volltexte/2023/18457, doi:10.4230/LIPIcs.TYPES.2022.14.