# Univalent Foundations of Constructive Algebraic Geometry

Max Zeuner

(Department of Mathematics, Stockholm University
<EMAIL_ADDRESS>
)

###### Abstract

We investigate two constructive approaches to defining quasi-compact and
quasi-separated schemes (qcqs-schemes), namely qcqs-schemes as locally ringed
lattices and as functors from rings to sets. We work in Homotopy Type Theory
and Univalent Foundations, but reason informally. The main result is a
constructive and univalent proof that the two definitions coincide, giving an
equivalence between the respective categories of qcqs-schemes.

#### Acknowledgments

The author would like to thank Thierry Coquand for suggesting this project and
for his invaluable input and feedback. Further thanks go to Anders Mörtberg
for his supervision and to Felix Cherubini and Matthias Hutzler for being an
integral part of the project.

##  1 Introduction

Since its inception by Grothendieck and his school in the latter half of the
20th century, the notion of scheme has found important applications in various
fields of mathematics ranging from geometry to number theory. Arguably, it has
led to some of the most staggering mathematical achievements in recent
history. In spite of being a rather abstract notion that relies heavily on
modern set-theoretic machinery, the motivations for studying schemes coming
from classic algebraic geometry have a rather hands-on computational
character: studying the solutions to finite systems of polynomial equations.
Giving a satisfying constructive definition of schemes and determining the
computational content of scheme theory, is thus an important problem for the
program of constructive mathematics.

In this task, the constructive mathematician is confronted with two options:
Constructivizing the topological notion of scheme as a locally ringed space or
the categorical notion of scheme as a “functor of points”. At first glance,
categorical/functorial schemes seem more appropriate for constructive study,
as topological spaces are an inherently problematic notion from a constructive
point of view. The categorical approach was actually the preferred one of
Grothendieck himself [GG74]. Furthermore, all of the basic notions of the
functorial approach, as e.g. defined in the textbook “Introduction to
algebraic geometry and algebraic groups” By Demazure and Gabriel [DG80], are
constructively valid. Moreover, the functorial schemes embed into a sheaf
topos, the so-called _big Zariski topos_ and in the internal language of this
topos, which is constructive, one can develop algebraic geometry
synthetically. This line of work was pioneered by Kock [Koc76] and is studied
extensively in the thesis of Blechschmidt [Ble21]. The synthetic approach has
also been studied using Homotopy Type Theory and Univalent Foundations by
Cherubini, Coquand and Hutzler [CCH23].

As its name suggests, however, the big Zariski topos cannot be defined
rigorously without introducing size issues, which arise already when working
classically. Demazure and Gabriel assume _two_ Grothendieck universes for
precisely this reason [DG80]. More modern sources usually tend to ignore size
issues or leave “the appropriate modifications” to resolve these issues “to
the interested reader” [Jan87]. Of course, the size issues become even more
pressing in a constructive, predicative setting. Blechschmidt’s thesis
contains an insightful discussion [Ble21, Sec. 16.5], highlighting that it is
possible to work in an entirely constructive and predicative set-up for
synthetic algebraic geometry, by restricting oneself to _finitely presented_
algebras over some base ring $R$. One can then define _schemes of finite
presentation over_ $\mathsf{Spec}(R)$ in a purely functorial way that
corresponds to a well-behaved internal definition of “finitely presented
synthetic schemes” [Ble21, Def. 19.49].

In this context it is noteworthy that all _quasi-compact and quasi separated_
schemes (qcqs-schemes) can be defined constructively and predicatively. These
qcqs-schemes contain all schemes of finite presentation and need not be
defined over some affine base scheme. This is achieved through a careful
point-free reformulation of the topological approach. Initiated in a series of
papers by Schuster [Sch03, Sch06, Sch08] using formal topology, this approach
was subsequently refined by Coquand, Lombardi and Schuster [CLS07, CLS09]
using lattices. The main observation is that, since qcqs-schemes are always a
coherent or spectral space, it is sufficient to consider the distributive
lattice of quasi-compact opens and the structure sheaf restricted to this
lattice. Instead of locally ringed spaces, qcqs-schemes are defined as ringed
lattices in [CLS09].

In this paper we want to establish a common constructive framework for the
functorial and the lattice-theoretic approach. Classically, to each locally
ringed space $X$ one can associate a sheaf in the big Zariski topos called the
functor of points of $X$. This is the construction that most textbooks use,
when developing the functorial approach from the standard classical
approach.111 See e.g. [EH06]. Modulo size issues, this functor of points
construction has a left adjoint and when restricted schemes this adjunction
becomes an equivalence of categories. This result is called the _comparison
theorem_ in [DG80, Ch. I, §1, no 4.4] and the main result of this paper is a
constructive version of this result for qcqs-schemes and schemes of finite
presentation.

The main obstacle are not the size issues, but the circumstance that qcqs-
schemes in [CLS09] are defined as ringed lattices, while the functor of points
construction requires a _locally_ ringed space. What is needed are notions of
_locally ringed lattices_ and their _morphisms_ , such that a morphism of
qcqs-schemes (in the sense of [CLS09]) is just a morphism of locally ringed
lattices. In [CLS09], the study of such notions is omitted on purpose. The
authors argue that the paper shows that

> “ _up to a certain point one can get by on without any talk of locally
> ringed lattices and their morphisms, concepts which seem relatively involved
> if compared with the ones given in this paper._ ”

Yet, they do conclude that the study of locally ringed lattices is central to
a fully constructive foundation of algebraic geometry. In this paper we want
to fill this gap and provide an in-depth discussion of locally ringed lattices
and their morphisms. This is not just a means to the end of obtaining a
constructive comparison theorem. We want to show that qcqs-schemes as locally
ringed lattices actually admit a rather neat presentation.

The basics of the constructive approach to functorial qcqs-schemes that we use
in this paper have actually been formalized in the Cubical Agda [ZH24]. The
size issues are tackled by using enough type-theoretic universes. As Cubical
Agda is an extension of the Agda proof assistant supporting Homotopy Type
Theory and Univalent Foundations (HoTT/UF), these universes are univalent. We
use HoTT/UF as the foundation for this work as well and make crucial use of
univalence. This choice of foundation for (constructive) algebraic geometry is
further motivated by a Cubical Agda formalization of the structure sheaf of an
affine scheme [ZM23], suggesting that the structuralist approach to
mathematics of the Grothendieck school can be emulated more faithfully using
univalence. Generally, HoTT/UF is not only a foundation for “higher”
mathematics and synthetic homotopy theory. The internal notions of sets and
propositions provide a natural framework for set-level constructive
mathematics with convenient features like quotients. In the particular case of
the constructive comparison theorem, univalent type-theoretic universes let us
circumvent size issues and actually strengthen the main result.

This paper tries to strike a delicate balance between conceptual clarity and
formal rigor. On the one hand, many of the insights presented in the paper do
not actually depend on the choice of foundation and we do not want to bury
them under technicalities. On the other hand, with important parts of
constructive scheme theory already formalized in the univalent Cubical Agda
proof assistant [ZM23, ZH24], this paper aims to serve as a sort of blue-print
for formalized univalent and constructive algebraic geometry in the tradition
of Voevodsky’s Foundations library [Voe15]. The paper is structured as
follows:

  * •

In Section 2 we give some of the necessary background. We comment on our use
of HoTT/UF and provide some guidance for readers not familiar with type theory
or univalence. We also introduce the so-called Zariski lattice of a
commutative ring. This construction has been studied extensively in point-free
topology and constructive algebra and will play an important role throughout
this paper.

  * •

In Section 3 we introduce the notion of a locally ringed lattice, building on
an idea of Coquand. We show that the Zariski lattice of a commutative ring $R$
together with its structure sheaf is a locally ringed lattice, which can be
regarded as the constructive spectrum of $R$. We give a simple proof that the
thus induced spectrum functor is adjoint to the global sections functor. We
define qcqs-schemes as locally ringed lattices and show that scheme morphisms
as defined in [CLS09] are just morphisms of locally ringed lattices. We finish
the section discussing why schemes defined as locally ringed lattices coincide
with classical qcqs-schemes.

  * •

In Section 4 we describe the functor of points approach to qcqs-schemes. We
build on the Cubical Agda formalization described in [ZH24], but provide
strengthened results. We define $\mathbb{Z}$-functors, i.e. functors from
rings to sets, and the Zariski coverage on $\mathbb{Z}$-functors. We introduce
compact open subfunctors as subobjects of $\mathbb{Z}$-functors that are
classified by the Zariski lattice and use these to define functorial qcqs-
schemes. We prove that compact open subfunctors of functorial qcqs-schemes are
qcqs-schemes.

  * •

In Section 5 we prove a “comparison theorem” for the two notions of qcqs-
schemes given in this paper. The proof can be seen as an adaption of the
comparison theorem of Demazure and Gabriel to HoTT/UF, making some of the
steps more explicit and precise. We define the functor of points of a locally
ringed lattice and the realization of a $\mathbb{Z}$-functor as a locally
ringed lattice. We show that these functors are adjoint modulo size issues and
that on (functorial) qcqs-schemes both functors become fully faithful. With
the help of univalence, we can ignore size issues and obtain an equivalence of
the respective categories of qcqs-schemes.

  * •

In Section 6 we give an outline of how to adapt the above results to schemes
of finite presentation over some base ring $R$, without having to deal with
size issues. The classical definition is adapted to locally ringed lattices
and for functorial schemes of finite presentation we use Blechschmidt’s
parsimonious site of finitely presented $R$-functors [Ble21, Sec. 16.5]. We
indicate why in this setting the proof of the comparison theorem not only
still goes through, but can actually be simplified.

##  2 Background

This paper aims to give a self-contained introduction to the constructive
theory of schemes from the univalent point of view. Familiarity with classical
algebraic geometry and schemes as e.g. introduced in Hartshorne’s classic
“Algebraic Geometry” [Har13] is not strictly required, although certainly
helpful to gain an intuition for the notions introduced in this paper and for
understanding the motivations to study these notions in the first place. An
exception is Section 3.4, where we compare our definition using locally ringed
lattices to the classical one. What is assumed as a prerequisite, however, is
some commutative algebra including the basic theory of ideals and
localizations of commutative rings, i.e. rings of fractions.222 These
prerequisites are covered e.g. in the first three chapters of “Introduction to
Commutative Algebra” by Atiyah and MacDonald [AM69]. On top of that we will
also assume knowledge of category theory, in particular familiarity with (co-)
limits, adjunctions, presheaves, the Yoneda lemma and Kan extensions.333 This
is covered in e.g. chapters I-V and X of Mac Lane’s “Categories for the
working mathematician” [ML13] or Riehl’s “Category Theory in Context” [Rie17].

###  2.1 Univalent foundations

We work in HoTT/UF and all definitions and results are written in the informal
(or rather semi-formal) style of the “HoTT-book” [Uni13]. The paper aims to
present the key definitions and ideas with only a modicum of type-theoretic
notation that we quickly want to recapitulate here. For understanding the
details of this paper and the relation to the Cubical Agda formalizations
[ZM23, ZH24], acquaintance with HoTT/UF is required.444 This roughly amounts
to the material covered in first three chapters of the HoTT-book together with
some additional topics like set-quotients, truncations and of course the
consequences of univalence. The notation largely follows the conventions of
the HoTT-book [Uni13], with some exceptions inspired by the syntax of the Agda
proof assistant. We are first and foremost concerned with types and their
terms rather than sets and their elements and thus write $x:A$ to denote that
$x$ is of type $A$, instead of $x\in A$. Note that this is a stipulation, like
introducing a new variable, rather than a provable statement. In particular,
there is no general type-theoretic equivalent to $x\notin A$.

HoTT/UF is most commonly described as an extension of Martin-Löf’s _dependent
type theory_ (MLTT) [ML75]. For our purposes, we actually only need rather few
additions to MLTT namely, the univalence axiom and set-quotients, which can
then be used to define propositional truncations. For a type $A$, a dependent
type $B$ over $A$ can be seen as a family of types $B(a)$ for $a:A$. The type
of _dependent functions_ $(a:A)\to B(a)$ is the type of functions $f$ that
take an input $a:A$ and return an output $f(a):B(a)$, i.e. functions that vary
in their codomain depending on the input. Note that we are using Agda-syntax
for dependent functions rather than $\Pi$-types in order to avoid confusion
with products. The $\Sigma$-type or type of _dependent pairs_
$\Sigma_{a:A}B(a)$ is the type of pairs $(a,b)$ such that $a:A$ and $b:B(a)$,
i.e. pairs where the type of the second component depends on the first
component. These are incredible useful to define complex structures. However,
we will mostly introduce new structures informally and avoid writing
$\Sigma$-types in order to increase readability.

Martin-Löf type theory has two notions of equality. Definitional equality,
which we will denote by $\equiv$, is a stipulated equality that cannot be
(dis-) proven. We follow the HoTT-book and write $:\equiv$ for definitional
equalities that introduce new objects or notation. On top of that there are
_identity types_. For $x,y:A$, we may think of the type $x=y$ as the type of
proofs that $x$ equals $y$. Identity types can be rather complex objects in
HoTT/UF, but they let us define the notions of set and proposition internally,
meaning that we can define inside HoTT/UF, which types are propositions, sets
or neither. Propositions are subsingleton types or types with at most one
element. In other words, a proposition is a type $P$ such that for all $x,y:P$
we have $x=y$. The intuition for this is that giving an element of $P$ amounts
to proving $P$. A proposition can be given a proof, but no further structure.
There is nothing more to a proof than establishing the truth of the
corresponding proposition, as any two proofs are regarded as equal.

A type $S$ is called a set if for any $x,y:S$, the type of proofs of equality
$x=y$ is a proposition. The intuition for this definition is rooted in the
discrete nature of sets, where elements can be equal or not, but do not share
any other relation. A subset of $S$ is a function $S\to\mathsf{Prop}$ from $S$
into the type of propositions. This should be taken with a grain of salt, as
we need to introduce universes to talk about things like the type of all
propositions without running into paradoxes, see the discussion below. Only
for a subset $X$ of $S$, will we us the notation $x\in X$, denoting the type
of proofs that $x:S$ is in $X$, i.e. the proposition that $X$ (seen as a
function) maps $x$ to. For the $\Sigma$-type of $x:S$ with a proof that $x\in
X$, we will use set-theory inspired notation writing $\\{\,x:S\,|\,x\in
X\,\\}$ as in the HoTT-book [Uni13, 3.5.2]. As the proof of $x\in X$ can often
be ignored, we will sometimes write $x:X$ for introducing and element of $S$
that belongs to $X$. Strictly speaking, this is an abuse notation, identifying
$X$ as a function with the above $\Sigma$-type, but it reduces verbosity. The
univalence axiom actually implies that certain types are not sets. For sets
$X$ and $Y$, the type $X=Y$ is not a proposition, but a set and it is in
bijection with the set of bijections from $X$ to $Y$. This means that the
category of sets is a univalent category and we will discuss below, why this
is actually a helpful feature for our purposes.

In order to describe existential quantification as a proposition, we need so-
called _propositional truncation_ , an operation that turns any type into a
proposition, by “truncating” or “squashing” any structure on objects.
Following the HoTT-book we say that there _merely exists_ an $a:A$ such that
$P(a)$ if we have an object/proof of the truncated $\Sigma$-type, which we
will write as $\exists_{a:A}P(a)$. Note that the truncation prevents us from
extracting the “witness” $a$. This way choice principles when stated in terms
of mere existence become unprovable in HoTT/UF. This is of course in line with
constructive mathematics. Reasoning constructively about sets using
propositions and truncations in HoTT/UF requires some getting used to,
especially when concepts like set-quotients are involved.555 Here, we will not
get into the details of how set-quotients are defined, but obersve that for
sets they work very much as expected. Ultimately, it is a rather rewarding
approach that can provide some useful intuition for constructivity issues.

A point in which we depart from the HoTT-book in more than just notation is
the treatment of universes. We do a assume a (potentially infinite) hierarchy
of univalent universes, closed under the usual type formers, indexed by their
_level_ : $\mathsf{Type}_{0},\mathsf{Type}_{1},$ etc. However, we do not take
these universes to be cumulative. Instead, we assume explicit embeddings
$\mathsf{lift}:\mathsf{Type}_{\ell}\hookrightarrow\mathsf{Type}_{\ell+1}$
commuting with all the type formers. The reason for this is that we want our
work to be in line with the results of [ZM23, ZH24] that are already
formalized in Cubical Agda, which does not have cumulative universes. To
remind the reader that we work with non-cumulative universes, we use Agda-like
notation, but we omit levels whenever we are working within a single universe.
For example, we write $\mathsf{Set}$ for the type or category of sets in a
universe $\mathsf{Type}$ at an unspecified level. This type itself lives in
the successor universe, but this can often be ignored. If size issues do
matter, we will always be careful to annotate universe levels. Note that we
are not assuming any form of impredicativity for our universes, such as
Voevodsky’s resizing axioms [Voe11]. This means that the type
$\mathsf{Prop}_{\ell}$ of propositions in $\mathsf{Type}_{\ell}$ lives in
$\mathsf{Type}_{\ell+1}$. Similarly, for a set $S:\mathsf{Type}_{\ell}$ the
type of subsets $S\to\mathsf{Prop}_{\ell}$ lives in $\mathsf{Type}_{\ell+1}$
as well.

Apart from the basics, we use concepts and results from category theory in
HoTT/UF, as described in chapter 9 of the HoTT-book [Uni13]. An important
difference in nomenclature is that by a _category_ we denote what the HoTT-
book would call a pre-category [Uni13, Def. 9.1.1], i.e. a structure
consisting of a _type of objects_ and _sets of arrows_ between any two objects
with identities and composition, satisfying the usual laws. For a category
$\mathcal{C}$, we denote (with some abuse of notation) its type of objects by
$\mathcal{C}$ as well and the type of arrows as $\mathcal{C}\big{(}x,y\big{)}$
for $x,y:\mathcal{C}$. For example $\mathsf{Set}$ is both the type of sets and
the corresponding category (with functions as arrows) in a given universe. The
basic theory of functors, natural transformations, (co-) limits and the Yoneda
lemma can be developed in a very familiar, straightforward fashion in HoTT/UF
for this notion of category. We write functors as if they were functions
$F:\mathcal{C}\to\mathcal{D}$ and omit projections for the action on objects
or arrows. In particular, we have $F(x):\mathcal{D}$ for $x:\mathcal{C}$ and
$F(f):\mathcal{D}\big{(}F(x),F(y)\big{)}$ for
$f:\mathcal{C}\big{(}x,y\big{)}$. Natural transformations between functors $F$
and $G$ are denoted by ${F}\Rightarrow{G}$ and the category of functors from
$\mathcal{C}$ to $\mathcal{D}$ is denoted by
$\mathsf{Fun}\big{(}\mathcal{C},\mathcal{D}\big{)}$.

Of special interest are so-called _univalent categories_. Those are categories
for which the identity types on objects are canonically equivalent to types of
isomorphisms (defined through inverse arrows). Arguably, they are the central
notion of univalent category theory and are thus simply called categories in
the HoTT-book [Uni13, Def. 9.1.6]. They are, however, a truly novel concept
that has no counterpart outside of HoTT/UF. Certain things that are usually
not provable in constructive category theory do hold for univalent categories
in HoTT/UF. If $F:\mathcal{C}\to\mathcal{D}$ is a functor between univalent
categories that is fully-faithful and essentially surjective, we can actually
construct an adjoint inverse to $F$ [Uni13, Lemma 9.4.5 & 9.4.7]. This will be
used in the main Theorem 5.22.

Proving that a category is univalent usually requires the univalence axiom, or
rather the so-called “structure identity principle” in combination with
univalence [Uni13, Sec. 9.8]. This way, one can prove that not only the
category of sets $\mathsf{Set}$, but also categories of algebraic structures
like commutative rings $\mathsf{CommRing}$ and distributive lattices
$\mathsf{DistLattice}$ are univalent. There are several versions of the
structure identity principle in the literature,666See [CD13, Uni13, Esc22,
AL19, vBB21, ACMZ21]. so we do not want to go into details here. However, we
will use it to prove that locally ringed lattices form a univalent category in
Proposition 3.7. Readers not familiar with univalent category theory can
regard this fact together with the aforementioned fact about functors between
univalent categories as a black box, only required in the last step of proving
the comparison theorem.

When working with univalent categories we can only give definitions and proofs
that are invariant under isomorphisms. As mentioned in the introduction, this
seems to fit the approach of the Grothendieck school. It is then not too
surprising that virtually all of the categories appearing in this paper are
univalent. As we saw for sets, however, objects of a univalent category do not
necessarily form a set. This is not an issue of size but of identity types.
The type of objects of a univalent category is in general a so-called
“homotopy groupoid”. Even though the aim of this paper is to develop set-level
constructive mathematics in HoTT/UF, non-sets will thus play an important
role. The only place in the paper, where this is actually an issue is Example
3.9, where we define the structure sheaf of an affine scheme. Here, we do not
want to get into any details and refer the interested reader to [ZM23].
Especially in view of the results of [ZM23] and this paper, we would like to
argue that one should regard the occurrence of non-sets as a feature rather
than a bug of univalent foundations of algebraic geometry.

###  2.2 The Zariski lattice

Both definitions of qcqs-schemes that we will give in this paper crucially
rely on an important notion from constructive algebra, called the Zariski
lattice of a ring. It can be seen as the constructive counterpart to the
Zariski spectrum of a ring. A common starting point for algebraic geometry is
the observation that for a any ring $R$, the set of prime ideals
$\mathfrak{p}\subseteq R$ can be equipped with a topology, the so-called
Zariski topology. One can then define affine schemes and schemes using this
“spectrum” $\mathsf{Spec}(R)$. The Zariski open sets are generated by basic
opens. For $f:R$, the corresponding basic open is given as

$\displaystyle D(f)=\big{\\{}\mathfrak{p}\leavevmode\nobreak\
|\leavevmode\nobreak\ f\notin\mathfrak{p}\leavevmode\nobreak\ \big{\\}}$

From a constructive point of view this definition is not really workable.
Point-set topology is already in itself inherently non-constructive and in the
case of the Zariski spectrum of some general $R$, it is impossible to prove
that there are any points (prime ideals) without invoking Zorn’s lemma or some
other choice principle. One can, however, restrict to (quasi-) compact open
subsets, which form a distributive lattice with finite set-theoretic union and
intersection, the so-called Zariski lattice $\mathcal{L}_{R}$. Joyal observed
that $\mathcal{L}_{R}$ is described by a universal property, which is stated
in terms of so-called _supports_ [Joy76]. Note that in this paper we will
always work with bounded distributive lattices, i.e. distributive lattices
with a top and bottom element, and commutative rings with $1$.

######  Definition 2.1.

Let $R$ be a commutative ring and $L$ be a distributive lattice. A map $d:R\to
L$ is called a _support_ of $L$ if

  1. 1.

$d(0)=0$ and $d(1)=1$

  2. 2.

$d(xy)=d(x)\wedge d(y)$ for all $x,y:R$

  3. 3.

$d(x+y)\leq d(x)\vee d(y)$ for all $x,y:R$

Basic opens are always compact and the map $D:R\to\mathcal{L}_{R}$ is a
support. In fact, it is a universal support in the following sense: For any
support $d:R\to L$ there is a unique lattice homomorphism such that the
following diagram commutes

${R}$${\mathcal{L}_{R}}$${L}$$\scriptstyle{D}$$\scriptstyle{d}$$\scriptstyle{\exists!}$

This means that we can define $\mathcal{L}_{R}$ as the lattice generated by
formal elements $D(f)$, modulo the equations given by the support conditions.
There is also a more direct but still point-free way to construct the Zariski
lattice. This is the approach taken by Español [En83] and Coquand and Lombardi
[CL03].777The term Zariski lattice was coined in the paper by Coquand and
Lombardi. It allows one to prove another important property of
$\mathcal{L}_{R}$. The formalization of the Zariski lattice described in
[ZM23] adopts this approach to the setting of Cubical Agda, i.e. to a
dependent type theory with set-quotients but without impredicativity in the
form of propositional resizing.

Classically, the Zariski open sets of $\mathsf{Spec}(R)$ are in bijection with
the radical ideals of $R$. Recall that an ideal $I\subseteq R$ is called a
radical ideal if $I=\sqrt{I}$, where
$\sqrt{I}:\equiv\\{\,x:R\;|\;\exists_{n:\mathbb{N}}\leavevmode\nobreak\
x^{n}\in I\,\\}$. Predicatively, the type of ideals of
$R:\mathsf{CommRing}_{\ell}$ lives in $\mathsf{Type}_{\ell+1}$. So, even
though this gives us a point-free description of Zariski opens, it also
introduces size issues or requires us to assume resizing. Fortunately, the
situation is better behaved for (quasi-) compact opens. These are in bijection
with radicals of finitely generated ideals, i.e. ideals of the form
$\sqrt{\langle f_{1},...,f_{n}\rangle}$, where $f_{1},...,f_{n}:R$. Moreover,
union and intersection of (quasi-) compact opens, i.e. join and meet of
$\mathcal{L}_{R}$, correspond to addition and multiplication of finitely
generated ideals. In other words, we can define $\mathcal{L}_{R}$ as follows.

######  Definition 2.2.

The _Zariski lattice_ $\mathcal{L}_{R}$ of a ring $R$ has as elements lists of
generators $f_{1},...,f_{n}:R$ modulo taking the radical of the ideal
generated by the $f_{i}$. This means that lists of generators
$f_{1},...,f_{n}:R$ and $g_{1},...,g_{m}:R$ are in the same equivalence class
of $\mathcal{L}_{R}$, if ${\sqrt{\langle
f_{1},\dots,f_{n}\rangle}}={\sqrt{\langle g_{1},\dots,g_{m}\rangle}}$.888
Technically, the identity type $I=J$ of two (radical) ideals lives in
$\mathsf{Type}_{\ell+1}$, but in this particular instance we can replace it
with a small proposition, as ${\sqrt{\langle
f_{1},\dots,f_{n}\rangle}}={\sqrt{\langle g_{1},\dots,g_{m}\rangle}}$ is
equivalent to all the $f_{i}$ being in ${\sqrt{\langle
g_{1},\dots,g_{m}\rangle}}$ and vice versa. The equivalence class of the
generators $f_{1},...,f_{n}:R$ is denoted by
$D(f_{1},...,f_{n}):\mathcal{L}_{R}$. Join and meet are given by

$\displaystyle D(f_{1},...,f_{n})\vee D(g_{1},...,g_{m})$
$\displaystyle:\equiv D(f_{1},...,f_{n},g_{1},...,g_{m})$ $\displaystyle
D(f_{1},...,f_{n})\wedge D(g_{1},...,g_{m})$ $\displaystyle:\equiv
D(f_{1}g_{1},...,f_{i}g_{j},...,f_{n}g_{m})$

The map $D:R\to\mathcal{L}_{R}$, sending $f:R$ to $D(f)$, the equivalence
class of the radical of the principal ideal generated by $f$, $\sqrt{\langle
f\rangle}$, is a support. It is straightforward to show that $\mathcal{L}_{R}$
and $D$ thus defined, satisfy the universal property of the Zariski lattice.
However, we can also prove the following characterization of the induced order
on $\mathcal{L}_{R}$:

$\displaystyle D(f_{1},...,f_{n})\leq D(g_{1},...,g_{m})\leavevmode\nobreak\ $
$\displaystyle\Leftrightarrow\leavevmode\nobreak\ {\sqrt{\langle
f_{1},\dots,f_{n}\rangle}}\subseteq{\sqrt{\langle g_{1},\dots,g_{m}\rangle}}$
$\displaystyle\Leftrightarrow\leavevmode\nobreak\ f_{i}\in{\sqrt{\langle
g_{1},\dots,g_{m}\rangle}}\leavevmode\nobreak\ \text{for}\leavevmode\nobreak\
i=1,...,n$

This fact999This fact is called the “formal Hilbert Nullstellensatz” in
[CLS09]. and the universal property let us prove all the relevant properties
of the Zariski lattice without having to appeal to prime ideals.

If $\varphi:\mathsf{Hom}(A,B)$ is a morphism of rings,
$D\circ\varphi:A\to\mathcal{L}_{B}$ is a support and we get an induced
morphism between Zariski lattices

${A}$${\mathcal{L}_{A}}$${\mathcal{L}_{B}}$$\scriptstyle{D}$$\scriptstyle{D\circ\varphi}$$\scriptstyle{\exists!}$

which we will denote by $\varphi^{\mathcal{L}}$. Classically, this lattice
morphism takes pre-images of (quasi-) compact opens under the continuous map
$\mathsf{Spec}(B)\to\mathsf{Spec}(A)$ induced by $\varphi:\mathsf{Hom}(A,B)$.
For $f_{1},...,f_{n}:R$, we have
$\varphi^{\mathcal{L}}\big{(}D(f_{1},\dots,f_{n})\big{)}=D(\varphi(f_{1}),\dots,\varphi(f_{n}))$.

An important fact in classical algebraic geometry is that $D(f)$ (as a
subspace of $\mathsf{Spec}(R)$) is homeomorphic to
$\mathsf{Spec}(R[\nicefrac{{1}}{{f}}])$. The result carries over to the
Zariski lattice, giving a bijection between (quasi-) compact opens of the two
spaces. We want to finish this section on the Zariski lattice by giving a
point-free proof of this fact that only uses the universal property. The
result will be of importance later. For the remainder of this section we fix
an element $f:R$. Recall that the ring $R[\nicefrac{{1}}{{f}}]$ is a special
case of a localization of $R$ [AM69, Ch. 3].

######  Definition 2.3.

The _localization of_ $R$ _away from_ $f$ is the ring $R[\nicefrac{{1}}{{f}}]$
of fractions $\nicefrac{{r}}{{f^{n}}}$ where $r:R$ and the denominator is a
power of $f$. Equality of two fractions is given by:
${\nicefrac{{r}}{{f^{n}}}}={\nicefrac{{r^{\prime}}}{{f^{m}}}}$ if and only if
there merely exists a $k\geq 0$ such that ${rf^{k+m}}={r^{\prime}f^{k+n}}$.
The universal property of the localization away from $f$ can be stated as: For
any ring $A$ with a homomorphism $\varphi:\mathsf{Hom}(R,A)$ such that
$\varphi(f)\in A^{\times}$ (i.e. $\varphi(f)$ is a unit/invertible), there is
a unique $\psi:\mathsf{Hom}(R[\nicefrac{{1}}{{f}}],A)$ making the following
diagram commute

${R}$${R[\nicefrac{{1}}{{f}}]}$${A}$$\scriptstyle{\nicefrac{{\\_}}{{1}}}$$\scriptstyle{\varphi}$$\scriptstyle{\exists!\leavevmode\nobreak\
\psi}$

where $\nicefrac{{\\_}}{{1}}:\mathsf{Hom}(R,R[\nicefrac{{1}}{{f}}])$ is the
canonical morphism mapping $r:R$ to the fraction $\nicefrac{{r}}{{1}}$. In
other words, $R[\nicefrac{{1}}{{f}}]$ is the initial $R$-algebra where $f$
becomes invertible.

######  Lemma 2.4.

For $f:R$ we have an isomorphism of lattices
$\psi_{f}:\mathcal{L}_{R[\nicefrac{{1}}{{f}}]}\leavevmode\nobreak\
\cong\leavevmode\nobreak\ \downarrow\\!D(f)$ between the Zariski lattice of
the localization $R[\nicefrac{{1}}{{f}}]$ and the elements of
$\mathcal{L}_{R}$ below $D(f)$, i.e the down-set
$\downarrow\\!D(f):\equiv\leavevmode\nobreak\
{\\{\,u:\mathcal{L}_{R}\leavevmode\nobreak\ |\leavevmode\nobreak\ u\leq
D(f)\,\\}}$.

###### Proof.

Consider the map $d:R[\nicefrac{{1}}{{f}}]\to\,{\downarrow\\!{D(f)}}$ given by
$d(\nicefrac{{r}}{{f^{n}}}):\equiv\leavevmode\nobreak\ D(r)\wedge D(f)$. This
defines a support and thus induces
$\psi_{f}:\mathcal{L}_{R[\nicefrac{{1}}{{f}}]}\to\,{\downarrow\\!D(f)}$. For
the inverse direction take the support
$D(\nicefrac{{\\_}}{{1}}):R\to\mathcal{L}_{R[\nicefrac{{1}}{{f}}]}$ and the
induced map
$(\nicefrac{{\\_}}{{1}})^{\mathcal{L}}:\mathcal{L}_{R}\to\mathcal{L}_{R[\nicefrac{{1}}{{f}}]}$.
Restricting this to $\downarrow\\!D(f)$, gives us the inverse $\psi_{f}^{-1}$.
Note that this is indeed a lattice morphism, since the top element of
$\downarrow\\!D(f)$ is $D(f)$ and
$\psi_{f}^{-1}(D(f))=D(\nicefrac{{f}}{{1}})=D(\nicefrac{{1}}{{1}})$ as
$\nicefrac{{f}}{{1}}$ is a unit in $R[\nicefrac{{1}}{{f}}]$.

In order to prove that the two maps are inverse to each other, we claim that
the map $\\_\wedge D(f):\mathcal{L}_{R}\to\,{\downarrow\\!D(f)}$ factors
through $\psi_{f}$. In particular, we claim that the following diagram
commutes

${R}$${{R[\nicefrac{{1}}{{f}}]}}$${\mathcal{L}_{R}}$${{\mathcal{L}_{R[\nicefrac{{1}}{{f}}]}}}$${{\downarrow
D(f)}}$$\scriptstyle{d}$$\scriptstyle{(\nicefrac{{\\_}}{{1}})^{\mathcal{L}}}$$\scriptstyle{\psi_{f}}$$\scriptstyle{\\_\wedge
D(f)}$$\scriptstyle{D}$$\scriptstyle{\nicefrac{{\\_}}{{1}}}$$\scriptstyle{D}$

This follows from the universal property of $\mathcal{L}_{R}$, which gives a
unique $\phi:\mathcal{L}_{R}\to\,\downarrow\\!D(f)$, such that ${\phi\circ
D}={d(\nicefrac{{\\_}}{{1}})}$. But both $\\_\wedge D(f)$ and
$\psi_{f}\circ(\nicefrac{{\\_}}{{1}})^{\mathcal{L}}$ satisfy the same
commutativity condition as $\phi$, which implies that they have to be the same
lattice morphism. For $u\leq D(f)$ we therefore get
$\big{(}\psi_{f}\circ\psi_{f}^{-1}\big{)}(u)=u\wedge D(f)=u$.

For the converse direction, observe that $\psi_{f}^{-1}\circ
d=\psi_{f}^{-1}\circ\psi_{f}\circ D$ is a support. Consequently, there is a
unique morphism such that the following commutes:

${R[\nicefrac{{1}}{{f}}]}$${\mathcal{L}_{R[\nicefrac{{1}}{{f}}]}}$${\mathcal{L}_{R[\nicefrac{{1}}{{f}}]}}$$\scriptstyle{D}$$\scriptstyle{\psi_{f}^{-1}\circ
d\leavevmode\nobreak\ =\leavevmode\nobreak\ \psi_{f}^{-1}\circ\psi_{f}\circ
D}$$\scriptstyle{\exists!}$

Obviously, $\psi_{f}^{-1}\circ\psi_{f}$ satisfies this, but also the identity
morphism as

$\displaystyle\big{(}\psi_{f}\circ\psi_{f}^{-1}\big{)}\big{(}D(\nicefrac{{r}}{{f^{n}}})\big{)}=(\nicefrac{{\\_}}{{1}})^{\mathcal{L}}\big{(}D(rf)\big{)}=D(\nicefrac{{rf}}{{1}})=D(\nicefrac{{r}}{{f^{n}}})$

since $\nicefrac{{f}}{{1}}$ is a unit and $D$ is a support. This finishes the
proof that $\psi_{f}$ and $\psi_{f}^{-1}$ are inverse. ∎

##  3 Spectral schemes as locally ringed lattices

In the previous section we claimed that the Zariski lattice should be used as
the point-free, constructive spectrum of a ring. Much like in the classical
case, a ring is not determined by its Zariski lattice. Indeed, for any ring
$R$ we have
$\mathcal{L}_{R}\cong\mathcal{L}_{\nicefrac{{R}}{{\mathfrak{N}}}}$, where
$\mathfrak{N}=\sqrt{\langle 0\rangle}$ is the nilradical of $R$. In order to
recover the original ring, one needs to equip the Zariski spectrum or lattice
with its _structure sheaf_. This construction was used as the point of
departure by Coquand, Lombardi and Schuster to develop “Spectral Schemes as
Ringed Lattices” [CLS09]. If one wants to recover ring morphisms from their
action on Zariski lattice and structure sheaf, one needs to introduce some
additional structure making the constructive spectrum a locally ringed
lattice. In this section we want to redevelop key results of [CLS09] for
“spectral schemes” as _locally_ ringed lattices. This gives a rather neat and
point-free account of these spectral schemes. From a classical perspective
these are really just qcqs-schemes, as we will see at the end of this section.
In particular, this lets us relate the lattice theoretic approach to schemes
with the functor of points approach, as we will show in this paper.

###  3.1 From ringed lattices to locally ringed lattices

Let us begin by repeating the definition of a ringed lattice as given by
Coquand, Lombardi and Schuster [CLS09].

######  Definition 3.1.

Let $L$ be a distributive lattice and $\mathcal{F}:L^{op}\to\mathsf{CommRing}$
a ring-valued presheaf on $L$ (seen as a poset category). We say that
$\mathcal{F}$ is a sheaf if for all $x,u_{1},\dots,u_{n}:L$ with
$x=\textstyle\bigvee_{i=1}^{n}u_{i}$ we get a canonical equalizer diagram

$\displaystyle\mathcal{F}(x)\to\prod_{i=1}^{n}\mathcal{F}(u_{i})\rightrightarrows\prod_{i,j}\mathcal{F}(u_{i}\wedge
u_{j})$

A _ringed lattice lattice_ is a distributive lattice with a sheaf of rings.
Given ringed lattices $(L,\mathcal{F})$ and $(M,\mathcal{G})$, a morphism of
ringed lattices $\pi:(L,\mathcal{F})\to(M,\mathcal{G})$ is a pair
$\pi:\equiv(\pi^{*},\pi^{\sharp})$ consisting of a lattice homomorphism
$\pi^{*}:L\to M$ and a natural transformation
$\pi^{\sharp}:{\mathcal{F}}\Rightarrow{\pi_{*}\mathcal{G}}$, where
$\pi_{*}\mathcal{G}:L^{op}\to\mathsf{CommRing}$ is the sheaf defined by
$\pi_{*}\mathcal{G}(u):\equiv\mathcal{G}(\pi^{*}(u))$. The category of ringed
lattices and their morphisms is denoted $\mathsf{RDL}$.

The motivation for this definition is based on the classical fact that
distributive lattices correspond to the compact open subsets of so-called
coherent or spectral spaces. An in-depth discussion is included in Section
3.4. Building on the definition of ringed lattice, and with the correspondence
to ringed spectral spaces in mind, the question arises whether one can define
locally ringed lattices corresponding to locally ringed spectral spaces
without appealing to point-set topology or the notion of stalk of a sheaf.

In the context of formal topology, it was observed by Schuster [Sch08] that
sheaves of local rings can be characterized in a point-free way by using
supports and a second notion, which we will call invertibility suprema or
invertibility opens. The notion of invertibility opens was used by Hakim
[Hak72, Sec. III.2] to define locally ringed _topoi_. We want to apply these
notions to ringed lattices, following a suggestion by Thierry Coquand. Coquand
observed that one can always define an “invertibility support” on a spectral
scheme and use it to characterize local morphisms. We will discuss why this
works classically in Section 3.4.

######  Definition 3.2.

Let $P$ be a poset and $\mathcal{F}:P^{op}\to\mathsf{CommRing}$ a ring-valued
presheaf. For an object $u:P$ and a section $s:\mathcal{F}(u)$, an element
$u_{s}\leq u$ is called an _invertibility supremum_ of $s$, if for all $w\leq
u$ we have that

$\displaystyle w\leq u_{s}\quad\Leftrightarrow\quad
s\\!\\!\restriction_{w}\leavevmode\nobreak\ \in\leavevmode\nobreak\
\mathcal{F}(w)^{\times}$

In other words, $u_{s}$ is the largest element smaller than $u$ where the
restriction of $s$ becomes invertible.

A dependent function
$\mathcal{D}:(u:P)\to\mathcal{F}(u)\to\leavevmode\nobreak\ \downarrow\\!u$, is
called an _invertibility map_ if $\mathcal{D}_{u}(s)$ is an invertibility
supremum of $s$ for all $u:P$ and $s:\mathcal{F}(u)$.

######  Remark 3.3.

If $u_{s}$ is an invertibility supremum of $s:\mathcal{F}(u)$, for $u:P$, then
clearly $s\\!\\!\restriction_{u_{s}}\in\mathcal{F}(u_{s})^{\times}$. In
particular, by anti-symmetry, invertibility suprema are uniquely determined if
they exist and we will henceforth speak of _the_ invertibility supremum of
$s$. In univalent terms, the type of invertibility suprema of $u$ and $s$ is a
proposition. It follows that for a poset $P$ and presheaf $\mathcal{F}$, the
type of invertibility maps is a proposition as well.

######  Definition 3.4.

A _locally ringed lattice_ is a distributive lattice $L$ with a sheaf of rings
$\mathcal{F}$ and an invertibility map
$\mathcal{D}:(u:L)\to\mathcal{F}(u)\to\leavevmode\nobreak\ \downarrow\\!u$,
such that $\mathcal{D}_{u}$ is a support for all $u:L$. We call $\mathcal{D}$
the _invertibility support_ on $(L,\mathcal{F})$.

A morphism of locally ringed lattices is a morphism of ringed lattices
$\pi:\equiv(\pi^{*},\pi^{\sharp}):(L,\mathcal{F})\to(M,\mathcal{G})$ such that
for all $u:L$ and $s:\mathcal{F}(u)$:

$\displaystyle\pi^{*}\big{(}\mathcal{D}_{u}(s)\big{)}\;=\;\mathcal{D}_{\pi^{*}(u)}(\pi^{\sharp}(s))$

The category of locally ringed distributive lattices will be denoted by LRDL.

######  Remark 3.5.

Although invertibility supports are given as additional structure on ringed
lattices, we will write locally ringed lattices as pairs $(L,\mathcal{F})$ and
always denote the implicit invertibility support by $\mathcal{D}$. It will
always be clear from context which locally ringed lattice an invertibility
support corresponds to. This notation is motivated by the fact that
invertibility supports are uniquely determined (if they exist), as explained
in Remark 3.3.

######  Remark 3.6.

If $\pi:(L,\mathcal{F})\to(M,\mathcal{G})$ is a morphism of ringed lattices,
then for $u:L$ and $s:\mathcal{F}(u)$ one always has
$\pi^{*}\big{(}\mathcal{D}_{u}(s)\big{)}\leq\mathcal{D}_{\pi^{*}(u)}(\pi^{\sharp}(s))$,
as by the naturality of $\pi^{\sharp}$:

$\displaystyle\pi^{\sharp}(s)\\!\\!\restriction_{\pi^{*}(\mathcal{D}_{u}(s))}=\pi^{\sharp}\big{(}s\\!\\!\restriction_{\mathcal{D}_{u}(s)}\big{)}\leavevmode\nobreak\
\in\leavevmode\nobreak\
\mathcal{G}\big{(}\pi^{*}(\mathcal{D}_{u}(s))\big{)}^{\times}$

$\pi$ is thus a morphism of locally ringed lattices if and only if the
converse inequality holds for all $u$ and $s$.

Nothing in the definition of locally ringed lattices depends on univalent
features and the notion can and should be studied in other settings than
HoTT/UF, such as Bishop-style constructive mathematics. What is, however,
important for our purposes, is that it is a structurally well-behaved notion
in the sense that for locally ringed lattices “isomorphisms are equalities”.
This will actually be a key fact in the proof of our main comparison theorem.

######  Proposition 3.7.

$\mathsf{LRDL}$ is a univalent category.

###### Proof.

Instead of proving that locally ringed lattices and their isomorphisms are a
“standard notion of structure” [Uni13, Def. 9.8.1] directly, it is easier to
use a “displayed” approach [AL19, vBB21].101010 The agda/cubical-library uses
the approach of [vBB21] and supports some automation for proving that
structures are univalent. An earlier version described in [ACMZ21] was based
on [Esc22] that also has a modular approach to building univalent structures,
albeit not a displayed one. Formalizing locally ringed lattices and proving
them univalent could figure as an interesting test case for the proof
automation tools, as it involves two layers of displayedness. It is not hard
to show that bounded distributive lattices with lattice morphisms form a
univalent category and lattice sheaves with natural transformations form a
univalent displayed category on lattices. Finally, invertibility supports,
with their canonical notion of (displayed) morphism being exactly that of a
morphism of locally ringed lattices, form a univalent displayed category on
ringed lattices. ∎

######  Corollary 3.8.

The forgetful functor $\mathcal{U}$ from locally ringed lattices to ringed
lattices reflects isomorphisms.

###### Proof.

Since the type of invertibility supports over a ringed lattice is a
proposition, the structure identity principle implies that both of the
canonical maps $X=Y\to X\cong_{\mathsf{LRDL}}Y$ and
$X=Y\to\mathcal{U}(X)\cong_{\mathsf{RDL}}\mathcal{U}(Y)$ are equivalences for
$X,Y:\mathsf{LRDL}$. ∎

######  Example 3.9.

The main example of a locally ringed lattice will of course be the
“constructive spectrum” of a ring. For $R:\mathsf{CommRing}$ we can equip the
Zariski lattice $\mathcal{L}_{R}$ with its structure sheaf $\mathcal{O}_{R}$.
The structure sheaf is defined on basic opens and then lifted to the entire
Zariski lattice. The basic opens as a subset
$\mathcal{B}_{R}:\equiv\\{u:\mathcal{L}_{R}\leavevmode\nobreak\
|\leavevmode\nobreak\ \exists_{f:R}\leavevmode\nobreak\
u=D(f)\\}\subseteq\mathcal{L}_{R}$ form a basis of the Zariski lattice in the
sense that for every $u:\mathcal{L}_{R}$ there merely exist
$b_{1},...,b_{n}:\mathcal{B}_{R}$ such that $u=\bigvee_{i=1}^{n}b_{i}$.111111
As $\mathcal{L}_{R}$ is defined as a quotient, we know that merely
$u=D(f_{1},...,f_{n})=\bigvee_{i=1}^{n}D(f_{i})$. By the _comparison lemma for
distributive lattices_ [CLS09, Lemma 1]121212 This is a special case of the
general comparison lemma for sites [MLM12, Cor. 3, p. 590]. The lattice case
is formalized in Cubical Agda and can be found in:
https://github.com/agda/cubical/blob/master/Cubical/Categories/DistLatticeSheaf/ComparisonLemma.agda.
there is an equivalence of categories between sheaves on $\mathcal{L}_{R}$ and
sheaves on the basis $\mathcal{B}_{R}$. Here, sheaves on a basis of a
distributive lattice are defined completely analogously to Definition 3.1 and
morphisms of sheaves are just natural transformations. Given a sheaf
$\mathcal{F}$ on $\mathcal{B}_{R}$, the equivalence of the comparison lemma
maps this to a sheaf on $\mathcal{L}_{R}$ by taking the _right Kan extension_
$\mathsf{Ran}(\mathcal{F})$ along the basis inclusion.

As was shown in the Cubical Agda formalization of the structure sheaf
described in [ZM23], we can use univalence to define the structure sheaf on
basic opens by mapping $D(f)\mapsto R[\nicefrac{{1}}{{f}}]$.131313 In [CLS09,
Sec. 2.3], the structure sheaf on basic opens is defined using localization at
the saturation $S_{f}=\\{g\,|\,D(f)\leq D(g)\,\\}$. In this paper we do not
want to get into the details of how the structure sheaf is defined and just
work with a sheaf
$\mathcal{O}_{R}:(\mathcal{L}_{R})^{op}\to\mathsf{CommRing}$, such that
$\mathcal{O}_{R}(D(f))\cong R[\nicefrac{{1}}{{f}}]$ canonically. This means
that these isomorphisms satisfy all of the expected functoriality and
naturality conditions. Note however, that definitions and proofs appealing to
the canonical isomorphism need to be rephrased to accommodate for the formal
definition of the structure sheaf, before becoming formalizable themselves.

Observe that in any locally ringed lattice one has
$w\wedge\mathcal{D}_{u}(s)\leavevmode\nobreak\ =\leavevmode\nobreak\
\mathcal{D}_{w}(s\\!\\!\restriction_{w})$, for $w\leq u$ and thus for joins we
must have

$\displaystyle\mathcal{D}_{u_{1}\vee\dots\vee u_{n}}(s)\leavevmode\nobreak\
=\leavevmode\nobreak\
\textstyle\bigvee_{i=1}^{n}\mathcal{D}_{u_{i}}(s\\!\\!\restriction_{u_{i}})$

In order to define an invertibility support on
$(\mathcal{L}_{R},\mathcal{O}_{R})$, it is thus sufficient to define
$\mathcal{D}$ on the basic opens. Modulo the canonical isomorphism we can set:

$\displaystyle\mathcal{D}_{D(f)}(\nicefrac{{r}}{{f^{n}}})\leavevmode\nobreak\
:\equiv\leavevmode\nobreak\ D(fr)\quad(=D(f)\wedge D(r))$

Indeed, this gives us the invertibility supremum, since
$R[\nicefrac{{1}}{{fr}}]\cong{R[\nicefrac{{1}}{{f}}][\nicefrac{{1}}{{r}}]}$ is
the initial $R[\nicefrac{{1}}{{f}}]$-algebra where $\nicefrac{{r}}{{1}}$
becomes invertible.141414Note that $\mathcal{D}_{D(f)}$ is the support $d$ in
the proof of Lemma 2.4. For arbitrary elements of the Zariski lattice we can
then set:

$\displaystyle\mathcal{D}_{D(f_{1},\dots,f_{n})}(s)\leavevmode\nobreak\
:\equiv\leavevmode\nobreak\
\textstyle\bigvee_{i=1}^{n}\mathcal{D}_{D(f_{i})}(s\\!\\!\restriction_{D(f_{i})})$

By the above remark, this gives us an invertibility map.151515The well-
definedness of this construction follows from the fact that the type of
invertibility maps is a proposition. To check the support conditions we can
again restrict our attention to basic opens where everything follows the fact
that $D$ is a support. Note that $\mathcal{D}_{D(1)}=D$ modulo the canonical
$\mathcal{O}_{R}(D(1))\cong R$.

###  3.2 Universal property

In classical algebraic geometry, the following proposition is sometimes called
the “universal property of schemes”:

> _The functor Spec is left-adjoint to the global sections functor $\Gamma$
> and the unit of this adjunction is an isomorphism._

This is of course already true when regarding Spec as a functor from rings to
locally ringed spaces [DG71, Prop 1.6.3], Schuster [Sch08] gives a
constructive proof of a point-free version of this statement using formal
topology.161616 Curiously, previous proofs in the literature, such as the one
given by Johnstone in “Stone Spaces” [Joh82, V.3.5], appeal to classical
reasoning by using the points of Spec, even if the Zariski spectrum is defined
in a point-free way. We want to show the corresponding statement for locally
ringed lattices.

Let us start by addressing the issue of variance that arises when the spectrum
functor Spec is introduced as a contra-variant functor from rings to locally
ringed spaces. This makes the direction of the adjunction somewhat arbitrary.
In the functorial setting of Proposition 4.6 it is more natural to think of
the spectrum functor as the right adjoint. In order to match this we will thus
work in opposite categories $\mathsf{CommRing}^{op}$ and $\mathsf{LRDL}^{op}$.

This actually makes a lot of sense for morphisms locally ringed lattices. As
is explained in Section 3.4, readers familiar with classical algebraic
geometry should think of a locally ringed lattice $(L_{X},\mathcal{O}_{X})$ as
a so-called spectral space $X$ with a sheaf of rings that is local on the
stalks. The lattice $L_{X}$ is the lattice of compact open subsets of $X$. A
spectral morphism of suitable locally ringed spectral spaces $f:X\to Y$
induces a lattice morphism $f^{*}:L_{Y}\to L_{X}$, by taking the pre-image of
compact opens of $Y$ (spectral morphism means that pre-images of compact opens
are compact open).

For an object in $X:\mathsf{LRDL}^{op}$ we denote its lattice by $L_{X}$ and
its sheaf by $\mathcal{O}_{X}$. A morphism
$\pi:\mathsf{LRDL}^{op}\big{(}X,Y\big{)}$ is given by the lattice morphism
$\pi^{*}:L_{Y}\to L_{X}$, similar to how a morphism of locales is given by a
frame homomorphism in the opposite direction, and the natural transformation
$\pi^{\sharp}:{\mathcal{O}_{Y}}\Rightarrow{\pi_{*}\mathcal{O}_{X}}$.

######  Definition 3.10.

The _global sections functor_
$\Gamma:\mathsf{LRDL}^{op}\to\mathsf{CommRing}^{op}$ is defined on objects by
$\Gamma(L_{X},\mathcal{O}_{X}):\equiv\mathcal{O}_{X}(1)$ and on morphisms
$\pi:\mathsf{LRDL}^{op}\big{(}X,Y\big{)}$ by
$\Gamma(\pi):\equiv\pi^{\sharp}_{1}$ modulo the identification
$\mathcal{O}_{X}(\pi^{*}(1))=\mathcal{O}_{X}(1)$.

######  Definition 3.11.

The functor $\mathsf{Spec}:\mathsf{CommRing}^{op}\to\mathsf{LRDL}^{op}$ is
defined on objects by
$\mathsf{Spec}(R):\equiv(\mathcal{L}_{R},\mathcal{O}_{R})$ as described in
Example 3.9. For a ring morphism $\varphi:\mathsf{Hom}(R,A)$, we set
$\mathsf{Spec}(\varphi)^{*}:\equiv\varphi^{\mathcal{L}}:\mathcal{L}_{R}\to\mathcal{L}_{A}$.
To define the natural transformation $\mathsf{Spec}(\varphi)^{\sharp}$, we
only have to define it on basic opens. For $f:R$, we set modulo the canonical
isomorphisms $\mathcal{O}_{R}(D(f))\cong R[\nicefrac{{1}}{{f}}]$ and
$\mathcal{O}_{A}(\varphi^{\mathcal{L}}(D(f)))=\mathcal{O}_{A}(D(\varphi(f)))\cong
A[\nicefrac{{1}}{{\varphi(f)}}]$

${R}$${R[\nicefrac{{1}}{{f}}]}$${A[\nicefrac{{1}}{{\varphi(f)}}]}$$\scriptstyle{\nicefrac{{\\_}}{{1}}}$$\scriptstyle{\nicefrac{{\varphi(\\_)}}{{1}}}$$\scriptstyle{\exists!\leavevmode\nobreak\
\mathsf{Spec}(\varphi)^{\sharp}}$

One easily checks that this defines a morphism of locally ringed lattices.

######  Theorem 3.12.

Spec is right adjoint to $\Gamma$ and the counit of this adjunction is an
isomorphism.

###### Proof.

Given a commutative ring $R$ and a locally ringed lattice
$X:\equiv(L_{X},\mathcal{O}_{X})$, there is a canonical function

$\displaystyle\mathsf{CommRing}^{op}\big{(}\mathcal{O}_{X}(1),R\big{)}\to\mathsf{LRDL}^{op}\big{(}X,\mathsf{Spec}(R)\big{)}$

Let $\varphi:\mathsf{Hom}(R,\mathcal{O}_{L}(1))$ be a ring homomorphism. Note
that $\mathcal{D}_{1}\circ\,\varphi:R\to L_{X}$ is a support. This induces a
lattice homomorphism

${R}$${\mathcal{L}_{R}}$${L}$$\scriptstyle{D}$$\scriptstyle{\mathcal{D}_{1}\circ\,\varphi}$$\scriptstyle{\exists!\leavevmode\nobreak\
\pi^{*}}$

Furthermore, for every $f:R$ we get a map

${R}$${R[\nicefrac{{1}}{{f}}]}$${\mathcal{O}_{L}\big{(}\underbrace{\mathcal{D}_{1}(\varphi(f))}_{=\leavevmode\nobreak\
\pi^{*}(D(f))}\big{)}}$$\scriptstyle{\varphi(\\_)\,\,\\!\\!\restriction_{\mathcal{D}_{1}(\varphi(f))}}$$\scriptstyle{\exists!\leavevmode\nobreak\
\pi^{\sharp}}$

This defines a natural transformation between sheaves on basic opens and thus
on $\mathcal{L}_{R}$ by the comparison lemma for distributive lattices. It
remains to check that this defines a morphism of locally ringed lattices. Note
that on global sections we have by the definition of $\pi^{*}$ and
$\pi^{\sharp}$ that

$\displaystyle\pi^{*}\big{(}D(f)\big{)}\leavevmode\nobreak\
=\leavevmode\nobreak\ \mathcal{D}_{1}(\varphi(f))\leavevmode\nobreak\
=\leavevmode\nobreak\ \mathcal{D}_{\pi^{*}(D(1))}(\pi^{\sharp}(f))$

modulo identifying $\mathcal{O}_{R}(D(1))$ with $R$. Thus on arbitrary basic
opens, we have

$\displaystyle\pi^{*}\big{(}\mathcal{D}_{D(f)}(\nicefrac{{r}}{{f^{n}}})\big{)}\leavevmode\nobreak\
$ $\displaystyle=\leavevmode\nobreak\ \mathcal{D}_{1}(\pi^{\sharp}(rf))$
$\displaystyle=\leavevmode\nobreak\
\mathcal{D}_{1}(\pi^{\sharp}(r))\wedge\mathcal{D}_{1}(\pi^{\sharp}(f))\leavevmode\nobreak\
=\leavevmode\nobreak\
\mathcal{D}_{\mathcal{D}_{1}(\pi^{\sharp}(f))}(\pi^{\sharp}(\nicefrac{{r}}{{f^{n}}}))$

and finally on arbitrary elements

$\displaystyle\pi\big{(}\mathcal{D}_{D(f_{1})\vee\dots\vee
D(f_{n})}(s)\big{)}\leavevmode\nobreak\ $ $\displaystyle=\leavevmode\nobreak\
\textstyle\bigvee_{i=1}^{n}\mathcal{D}_{\pi(D(f_{i}))}(\pi^{\sharp}(s)\restriction_{\pi(D(f_{i}))})$
$\displaystyle=\leavevmode\nobreak\ \mathcal{D}_{\pi(D(f_{1})\vee\dots\vee
D(f_{n}))}(\pi^{\sharp}(s))$

Note that the action of $\mathsf{Spec}$ on morphisms is essentially the same
construction. We omit the computations for showing that this is natural in
both $R$ and $X$.

The inverse of this map is given by $\Gamma$. Indeed, it follows directly that
for a ring morphism $\varphi:\mathsf{Hom}(R,\mathcal{O}_{L}(1))$ one has
$\varphi=\pi^{\sharp}$ on global sections. For the other direction fix a
morphism $\pi:\mathsf{LRDL}^{op}\big{(}X,\mathsf{Spec}(R)\big{)}$ and observe
that the following diagram commutes for $\pi^{\sharp}$ at global sections.

${R}$${\mathcal{L}_{R}}$${L_{X}}$$\scriptstyle{D}$$\scriptstyle{\mathcal{D}_{1}\circ\,\pi^{\sharp}}$$\scriptstyle{\pi^{*}}$

as well as for $f:R$

${R}$${R[\nicefrac{{1}}{{f}}]}$${\mathcal{O}_{L}\big{(}\pi(D(f))\big{)}}$$\scriptstyle{\pi^{\sharp}(\\_)\restriction_{\mathcal{D}_{1}(\pi^{\sharp}(f))}}$$\scriptstyle{\pi^{\sharp}}$

This shows that $\pi$ is just the morphism obtained from applying the
adjunction map to $\pi^{\sharp}$ at global sections. From this we also get
that the counit is an isomorphism. Indeed, for a ring $R$ it is the canonical
isomorphism ${R}\cong\mathcal{O}_{R}(D(1))$. ∎

######  Corollary 3.13.

Spec is fully faithful.

###  3.3 Spectral schemes

Let $X$ be a locally ringed lattice and $R:\equiv\mathcal{O}_{X}(1)$ be the
ring of global sections. We saw that the counit of the adjunction of Theorem
3.12 is an isomorphism. But what about its unit? Following the proof of
Theorem 3.12 for the identity on $R$, we see that the lattice homomorphism is
induced by

${R}$${\mathcal{L}_{R}}$${L_{X}}$$\scriptstyle{D}$$\scriptstyle{\mathcal{D}_{1}}$$\scriptstyle{\exists!\leavevmode\nobreak\
\eta^{*}_{X}}$

and the natural transformation
$\eta^{\sharp}_{X}:\mathcal{O}_{R}\to(\eta_{X})_{*}\mathcal{O}_{X}$ is given
on a basic open $D(f)$, $f:R$, by

${R}$${R[\nicefrac{{1}}{{f}}]}$${\mathcal{O}_{X}\big{(}\underbrace{\mathcal{D}_{1}(f)}_{=\leavevmode\nobreak\
\eta^{*}_{X}(D(f))}\big{)}}$$\scriptstyle{\\_\restriction_{\mathcal{D}_{1}(f)}}$$\scriptstyle{\exists!\leavevmode\nobreak\
\eta^{\sharp}_{X}}$

######  Definition 3.14.

$X$ is an _affine scheme_ , if $\eta_{X}$ is an isomorphism of locally ringed
lattices.

######  Lemma 3.15.

$\mathsf{Spec}(R)$ is affine.

######  Lemma 3.16.

$X$ is affine if and only if there exists a ring $A$ such that
$X\cong\mathsf{Spec}(A)$ as locally ringed lattices.

###### Proof.

Spec is fully faithful. ∎

######  Remark 3.17.

The advantage of Definition 3.14, compared to characterizing affine schemes by
the equivalent statement of Lemma 3.16, is that the latter is a “big”
proposition living in the next higher universe as it quantifies over the type
of all rings.

For a locally ringed lattice $X$ and $u:L_{X}$, we get a locally ringed
lattice $X\\!\\!\restriction_{u}:\equiv(\downarrow\\!u,\leavevmode\nobreak\
\mathcal{O}_{X}\\!\\!\restriction_{\downarrow u})$ of elements below $u$ with
the sheaf $\mathcal{O}_{X}$ restricted to those elements. The lattice morphism
$\\_\wedge u:L_{X}\to\,\downarrow\\!u$ induces a map
$\mathsf{LRDL}^{op}\big{(}X\\!\\!\restriction_{u},X\big{)}$, which we think of
as the “inclusion” of the compact open $u$ into $X$.

######  Definition 3.18.

$X$ is a _qcqs-scheme_ , if there merely exist $u_{1},\dots,u_{n}:L_{X}$,
which cover $X$ in the sense that $1=u_{1}\vee\dots\vee u_{n}$ and such that
$X\\!\\!\restriction_{u_{i}}$ is affine for all $i$ in $1,...,n$.

######  Example 3.19.

Let us discuss the standard example of a qcqs-scheme that is not affine: The
plane without the origin $\mathbb{A}^{2}\setminus\\{0\\}$ over some fixed
field $k$. Classically, the points of $\mathbb{A}^{2}\setminus\\{0\\}$
correspond to $D(x,y)\subseteq\mathsf{Spec}\big{(}k[x,y]\big{)}$. The goal is
thus to prove that
$\mathsf{Spec}\big{(}k[x,y]\big{)}\\!\\!\restriction_{D(x,y)}$ is not affine,
where $D(x,y):\mathcal{L}_{k[x,y]}$. By the sheaf property of the structure
sheaf, we get the following pullback square

${\mathcal{O}_{k[x,y]}(D(x,y))}$${k[x,y,y^{-1}]}$${k[x,y,x^{-1}]}$${k[x,y,x^{-1},y^{-1}]}$

$\lrcorner$

Since this is a pullback of integral domains we can identify
$\mathcal{O}_{k[x,y]}\big{(}D(x,y)\big{)}$ with the subring $k[x,y,x^{-1}]\cap
k[x,y,y^{-1}]\subseteq k[x,y,x^{-1},y^{-1}]$. One can show that this already
gives us a unique isomorphism of $k$-algebras
$k[x,y]\cong\mathcal{O}_{k[x,y]}\big{(}D(x,y)\big{)}$. If
$\mathsf{Spec}\big{(}k[x,y]\big{)}\\!\\!\restriction_{D(x,y)}$ was affine we
would get an isomorphism of lattices

${k[x,y]}$${\mathcal{L}_{k[x,y]}}$${\downarrow
D(x,y)}$$\scriptstyle{D}$$\scriptstyle{(D(x)\vee D(y))\leavevmode\nobreak\
\wedge\leavevmode\nobreak\
D(\\_)}$$\scriptstyle{\exists!}$$\scriptstyle{\simeq}$

This morphism has to be $D(x,y)\wedge\\_$, which is not an isomorphism, giving
the desired contradiction.

It was already shown in [CLS09] that qcqs-schemes are obtained by “gluing”
together affine schemes. For a cover $u_{1},...,u_{n}$ of $X$ we can glue
along the corresponding “inclusions” $X\\!\\!\restriction_{u_{i}}\to X$ to
recover $X$. This was shown for ringed lattices in [CLS09, Lemma 2], but the
proof extends directly to locally ringed lattices. We thus give the following
proposition without proof.

######  Proposition 3.20.

If $X$ is a qcqs-scheme and $u_{1},...,u_{n}:L_{X}$ an (affine) cover of $X$,
then

$\displaystyle X\leavevmode\nobreak\ \cong\leavevmode\nobreak\
\mathsf{colim}\,\big{\\{}X\\!\\!\restriction_{u_{i}}\leftarrow
X\\!\\!\restriction_{u_{i}\wedge u_{j}}\rightarrow
X\\!\\!\restriction_{u_{j}}\big{\\}}$

in the opposite category of locally ringed lattices $\mathsf{LRDL}^{op}$. In
particular, if we have $X\\!\\!\restriction_{u_{i}}\cong\mathsf{Spec}(A_{i})$,
and we are given affine covers $\big{(}v_{ijk}:\leavevmode\nobreak\
\downarrow\\!(u_{i}\wedge u_{j})\big{)}_{k}$ of the subschemes
$X\\!\\!\restriction_{u_{i}\wedge u_{j}}$ with
$X\\!\\!\restriction_{v_{ijk}}\cong\mathsf{Spec}(A_{ijk})$, we have

$\displaystyle X\leavevmode\nobreak\ \cong\leavevmode\nobreak\
\mathsf{colim}\,\big{\\{}\mathsf{Spec}(A_{i})\leftarrow\mathsf{Spec}(A_{ijk})\rightarrow\mathsf{Spec}(A_{j})\big{\\}}$

######  Corollary 3.21.

Let $X$ be a qcqs-scheme, then
$\mathcal{O}_{X}\big{(}\mathcal{D}_{u}(s)\big{)}\cong\mathcal{O}_{X}(u)[\nicefrac{{1}}{{s}}]$,
for any $u:L_{X}$ and $s:\mathcal{O}_{X}(u)$.171717This is also known as the
“Qcqs-Lemma” in “The Rising Sea” [Vak24].

We conclude this section on our first definition of qcqs-schemes by showing
that the notion of morphism of spectral schemes given in [CLS09, Def. 16]
coincides with morphisms of locally ringed lattices.

######  Definition 3.22.

Let $X:\equiv(L_{X},\mathcal{O}_{X})$ and $Y:\equiv(L_{Y},\mathcal{O}_{Y})$ be
two qcqs-schemes, a morphism of _ringed_ lattices
$\pi:\mathsf{RDL}^{op}\big{(}X,Y\big{)}$ is called _locally affine_ if there
are affine covers $u_{1},\dots,u_{n}$ of $L_{X}$ and $w_{1},\dots,w_{m}$ of
$L_{Y}$ respectively, which are compatible in the following way: For every
$u_{i}$ exists a $w_{j}$ with $u_{i}\leq\pi^{*}(w_{j})$ such that the morphism
of ringed lattices
$\pi\\!\\!\restriction_{u_{i}}:\mathsf{RDL}^{op}\big{(}X\\!\\!\restriction_{u_{i}},Y\\!\\!\restriction_{w_{j}}\\!\\!\big{)}$,
which is induced by the lattice morphism $\pi^{*}(\\_)\wedge
u_{i}:\,\downarrow\\!w_{j}\to\,\downarrow\\!u_{i}$, is just $\mathsf{Spec}$
applied to the ring morphism
$\pi^{\sharp}\\!\\!\restriction_{u_{i}}:\mathcal{O}_{Y}(w_{j})\to\mathcal{O}_{X}(u_{i})$,
i.e. the following diagram commutes:

${{X\\!\\!\restriction_{u_{i}}}}$${{Y\\!\\!\restriction_{w_{j}}}}$${{\mathsf{Spec}\big{(}\mathcal{O}_{X}(u_{i})\big{)}}}$${{\mathsf{Spec}\big{(}\mathcal{O}_{Y}(w_{j})\big{)}}}$$\scriptstyle{\pi\,\\!\\!\restriction_{u_{i}}}$$\scriptstyle{\eta_{X\\!\\!\restriction_{u_{i}}}}$$\scriptstyle{\mathbin{\text{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\simeq$}}}}$$\scriptstyle{\eta_{Y\\!\\!\restriction_{w_{j}}}}$$\scriptstyle{\mathbin{\text{\rotatebox[origin={c}]{90.0}{$\scriptstyle\simeq$}}}}$$\scriptstyle{\mathsf{Spec}(\pi^{\sharp}\,\\!\\!\restriction_{u_{i}})}$

######  Remark 3.23.

Since $\mathsf{Spec}$ is fully-faithful, a morphism
$\pi:\mathsf{RDL}^{op}\big{(}X,Y\big{)}$ is locally affine if and only 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 $u_{i}\leq\pi^{*}(w_{j})$ the
induced morphism
$\pi\\!\\!\restriction_{u_{i}}:\mathsf{RDL}^{op}\big{(}X\\!\\!\restriction_{u_{i}},Y\\!\\!\restriction_{w_{j}}\\!\\!\big{)}$
is a morphism of locally ringed lattices.

######  Lemma 3.24.

Let $X$ and $Y$ be two qcqs-schemes, then any morphism of ringed lattices
$\pi:\mathsf{RDL}^{op}\big{(}X,Y\big{)}$ is locally affine if and only if it
is a morphism of locally ringed lattices.

###### Proof.

First, assume that $(\pi^{*},\pi^{\sharp})$ is a morphism of locally ringed
lattices. take affine covers $u_{1},\dots,u_{n}$ of $L_{X}$ and
$w_{1},\dots,w_{m}$ of $L_{Y}$. We can refine the $u_{i}$’s to a compatible
cover in the following way. For each $i$ and $j$ take a cover
$\pi^{*}(w_{j})\wedge u_{i}=\bigvee_{k}\mathcal{D}_{u_{i}}(s_{ijk})$. Such a
cover exists because $u_{i}$ is affine and all $\mathcal{D}_{u_{i}}(s_{ijk})$
are affine as well, i.e.
$X\\!\\!\restriction_{\mathcal{D}_{u_{i}}(s_{ijk})}=\mathsf{Spec}(\mathcal{O}_{X}(u_{i})[\nicefrac{{1}}{{s_{ijk}}}])$.
Then $1_{L_{X}}=\bigvee_{i,j,k}\mathcal{D}_{u_{i}}(s_{ijk})$, with
$\mathcal{D}_{u_{i}}(s_{ijk})\leq\pi^{*}(w_{j})$ and the induced/restricted
morphism $X\\!\\!\restriction_{\mathcal{D}_{u_{i}}(s_{ijk})}\to
Y\\!\\!\restriction_{w_{j}}$ is one of locally ringed lattices, hence affine.

Now, assume that we have compatible covers $u_{1},\dots,u_{n}$ of $L_{X}$ and
$w_{1},\dots,w_{m}$ of $L_{Y}$, with $u_{i}\leq\pi^{*}(w_{j})$ such that
$\pi\\!\\!\restriction_{u_{i}}:\mathsf{RDL}^{op}\big{(}X\\!\\!\restriction_{u_{i}},Y\\!\\!\restriction_{w_{j}}\\!\\!\big{)}$
is actually a morphism of locally ringed lattices. This means that for $v\leq
w_{j}$ and $s:\mathcal{O}_{Y}(v)$ we have

$\displaystyle
u_{i}\wedge\pi^{*}\big{(}\mathcal{D}_{v}(s)\big{)}=\mathcal{D}_{u_{i}\wedge\pi^{*}(v)}(\pi^{\sharp}(s)\\!\\!\restriction_{u_{i}\wedge\pi^{*}(v)})=u_{i}\wedge\mathcal{D}_{\pi^{*}(v)}(\pi^{\sharp}(s))$

For $w:L_{Y}$ and $s:\mathcal{O}_{Y}(w)$ we have that
$u_{i}\wedge\pi^{*}(w)=u_{i}\wedge\pi^{*}(w_{j}\wedge w)$, since
$u_{i}\leq\pi^{*}(w_{j})$, and hence

$\displaystyle\mathcal{D}_{u_{i}\wedge\pi^{*}(w)}(\pi^{\sharp}(s)\\!\\!\restriction_{u_{i}\wedge\pi^{*}(w)})\leavevmode\nobreak\
$ $\displaystyle=\leavevmode\nobreak\
u_{i}\wedge\mathcal{D}_{\pi^{*}(w_{j}\wedge
w)}(\pi^{\sharp}(s)\\!\\!\restriction_{\pi^{*}(w_{j}\wedge w)})$
$\displaystyle=\leavevmode\nobreak\
u_{i}\wedge\pi^{*}\big{(}\mathcal{D}_{w_{j}\wedge
w}(s\\!\\!\restriction_{w_{j}\wedge w})\big{)}$
$\displaystyle\leq\leavevmode\nobreak\ \pi^{*}\big{(}\mathcal{D}_{w_{j}\wedge
w}(s\\!\\!\restriction_{w_{j}\wedge w})\big{)}$

and hence, since for each $i$ there exists a compatible $j$,

$\displaystyle\mathcal{D}_{\pi^{*}(w)}(\pi^{\sharp}(s))\leavevmode\nobreak\ $
$\displaystyle=\leavevmode\nobreak\
\textstyle\bigvee_{i=1}^{n}\mathcal{D}_{u_{i}\wedge\pi^{*}(w)}(\pi^{\sharp}(s)\\!\\!\restriction_{u_{i}\wedge\pi^{*}(w)})$
$\displaystyle\leq\leavevmode\nobreak\
\textstyle\bigvee_{j=1}^{m}\pi^{*}\big{(}\mathcal{D}_{w_{j}\wedge
w}(s\\!\\!\restriction_{w_{j}\wedge w})\big{)}$
$\displaystyle=\leavevmode\nobreak\
\pi^{*}\big{(}\mathcal{D}_{w}(s)\big{)}\qed$

###  3.4 Classical characterization

Before moving on, we want to sketch why the definition of qcqs-schemes as
locally ringed lattices given above is actually equivalent to the standard
definition using locally ringed spaces. This section is addressed to readers
familiar with classical algebraic geometry. For this section only, we leave
the realm of constructive type theory and adopt set-theoretic notation.

First, it is worth checking that invertibility supports are related to sheaves
of local rings. Observe that any ringed space $(X,\mathcal{O}_{X})$ has
arbitrary invertibility suprema. For any open $U\subseteq X$ and
$s\in\mathcal{O}_{X}(U)$, we can define

$\displaystyle\mathcal{D}_{U}(s)=\big{\\{}x\in U\leavevmode\nobreak\
|\leavevmode\nobreak\ s_{x}\in\mathcal{O}_{X,x}^{\,\times}\big{\\}}$

$\mathcal{D}$ is easily seen to be an invertibility map (on opens of $X$ and
$\mathcal{O}_{X}$). $\mathcal{D}_{U}(s)$ is sometimes called the
_invertibility open_ of s.181818 See [Hak72, Def. 2.1]. Moreover, it contains
all information about locality on the stalks, as the following propositions
show.

######  Proposition 3.25.

$(X,\mathcal{O}_{X})$ is a locally ringed space if and only if
$\mathcal{D}_{U}$ is a support for all opens $U\subseteq X$.

###### Proof.

Note that we always have

$\displaystyle\mathcal{D}_{U}(1)=U\quad\&\quad\forall
s,t:\;\mathcal{D}_{U}(st)=\mathcal{D}_{U}(s)\cap\mathcal{D}_{U}(t)$

So what we actually want to prove is that $(X,\mathcal{O}_{X})$ is a locally
ringed space if and only if for all open sets $U$ we have:

$\displaystyle\mathcal{D}_{U}(0)=\emptyset\quad\&\quad\forall
s,t:\;\mathcal{D}_{U}(s+t)\subseteq\mathcal{D}_{U}(s)\cup\mathcal{D}_{U}(t)$

Recall that a ring $A$ is local if and only if it is non-trivial and the non-
units $A\setminus A^{\times}$ form an ideal, which is the case if and only if
$A\setminus A^{\times}$ is closed under addition. Taking the contrapositive of
the last statement, we arrive at: _$A$ is local iff it is non-trivial and
$s+t\in A^{\times}$ implies $s\in A^{\times}$ or $t\in A^{\times}$_.191919In
fact, this is usually taken to be the constructive definition of a local ring.
Using this characterization for the stalks $\mathcal{O}_{X,x}$ the claim
immediately follows. ∎

######  Proposition 3.26.

$(f,f^{\sharp}):(X,\mathcal{O}_{X})\to(Y,\mathcal{O}_{Y})$ is a morphism of
locally ringed spaces if and only if for every open $U\subseteq Y$ and section
$s\in\mathcal{O}_{Y}(U)$:202020In [Hak72, Def. 2.9], a morphism of ringed
topoi satisfying the analoguous condition is called _admissible_.

$\displaystyle
f^{-1}\big{(}\mathcal{D}_{U}(s)\big{)}\;=\;\mathcal{D}_{f^{-1}(U)}(f^{\sharp}(s))$

###### Proof.

This follows from the fact that a homomorphism of local rings $\varphi:A\to B$
is local if and only if $\varphi(a)\in B^{\times}$ implies $a\in A^{\times}$.
∎

The next step is to establish a connection between (ringed) lattices and
(ringed) spaces. The main result that makes this possible is _Stone’s
representation theorem for distributive lattices_ [Sto38]. It gives a
(contravariant) equivalence of categories between distributive lattices and a
special class of topological spaces, called _coherent_ or _spectral_ spaces. A
topological space $X$ is coherent if it is _quasi-compact_ , _sober_ (its non-
empty irreducible closed subsets are the closure of a single point), and its
quasi-compact opens are closed under finite intersections and form a basis of
the topology of $X$. A coherent map between coherent spaces $X$ and $Y$ is a
continuous map $f:X\to Y$ such that for any quasi-compact open $K\subseteq Y$,
its pre-image $f^{-1}(K)$ is quasi-compact.

The category $\mathsf{CohSp}$ consists of coherent spaces with coherent maps.
The equivalence $\mathsf{CohSp}\simeq\mathsf{DL}^{op}$ sends a coherent space
$X$ to its lattice of quasi-compact opens $\mathbf{K}^{o}(X)$ and a coherent
map $f:X\to Y$ to the pre-image lattice homomorphism
$f^{-1}:\mathbf{K}^{o}(Y)\to\mathbf{K}^{o}(X)$. The inverse can also be
defined explicitly, assigning to a distributive lattice $L$ the space of
points of the locale of $L$-_ideals_
$\text{pt}\,\big{(}\mathsf{Idl}(L)\big{)}$. See [Joh82, Sec. II.3.3] for
details.

By extension of Stone’s representation theorem, ringed lattices are equivalent
to ringed coherent spaces. Sheaves on a topological space $X$ are in bijection
with sheaves on any basis of $X$ by the comparison lemma for topological
spaces. Hence, for any coherent space $X$ we get an equivalence of categories

$\displaystyle\mathsf{Sh}\big{(}\mathbf{K}^{o}(X)\big{)}\leavevmode\nobreak\
\simeq\leavevmode\nobreak\ \mathsf{Sh}(X)$

Since the quasi-compact opens are all quasi-compact, we only have to consider
finite covers for the sheaf property and we can thus identify
$\mathsf{Sh}\big{(}\mathbf{K}^{o}(X)\big{)}$ with the category of lattice
sheaves on $\mathbf{K}^{o}(X)$.

However, in the locally ringed case things get a bit more complicated. In
Definition 3.4 we had to add the invertibility map as an extra structure on
the ringed lattice that could not be defined automatically. This is for the
subtle reason that we required $\mathcal{D}_{u}(s)$ to be an element of the
lattice. In other words, locally ringed lattices correspond to locally ringed
spaces $(X,\mathcal{O}_{X})$ where $X$ is a coherent space and _for any quasi-
compact open $U\subseteq X$ and section $s:\mathcal{O}_{X}(U)$, the
invertibility open $\mathcal{D}_{U}(s)$ is quasi-compact as well_. This last
condition need not always hold, as the following counterexample due to Thierry
Coquand shows:

######  Example 3.27.

The one-point compactification of the naturals (as a discrete space)
$X=\mathbb{N}\cup\\{\infty\\}$ is coherent.212121It is also Hausdorff and
hence a Stone space, corresponding to the boolean algebra of finite and
cofinite subsets of $\mathbb{N}$. Let
$\mathcal{O}_{X}(U)=\\{f:U\to\mathbb{R}\leavevmode\nobreak\
\text{continuous}\leavevmode\nobreak\ \\}$ and take the global section defined
by $s(n)=\nicefrac{{1}}{{n}}$ and $s(\infty)=0$. Then the invertibility open
$\mathcal{D}_{X}(s)=\\{x\in\mathbb{N}\cup\\{\infty\\}\leavevmode\nobreak\
|\leavevmode\nobreak\ s(x)\neq 0\\}=\mathbb{N}$ is not compact. Hence we can
not describe this locally ringed coherent space as a locally ringed lattice.

In the lingo of Grothendieck’s “EGA 1” [DG71], coherent spaces are precisely
the qcqs-spaces which are sober. The technical notion of sobriety ensures that
the points of a space can be recovered from the locale of opens and is crucial
to make the representation theorem work. However, as schemes are always sober,
qcqs-schemes are precisely the schemes with a coherent topology. Now, for a
qcqs-scheme $X$, any quasi-compact open $U\subseteq X$ has a finite affine
cover $U=\bigcup_{i=1}^{n}\mathsf{Spec}(R_{i})$. It follows that for any
$s\in\mathcal{O}_{X}(U)$, its invertibility open can be computed as
$\mathcal{D}_{U}(s)=\bigcup_{i=1}^{n}D\big{(}s\\!\\!\restriction_{\mathsf{Spec}(R_{i})}\big{)}$
and is thus quasi-compact.

Moreover, any morphism of schemes between two qcqs-schemes $X\to Y$ is
coherent (quasi-compact). The key result [CLS09, Lemma 15]

_If $X$ is a qc- and $Y$ a qs-scheme, then any morphism $X\to Y$ is quasi-
compact._

is proved by combining several results from [DG71, Ch. 6].222222In “The Rising
Sea” this is proved using the so-called “cancellation theorem” [Vak24]. This
shows that the category of locally ringed lattices contains qcqs-schemes as a
full subcategory and that Definition 3.18 gives an equivalent description of
this subcategory.

##  4 The functor of points approach

For algebraic geometers it is often convenient to identify a scheme with its
“functor of points”.232323see e.g. [EH06, Ch. VI] or [Mum99, Ch. II §6]. Given
a scheme $X$, we can look at the presheaf
$\mathsf{Sch}(\\_,X):\mathsf{Sch}^{op}\to\mathsf{Set}$ and by the Yoneda
lemma, two schemes $X$ and $Y$ are isomorphic as schemes if and only if the
presheaves $\mathsf{Sch}(\\_,X)$ and $\mathsf{Sch}(\\_,Y)$ are naturally
isomorphic. Since affine schemes form a dense subcategory of the category of
schemes, $X$ and $Y$ are isomorphic schemes if the restrictions
$\mathsf{Sch}(\\_,X)\\!\\!\restriction_{\mathsf{Aff}^{op}}$ and
$\mathsf{Sch}(\\_,Y)\\!\\!\restriction_{\mathsf{Aff}^{op}}$ are isomorphic as
presheaves. We can push this even further by using that the functor
$\mathsf{Spec}$ is an equivalence of categories between $\mathsf{Aff}$ and
$\mathsf{CommRing}^{op}$. For any scheme $X$ we can define its functor of
points
$h_{X}:\equiv\mathsf{Sch}(\operatorname{\mathsf{Spec}}{(\\_)},X):\mathsf{CommRing}\to\mathsf{Set}$
(a presheaf on $\mathsf{CommRing}^{op}$) and two schemes are isomorphic if and
only if their functors of points are naturally isomorphic. We can do this for
our definition of qcqs-schemes as locally ringed lattices where a morphism of
schemes is just a morphism of locally ringed lattices or equivalently a
locally affine morphism of ringed lattices. We will study the functor of
points for locally ringed lattices in Section 5.1.

In this section we want to answer the following question: Is it possible to
characterize the image of the functor
$h:\mathsf{qcqsSch}\hookrightarrow\mathsf{Psh}(\mathsf{CommRing}^{op})$
directly, using purely algebraic and categorical methods, while staying
constructive and predicative? In the classical literature, this is the so-
called _functor of points approach_ , which allows one to introduce schemes
without having to introduce locally ringed spaces first. Affine schemes are
readily accounted for in this approach, as they correspond to the
_representable_ presheaves given by the Yoneda embedding, which we will
henceforth denote by
$\mathsf{Sp}:\mathsf{CommRing}^{op}\hookrightarrow\mathsf{Psh}(\mathsf{CommRing}^{op})$.
Indeed, one can immediately verify that $\mathsf{Sp}(A)\cong
h_{\operatorname{\mathsf{Spec}}{(A)}}$. Functorial schemes turn out to be
those presheaves $X:\mathsf{CommRing}\to\mathsf{Set}$ that satisfy a certain
locality condition and have an _open cover_ by affine sub-presheaves
$\mathsf{Sp}(A)\hookrightarrow X$.

The standard reference developing the basics of algebraic geometry starting
from functors $\mathsf{CommRing}\to\mathsf{Set}$ is “Introduction to Algebraic
Geometry and Algebraic Groups” by Demazure and Gabriel [DG80]. The central
notion here is that of an _open subfunctor_. These are in a certain sense
classified by the locale of “Zariski opens”.242424See e.g. [Mad13]. This fact
is usually not stated explicitly in textbooks. Focusing instead on the notion
of _compact open subfunctors_ , which are classified by the Zariski lattice,
we can obtain a constructive functorial approach to qcqs-schemes. In this
approach we have to be careful about size issues, so we will annotate
categories with the universe level at which the type of objects live. Fixing a
base level $\ell$, $\mathsf{CommRing}_{\ell}$ will be the type or category of
“small” commutative rings, whose carrier type lives in $\mathsf{Type}_{\ell}$.
Big commutative rings will be denoted by $\mathsf{CommRing}_{\ell+1}$ and the
same applies to lattices, locally ringed lattices and the like.

Since it only requires standard tools from category theory and algebra, this
approach lends itself to a concise definition of qcqs-schemes that is
convenient to formalize. In particular, many of the definitions and results
given in this section are formalized using the Cubical Agda proof assistant
and are already described in [ZH24], which adapts [DG80] to HoTT/UF while
staying constructive and predicative. We repeat definitions and results from
[ZH24] here for convenience and for the sake of self-containedness but omit
proofs.

######  Definition 4.1.

The category of $\mathbb{Z}$-functors, denoted
$\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$, is the category of functors from
$\mathsf{CommRing}_{\ell}$ to $\mathsf{Set}_{\ell}$. We write
$\mathsf{Sp}:\mathsf{CommRing}_{\ell}^{op}\to\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$
for the Yoneda embedding and
$\mathbb{A}^{1}:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$ for the forgetful
functor from commutative rings to sets. We say that
$X:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$ is an _affine scheme_ if there
exists a $R:\mathsf{CommRing}_{\ell}$ with a natural isomorphism
$X\cong\mathsf{Sp}(R)$.252525As the category of $\mathbb{Z}$-functors is
univalent and $\mathsf{Sp}$ is fully faithful, it is not necessary to use mere
existence for defining affine schemes, as the type of rings $R$ with
$X\cong\mathsf{Sp}(R)$ is a proposition.

######  Example 4.2.

$\mathbb{A}^{1}$ is an affine scheme, as
$\mathbb{A}^{1}\cong\mathsf{Sp}(\mathbb{Z}[x])$. The $\mathbb{Z}$-functor
$\mathbb{G}_{m}$ that sends a ring to its set of units, i.e.
$\mathbb{G}_{m}(R):\equiv R^{\times}$, is an affine scheme as
$\mathbb{G}_{m}\cong\mathsf{Sp}(\mathbb{Z}[x][\nicefrac{{1}}{{x}}])$.

######  Definition 4.3.

Let $X:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$, the _ring of functions_
$\mathcal{O}(X)$ is the type of natural transformations
${X}\Rightarrow{\mathbb{A}^{1}}$ equipped with the canonical point-wise
operations, i.e. for $R:\mathsf{CommRing}_{\ell}$ and $x:X(R)$, zero, one,
addition and multiplication are given by

$\displaystyle 0_{R}(x):\equiv 0,\quad 1_{R}(x):\equiv 1$
$\displaystyle(\alpha+\beta)_{R}(x)\leavevmode\nobreak\
:\equiv\leavevmode\nobreak\ \alpha_{R}(x)+\beta_{R}(x)$
$\displaystyle(\alpha\cdot\beta)_{R}(x)\leavevmode\nobreak\
:\equiv\leavevmode\nobreak\ \alpha_{R}(x)\cdot\beta_{R}(x)$

This defines a functor
$\mathcal{O}:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}\to\mathsf{CommRing}_{\ell+1}^{op}$,
whose action on morphisms (natural transformations) is given by
precomposition.

Because the ring of functions of a $\mathbb{Z}$-functor is lives in the
successor universe, we cannot have an adjunction between $\mathsf{Sp}$ and
$\mathcal{O}$. However, the two functors form what is called a _relative
coadjunction_ with respect to the functor induced by universe lifting
$\mathsf{lift}:\mathsf{CommRing}^{op}_{\ell}\to\mathsf{CommRing}^{op}_{\ell+1}$.

######  Definition 4.4 ([nLa24b]).

Let $\mathcal{B},\mathcal{C},\mathcal{D}$ be categories with functors
$l:\mathcal{C}\to\mathcal{D}$, $F:\mathcal{B}\to\mathcal{D}$ and
$G:\mathcal{C}\to\mathcal{B}$. We say that $F$ and $G$ are $l$-relative
adjoint, written as $G\prescript{}{l}{\dashv}\leavevmode\nobreak\ F$, if there
is a natural family of equivalences

$\displaystyle(c:\mathcal{C})\leavevmode\nobreak\
(b:\mathcal{B})\to\mathcal{B}\big{(}G(c),b\big{)}\leavevmode\nobreak\
\simeq\leavevmode\nobreak\ \mathcal{D}\big{(}l(c),F(b)\big{)}$

Dually, we say that $F$ and $G$ are $l$-relative coadjoint, written as
$F\dashv_{\,l}G$, if there is a natural family of equivalences

$\displaystyle(c:\mathcal{C})\leavevmode\nobreak\
(b:\mathcal{B})\to\mathcal{D}\big{(}F(b),l(c)\big{)}\leavevmode\nobreak\
\simeq\leavevmode\nobreak\ \mathcal{B}\big{(}b,G(c)\big{)}$

######  Remark 4.5.

In the setting of Definition 4.4, a relative adjunction
$G\prescript{}{l}{\dashv}\leavevmode\nobreak\ F$ induces a relative unit, i.e.
for $c:\mathcal{C}$ a map $\eta_{c}:\mathcal{D}\big{(}l(c),F(G(c))\big{)}$
natural in $c$. Analogously, a relative coadjunction $F\dashv_{\,l}G$ induces
a relative counit, i.e. for $c:\mathcal{C}$ a map
$\varepsilon_{c}:\mathcal{D}\big{(}F(G(c)),l(c)\big{)}$ natural in $c$. Note
that we do not get the other direction in either case.

######  Proposition 4.6.

We have a relative coadjunction
$\mathcal{O}\dashv_{\mathsf{lift}}\mathsf{Sp}$. In particular, for
$R:\mathsf{CommRing}_{\ell}$ and $X:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$
there is an equivalence of types

$\displaystyle{\mathsf{Hom}\big{(}R,\mathcal{O}(X)\big{)}}\simeq\big{(}{X}\Rightarrow{\mathsf{Sp}(R)}\big{)}$

which is natural in both $R$ and $X$. For any $R:\mathsf{CommRing}_{\ell}$,
the relative counit
$\varepsilon_{R}:\mathsf{Hom}\big{(}R,\mathcal{O}(\mathsf{Sp}(R))\big{)}$,
which is obtained by applying the inverse of above isomorphism to the identity
${\mathsf{Sp}(R)}\Rightarrow{\mathsf{Sp}(R)}$, is an isomorphisms of rings.

######  Remark 4.7.

Proposition 4.6 type-checks because the type of ring homomorphisms is universe
polymorphic, meaning that it can take rings living in different universes as
arguments. The same holds for the type of isomorphisms/equivalences between
two types. Since universe lifting commutes with type formers, we get

$\displaystyle{\mathsf{Hom}\big{(}R,\mathcal{O}(X)\big{)}}\simeq\mathsf{CommRing}^{op}_{\ell+1}\big{(}\mathcal{O}(X),\mathsf{lift}(R)\big{)}$

which is natural in $R$ and $X$. It is modulo this equivalence that we
actually get the relative coadjunction
$\mathcal{O}\dashv_{\mathsf{lift}}\mathsf{Sp}$ in Proposition 4.6.

###  4.1 Zariski coverage

The category of $\mathbb{Z}$-functors, contains a lot more than the functorial
schemes we want to define. For example, for a qcqs-scheme $X$, we also have a
functor mapping a ring $A$ to the set
$\mathsf{RDL}^{op}\big{(}\mathsf{Spec}(A),X\big{)}$ of morphisms of _ringed
lattices_ from $X$ to $\mathsf{Spec}(A)$. This functor is of course of little
interest to algebraic geometers and we need to set it apart from the functor
of points $\mathsf{LRDL}^{op}\big{(}\mathsf{Spec}(\\_),X\big{)}$ by
introducing a “locality” condition on $\mathbb{Z}$-functors. This condition is
induced by a certain coverage or Grothendieck topology on
$\mathsf{CommRing}_{\ell}^{op}$, called the Zariski coverage or topology.
Local $\mathbb{Z}$-functors turn out to be Zariski sheaves.

The notion of Grothendieck topology or coverage generalizes point-set
topologies to arbitrary categories. It associates to each object in a category
$X:\mathcal{C}$ a family $\mathsf{Cov}(X)$ of covers, where a cover
$\big{\\{}f_{i}:\mathcal{C}\big{(}U_{i},X\big{)}\big{\\}}_{i:I}$ is a family
of maps into $X$, i.e. a family of objects in the slice category
$\nicefrac{{\mathcal{C}}}{{X}}$. These $\mathsf{Cov}(X)$ should satisfy
certain closure properties. If $\mathcal{C}$ has pullbacks, $\mathsf{Cov}$
should be closed under pullbacks, meaning that for
$\big{\\{}f_{i}:\mathcal{C}\big{(}U_{i},Y\big{)}\big{\\}}_{i:I}$ in
$\mathsf{Cov}(Y)$ and $g:\mathcal{C}\big{(}X,Y\big{)}$, the family
$\big{\\{}g^{*}f_{i}:\mathcal{C}\big{(}X\times_{Y}U_{i},X\big{)}\big{\\}}_{i:I}$
should be in $\mathsf{Cov}(X)$. A presheaf
$\mathcal{F}:\mathcal{C}^{op}\to\mathsf{Set}$ can then be defined to be a
sheaf if for any
$\big{\\{}f_{i}:\mathcal{C}\big{(}U_{i},X\big{)}\big{\\}}_{i:I}$ in
$\mathsf{Cov}(X)$ we get an equalizer diagram

$\displaystyle\mathcal{F}(X)\to\prod_{i:I}\mathcal{F}(U_{i})\rightrightarrows\prod_{i,j:I}\mathcal{F}(U_{i}\times_{X}U_{j})$
(4.1)

In the case where $\mathcal{C}$ is the poset of open subsets of a topological
space $X$, covers are defined the usual way: A family $(U_{i}\subseteq
U)_{i:I}$ is in $\mathsf{Cov}(U)$ if $\bigcup_{i}U_{i}=U$. Pullbacks are just
given by intersection and we recover the usual topological notion of sheaf.

Note that, while coverages are generally defined as pullback-stable families
of covers, Grothendieck topologies require more closure properties and their
covering families are usually required to be so-called sieves. Moreover,
coverages can be defined on categories without pullbacks with a slightly
weaker condition of “pullback stability”. Accordingly, the definition of sheaf
with respect to such a generalized coverage is rephrased in a pullback-free
way. For an overview of coverages with and without pullbacks and Grothendieck
topologies see [nLa24a]. For a coverage (with or without pullbacks) one can
always find a unique Grothendieck topology inducing the same notion of sheaf,
by taking “closures” of covers in a certain sense.262626See e.g. [Joh02, Prop.
C2.1.9]. Still, it is often convenient to work with concrete covers and not
their generated sieves, as they give a simpler description of sheaves.

The formalization of functorial qcqs-schemes described in [ZH24] uses
coverages without pullbacks, even though $\mathsf{CommRing}^{op}_{\ell}$ has
pullbacks (given by the tensor product of rings). This does seem to make
certain things easier to formalize, as it requires less categorical machinery.
For the sake of conceptually simplicity, however, we want to think of the
specific coverage that we are interested in, the Zariski coverage, as
pullback-stable families of covers on $\mathsf{CommRing}_{\ell}^{op}$ with the
corresponding notion of Zariski sheaf given as in (4.1). Consequently, results
and proofs regarding the Zariski coverage are perhaps not as straightforwardly
formalizable and may require careful rephrasing. Ultimately, this should
always be possible as both coverages (with or without pullbacks) generate the
same Grothendieck topology and thus give the same notion of Zariski sheaf.

######  Definition 4.8.

For $R:\mathsf{CommRing}_{\ell}^{op}$, a _Zariski cover_ is indexed by
finitely many elements $f_{1},...,f_{n}:R$ such that $1\in\langle
f_{1},...,f_{n}\rangle$ and assigns to each $f_{i}$ the canonical morphism
$\nicefrac{{\\_}}{{1}}:\mathsf{CommRing}_{\ell}^{op}\big{(}R[\nicefrac{{1}}{{f_{i}}}],R\big{)}$.
This defines a coverage, called the _Zariski coverage_ , as Lemma 4.9 shows. A
$\mathbb{Z}$-functor is called _local_ if it is a sheaf with respect to the
Zariski coverage.

######  Lemma 4.9.

Zariski covers are stable under pullbacks.

###### Proof.

Let $R,A:\mathsf{CommRing}_{\ell}$ and $\varphi:\mathsf{Hom}(R,A)$. For
$f_{1},...,f_{n}:R$ with $1\in\langle f_{1},...,f_{n}\rangle$, we get that
$1\in\langle\varphi(f_{1}),...,\varphi(f_{n})\rangle$ and this cover is indeed
the pullback (in $\mathsf{CommRing}_{\ell}^{op}$) of the Zariski cover on $R$,
as we have a canonical isomorphism $A[\nicefrac{{1}}{{\varphi(f_{i})}}]\cong
A\otimes_{R}R[\nicefrac{{1}}{{f_{i}}}]$. ∎

######  Theorem 4.10.

The Zariski coverage is subcanonical, meaning that $\mathsf{Sp}(A)$ is local
for $A:\mathsf{CommRing}_{\ell}$.

###### Proof.

This is essentially the standard algebraic fact that is used to prove that the
structure sheaf of an affine sheaf satisfies the sheaf property [EH06, Prop.
I-18]: For $f_{1},...,f_{n}:R$ with $1\in\langle f_{1},...,f_{n}\rangle$ we
have an equalizer diagram

$\displaystyle
R\to\prod_{i=1}^{n}R[\nicefrac{{1}}{{f_{i}}}]\rightrightarrows\prod_{i,j}R[\nicefrac{{1}}{{f_{i}f_{j}}}]$

Since $R[\nicefrac{{1}}{{f_{i}f_{j}}}]\cong
R[\nicefrac{{1}}{{f_{i}}}]\otimes_{R}R[\nicefrac{{1}}{{f_{j}}}]$, i.e.
$R[\nicefrac{{1}}{{f_{i}f_{j}}}]$ is the pullback in
$\mathsf{CommRing}_{\ell}^{op}$, and $\mathsf{Hom}(A,\\_)$ is left exact, the
sheaf property (4.1) follows. For a formal proof for the Zariski coverage
defined without using pullbacks, see [ZH24, Thm. 12]. ∎

###  4.2 Compact opens

The main idea that allowed for a formalization of functorial qcqs-schemes in
[ZH24] was a streamlined definition of compact open subfunctors of a
$\mathbb{Z}$-functor. The compact open subfunctors are investigated
extensively in the thesis of Blechschmidt [Ble21]. They play a prominent role
in the development of synthetic algebraic geometry, i.e. algebraic geometry
done internally in the topos of local $\mathbb{Z}$-functors, in the form of
compact open propositions. Openness is usually defined as a property of a
subfunctor $U\hookrightarrow X$. Recall that a subfunctor of a
$\mathbb{Z}$-functor $X$ is a $\mathbb{Z}$-functor $U$ with a natural
transformation ${U}\Rightarrow{X}$ that is pointwise injective. The property
of being an open subfunctor can directly be restricted to compact openness as
in [Ble21, Def. 19.15].

######  Definition 4.11.

A subfunctor $U\hookrightarrow\mathsf{Sp}(A)$ is an _affine open_ subfunctor
if there merely exists an ideal $I\subseteq A$ such that for any ring $B$ we
have

$\displaystyle
U(B)\;\cong\;\big{\\{}\varphi:\mathsf{Hom}(A,B)\leavevmode\nobreak\
|\leavevmode\nobreak\ \varphi^{*}I=B\big{\\}}$ (4.2)

naturally and commuting with the embeddings into $\mathsf{Sp}(A)$. Here
$\varphi^{*}I$ is the ideal generated by the image of $I$ under $\varphi$. We
say that $U\hookrightarrow\mathsf{Sp}(A)$ is an _affine compact open_
subfunctor if there merely exists a _finitely generated_ ideal $I\subseteq A$
such that we have an isomorphism of subobjects as in (4.2).

######  Remark 4.12.

Note that the ideal $I$ is not uniquely determined for an affine (compact)
open subfunctor $U\hookrightarrow\mathsf{Sp}(A)$. For ideals $I,J$ of $A$ we
have that $\sqrt{I}=\sqrt{J}$ if and only if for all rings $B$ and
$\varphi:\mathsf{Hom}(A,B)$ we have

$\displaystyle\varphi^{*}I=B\leavevmode\nobreak\
\Leftrightarrow\leavevmode\nobreak\ \varphi^{*}J=B$

If $I=\langle a_{1},...,a_{n}\rangle$ is finitely generated, $U$ is isomorphic
(as subobjects) to the affine compact open subfunctor given by

$\displaystyle
B\;\mapsto\;\;\big{\\{}\varphi:\mathsf{Hom}(A,B)\leavevmode\nobreak\
|\leavevmode\nobreak\
1\in\langle\varphi(a_{1}),\dots,\varphi(a_{n})\rangle\,\big{\\}}$

By the above argument it follows that this subfunctor is really determined by
the element $D(a_{1},\dots,a_{n}):\mathcal{L}_{A}$, since for $J=\langle
b_{1},\dots,b_{m}\rangle$ we have

$\displaystyle
D(a_{1},\dots,a_{n})=D(b_{1},\dots,b_{m})\;\Leftrightarrow\;\sqrt{\langle
a_{1},\dots,a_{n}\rangle}=\sqrt{\langle b_{1},\dots,b_{m}\rangle}$

We can thus write the corresponding subfunctor as

$\displaystyle
B\;\mapsto\;\;\big{\\{}\varphi:\mathsf{Hom}(A,B)\leavevmode\nobreak\
|\leavevmode\nobreak\ D(1)=D(\varphi(a_{1}),...,\varphi(a_{n}))\,\big{\\}}$

In other words the compact open subfunctors of the affine scheme
$\mathsf{Sp}(A)$ are in bijection with elements of $\mathcal{L}_{A}$.

######  Definition 4.13.

For $\mathbb{Z}$-functors $U\hookrightarrow X$, we say that $U$ is a
_(compact) open_ subfunctor of $X$, if for any ring $A$ and $A$-valued point
of $X$, i.e. natural transformation $\phi:{\mathsf{Sp}(A)}\Rightarrow{X}$, the
pullback $V:\equiv\mathsf{Sp}(A)\times_{X}U$ is an affine (compact)
subfunctor:

${V}$${U}$${\mathsf{Sp}(A)}$${X}$

$\lrcorner$

$\scriptstyle{\phi}$

######  Remark 4.14.

One easily checks that on $\mathsf{Sp}(A)$ compact open subfunctors and affine
compact open subfunctors coincide.

One usually wants to identify subobjects up to natural isomorphism commuting
with embeddings. This complicates things substantially in a formal setting.
The key observation in [ZH24], allowing to circumvent this issue, is that the
compact open subfunctors are classified by the Zariski lattice.

######  Definition 4.15.

Let $\mathcal{L}:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$ be the
$\mathbb{Z}$-functor mapping $R:\mathsf{CommRing}_{\ell}$ to the underlying
set of the Zariski lattice $\mathcal{L}_{R}$. The action on morphisms is
induced by the universal property of the Zariski lattice, i.e. for
$\varphi:\mathsf{Hom}(A,B)$ we take

${A}$${\mathcal{L}_{A}}$${\mathcal{L}_{B}}$$\scriptstyle{D}$$\scriptstyle{D\circ\varphi}$$\scriptstyle{\exists!\leavevmode\nobreak\
\varphi^{\mathcal{L}}}$

The transformation $D(1):{\mathbf{1}}\Rightarrow{\mathcal{L}}$ from the
terminal $\mathbb{Z}$-functor $\mathbf{1}(\\_):\equiv\\{\ast\\}$ to
$\mathcal{L}$ is the “pointwise constant” map $\ast\mapsto D(1)$.

######  Proposition 4.16.

For each presheaf with compact open subfunctor $U\hookrightarrow X$ there
exists a unique natural transformation $\chi:{X}\Rightarrow{\mathcal{L}}$ such
that the following is a pullback square

${U}$${\mathbf{1}}$${X}$${\mathcal{L}}$

$\lrcorner$

$\scriptstyle{D(1)}$$\scriptstyle{\exists!\chi}$

###### Proof.

For a ring $A$ and an $A$-valued point of $X$, which modulo Yoneda we can
write as $\phi:{\mathsf{Sp}(A)}\Rightarrow{X}$, we can pull back $U$ along
$\phi$ to obtain an affine compact open subfunctor corresponding to a unique
$u:\mathcal{L}_{A}$ and set $\chi(\phi):\equiv u$. This is well-defined by
Remark 4.12 and easily seen to be natural in $A$. It also follows directly
that this gives a pullback square. ∎

######  Definition 4.17.

Let $X:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$, a _compact open_ of $X$ is a
natural transformation $U:{X}\Rightarrow{\mathcal{L}}$. The _realization_
$\llbracket\,{U}\,\rrbracket:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$ of a
compact open $U$ of $X$, is given by

$\displaystyle\llbracket\,{U}\,\rrbracket\,(R)\leavevmode\nobreak\
=\leavevmode\nobreak\ {\\{\,x:X(R)\leavevmode\nobreak\ |\leavevmode\nobreak\
{U(x)}={D(1)}\,\\}}$

A compact open $U$ is called _affine_ , if its realization is affine, i.e. if
there merely exists $R:\mathsf{CommRing}_{\ell}$ such that
$\llbracket\,{U}\,\rrbracket\cong\mathsf{Sp}(R)$.

######  Remark 4.18.

Indeed, one can check that

${\llbracket\,{U}\,\rrbracket}$${\mathbf{1}}$${X}$${\mathcal{L}}$

$\lrcorner$

$\scriptstyle{D(1)}$$\scriptstyle{U}$

Working with Definition 4.17 instead of Definition 4.13, can be seen as an
instance of a common trick in constructive mathematics and type theory in
particular. In order to avoid setoid or transport hell, when working with
objects up to some non-trivial equivalence relation, one can instead use a
suitable index set which is in bijection with the equivalence classes, and
where each “index” corresponds to a canonical member of the corresponding
equivalence class.

######  Definition 4.19.

Let $X:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$, the _lattice of compact opens_
$\mathsf{CompOpen}(X)$ is the type ${X}\Rightarrow{\mathcal{L}}$ equipped with
the canonical point-wise operations, i.e. for $R:\mathsf{CommRing}_{\ell}$ and
$x:X(R)$, top, bottom, join and meet are given by

$\displaystyle 1_{R}(x)=D(1),\quad 0_{R}(x)=D(0)$ $\displaystyle(U\wedge
V)_{R}(x)\leavevmode\nobreak\ =\leavevmode\nobreak\ U_{R}(x)\wedge V_{R}(x)$
$\displaystyle(U\vee V)_{R}(x)\leavevmode\nobreak\ =\leavevmode\nobreak\
U_{R}(x)\vee V_{R}(x)$

This defines a functor
$\mathsf{CompOpen}:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}\to\mathsf{DistLattice}_{\ell+1}^{op}$.

######  Definition 4.20.

Let $X:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$ and
$U_{1},...,U_{n}:{X}\Rightarrow{\mathcal{L}}$. We say that the $U_{i}$ form a
_compact open cover_ of $X$, if ${1}={\bigvee_{i=1}^{n}U_{i}}$ in the lattice
$\mathsf{CompOpen}(X)$.

######  Remark 4.21.

Being able to define the notion of cover using the lattice structure on
compact opens is one of the main advantages of using the internal Zariski
lattice as a classifier. In the literature, the classically valid fact that
$U_{1},...,U_{n}:{X}\Rightarrow{\mathcal{L}}$ cover $X$ if and only if
$\bigcup_{i=1}^{n}\llbracket\,{U_{i}}\,\rrbracket(k)=X(k)$ for all fields $k$,
is sometimes used as a definition for the notion of cover [EH06, Thm. VI-14].
As the notion of field is ambiguous from the constructive point of view, such
a definition does not appear to be suitable for our purposes. The alternative
of pulling back to affine compact opens and defining covers in terms of ideal
addition does work, but Definition 4.20 streamlines this by making the
occurrence of ideal addition implicit in the definition of the join operation
on the Zariski lattice. This lets us define functorial qcqs-schemes.

######  Definition 4.22.

$X:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$ is a _qcqs-scheme_ if it is a local
$\mathbb{Z}$-functor and merely has an affine compact open cover, i.e. a
compact open cover $U_{1},...,U_{n}:{X}\Rightarrow{\mathcal{L}}$ such that
each $U_{i}$ is affine.

As an immediate sanity check we get that affine schemes are qcqs-schemes:

######  Proposition 4.23.

$\mathsf{Sp}(R)$ is a qcqs-scheme, for $R:\mathsf{CommRing}_{\ell}$.

###### Proof.

[ZH24, Prop. 17] ∎

For locally ringed lattices we saw that qcqs-schemes are obtained by “gluing”
together affine schemes in the sense that they are a colimit of affine
subschemes of a certain shape. This holds for functorial qcqs-schemes as well,
but only in the big Zariski topos, i.e. the category of local
$\mathbb{Z}$-functors. The following lemma is taken from Nieper-Wißkirchen’s
lecture notes [NW08] and adapted to our setting.

######  Lemma 4.24.

Let $X$ be a $\mathbb{Z}$-functor and
$U_{1},...,U_{n}:{X}\Rightarrow{\mathcal{L}}$ be a compact open cover of $X$.
Let $Y$ be a _local_ $\mathbb{Z}$-functor with morphisms
$\alpha_{i}:{\llbracket\,{U_{i}}\,\rrbracket}\Rightarrow{Y}$ for $i$ in
$1,...,n$ such that for every $i,j$ the following square commutes

${\llbracket\,{U_{i}\wedge
U_{j}}\,\rrbracket}$${\llbracket\,{U_{i}}\,\rrbracket}$${\llbracket\,{U_{j}}\,\rrbracket}$${Y}$$\scriptstyle{\alpha_{i}}$$\scriptstyle{\alpha_{j}}$

Then there exists a unique $\alpha:{X}\Rightarrow{Y}$ such that for every $i$
in $1,...,n$ the following triangle commutes

${X}$${\llbracket\,{U_{i}}\,\rrbracket}$${Y}$$\scriptstyle{\alpha}$$\scriptstyle{\alpha_{i}}$

###### Proof.

First, we treat the case where $X=\mathsf{Sp}(R)$ is affine. Without loss of
generality, we can assume that for every $i$ in $1,...,n$, $U_{i}=D(f_{i})$ is
a basic open. Otherwise, we may use that, by Yoneda, we have a cover by basic
opens $U_{i}=\bigvee_{k}D(f_{ik})$ and refine our cover accordingly. Note that
the assumption of the lemma still holds for the refined cover. However, in the
case of a cover by basic opens, $\alpha_{i}$ corresponds to an element of
$Y(R[\nicefrac{{1}}{{f_{i}}}])$ by Yoneda, and the lemma follows as $Y$ was
assumed local.

For the general case let $R:\mathsf{CommRing}_{\ell}$ and $x:X(R)$. By Yoneda
we can regard the $U_{i}(x):\mathcal{L}_{R}$ as a compact open cover of
$\mathsf{Sp}(R)$. The $\alpha_{i}$ induce natural transformations
${\llbracket\,{U_{i}(x)}\,\rrbracket}\Rightarrow{Y}$, given on $A$-valued
points by the function

$\displaystyle\llbracket\,{U_{i}(x)}\,\rrbracket(A)=\\{\,\varphi:\mathsf{Hom}(R,A)\,|\,U_{i}(x\\!\\!\restriction_{\varphi})=D(1)\,\\}\leavevmode\nobreak\
\to\leavevmode\nobreak\ Y(A)$

mapping $\varphi$ to $\alpha_{i}(x\\!\\!\restriction_{\varphi})$, where
$x\\!\\!\restriction_{\varphi}\,:\equiv X(\varphi)(x)$ is the restriction of
$x$ along $\varphi$. We can apply the above argument for the affine case to
obtain a unique ${\mathsf{Sp}(R)}\Rightarrow{Y}$, which gives us the desired
$\alpha(x):Y(R)$. We omit the proof that this is natural and commutes with the
$\alpha_{i}$. ∎

######  Corollary 4.25.

If $X:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$ is a qcqs-scheme and
$U_{1},...,U_{n}:{X}\Rightarrow{\mathcal{L}}$ an (affine) compact open cover
of $X$, then

$\displaystyle X\leavevmode\nobreak\ \cong\leavevmode\nobreak\
\mathsf{colim}\,\big{\\{}\llbracket\,{U_{i}}\,\rrbracket\leftarrow\llbracket\,{U_{i}\wedge
U_{j}}\,\rrbracket\rightarrow\llbracket\,{U_{j}}\,\rrbracket\big{\\}}$

in the category if local $\mathbb{Z}$-functors, i.e. Zariski sheaves. In
particular, if we have
$\llbracket\,{U_{i}}\,\rrbracket\cong\mathsf{Sp}(A_{i})$, and affine compact
open covers $\big{(}V_{ijk}:{\llbracket\,{U_{i}\wedge
U_{j}}\,\rrbracket}\Rightarrow{\mathcal{L}}\big{)}_{k}$ with
$\llbracket\,{V_{ijk}}\,\rrbracket\cong\mathsf{Sp}(A_{ijk})$, we have

$\displaystyle X\leavevmode\nobreak\ \cong\leavevmode\nobreak\
\mathsf{colim}\,\big{\\{}\mathsf{Sp}(A_{i})\leftarrow\mathsf{Sp}(A_{ijk})\rightarrow\mathsf{Sp}(A_{j})\big{\\}}$

###  4.3 Open subschemes

Let us conclude this section by proving that compact opens of qcqs-schemes are
qcqs-schemes. The special case of compact opens of affine schemes is
formalized in [ZH24]. First, we treat locality.

######  Lemma 4.26.

$\mathcal{L}$ is local.

###### Proof.

For $f_{1},...,f_{n}:R$ with $1\in\langle f_{1},...,f_{n}\rangle$, we get
$D(1)=D(f_{1},...,f_{n})$ in $\mathcal{L}_{R}$. By the “gluing lemma for
distributive lattices” [CLS07, Lemma 5] we get an equalizer diagram

$\displaystyle\mathcal{L}_{R}\to\prod_{i=1}^{n}\downarrow\\!D(f_{i})\rightrightarrows\prod_{i,j}\downarrow\\!D(f_{i}f_{j})$

Now, for $i,j$ in $1,...,n$ let
$\psi_{i}:\mathcal{L}_{R[\nicefrac{{1}}{{f_{i}}}]}\cong\,\downarrow\\!D(f_{i})$
and
$\psi_{ij}:\mathcal{L}_{R[\nicefrac{{1}}{{f_{i}f_{j}}}]}\cong\,\downarrow\\!D(f_{i}f_{j})$
be the respective isomorphisms given by Lemma 2.4. The following diagram
commutes

${\mathcal{L}_{R[\nicefrac{{1}}{{f_{i}}}]}}$${\downarrow\\!D(f_{i})}$${\mathcal{L}_{R[\nicefrac{{1}}{{f_{i}f_{j}}}]}}$${\downarrow\\!D(f_{i}f_{j})}$$\scriptstyle{\simeq}$$\scriptstyle{\psi_{i}}$$\scriptstyle{\\_\wedge
D(f_{j})}$$\scriptstyle{\simeq}$$\scriptstyle{\psi_{ij}}$

giving us an equalizer diagram

$\displaystyle\mathcal{L}_{R}\to\prod_{i=1}^{n}\mathcal{L}_{R[\nicefrac{{1}}{{f_{i}}}]}\rightrightarrows\prod_{i,j}\mathcal{L}_{R[\nicefrac{{1}}{{f_{i}f_{j}}}]}$

which finishes the proof. ∎

######  Lemma 4.27.

The realization $\llbracket\,{U}\,\rrbracket$ of a compact open
$U:{X}\Rightarrow{\mathcal{L}}$ of a local $\mathbb{Z}$-functor $X$ is local.

###### Proof.

[ZH24, Lemma 21]. Note that this proof uses the fact that $\mathcal{L}$ is
_separated_ wrt. the Zariski coverage. This follows from Lemma 4.26, as
sheaves are always separated. Alternatively, see [ZH24, Lemma 20] for a direct
proof. ∎

It remains to prove that compact opens of qcqs-schemes merely have an affine
cover. Compact opens of affine schemes can be covered by “basic opens”, as was
shown in [ZH24].

######  Definition 4.28.

Let $R:\mathsf{CommRing}_{\ell}$ and $f:R$, the standard open
$D(f):{\mathsf{Sp}(R)}\Rightarrow{\mathcal{L}}$ is given by applying the
Yoneda lemma to the basic open $D(f):\mathcal{L}_{R}$.

######  Lemma 4.29.

For $R:\mathsf{CommRing}_{\ell}$ and $f:R$, the standard open $D(f)$ is
affine. In particular one has a natural isomorphism
${\llbracket\,{D(f)}\,\rrbracket}\cong{\mathsf{Sp}\big{(}R[\nicefrac{{1}}{{f}}]\big{)}}$.

###### Proof.

[ZH24, Prop. 23] ∎

######  Lemma 4.30.

For any ring $R:\mathsf{CommRing}_{\ell}$, the realization
$\llbracket\,{U}\,\rrbracket$ of a compact open
$U:{\mathsf{Sp}(R)}\Rightarrow{\mathcal{L}}$ is a qcqs-scheme.

###### Proof.

[ZH24, Thm. 24] ∎

Now we want to generalize this to the case of a compact open of an arbitrary
qcqs-scheme. The key result is the following lemma that will play an important
role later on as well.

######  Lemma 4.31.

For any $\mathbb{Z}$-functor $X$ and $U:{X}\Rightarrow{\mathcal{L}}$, we have
an isomorphism of lattices

$\displaystyle\psi_{U}:\mathsf{CompOpen}\big{(}\llbracket\,{U}\,\rrbracket\big{)}\leavevmode\nobreak\
\cong\leavevmode\nobreak\ \downarrow U$

that preserves realizations, i.e.
$\llbracket\,{V}\,\rrbracket\cong\llbracket\,{\psi_{U}(V)}\,\rrbracket$
naturally for $V:{\llbracket\,{U}\,\rrbracket}\Rightarrow{\mathcal{L}}$.

###### Proof.

Constructing the inverse map $\psi_{U}^{-1}:\leavevmode\nobreak\
\downarrow\\!U\to\big{(}{\llbracket\,{U}\,\rrbracket}\Rightarrow{\mathcal{L}}\big{)}$
is actually the straightforward part. We have a map

$\displaystyle\big{(}{X}\Rightarrow{\mathcal{L}}\big{)}\leavevmode\nobreak\
\to\leavevmode\nobreak\
\big{(}{\llbracket\,{U}\,\rrbracket}\Rightarrow{\mathcal{L}}\big{)}$

which is given as follows: For $V:{X}\Rightarrow{\mathcal{L}}$ we compose with
the canonical inclusion $i_{U}:{\llbracket\,{U}\,\rrbracket}\Rightarrow{X}$,
i.e. take $V\circ i_{U}$. Note that we have $V\circ i_{U}=(U\wedge V)\circ
i_{U}$. We can then take $\psi_{U}^{-1}$ to be the restriction of this map to
$\downarrow\\!U$, which clearly is a lattice morphism. We also get that
$\llbracket\,{V}\,\rrbracket\cong\llbracket\,{\psi_{U}^{-1}(V)}\,\rrbracket$
for $V\leq U$, as for any ring $R$ and point $x:X(R)$, $V(x)=D(1)$ implies
$U(x)=D(1)$.

To construct $\psi_{U}$ let
$V:{\llbracket\,{U}\,\rrbracket}\Rightarrow{\mathcal{L}}$, $R$ a ring and
$x:X(R)$. Assume that we have $f_{1},...,f_{n}:R$ such that
$U(x)=D(f_{1},...,f_{n})$. Let $x_{i}:\equiv
X(\nicefrac{{\\_}}{{1}})(x):X\big{(}R[\nicefrac{{1}}{{f_{i}}}]\big{)}$ be the
restriction of $x$ along the canonical $\nicefrac{{\\_}}{{1}}:R\to
R[\nicefrac{{1}}{{f_{i}}}]$, where $i$ in $1,...,n$. Now, $U(x_{i})=D(1)$ and
we may apply $V$ to $x_{i}$, giving us
$V(x_{i}):\mathcal{L}_{R[\nicefrac{{1}}{{f_{i}}}]}$. Using the isomorphisms
$\psi_{f_{i}}:\mathcal{L}_{R[\nicefrac{{1}}{{f_{i}}}]}\cong\,\downarrow\\!D(f_{i})$
from Lemma 2.4, we get $\psi_{f_{i}}(V(x_{i})):\leavevmode\nobreak\
\downarrow\\!D(f_{i})$ for each $i$ in $1,...,n$. We want to set

$\displaystyle\psi_{U}(V)(x)\leavevmode\nobreak\ :\equiv\leavevmode\nobreak\
\textstyle\bigvee_{i=1}^{n}\psi_{f_{i}}(V(x_{i}))\leavevmode\nobreak\
\leq\leavevmode\nobreak\ U(x)$

but we need to check that this is well-defined, i.e. independent of the choice
of the $f_{i}$. So let $g_{1},...,g_{m}:R$ be such that
$D(f_{1},...,f_{n})=D(g_{1},...,g_{m})=U(x)$. For $i$ in $1,...,n$ and $j$ in
$1,...,m$, let $x_{ij}:X\big{(}R[\nicefrac{{1}}{{f_{i}g_{j}}}]\big{)}$ be the
restriction of $x$ along $\nicefrac{{\\_}}{{1}}:R\to
R[\nicefrac{{1}}{{f_{i}g_{j}}}]$ and
$\psi_{f_{i}g_{j}}:\mathcal{L}_{R[\nicefrac{{1}}{{f_{i}g_{j}}}]}\cong\,\downarrow\\!D(f_{i}g_{j})$
be the corresponding isomorphism given by Lemma 2.4. For the canonical map
$\gamma_{ij}:R[\nicefrac{{1}}{{f_{i}}}]\to R[\nicefrac{{1}}{{f_{i}g_{j}}}]$ we
get that the following diagram commutes

${\mathcal{L}_{R[\nicefrac{{1}}{{f_{i}}}]}}$${\downarrow\\!D(f_{i})}$${\mathcal{L}_{R[\nicefrac{{1}}{{f_{i}g_{j}}}]}}$${\downarrow\\!D(f_{i}g_{j})}$$\scriptstyle{\simeq}$$\scriptstyle{\psi_{f_{i}}}$$\scriptstyle{\gamma_{ij}^{\mathcal{L}}}$$\scriptstyle{\\_\wedge
D(g_{j})}$$\scriptstyle{\simeq}$$\scriptstyle{\psi_{f_{i}g_{j}}}$

Moreover, we get $\gamma_{ij}^{\mathcal{L}}(V(x_{i}))=V(x_{ij})$ by the
naturality of $X$ and $V$. This gives us

$\displaystyle\psi_{f_{i}}(V(x_{i}))\leavevmode\nobreak\ =\leavevmode\nobreak\
\textstyle\bigvee_{j=1}^{m}\big{(}\psi_{f_{i}}(V(x_{i}))\wedge
D(g_{j})\big{)}\leavevmode\nobreak\ =\leavevmode\nobreak\
\textstyle\bigvee_{j=1}^{m}\psi_{f_{i}g_{j}}(V(x_{ij}))$

Repeating the above argument with $i$ and $j$ swapped shows well-definedness:

$\displaystyle\textstyle\bigvee_{i=1}^{n}\psi_{f_{i}}(V(x_{i}))\leavevmode\nobreak\
=\leavevmode\nobreak\
\textstyle\bigvee_{i,j}\psi_{f_{i}g_{j}}(V(x_{ij}))\leavevmode\nobreak\
=\leavevmode\nobreak\ \textstyle\bigvee_{j=1}^{m}\psi_{g_{j}}(V(x_{j}))$

To show the naturality of this construction, take $\varphi:\mathsf{Hom}(R,A)$
and $x:X(R)$ with its restriction along $\varphi$ denoted
$x\\!\\!\restriction_{\varphi}\,:\equiv X(\varphi)(x)$. Since we have to prove
a proposition, we can assume that we have $f_{1},...,f_{n}:R$ such that
$U(x)=D(f_{1},...,f_{n})$ and thus $\psi_{U}(V)(x)\leavevmode\nobreak\
=\leavevmode\nobreak\ \textstyle\bigvee_{i=1}^{n}\psi_{f_{i}}(V(x_{i}))$, with
$x_{i}$ defined as above for $i$ in $1,...,n$. It follows that

$\displaystyle\varphi^{\mathcal{L}}\big{(}\psi_{U}(V)(x))\leavevmode\nobreak\
$ $\displaystyle=\leavevmode\nobreak\
\textstyle\bigvee_{i=1}^{n}\varphi^{\mathcal{L}}(\psi_{f_{i}}(V(x_{i})))$
$\displaystyle=\leavevmode\nobreak\
\textstyle\bigvee_{i=1}^{n}\psi_{f_{i}}\big{(}(\nicefrac{{\varphi}}{{1}})^{\mathcal{L}}(V(x_{i}))\big{)}$
$\displaystyle=\leavevmode\nobreak\
\textstyle\bigvee_{i=1}^{n}\psi_{\varphi(f_{i})}\big{(}V(x\\!\\!\restriction_{\nicefrac{{\varphi}}{{1}}})\big{)}$
$\displaystyle=\leavevmode\nobreak\
\psi_{U}(V)(x\\!\\!\restriction_{\varphi})$

Here $x\\!\\!\restriction_{\nicefrac{{\varphi}}{{1}}}$ is the restriction
along the canonical $\nicefrac{{\varphi}}{{1}}:R\to
A[\nicefrac{{1}}{{\varphi(f_{i})}}]$ for each respective $i$ in $1,...,n$. The
second equality above holds because the following diagram commutes:

${\mathcal{L}_{R[\nicefrac{{1}}{{f_{i}}}]}}$${\downarrow\\!D(f_{i})}$${\mathcal{L}_{A[\nicefrac{{1}}{{\varphi(f_{i})}}]}}$${\downarrow\\!D(\varphi(f_{i}))}$$\scriptstyle{\simeq}$$\scriptstyle{\psi_{f_{i}}}$$\scriptstyle{(\nicefrac{{\varphi}}{{1}})^{\mathcal{L}}}$$\scriptstyle{\varphi^{\mathcal{L}}}$$\scriptstyle{\simeq}$$\scriptstyle{\psi_{\varphi(f_{i})}}$

The last equality holds since
$U(x\\!\\!\restriction_{\varphi})=D(\varphi(f_{1}),...,\varphi(f_{n}))$. This
finishes the proof that $\psi_{U}(V)$ is a natural transformation. We omit the
proof that $\psi_{U}$ is inverse to $\psi^{-1}_{U}$. ∎

######  Lemma 4.32.

Let $X$ be $\mathbb{Z}$-functor and $U,V:{X}\Rightarrow{\mathcal{L}}$ be
compact opens. If both $\llbracket\,{U}\,\rrbracket$ and
$\llbracket\,{V}\,\rrbracket$ merely have an affine cover, then
$\llbracket\,{U\vee V}\,\rrbracket$ merely has an affine cover.

###### Proof.

Let $U_{1},..,U_{n}:{\llbracket\,{U}\,\rrbracket}\Rightarrow{\mathcal{L}}$ and
$V_{1},..,V_{m}:{\llbracket\,{V}\,\rrbracket}\Rightarrow{\mathcal{L}}$ be
affine covers of $\llbracket\,{U}\,\rrbracket$ and
$\llbracket\,{V}\,\rrbracket$ respectively. Using the isomorphisms $\psi_{U}$
and $\psi_{V}$ given by applying Lemma 4.31 to $U$ and $V$, we get compact
opens $\psi_{U}(U_{i})$ and $\psi_{V}(V_{j})$ of $X$ that are affine and cover
$U\vee V$, i.e.

$\displaystyle\big{(}\textstyle\bigvee_{i=1}^{n}\psi_{U}(U_{i})\big{)}\,\vee\,\big{(}\bigvee_{j=1}^{m}\psi_{V}(V_{j})\big{)}\leavevmode\nobreak\
=\leavevmode\nobreak\ U\vee V$

Using Lemma 4.31 for $U\vee V$, we get that the $\psi_{U\vee
V}^{-1}(\psi_{U}(U_{i}))$ and $\psi_{U\vee V}^{-1}(\psi_{V}(V_{j}))$ together
give an affine cover of $\llbracket\,{U\vee V}\,\rrbracket$. ∎

######  Theorem 4.33.

The realization $\llbracket\,{U}\,\rrbracket$ of a compact open
$U:{X}\Rightarrow{\mathcal{L}}$ of a qcqs-scheme $X$ is a qcqs-scheme.

###### Proof.

$\llbracket\,{U}\,\rrbracket$ is local by Lemma 4.27. To show that it has an
affine cover, let $U_{1},...,U_{n}:{X}\Rightarrow{\mathcal{L}}$ be an affine
cover of $X$. For $i$ in $1,...,n$, the compact open
$\psi_{U_{i}}^{-1}(U\wedge U_{i})$ of $\llbracket\,{U_{i}}\,\rrbracket$ has an
affine cover by Lemma 4.30.272727For
$\llbracket\,{U_{i}}\,\rrbracket\cong\mathsf{Sp}(A_{i})$, one may think of
$\psi_{U_{i}}^{-1}(U\wedge U_{i})$ as representing the compact open subscheme
$\llbracket\,{U\wedge U_{i}}\,\rrbracket\hookrightarrow\mathsf{Sp}(A_{i})$. As
explained in the proof of Lemma 4.31, we get natural isomorphisms of
$\mathbb{Z}$-functors

$\displaystyle\llbracket\,{\psi_{U_{i}}^{-1}(U\wedge
U_{i})}\,\rrbracket\leavevmode\nobreak\ \cong\leavevmode\nobreak\
\llbracket\,{U\wedge U_{i}}\,\rrbracket\leavevmode\nobreak\
\cong\leavevmode\nobreak\ \llbracket\,{\psi_{U}^{-1}(U\wedge
U_{i})}\,\rrbracket$

which can be made into equalities of $\mathbb{Z}$-functors, as categories of
functors into a univalent category are always univalent. We can transport the
property of having an affine cover along these equalities, giving us that each
$\psi_{U}^{-1}(U\wedge U_{i})$ (a compact open of
$\llbracket\,{U}\,\rrbracket$) has an affine cover. We can then iterate Lemma
4.32 to obtain an affine cover of $\llbracket\,{U}\,\rrbracket$. ∎

##  5 Equivalence of approaches

Having given two constructive definitions of qcqs-scheme, we want show that
these two notions coincide. The proof strategy is mostly analogous to that of
the classical _comparison theorem_ given by Demazure and Gabriel [DG80, Ch. I,
§1, no 4.4]. We construct an adjunction between $\mathbb{Z}$-functors and the
opposite category of locally ringed lattices. For proving properties of the
left adjoint that “realizes” a $\mathbb{Z}$-functor as a locally ringed
lattice (in particular Proposition 5.19 and Proposition 5.20), we take
inspiration from the lecture notes of Nieper-Wißkirchen [NW08]. The notes
often include concrete computations that can be constructivized even when
being explicit about universe levels. Technically, the purported adjunction
will be a coadjunction relative to universe lifting, as in Proposition 4.6. We
then show that when restricted to the respective full subcategories of qcqs-
schemes, this becomes an equivalence of categories. In order to dispose of
relativity with respect to universe lifting, we use univalence.

###  5.1 Functor of points of a locally ringed lattice

Developing scheme theory starting from $\mathbb{Z}$-functors is an exception
rather than norm in the introductory literature on algebraic geometry. Most
often schemes are defined as locally ringed spaces and in a second step they
are assigned a $\mathbb{Z}$-functor, called the functor of points of a scheme
or locally ringed space.282828See e.g. [EH06, Ch. 6] for an in-depth
discussion in a classical source. We can do the same for locally ringed
lattices. In this section we want to define the functor of points for locally
ringed lattices and prove some basic properties for the functor of points of a
qcqs-scheme. In order to avoid confusion, we will henceforth use qcqs-scheme
only for lattice-theoretic qcqs-schemes and speak of functorial qcqs-schemes
otherwise.

######  Definition 5.1.

The _functor of points_ associated to a locally ringed lattice
$X:\equiv(L_{X},\mathcal{O}_{X})$ is the $\mathbb{Z}$-functor given by

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

This defines a functor
$\mathsf{LRDL}_{\ell}^{op}\to\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}$ where the
action on moprhisms is given point-wise by post-composition.

######  Lemma 5.2.

The functor of points $h_{X}$ of a locally ringed lattice $X$ is local.

###### Proof.

Let $f_{1},...,f_{n}:R$ be such that $1\in\langle f_{1},...,f_{n}\rangle$.
Since
$\mathsf{Spec}(R)\\!\\!\restriction_{D(f_{i})}\cong\mathsf{Spec}(R[\nicefrac{{1}}{{f_{i}}}])$
as locally ringed lattices [CLS09, Ex. 1], we get by Proposition 3.20 that in
$\mathsf{LRDL}^{op}$

$\displaystyle\mathsf{Spec}(R)\leavevmode\nobreak\ \cong\leavevmode\nobreak\
\mathsf{colim}\,\big{\\{}\mathsf{Spec}(R[\nicefrac{{1}}{{f_{i}}}])\leftarrow\mathsf{Spec}(R[\nicefrac{{1}}{{f_{i}f_{j}}}])\rightarrow\mathsf{Spec}(R[\nicefrac{{1}}{{f_{j}}}])\big{\\}}$

Thus the following is an equalizer diagram

$\displaystyle
h_{X}(R)\to\prod_{i=1}^{n}h_{X}(R[\nicefrac{{1}}{{f_{i}}}])\rightrightarrows\prod_{i,j}h_{X}(R[\nicefrac{{1}}{{f_{i}f_{j}}}])$

which finishes the proof. ∎

######  Lemma 5.3.

$h_{\mathsf{Spec}(R)}$ is naturally isomorphic to $\mathsf{Sp}(R)$.

###### Proof.

$\mathsf{Spec}$ is fully faithful. ∎

######  Lemma 5.4.

For a locally ringed lattice $X:\equiv(L_{X},\mathcal{O}_{X})$, we have a
lattice homomorphism $\varepsilon^{*}:L_{X}\to\mathsf{CompOpen}(h_{X})$ such
that for each $u:L_{X}$ we get a natural isomorphism
$\llbracket\,{\varepsilon^{*}(u)}\,\rrbracket\cong
h_{X\,\\!\\!\restriction_{u}}$.292929This $\varepsilon^{*}$ turns out to be
the lattice morphism corresponding to the relative counit induced by
Proposition 5.20, hence the name. We will not use this fact explicitly,
however.

###### Proof.

Let $u:L_{X}$. For a ring $R$ and
$\pi:\mathsf{LRDL}_{\ell}^{op}\big{(}\mathsf{Spec}(R),X\big{)}$ we can define
a compact open by setting $\varepsilon^{*}(u)_{R}(\pi):\equiv\pi^{*}(u)$. This
clearly defines a morphism of lattices. Moreover, this gives us

$\displaystyle\llbracket\,{\varepsilon^{*}(u)}\,\rrbracket(R)\leavevmode\nobreak\
$ $\displaystyle\simeq\leavevmode\nobreak\
{\\{\,\pi:\mathsf{LRDL}_{\ell}^{op}\big{(}\mathsf{Spec}(R),X\big{)}\leavevmode\nobreak\
|\leavevmode\nobreak\ \pi^{*}(u)=D(1)\,\\}}$
$\displaystyle\simeq\leavevmode\nobreak\
\mathsf{LRDL}_{\ell}^{op}\big{(}\mathsf{Spec}(R),X\\!\\!\restriction_{u}\big{)}$

where the second equivalence is given composition with the “inclusion”
$(\\_\wedge
u):\mathsf{LRDL}_{\ell}^{op}\big{(}X\\!\\!\restriction_{u},X\big{)}$. We omit
the proof that this is natural in $R$. ∎

######  Lemma 5.5.

If $X:\equiv(L_{X},\mathcal{O}_{X})$ is a qcqs-scheme, then $h_{X}$ is a
functorial qcqs-scheme.

###### Proof.

By Lemma 5.2, $X$ is local. Assume that $u_{1},...,u_{n}:L_{X}$ is an affine
cover with $X\\!\\!\restriction_{u_{i}}\cong\mathsf{Spec}(R_{i})$ as locally
ringed lattices. Then the $\varepsilon^{*}(u_{i})$ cover $h_{X}$ and are
affine as

$\displaystyle\llbracket\,{\varepsilon^{*}(u)}\,\rrbracket\cong
h_{X\,\\!\\!\restriction_{u_{i}}}\cong
h_{\mathsf{Spec}(R_{i})}\cong\mathsf{Sp}(R_{i})$

By Lemma 5.4 and Lemma 5.3 ∎

This allows us to regard $h_{(\\_)}$ as a functor
$\mathsf{QcQsSch}_{\ell}\to\mathsf{FunQcQsSch}_{\ell}$. This restricted
functor of points functor is fully faithful.

######  Proposition 5.6.

The functor $h_{(\\_)}:\mathsf{QcQsSch}_{\ell}\to\mathsf{FunQcQsSch}_{\ell}$
is fully faithful.

###### Proof.

Let $X,Y$ be qcqs-schemes and let $u_{1},...,u_{n}:L_{X}$ be an affine cover
with $X\\!\\!\restriction_{u_{i}}\cong\mathsf{Spec}(R_{i})$. By Lemma 4.24,
any $\alpha:{h_{X}}\Rightarrow{h_{Y}}$ is uniquely determined by the induced
restrictions
$\alpha_{i}:\big{(}{\llbracket\,{\varepsilon^{*}(u_{i})}\,\rrbracket}\Rightarrow{h_{Y}}\big{)}$.
Combining the proof of Lemma 5.5 with Yoneda and our assumptions, we get a
chain of equivalences

$\displaystyle\big{(}{\llbracket\,{\varepsilon^{*}(u_{i})}\,\rrbracket}\Rightarrow{h_{Y}}\big{)}\leavevmode\nobreak\
$ $\displaystyle\simeq\leavevmode\nobreak\
\big{(}{\mathsf{Sp}(R_{i})}\Rightarrow{h_{Y}}\big{)}$
$\displaystyle\simeq\leavevmode\nobreak\
\mathsf{LRDL}_{\ell}^{op}\big{(}\mathsf{Spec}(R_{i}),Y\big{)}\leavevmode\nobreak\
\simeq\leavevmode\nobreak\
\mathsf{LRDL}_{\ell}^{op}\big{(}X\\!\\!\restriction_{u_{i}},Y\big{)}$

Now, let
$\pi_{i}:\mathsf{LRDL}^{op}\big{(}X\\!\\!\restriction_{u_{i}},Y\big{)}$ be the
morphism that we obtain by applying the chain of equivalences to $\alpha_{i}$.
By Proposition 3.20, the $\pi_{i}$ determine a
$\pi:\mathsf{LRDL}^{op}\big{(}{X},Y\big{)}$. Cumbersome computations reveal
that modulo precomposition with the natural isomorphism
$\llbracket\,{\varepsilon^{*}(u_{i})}\,\rrbracket\cong
h_{X\,\\!\\!\restriction_{u_{i}}}$, given by Lemma 5.4, $h_{\pi_{i}}$ is just
$\alpha_{i}$. Hence, $\pi$ is unique such that $h_{\pi}=\alpha$. ∎

###  5.2 Geometric realization of a $\mathbb{Z}$-functor

We have seen that to a $\mathbb{Z}$-functor $X$ we can assign a (big)
distributive lattice. We can actually make this into a locally ringed lattice
that on representables $\mathsf{Sp}(R)$ is just $\mathsf{Spec}(R)$, modulo
universe lifting.

######  Definition 5.7.

For a presheaf $X$, the locally ringed lattice $\lvert
X\rvert:\mathsf{LRDL}_{\ell+1}^{op}$ is the lattice $L_{\lvert
X\rvert}:\equiv\mathsf{CompOpen}(X)$ with a sheaf $\mathcal{O}_{\lvert
X\rvert}$ assigning to each $U:{X}\Rightarrow{\mathcal{L}}$ the ring of
functions ${\llbracket\,{U}\,\rrbracket}\Rightarrow{\mathbb{A}^{1}}$ on $U$’s
realization, i.e.

$\displaystyle\mathcal{O}_{\lvert X\rvert}(U)\leavevmode\nobreak\
:\equiv\leavevmode\nobreak\
\mathcal{O}\big{(}\llbracket\,{U}\,\rrbracket\big{)}$

The invertibility support on $(\mathsf{CompOpen}(X),\mathcal{O}_{\lvert
X\rvert})$ is given as follows: For a compact open
$U:{X}\Rightarrow{\mathcal{L}}$ and function
$s:{\llbracket\,{U}\,\rrbracket}\Rightarrow{\mathbb{A}^{1}}$ we get a natural
transformation $U_{s}:{\llbracket\,{U}\,\rrbracket}\Rightarrow{\mathcal{L}}$,
which for $x:X(R)$ with $U(x)=D(1)$ is given by $U_{s}(x):\equiv D(s(x))$. By
Lemma 4.31 this corresponds to a compact open in $\downarrow\\!U$, i.e. we can
define

$\displaystyle\mathcal{D}_{U}(s)\leavevmode\nobreak\
:\equiv\leavevmode\nobreak\ \psi_{U}(U_{s})$

For a natural transformation $\alpha:{X}\Rightarrow{Y}$ we get a morphism of
locally ringed lattices
$\lvert\alpha\rvert:\mathsf{LRDL}_{\ell+1}^{op}\big{(}\lvert X\rvert,\lvert
Y\rvert\big{)}$ as follows: The lattice morphism $\lvert\alpha\rvert^{*}$ acts
on compact opens by precomposition with $\alpha$. For
$U:{Y}\Rightarrow{\mathcal{L}}$, we get a canonical transformation
$\alpha\\!\\!\restriction_{U}:{\llbracket\,{U\circ\alpha}\,\rrbracket}\Rightarrow{\llbracket\,{U}\,\rrbracket}$
and we can define

$\displaystyle\lvert\alpha\rvert^{\sharp}_{U}:\equiv(\\_\circ\alpha\\!\\!\restriction_{U})\leavevmode\nobreak\
:\leavevmode\nobreak\ \mathsf{Hom}\big{(}\mathcal{O}_{\lvert
Y\rvert}(U),\mathcal{O}_{\lvert
X\rvert}(\underbrace{U\circ\alpha}_{\equiv\,\lvert\alpha\rvert^{*}(U)})\big{)}$

This defines the desired natural transformation
$\lvert\alpha\rvert^{\sharp}:{\mathcal{O}_{\lvert
Y\rvert}}\Rightarrow{\lvert\alpha\rvert_{*}\mathcal{O}_{\lvert X\rvert}}$. The
functor
$\lvert\\_\rvert:\mathbb{Z}\text{-}\mathsf{Fun}_{\ell}\to\mathsf{LRDL}_{\ell+1}^{op}$
is called the _geometric realization functor_.

There are several things to check in order to show that the above is a
sensible definition. Apart from various functoriality, naturality and
homomorphism conditions, we have to check the following four lemmas.

######  Lemma 5.8.

For any $\mathbb{Z}$-functor $X$, $\mathcal{O}_{\lvert X\rvert}$ is a sheaf on
the lattice $\mathsf{CompOpen}(X)$.

###### Proof.

For $U=\bigvee_{i=1}^{n}U_{i}$, we get a cover of
$\mathsf{CompOpen}\big{(}\llbracket\,{U}\,\rrbracket\big{)}$ by the compact
opens $\psi_{U}^{-1}(U_{i})$. Since $\mathbb{A}^{1}$ is affine and hence
local, we can use Lemma 4.24 to see that any function
$\mathcal{O}\big{(}\llbracket\,{U}\,\rrbracket\big{)}$ is uniquely determined
by its restriction to the
$\mathcal{O}\big{(}\llbracket\,{\psi_{U}^{-1}(U_{i})}\,\rrbracket\big{)}\cong\mathcal{O}\big{(}\llbracket\,{U_{i}}\,\rrbracket\big{)}$.
This means that we have an equalizer diagram

$\displaystyle\mathcal{O}\big{(}\llbracket\,{U}\,\rrbracket\big{)}\to\prod_{i=1}^{n}\mathcal{O}\big{(}\llbracket\,{U_{i}}\,\rrbracket\big{)}\rightrightarrows\prod_{i,j}\mathcal{O}\big{(}\llbracket\,{U_{i}\wedge
U_{j}}\,\rrbracket\big{)}$

which finishes the proof. ∎

######  Lemma 5.9.

For any $\mathbb{Z}$-functor $X$, compact open $U:{X}\Rightarrow{\mathcal{L}}$
and function $s:{\llbracket\,{U}\,\rrbracket}\Rightarrow{\mathbb{A}^{1}}$,
$\mathcal{D}_{U}(s)$ is an invertibility supremum in $\downarrow\\!U$.

###### Proof.

By Lemma 4.31, it suffices to check that $U_{s}$ is the largest element of
$\mathsf{CompOpen}\big{(}\llbracket\,{U}\,\rrbracket\big{)}$ where (the
restriction of) $s$ becomes invertible. This follows immediately from the fact
that, for $x:X(R)$ with $U(x)=D(1)$, we have $U_{s}(x)\equiv D(s(x))=D(1)$ if
and only if $s(x)\in R^{\times}$. ∎

######  Lemma 5.10.

For any $\mathbb{Z}$-functor $X$ and compact open
$U:{X}\Rightarrow{\mathcal{L}}$, $\mathcal{D}_{U}$ is a support.

###### Proof.

Again by Lemma 4.31, it suffices to verify that

$\displaystyle
U_{(\\_)}:\big{(}{\llbracket\,{U}\,\rrbracket}\Rightarrow{\mathbb{A}^{1}}\big{)}\to\big{(}{\llbracket\,{U}\,\rrbracket}\Rightarrow{\mathcal{L}}\big{)}$

is a support. This can be checked point-wise. For example, $U_{s+t}\leq
U_{s}\vee U_{t}$ follows from the fact that $D(s(x)+t(x))\leq D(s(x))\vee
D(t(x))$ for $x:X(R)$ with $U(x)=D(1)$. ∎

######  Lemma 5.11.

For a natural transformation $\alpha:{X}\Rightarrow{Y}$, the realization
$\lvert\alpha\rvert$ is a morphism of locally ringed lattices, i.e. for a
compact open $U:{Y}\Rightarrow{\mathcal{L}}$ and function
$s:{\llbracket\,{U}\,\rrbracket}\Rightarrow{\mathbb{A}^{1}}$ we have

$\displaystyle\lvert\alpha\rvert^{*}\big{(}\mathcal{D}_{U}(s)\big{)}\leavevmode\nobreak\
=\leavevmode\nobreak\
\mathcal{D}_{\lvert\alpha\rvert^{*}(U)}(\lvert\alpha\rvert^{\sharp}(s))$

###### Proof.

Unfolding the definition of $\lvert\alpha\rvert$, we have to show that
$\psi_{U}(U_{s})\circ\alpha$ is equal to
$\psi_{U\circ\alpha}\big{(}(U\circ\alpha)_{s\circ\alpha\leavevmode\nobreak\
\\!\\!\restriction_{U}}\big{)}$ as a natural transformation
${X}\Rightarrow{\mathcal{L}}$. Applying either natural transformation to
$x:X(R)$ with $U(\alpha(x))=D(f_{1},...,f_{n})$ computes to the same value in
$\mathcal{L}_{R}$, namely
$\bigvee_{i=1}^{n}\psi_{f_{i}}\big{(}D(s(\alpha(x_{i})))\big{)}$, where
$x_{i}:X(R[\nicefrac{{1}}{{f_{i}}}])$ is the canonical restriction and
$\psi_{f_{i}}$ is given by Lemma 2.4. This proves the desired equality. ∎

Now, let
$\mathsf{lift}:\mathsf{LRDL}_{\ell}^{op}\to\mathsf{LRDL}_{\ell+1}^{op}$ be the
functor that is induced by universe lifting. Note that this overload of
notation, with $\mathsf{lift}$ being the operation on universes as well as the
induced functor for rings and locally ringed lattices, is justified by the
fact that lifting commutes with all the type formers. This is used in the
following lemma, which is needed to prove that the realization of a functorial
qcqs-scheme is a (big) qcqs-scheme.

######  Lemma 5.12.

We have
$\lvert\mathsf{Sp}(R)\rvert\cong\mathsf{lift}(\mathsf{Spec}(R))\cong\mathsf{Spec}(\mathsf{lift}(R))$
in $\mathsf{LRDL}_{\ell+1}^{op}$, for any $R:\mathsf{CommRing}_{\ell}$.

######  Lemma 5.13.

For $U:{X}\Rightarrow{\mathcal{L}}$, we have $\lvert
X\rvert\\!\\!\restriction_{U}\cong\lvert\llbracket\,{U}\,\rrbracket\rvert$ in
$\mathsf{LRDL}_{\ell+1}^{op}$.

###### Proof.

Follows directly from Lemma 4.31. ∎

######  Corollary 5.14.

If $X$ is a functorial qcqs-scheme, then $\lvert X\rvert$ is a qcqs-scheme in
$\mathsf{LRDL}_{\ell+1}^{op}$.

Realizations of functorial qcqs-schemes are not just any kind of big qcqs-
scheme, they admit a cover by small affine schemes.

######  Definition 5.15.

We say that $X:\mathsf{LRDL}_{\ell+1}$ is an _essentially small_ qcqs-scheme,
if there merely exists a cover $u_{1},\dots,u_{n}:L_{X}$ together with small
rings $R_{1},...,R_{n}:\mathsf{CommRing}_{\ell}$ and isomorphisms
$X\\!\\!\restriction_{u_{i}}\cong\mathsf{Spec}(\mathsf{lift}(R_{i}))$.

######  Corollary 5.16.

If $X$ is a functorial qcqs-scheme, then $\lvert X\rvert$ is an essentially
small qcqs-scheme.