# Categorical Foundations of Formalized Condensed Mathematics

Dagur Asgeirsson, Riccardo Brasca, Nikolas Kuhn, Filippo Alberto Edoardo

Nuccio Mortarino Majno di Capriglio, Adam Topaz

► To cite this version:

Dagur Asgeirsson, Riccardo Brasca, Nikolas Kuhn, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio, Adam Topaz. Categorical Foundations of Formalized Condensed Mathematics. The Journal of Symbolic Logic, In press, 10.1017/jsl.2024.69. hal-04633614v2

HAL Id: hal-04633614

https://hal.science/hal-04633614v2

Submitted on 16 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# CATEGORICAL FOUNDATIONS OF FORMALIZED CONDENSED MATHEMATICS

DAGUR ASGEIRSSON, RICCARDO BRASCA, NIKOLAS KUHN, FILIPPO ALBERTO EDOARDO NUCCIO MORTARINO MAJNO DI CAPRIGLIO, AND ADAM TOPAZ

**Abstract.** Condensed mathematics, developed by Clausen and Scholze over the last few years, proposes a generalization of topology with better categorical properties. It replaces the concept of a topological space by that of a condensed set, which can be defined as a sheaf for the coherent topology on a certain category of compact Hausdorff spaces. In this case, the sheaf condition has a fairly simple explicit description, which arises from studying the relationship between the coherent, regular and extensive topologies. In this paper, we establish this relationship under minimal assumptions on the category, going beyond the case of compact Hausdorff spaces. Along the way, we also provide a characterization of sheaves and covering sieves for these categories. All results in this paper have been fully formalized in the LEAN proof assistant.

## 1. INTRODUCTION

The main goal of condensed mathematics (see e.g. [Sch19a, Sch19b, CS22]) is to provide a better framework to study the interplay between algebra and geometry. To do this, one has to generalize the notion of a topological space to obtain better categorical properties; the category of condensed sets achieves this remarkably well. A condensed set is defined as a sheaf for the so-called coherent topology on the category of compact Hausdorff spaces. The category of condensed sets contains a very large class of topological spaces as a full subcategory. In addition, it almost forms a topos<fnref n="1" />, and the category of condensed abelian groups is a particularly well-behaved abelian category.

The formalization of the theory of condensed sets started with the *Liquid Tensor Experiment*, see [CT+22, Sch22]. In that work the authors formalized the definition and various properties of the category of condensed abelian groups and of liquid vector spaces, including the main result [Sch19a, Theorem 9.1], using the LEAN proof assistant. In §2 we will offer a brief outline both of LEAN and of its main mathematical library MATHLIB.

Even if the achievements of the *Liquid Tensor Experiment* are spectacular, most of the work is not suitable to be integrated into a large mathematical library like MATHLIB. Indeed, a lot of results in the Liquid Tensor Experiment were stated and proven in an *ad-hoc* way and are not applicable in other contexts. This approach contradicts many of the design decisions prevalent throughout MATHLIB, which we briefly discuss in §2.2.

The main goal of our work is to formalize the foundations of the theory of condensed sets in an organic way, being as general as possible in all the various prerequisites. Indeed, the present work has already been incorporated in the MATHLIB library. Besides correctness, which is checked by LEAN, this ensures that the results are stated in a way that is compatible with the rest of the library and that they can be used by others.

The goal of this paper is to prove, in the most general setting, results relating the coherent, regular and extensive topologies on a category, as well as characterizations of their sheaves. While the results we discuss in this paper are known to some experts as part of the folklore, we provide both a detailed exposition, while simultaneously minimizing various assumptions. The more general approach we take in this paper was motivated primarily by the formalization of these results.

Throughout the text, we use the symbol ☞ for external links. Almost every mathematical statement and definition will be accompanied by such a link directly to the source code for the corresponding statement in MATHLIB. The only exceptions are results that we use in the informal proof but not in the formal one. In particular, all relevant results are completely formalized in MATHLIB. In order for the links to stay usable, they are all to a fixed commit to the master branch (the most recent one at the time of writing).

<footnote n="1">¹There are some set-theoretic issues that prevent it from satisfying all the axioms of a topos; these can be resolved in various ways and, for all practical purposes, the category of condensed sets can be regarded as a topos.</footnote>
Here is a brief outline of the paper. In §2 we give a brief overview of the LEAN proof assistant and its mathematical library MATHLIB, explaining the general philosophy behind the library and the main design decisions that have been taken, focusing on the aspects that are most relevant to the present work. In §3, we review the theory of sheaves for Grothendieck topologies as it is formalized in MATHLIB: this section is standard, but we think it is a good idea to fix the notation and the terminology, as the literature is not always consistent. In §4, we introduce the notions of strict, regular and effective epimorphism. We prove in Proposition 4.12 that the effective epimorphisms in the category $\mathcal{C}$ of topological spaces are the quotient maps and Proposition 4.13 characterizes effective epimorphisms in $\mathcal{C}$ as the continuous surjections. Strict, regular, and effective epimorphisms are then used in §5 to define the regular (resp. extensive, coherent) topology on a category satisfying the technical condition of being preregular (resp. finitary extensive, precoherent). We prove in Proposition 5.8 that a preregular and finitary extensive category is precoherent and in Proposition 5.9 that the coherent topology is generated by the union of the regular and extensive topologies. In §6, we study sheaves on these three topologies: first of all we prove in Propositions 6.1, 6.6, and 6.8 that the three topologies are subcanonical. We then give in Propositions 6.4, 6.5, 6.13, and 6.14 various conditions for a presheaf to be a sheaf (characterizing sheaves in terms of the preservation of finite products and equalizers). We then give in Proposition 6.15 a condition for a functor<fnref n="2" /> to induce an equivalence between the categories of sheaves for certain topologies. In §7 we apply our general categorical framework to the theory of condensed sets, proving our main theorems, that we now summarize.

Consider the following three categories, each containing the next as a full subcategory, and whose morphisms are continuous maps:

* **CompHaus**: the category of compact Hausdorff spaces ⌜.

* **Profinite**: the category of *profinite spaces*, that we define, following MATHLIB, as totally disconnected compact Hausdorff spaces. This category is equivalent to the pro-category of the category of finite sets (this last statement has not yet been formalized; see [Asg24, Section 6] for a more detailed discussion of the state of the category *Profinite* in MATHLIB) ⌜.

* **Stonean**: the category of *Stonean spaces*, whose objects are extremally disconnected compact Hausdorff spaces ⌜. The condition of being extremally disconnected means that the closure of every open set is open. These spaces are precisely the projective objects in **CompHaus** (see [Gle58, Theorem 2.5] and ⌜). It is easy to see that Stonean spaces are totally disconnected, so we have a fully faithful inclusion **Stonean** ⊆ **Profinite** ⌜.

Let $\mathcal{C}$ be any of these categories. We prove in Proposition 5.8 and Proposition 7.1 that the categories $\mathcal{C}$ fit into the general framework we describe in this paper. As a consequence, we recover the following two key results (stated here as Theorem 7.4 and 7.7) which have appeared early on in the theory of condensed mathematics [Sch19b, Definition 1.2 and Proposition 2.7].

**Theorem.** We have the following characterizations of sheaves on $\mathcal{C}$.

* When $\mathcal{C}$ is **CompHaus** or **Profinite**, a presheaf $X: \mathcal{C}^{\text{op}} \to \text{Set}$ is a sheaf for the coherent topology on $\mathcal{C}$ if and only if it satisfies the following two conditions:

1) $X$ preserves finite products: in other words, for every finite family $(T_i)$ of objects of $\mathcal{C}$, the natural map

$$X(\coprod_i T_i) \to \coprod_i X(T_i)$$

is a bijection.

2) For every surjection $\pi: S \to T$ in $\mathcal{C}$, the diagram

$$X(T) \xrightarrow{X(\pi)} X(S) \iff X(S \times_T S)$$

is an equalizer (the two parallel morphisms being induced by the projections in the pullback).

<footnote n="2">²In this work we follow the convention that all functors are, by definition, covariant; we refer to contravariant functors as presheaves.</footnote>
* A presheaf $X: \text{Stonean}^{\text{OP}} \to \text{Set}$ is a sheaf for the coherent topology on Stonean if and only if it preserves finite products: in other words, for every finite family $(T_i)$ of object of $\mathcal{C}$, the natural map

$$X(\coprod_i T_i) \to \prod_i X(T_i)$$

is a bijection.

**Theorem.** The inclusion functors $\text{Profinite} \to \text{CompHaus}$ and $\text{Stonean} \to \text{CompHaus}$ induce equivalences of categories between the categories of sheaves for the coherent topology on $\text{CompHaus}$, $\text{Profinite}$, and $\text{Stonean}$.

Recall that a condensed set is defined as a sheaf for the coherent topology on $\text{CompHaus}$. Thanks to the second theorem, the category of condensed sets is equivalent to the category of sheaves for the coherent topology on $\text{Profinite}$ or $\text{Stonean}$.

In fact these theorems hold for very general target categories other than that of sets, they certainly hold for the category of modules over a ring, for example. Regarding condensed objects simply as product-preserving presheaves on $\text{Stonean}$ allows us to perform many constructions “objectwise” on $\text{Stonean}$. For example, limits and filtered colimits of condensed sets are given objectwise on $\text{Stonean}$; in the setting of condensed abelian groups or modules, the situation is even better — all colimits are computed objectwise on $\text{Stonean}$. Furthermore, epimorphisms of condensed objects in a sufficiently nice concrete category are simply those morphisms $X \to Y$ which satisfy the property that the induced map $X(S) \to Y(S)$ is surjective for every object $S$ of $\text{Stonean}$. These two facts are essential in proving that condensed abelian groups form an abelian category which satisfies all the same of Grothendieck’s AB axioms as the category of abelian groups. This result has not yet made it into MATHLIB, but is well within reach.

## 2. MATHLIB

The results we describe in this paper have all been formalized using the LEAN interactive theorem prover, and incorporated into its open-source formalized mathematical library MATHLIB [mC20]. The LEAN community maintains MATHLIB as a large monolith with a number of overarching design decisions, which must be taken into account in all mathematical contributions to it. This section explains the particulars of MATHLIB that played a key motivating role in the presentation results we discuss in this paper. While we do not provide an introduction to the LEAN theorem prover itself, we refer the reader to [dMU21] for a comprehensive discussion.

### 2.1. Mathematical cohesion.
One of the key design decisions made in MATHLIB is that it strives to be a cohesive library. This point of view manifests concretely in a few ways. Most notably, it often means that mathematical concepts usually have one “official” definition in MATHLIB, and various related definitions and lemmas are built around such official definitions (this collection of ancillary results is often referred to as “the API”) allowing users to work with them effectively. The importance of this approach cannot be understated when it comes to formalization of advanced mathematics.

MATHLIB allows formalizers to efficiently use the constructions from the library, even when their work lies at the intersection of several subjects, which condensed mathematics certainly does. To take a small example, the definition of a condensed set mentions the category of compact Hausdorff spaces, and one frequently has to use both the topological properties of the objects of this category and the more abstract properties of the category itself. The cohesive nature of MATHLIB ensures that the interplay between these two aspects of compact Hausdorff spaces runs smoothly. This is in contrast with the alternative approach where there are separate libraries for different areas of mathematics, which can potentially be problematic should the same concept appear in two different libraries following different conventions, since results from one library would not be directly compatible with results in the other

### 2.2. The “right” generality.
A related and equally important design decision in MATHLIB is that mathematical contributions should be developed in the “right” level of generality. Although the utility of this approach is clear — a more general result applies in more contexts — it is often more convenient for mathematicians to work in the correct level of generality for their current project. However, when making
contributions to MATHLIB, formalizers are encouraged to keep in mind the cohesive and interconnected nature of the library, since it is often impossible to know how an initial contribution may be used in the future, and in what context.

Nevertheless, it is important to mention that it is usually difficult to find the right level of generality for MATHLIB at first. It often happens that preexisting code in MATHLIB is *refactored* to bring it closer to MATHLIB prescribed ideals. In fact, such a refactoring process often occurs in conjunction or in parallel with API development as discussed above.

2.3. **Contribution Process.** Ensuring that the design decisions of MATHLIB are maintained requires significant experience with the library. In practice, this means that contributions must pass a process resembling peer review, whereby “pull requests” are opened for potential contributions, which are then reviewed by a team of reviewers and maintainers before being incorporated into the library.

2.4. **Condensed Mathematics.** Having discussed some of the key design decisions of MATHLIB, and how these relate to contributions of formalized mathematics within the library, it should come as no surprise that the development of condensed mathematics in MATHLIB follows the same lines. The goal of this paper is to describe the mathematics behind the foundations of condensed mathematics in a way which is suitable for inclusion in MATHLIB. In fact, the general categorical approach we outline in this paper was originally *motivated* by the goal of finding the “right” level of generality appropriate for its inclusion in MATHLIB.

2.5. **Size issues.** Condensed mathematics is known to raise subtle set-theoretic issues, see [Sch19b, Remark 1.3]. These can be solved in different ways, one is explained in [Sch19b, Appendix to Lecture II] and another in [BH19, 1.2–1.4], the latter being closer to the approach used in MATHLIB. One advantage of formalizing the theory is to guarantee that all these problems are solved in a precise way. Roughly speaking, the idea is to use Grothendieck’s universes. These are more or less built into the axiomatic framework of LEAN, which is a version of dependent type theory relying on the calculus of inductive constructions. For a more detailed explanation of the foundations of LEAN, we refer the reader to [Car19].

The basic objects of the theory are *terms* and *types*. Every term has a type, and a type can be regarded as a collection of elements, which are the terms of that type. In this way, types replace sets in their everyday use in mathematics as “collections of elements”. The notation $a : A$ is used to signify that $a$ is a term of the type $A$. To avoid an analogue of Russell’s paradox known as Girard’s paradox, LEAN uses a *hierarchy of universes* indexed by the natural numbers

Type = Type 0

Type 0 : Type 1

Type 1 : Type 2

...

MATHLIB’s definition of a category has two universe parameters $u$ and $v$. The definition consists of a “set of objects” ($C : Type u$), and for every pair of objects $X Y : C$, of a “set of morphisms” ($X \to Y : Type v$). Throughout this paper, we will use the word “set” informally in this way, letting LEAN take care of making sure that the “set” in question has a high enough universe level. For a concrete example, see Definition 3.11 where we mention the *top sieve* on an object $X$ in a category $C$. This is supposed to be the “set of all morphisms in $C$ with target $X$”. When $C$ is a large category, this is not a set in the sense of set-theoretic foundations, but as explained above, our use of the word “set” is not abusive in this case.

MATHLIB’s axioms are known to be equivalent to Zermelo–Fraenkel set theory plus the axiom of choice and the existence of $n$ inaccessible cardinals for all $n \in \mathbb{N}$, see [Car19, Corollary 6.8]. In particular, the existence of the hierarchy of universes (and their precise behavior with respect to various constructions) is provable in ZFC using a relatively weak assumption about large cardinals.

### 3. PRELIMINARIES

3.1. **Coverages.** There are various ways to formulate the notion of a site and Grothendieck topology on a category $C$, which allows us to define the notion of a *sheaf* on $C$. In order to fix the terminology, we start this section by recalling some basic definitions and results in this area. The terminology we describe here matches the terminology used in the corresponding definitions that can be found in MATHLIB.
Fix a category $\mathcal{C}$ throughout this section.

**Definition 3.1.** ⌜ Let $X$ be an object of $\mathcal{C}$. A presieve $S$ on $X$ is a set of morphisms with target $X$. If $f \in S$ is a morphism, we will use the notation $\text{dom } f$ for the domain of $f$.

**Remark 3.2.** It is sometimes convenient to consider an indexed family of morphisms $(f_i : X_i \to X)_{i \in I}$, indexed by some set $I$. Of course, any such family yields a presieve $S$ on $X$ which contains only the morphisms $f_i$ for $i \in I$. Conversely, any presieve can be considered as a family indexed by its elements.

The notion of an indexed family of morphisms over $X$ is not exactly equivalent to that of a presieve over $X$, as an indexed family may have duplicates while a presieve cannot. However, it is sometimes convenient to use indexed families as opposed to presieves, and we will allow ourselves to freely go back and forth as discussed above.

**Definition 3.3.** ⌜ Let $F: \mathcal{C}^{\text{op}} \to \text{Set}$ be a presheaf on $\mathcal{C}$ and let $S$ be a presieve on an object $X$ of $\mathcal{C}$. A family of elements for $S$ is a collection $(x_f)_{f \in S}$ where $x_f \in F(\text{dom } f)$ for all $f \in S$. We say that such a family of elements $(x_f)_f$ is compatible provided that for all commutative squares in $\mathcal{C}$ of the form

<figure><img src="image_2.png" /></figure>

with $f, f' \in S$, one has $F(g)(x_f) = F(g')(x_{f'})$. We say that $x \in F(X)$ is an amalgamation for $(x_f)_{f \in S}$ if $F(f)(x) = x_f$ for all $f \in S$.

**Definition 3.4.** ⌜ We say that a presheaf $F: \mathcal{C}^{\text{op}} \to \text{Set}$ is a sheaf for the presieve $S$ if for every compatible family of elements for $S$ there exists a unique amalgamation.

**Remark 3.5.** If a presieve $S$ on $X$ is constructed out of an indexed family $(f_i : X_i \to X)_{i \in I}$ such that for all $i, j \in I$, the pullback $X_i \times_X X_j$ exists, one can rephrase the sheaf condition for the presieve as saying that the diagram

$$F(X) \longrightarrow \prod_{i \in I} F(X_i) \longrightarrow \prod_{i,j \in I} F(X_i \times_X X_j)$$

is an equalizer, where the map on the left is given by the collection $(F(f_i))_{i \in I}$ and the two parallel maps are induced by the projections in the pullbacks. ⌜

**Definition 3.6.** ⌜ A coverage on $\mathcal{C}$ is the datum of a set of presieves on each object $X$ of $\mathcal{C}$, called covering presieves, satisfying the following property: For every morphism $f: X \to Y$ in $\mathcal{C}$ and every covering presieve $S$ on $Y$, there exists a covering presieve $T$ on $X$ such that for each $g \in T$, the composition $f \circ g$ factors through some morphism $h \in S$.

**Definition 3.7.** ⌜ A sieve $S$ on an object $X$ of $\mathcal{C}$ is a presieve on $X$ which is *downwards closed* in the sense that for each $f \in S$ and every $g$ that is composable with $f$, we have that $f \circ g \in S$. The sieve $\langle R \rangle$ generated by a presieve $R$ is the sieve consisting of all morphisms that factor through a morphism of $R$; this is the smallest sieve containing $R$. We also call $\langle R \rangle$ the sieve associated to $R$.

**Remark 3.8.** ⌜ A sieve $S$ on $X$ can be regarded as a full subcategory of the overcategory $\mathcal{C}/X$, and thus it comes equipped with a forgetful functor $S \to \mathcal{C}$. The sieve $S$ induces a cocone over this functor, whose cocone point is $X$, and whose coprojections are the morphisms in $S$. This cocone will be used later.

**Proposition 3.9.** ⌜ Let $X$ be an object in $\mathcal{C}$ and let $S$ be a presieve on $X$. A presheaf $F$ is a sheaf for $S$ if and only if it is a sheaf for $\langle S \rangle$.

*Proof.* See [Joh02, Lemma C.2.1.3] or MATHLIB. □

**Definition 3.10.** ⌜ The pullback of a sieve $S = (g_i : Y_i \to Y)_{i \in I}$ on $Y$ along a morphism $f: X \to Y$ is the sieve on $X$ consisting of all morphisms $g: Y_i \to X$ (for $i \in I$) such that $f \circ g \in S$. It is denoted $f^*S$.
**Definition 3.11.** ⤒ A Grothendieck topology on $\mathcal{C}$ is the datum of a set of sieves on each object $X$ of $\mathcal{C}$, called covering sieves satisfying the following properties:

GT-1) The top sieve — consisting of all morphisms in $\mathcal{C}$ with target $X$ — is a covering sieve on $X$.

GT-2) For every covering sieve $S$ on $Y$ and every morphism $f: X \to Y$, the pullback $f^*S$ is a covering sieve on $X$.

GT-3) Given a covering sieve $S$ on $Y$, suppose another sieve $R$ on $Y$ satisfies the property that for every $f: X \to Y \in S$, $f^*R$ is a covering sieve on $X$. Then $R$ is also a covering sieve on $Y$.

**Lemma 3.12.** ⤒ Let $\mathcal{T}$ be a Grothendieck topology on $\mathcal{C}$, let $X$ be an object of $\mathcal{C}$, and $S$ and $R$ be two sieves on $X$ such that $S$ is contained in $R$ (meaning that every morphism in $S$ is in $R$). If $S$ is a covering sieve for $\mathcal{T}$, then $R$ is a covering sieve as well.

*Proof.* By axiom GT-3), it suffices to show that for every $f: Y \to X$ in $S$, $f^*R$ is a covering sieve of $Y$. By axiom GT-1) it suffices to show that $f^*R$ contains every morphism to $Y$. So let $g: Z \to Y$ be a morphism. Since $f \circ g$ is in $S$, it is in $R$, meaning that $g$ is in $f^*R$, as desired. □

**Definition 3.13.** ⤒ ⤒ The coverage associated to a Grothendieck topology $\mathcal{T}$ is the coverage whose covering presieves are those whose associated sieve is a covering sieve in $\mathcal{T}$. The Grothendieck topology generated by a coverage $S$ is the intersection of all Grothendieck topologies whose associated coverage contains $S$.

Another definition of the Grothendieck topology $\mathcal{T}$ generated by a coverage can be given in terms of a saturation process. To define this, we start by ordering the collections of sieves on an object $X$ by objectwise inclusion; given a coverage $S$, its saturation is the smallest family $(C(X))_{X \in \mathcal{C}}$ of collections of sieves satisfying:

Sat-1) For every object $X$, the top sieve on $X$ is in $C(X)$.

Sat-2) For every object $X$ and every covering presieve $S$ on $X$ in $S$, we have $\langle S \rangle \in C(X)$.

Sat-3) For every object $X$ and every pair $S, R$ of sieves on $X$ such that $S \in C(X)$ and such that for each $f \in S$ the pullback $f^*R$ belongs to $C(Y)$, we have that $R$ lies in $C(X)$.

In terms of the dependent type theory underlying LEAN, requiring that this be “the smallest family” with a certain property is particularly handy, as it can be formalized in terms of *inductive types*, a notion that lies at the very core of the foundational set-up of LEAN and therefore whose implementation and development is remarkably well integrated. This inductive construction is the one that is currently implemented in MATHLIB as follows ⤒:

inductive saturate (K : Coverage C) : (X : C) → Sieve X → Prop where
| of (X : C) (S : Presieve X) (hS : S ∈ K X) : saturate K X (Sieve(generate S)
top (X : C) : saturate K X Top
| transitive (X : C) (R S : Sieve X) :
  saturate K X R →
  (∀ {Y : C} {f : Y → X}, R f → saturate K Y (S.pullback f)) →
  saturate K X S

To prove that the saturation of $S$ is in fact a Grothendieck topology, axioms GT-1) and GT-3) follow at once from the defining properties Sat-1) and Sat-3) of the saturation. Verifying property GT-2) requires a bit more work and is achieved by applying the principle of induction on this inductive type. The formalization of this property is ⤒:

def toGrothendieck (K : Coverage C) : GrothendieckTopology C where
  sieves := saturate K
top_mem' := .top
pullback_stable' := by ... --the inductive proof mentioned above
transitive' X S hS R hR := .transitive _ _ _ hS hR

It follows quite easily that the definition through saturations coincides with the one in Definition 3.13, an equivalence whose proof is formalized in the theorem ⤒:
theorem toGrothendieck_eq_sInf (K : Coverage C) : toGrothendieck _ K = sInf {J | K ≤ ofGrothendieck _ J } := by ...

**Definition 3.14.** ☐ Let $\mathcal{T}$ be a Grothendieck topology on $\mathcal{C}$. A presheaf $F: \mathcal{C}^{\mathrm{op}} \to \mathrm{Set}$ is a sheaf for $\mathcal{T}$ if it is a sheaf for every covering sieve.

**Proposition 3.15.** ☐ If a Grothendieck topology $\mathcal{T}$ is generated by a coverage, then a presheaf is a sheaf if and only if it is a sheaf for every covering presieve in the coverage.

*Proof.* A proof can be found in [Joh02, Proposition C.2.1.9]. The proof that appears in MATHLIB uses induction based on the inductive definition of the Grothendieck topology generated by a coverage discussed above. If one uses Definition 3.13 instead, a proof can be obtained by using the equivalence of this definition with the inductive construction. □

## 4. EFFECTIVE EPIMORPHISMS

In the literature, there are three related conditions on a morphism, designed to capture the property of surjectivity better than the standard notion of an epimorphism. These are called *strict*, *regular* and *effective* epimorphisms respectively; each property implies the previous one. However, each property requires more assumptions on the underlying category than the previous one, and when the assumptions to define *effective epimorphism* hold, then strict implies effective. So, in a sense, these conditions are all equivalent. This is why it was decided to use the name *effective* in MATHLIB for the most generally applicable notion, usually called *strict*. For a more precise explanation of this justification of terminology, see the text following Definition 4.6.

In the category of topological spaces and the category of compact Hausdorff spaces, the effective epimorphisms are precisely the quotient maps. In the latter, the quotient maps are simply the continuous surjections, so the properties of being surjective, an epimorphism and an effective epimorphism all coincide (see Propositions 4.12 and 4.13).

**Definition 4.1.** ☐ A morphism $f: X \to B$ in a category $\mathcal{C}$ is a *regular epimorphism* if it exhibits $B$ as a coequalizer of some pair of morphisms $g_1, g_2: Z \to X$.

**Remark 4.2.** ☐ If a regular epimorphism $f: X \to B$ has a kernel pair (meaning that the pullback $X \times_B X$ exists), then $B$ is the coequalizer of the two projections $X \times_B X \to X$.

**Definition 4.3.** ☐ A morphism $f: Y \to X$ in a category $\mathcal{C}$ is an *effective epimorphism* if it satisfies the following condition: for every morphism $e$ that coequalizes every pair of parallel morphisms which $f$ coequalizes, there exists a unique morphism $d$ such that $d \circ f = e$:

<figure><img src="image_3.png" /></figure>

**Remark 4.4.** It is easy to check that if $f: Y \to X$ is an *effective epimorphism*, then it is an *epimorphism*. Indeed, given a diagram

<figure><img src="image_4.png" /></figure>

such that $h_1 \circ f = h_2 \circ f$, observe that $h_1 \circ f$ equalizes every pair of morphisms $g_1, g_2: Z \to Y$ equalized by $f$. In particular, there is a unique map $d: X \to W$ such that $d \circ f = h_1 \circ f$, and since $h_1$ and $h_2$ both satisfy this property, we deduce $h_1 = h_2$.

In MATHLIB, the notion of *effective epimorphism* is implemented in two steps. First, we define a structure `EffectiveEpiStruct` that contains the data required to be an *effective epimorphism*:

```hsl
structure EffectiveEpiStruct {X Y : C} (f : Y → X) where
  desc : ∀ {W : C} (e : Y → W),
        (∀ {Z : C} (g₁ g₂ : Z → Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) → (X → W)
  fac : ∀ {W : C} (e : Y → W)
```
(h : ∀ {Z : C} (g₁ g₂ : Z → Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e),
f ≫ desc e h = e

uniq : ∀ {W : C} (e : Y → W)

(h : ∀ {Z : C} (g₁ g₂ : Z → Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e)

(m : X → W), f ≫ m = e → m = desc e h

The field `desc` provides, given a morphism `e`: $Y \to W$ which coequalizes every morphism that `f` coequalizes, the morphism `d`: $X \to W$; the field `fac` is a proof that $d \circ f = e$; and the field `uniq` is a proof that `d` is unique.

We then define a class `EffectiveEpi`, which is a proposition saying that the type of `EffectiveEpiStruct`'s associated to `f` is nonempty<fnref n="3" />:

class EffectiveEpi {X Y : C} (f : Y → X) : Prop where

effectiveEpi : Nonempty (EffectiveEpiStruct f)

**Definition 4.5.** Given a family of morphisms $f = (f_i : X_i \to B)_{i \in I}$ and a pair of morphisms $g_{j1} : Z \to X_{j1}$ and $g_{j2} : Z \to X_{j2}$, we say that the family *coequalizes* $g_{j1}$ and $g_{j2}$ if $f_{j1} \circ g_{j1} = f_{j2} \circ g_{j2}$.

**Definition 4.6.** A family of morphisms $(f_i : X_i \to B)_{i \in I}$ in a category $\mathcal{C}$ is *effective epimorphic* if it satisfies the following universal property:

Given any family $(e_i : X_i \to W)_{i \in I}$ coequalizing every pair of morphisms $g_i : Z \to X_i$, $g_j : Z \to X_j$ which $f$ coequalizes, there exists a unique morphism $d$ such that for all $i$, $d \circ f_i = e_i$:

<figure><img src="image_5.png" /></figure>

The notion of effective epimorphic family is formalized in a similar two-step process where we first define

```hsl
structure EffectiveEpiFamilyStruct {B : C} {α : Type*}
```

(X : α → C) (π : (a : α) → (X a → B)) where

desc : ∀ {W} (e : (a : α) → (X a → W)),
(∀ {Z : C} (a₁ a₂ : α) (g₁ : Z → X a₁) (g₂ : Z → X a₂),
g₁ ≫ π_ = g₂ ≫ π_ → g₁ ≫ e_ = g₂ ≫ e_) → (B → W)

fac : ∀ {W} (e : (a : α) → (X a → W))
(h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z → X a₁) (g₂ : Z → X a₂),
g₁ ≫ π_ = g₂ ≫ π_ → g₁ ≫ e_ = g₂ ≫ e_)

(a : α), π a ≫ desc e h = e a

uniq : ∀ {W} (e : (a : α) → (X a → W))
(h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z → X a₁) (g₂ : Z → X a₂),
g₁ ≫ π_ = g₂ ≫ π_ → g₁ ≫ e_ = g₂ ≫ e_)

(m : B → W), (∀ (a : α), π a ≫ m = e a) → m = desc e h

and then

class EffectiveEpiFamily {B : C} {α : Type*} (X : α → C)

(π : (a : α) → (X a → B)) : Prop where

effectiveEpiFamily : Nonempty (EffectiveEpiFamilyStruct X π)

<footnote n="3">³The fact that **EffectiveEpi** is a class allows **LEAN** to use *typeclass inference* to infer that a morphism is effective epimorphic in some cases: for example, in **CompHaus**, given a morphism **f** with an [Epi **f**] instance, **LEAN** can automatically infer an instance **EffectiveEpi** **f**. Moreover, the internal axiomatic of **LEAN** guarantees that two terms of a proposition are definitionally equal: in particular, two *proofs* of non-emptiness of **EffectiveEpiStruct** **f** automatically coincide, whereas producing explicit witnesses might lead to different outcomes, and that would often be troublesome.</footnote>
Definitions 4.3 and 4.6 work in any category; the morphism in question is not required to have a kernel pair. It is easy to see that if $f$ is a regular epimorphism, then it is an effective epimorphism. Conversely, if an effective epimorphism $f$ has a kernel pair, then it is a regular epimorphism (see ↗). This justifies the use of the terminology “effective epimorphism”;

We give some characterizations of effective epimorphic families. For an object $W$ of $\mathcal{C}$, let $h_W$ denote the representable presheaf $h_W(X) = \operatorname{Hom}_{\mathcal{C}}(X, W)$.

**Lemma 4.7.** Let $(f_i: X_i \to B)$ be a family of morphisms in $\mathcal{C}$. Let $S$ be the sieve generated by the set $(f_i)_{i \in I}$, regarded as a presieve. Then the following are equivalent:

(i) The family $(f_i)_{i \in I}$ is effective epimorphic.

(ii) For every object $W$ of $\mathcal{C}$, the presheaf $h_W$ is a sheaf for $S$.

(iii) The cocone in $\mathcal{C}$ corresponding to the sieve $S$ (described in Remark 3.8) is colimiting.

*Proof.* (i) $\iff$ (ii): First of all, observe that (ii) is equivalent to $h_W$ being a sheaf for $(f_i)_{i \in I}$. Moreover, the data of a compatible family (in the sense of Definition 3.3) for $(f_i)_{i \in I}$ is a family $(x_i: X_i \to W)_{i \in I}$ that coequalizes every pair of morphisms that $(f_i)_{i \in I}$ coequalizes and an amalgamation for it is the morphism denoted $d$ in Definition 4.6. The equivalence between (i) and (ii) follows.

(ii) $\implies$ (iii): Suppose we have another cocone on the same functor, with cocone point $W$ and coprojections $x_f: X \to W$ for any $f: X \to B$ contained in $S$. We will now prove that this is precisely the data of a compatible family for $S$. Indeed, if $f: X \to B$ and $f': X' \to B$ are in $S$, and the square

$$ \begin{array}{ccc} Y & \xrightarrow{g'} & X' \\ \bigg\downarrow & & \bigg\downarrow \\ X & \xrightarrow{f} & B \end{array} $$

commutes, then $f \circ g = f' \circ g' \in S$ because of the downwards closed property of sieves. We have coprojections $x_f: X \to W$, $x_{f'}: X' \to W$ and $x_{f \circ g} = x_{f' \circ g'}: Y \to W$ of the cocone with cocone point $W$, which satisfy

$$ x_{f'} \circ g' = x_{f' \circ g'} = x_{f \circ g} = x_f \circ g $$

which is what we wanted. The unique amalgamation given by (ii) gives the unique cocone morphism required to satisfy the universal property of the colimit.

(iii) $\implies$ (i): Given a family $(e_i: X_i \to W)$ that coequalizes any pair of morphisms $g_i: Z \to X_i$, $g_j: Z \to X_j$ that is coequalized by $f$, we obtain a cone over $S$ with cone point $W$ as follows: recall that $S$ is generated by the $(f_i)_{i \in I}$, and thus the morphisms in $S$ are precisely those which factor through $f_i$ for some $i$. Thus, for each morphism $g: Y \to B$ in $S$, we may write $g = f_i \circ h$ for some $i$, and set $w_g := e_i \circ h$ — this is well-defined by the assumption on $(e_i)_{i \in I}$. We get the desired map $d: B \to W$ by the universal property of colimits. $\square$

**Lemma 4.8.** Let $(\pi_i: X_i \to B)_{i \in I}$ be an effective epimorphic family in $\mathcal{C}$, such that the coproduct of $(X_i)_{i \in I}$ exists. The map

$$ \pi: \coprod_i X_i \to B $$

induced by $(\pi_i)_{i \in I}$ is an effective epimorphism.

*Proof.* Let $\iota_i: X_i \to \coprod_i X_i$ denote the coprojections of the coproduct. Let $e: \coprod_i X_i \to W$ be a morphism which coequalizes every pair of morphisms that $\pi$ coequalizes. It is clear that the family $(e \circ \iota_i)_{i \in I}$ coequalizes every pair $g_i: Z \to X_i$, $g_j: Z \to X_j$ that $(\pi_i)_{i \in I}$ coequalizes. It is easy to see that the morphism $d: B \to W$ obtained from the universal property of the effective epimorphic family gives the universal property of effective epimorphisms for $\pi$. $\square$

**Lemma 4.9.** Let $(\pi_i: X_i \to B)_{i \in I}$ be a family of morphisms in $\mathcal{C}$. Suppose that

1) All coproducts and pullbacks appearing in 2) exist.

2) For every object $Z$ and every morphism

$$ g: Z \to \coprod_i X_i, $$
the induced map

$$i(g) := \coprod_i Z \times_{\coprod_i X_i} X_i \to Z$$

is an epimorphism.

3) The map

$$\pi: \coprod_i X_i \to B$$

induced by $(\pi_i)_i$ is an effective epimorphism.

Then $(\pi_i)_i$ is an effective epimorphic family.

*Proof.* Let $(e_i: X_i \to Z)_{i \in I}$ be a family which coequalizes every pair of morphisms $g_i: Z \to X_i$, $g_j: Z \to X_j$ which $(\pi_i)_i$ coequalizes. We need to show that there exists a unique $d: B \to Z$ such that for all such $g_i, g_j$, we have $d \circ g_i = d \circ g_j$. To obtain this, we will apply the property that $\pi$ is an effective epimorphism to the induced morphism $e: \coprod_i X_i \to Z$. To be able to do this, we need to check that $e$ coequalizes every pair of morphisms which $\pi$ coequalizes.

Let $f_1, f_2: Z \to \coprod_i X_i$ be given and suppose that $\pi \circ f_1 = \pi \circ f_2$. We want to show that $e \circ f_1 = e \circ f_2$. Applying the fact that $i(f_1)$ is an epimorphism, it suffices to prove that

$$e \circ f_1 \circ i(f_1) = e \circ f_2 \circ i(f_1).$$

This identity can be checked on each component of the coproduct $\coprod_i Z \times_{\coprod_i X_i} X_i$. In other words, we need to show that for every $a \in I$,

$$e \circ f_1 \circ i(f_1) \circ \iota_a = e \circ f_2 \circ i(f_1) \circ \iota_a,$$

where

$$\iota_a: Z \times_{\coprod_i X_i} X_a \to \coprod_i Z \times_{\coprod_i X_i} X_i$$

denotes the coprojection. One easily checks that

$$i(f_1) \circ \iota_a: Z \times_{\coprod_i X_i} X_a \to Z$$

is simply the first projection map in the pullback, which we denote by $p_1$. We thus need to show that

$$e \circ f_1 \circ p_1 = e \circ f_2 \circ p_1.$$

The left-hand side simplifies to $e_a \circ p_2$, where

$$p_2: Z \times_{\coprod_i X_i} X_a \to X_a$$

denotes the second projection in the pullback.

Now it again suffices to prove the equality after precomposition with the epimorphism $i(f_2 \circ p_1)$, i.e. to show that

$$e_a \circ p_2 \circ i(f_2 \circ p_1) = e \circ f_2 \circ p_1 \circ i(f_2 \circ p_1).$$

Again we can check this equality on the components of the coproduct $\coprod_b (Z \times_{\coprod_i X_i} X_a) \times_{\coprod_i X_i} X_b$, and similarly to above, this reduces to showing that for every $b \in I$,

$$e_a \circ g_a = e_b \circ g_b,$$

where

$$g_a: (Z \times_{\coprod_i X_i} X_a) \times_{\coprod_i X_i} X_b \to X_a$$

is the first projection followed by the second projection, and

$$g_b: (Z \times_{\coprod_i X_i} X_a) \times_{\coprod_i X_i} X_b \to X_b$$

is the second projection. Doing the same manipulation on the equality $\pi \circ f_1 = \pi \circ f_2$, we see that $g_a, g_b$ is a pair of morphisms that the family $(\pi_i)_i$ coequalizes. By assumption, the family $(e_i)_i$ coequalizes it as well. This means that $e \circ f_1 = e \circ f_2$ and we obtain the unique $d: B \to Z$ we wanted. $\square$
Propositions 4.12 and 4.13 provide an explicit description of effective epimorphisms in the categories of topological spaces, compact Hausdorff spaces, profinite spaces, and Stonean spaces. Both results ultimately rely on the observation that epimorphisms in these four categories are surjective, and we start with this result:

**Lemma 4.10.** ☐ Let $\mathcal{C}$ be any of the categories Top, CompHaus, Profinite or Stonean. Then epimorphisms in $\mathcal{C}$ are surjective (continuous) maps.

*Proof.* Note first that one direction is clear, because a surjective morphism in any concrete category is an epimorphism. Now let $f: Y \to X$ be a morphism in $\mathcal{C}$.

When $\mathcal{C} = \text{Top}$ the result is very well known: suppose $f$ is an epimorphism and consider the diagram

$$ Y \xrightarrow{f} X \xrightarrow[e_1]{\chi} \{0, 1\}^b $$

where $\{0, 1\}^b$ denotes the set $\{0, 1\}$ endowed with the indiscrete topology, where $\chi$ is the characteristic function of $\text{im}(f)$ and where $e_1$ is the constant map with image 1. Clearly, $\chi \circ f = e_1 \circ f$ and when $f$ is an epimorphism this implies that $\chi = e_1$, which is the statement $\text{im}(f) = X$.

When $\mathcal{C} = \text{CompHaus}$, the above proof breaks down because $\{0, 1\}^b$ is not in $\mathcal{C}$. But since spaces in $\mathcal{C}$ are normal, we can argue as follows: the subspace $\text{im}(f) \subseteq X$ is compact, hence closed. Suppose that $f$ is not surjective, and let $x \notin \text{im}(f)$: by Urysohn's lemma, there is a continuous function $\theta: X \to [0, 1]$ such that $\theta(x) = 0$ and $\theta(\text{im}(f)) = 1$. Denote by $e_1: X \to [0, 1]$ the constant function with image 1: then $e_1 \neq \theta$ and yet $f \circ \theta = f \circ e_1$ showing that $f$ is not an epimorphism.

When $\mathcal{C} = \text{Profinite}$ or $\mathcal{C} = \text{Stonean}$ the above proof breaks down, because the unit interval is not in $\mathcal{C}$. But the argument for Top can be adapted by replacing the indiscrete space $\{0, 1\}^b$ with the discrete space $\{0, 1\}^\delta$, which is in $\mathcal{C}$. First, observe that, given any topological space $Z$ and a clopen $U \subseteq Z$, the characteristic function $\chi_U$ is continuous. Moreover, since every object in $\mathcal{C}$ is totally disconnected, its topology admits a basis of open neighbourhoods that are clopen sets ☐. Now suppose $f$ is not surjective, and let $x \notin \text{im}(f)$. Since — as before — $\text{im}(f)$ is closed, there exists an open neighbourhood $V$ of $x$ contained in the complement $\text{im}(f)^c$ and we can find a clopen neighbourhood $U \subseteq V$ such that $x \in U$ and $U \cap \text{im}(f) = \emptyset$. Consider the diagram in $\mathcal{C}$

$$ Y \xrightarrow{f} X \xrightarrow[e_0]{\chi_U} \{0, 1\}^\delta $$

where $e_0$ is the constant function with value 0. Now $\chi_U \neq e_0$, as can be seen by evaluating them on $x$, yet $\chi_U \circ f = e_0 \circ f$ since $U \cap \text{im}(f) = \emptyset$. This shows that $f$ is not an epimorphism. ☐

**Lemma 4.11.** Let $\mathcal{C}$ be a full subcategory of Top and let $f: Y \to X$ be a morphism in $\mathcal{C}$ which is a quotient map. Then $f$ is an effective epimorphism in $\mathcal{C}$.

*Proof.* Suppose that $e: Y \to Z$ equalizes every morphism that $f$ equalizes. This means that for every pair of points $y_1, y_2 \in Y$ such that $f(y_1) = f(y_2)$, we have $e(y_1) = e(y_2)$, as can be seen by considering the parallel morphisms $e_{y_1}, e_{y_2}: Y \to Y$ sending everything to $y_1$ and to $y_2$, respectively. The universal property of the quotient topology on $X$ provides the existence of a unique continuous $d: X \to Z$ such that $d \circ f = e$, showing that $f$ is an effective epimorphism. ☐

**Proposition 4.12.** ☐ The effective epimorphisms in Top are the quotient maps.

*Proof.* A quotient map is an effective epimorphism in Top by Lemma 4.11.

In the other direction, let $f: Y \to X$ be an effective epimorphism in Top. By Remark 4.4 and Lemma 4.10, $f$ is surjective and we are simply left to prove that in this situation $X$ is endowed with the quotient topology, namely the final topology induced by $f$. Denote by $\tilde{X}$ the space whose underlying set coincides with $X$, but endowed with the final topology induced by $f$, so that the identity map $i: \tilde{X} \to X$ is continuous. In the diagram

<figure><img src="image_6.png" /></figure>
the morphism $\hat{f}$ equalizes every pair of morphisms equalized by $f$, so there exists a unique continuous map $d: X \to \hat{X}$ making the diagram commute. It follows that $d$ is induced by the identity, showing that $X$ is homeomorphic to $\hat{X}$, as required. $\square$

**Proposition 4.13.** ☑ ☑ ☑ The effective epimorphisms in CompHaus, Profinite and in Stonean are the (continuous) surjections.

*Proof.* Let $\mathcal{C}$ be any of the categories CompHaus, Profinite or Stonean and let $f: Y \to X$ be an effective epimorphism in $\mathcal{C}$. Combining Remark 4.4 and Lemma 4.10, yields that $f$ is a continuous surjection.

In the other direction, consider a continuous surjection $f: Y \to X$ in $\mathcal{C}$. Since the objects of $\mathcal{C}$ are compact Hausdorff spaces, $f$ is also a closed map and hence a quotient map, and thus an effective epimorphism by Lemma 4.11. $\square$

# 5. THREE GROTHENDIECK TOPOLOGIES

## 5.1. The regular topology.

**Definition 5.1.** ☑ A category $\mathcal{C}$ is *preregular* if the collection of presieves consisting of single effective epimorphisms forms a coverage. In other words, if for every effective epimorphism $g: Z \to Y$ and every morphism $f: X \to Y$, there exists an effective epimorphism $h: W \to X$ and a morphism $i: W \to Z$ such that the following diagram commutes:

<figure><img src="image_7.png" /></figure>

In this case, we call this coverage the *regular coverage* on $\mathcal{C}$, and the Grothendieck topology generated by this coverage is called the *regular topology* on $\mathcal{C}$.

In MATHLIB, we define a predicate **Preregular** ☑ on categories:

class Preregular : Prop where
exists_fac : ∀ {X Y Z : C} (f : X → Y) (g : Z → Y) [EffectiveEpi g],
(∃ (W : C) (h : W → X) (_ : EffectiveEpi h) (i : W → Z), i ≫ g = h ≫ f)

Then the definition of the regular topology follows ☑:

def regularCoverage [Preregular C] : Coverage C where
covering B := { S | ∃ (X : C) (f : X → B), S = Presieve.ofArrows (fun (_ : Unit) ↦
X)
 fun (_ : Unit) ↦ f ) ∧ EffectiveEpi f }
pullback := by ...

def regularTopology [Preregular C] : GrothendieckTopology C :=
Coverage.toGrothendieck _ <\| regularCoverage C

## 5.2. The extensive topology.

**Definition 5.2.** ☑ A category $\mathcal{C}$ is *finitary extensive* if it satisfies the following properties:

1) $\mathcal{C}$ has finite coproducts.

2) $\mathcal{C}$ has pullbacks along coprojections of finite coproducts.

3) Every commutative diagram

<figure><img src="image_8.png" /></figure>

consists of two pullback squares if and only if the top row is a coproduct diagram.
**Remark 5.3.** Our definition of finitary extensive category is precisely [CLW93, Definition 2.1 and Proposition 2.2].

MATHLIB already had the predicate **FinitaryExtensive** on categories:

```c
class FinitaryExtensive (C : Type u) [Category.{v} C] : Prop where
    [hasFiniteCoproducts : HasFiniteCoproducts C]
    [hasPullbacksOfInclusions : HasPullbacksOfInclusions C]
van_kampen' : ∀ {X Y : C} (c : BinaryCofan X Y), IsColimit c → IsVanKampenColimit c
```

The field `van_kampen'` is condition 3) in Definition 5.2.

**Proposition 5.4.** Let $\mathcal{C}$ be a finitary extensive category. The collection of finite families $(X_i \to X)_{i \in I}$ exhibiting $X$ as a coproduct of the family $(X_i)_{i \in I}$, forms a coverage.

*Proof.* The axioms of a finitary extensive category ensure that the required property holds, namely that given a morphism $f: X \to Y$ and a finite family of morphisms $(g_i: Y_i \to Y)_{i \in I}$, the family $(X \times_Y Y_i \to X)_{i \in I}$ exhibits $X$ as a coproduct of the family $(X \times_Y Y_i)_{i \in I}$. This has been formalized in MATHLIB ⚙️, but it appears *ibid.* as a definition: this is because the proof that the collection is a coverage is part of the definition in question. □

**Definition 5.5.** ⚙️ Let $\mathcal{C}$ be a finitary extensive category. The coverage defined in Proposition 5.4 is called the *extensive coverage* on $\mathcal{C}$, and the Grothendieck topology generated by this coverage is called the *extensive topology* on $\mathcal{C}$.

In MATHLIB, we define the extensive topology as follows ⚙️:

```h
def extensiveCoverage [FinitaryPreExtensive C] : Coverage C where
  covering B := { S | ∃ (α : Type) (_ : Finite α) (X : α → C) (π : (a : α) → (X a → B)),
                    S = Presieve.ofArrows X π ∧ IsIso (SigmaITA π) }
  pullback := by ...
```

```h
def extensiveTopology [FinitaryPreExtensive C] : GrothendieckTopology C :=
  Coverage.toGrothendieck _ <| extensiveCoverage C
```

Note that the definition of the extensive coverage and extensive topology only requires an assumption [FinitaryPreExtensive C]. This condition is slightly weaker than **FinitaryExtensive**, but the difference is unimportant. For the characterization of sheaves for the extensive topology, the stronger condition is indeed required.

## 5.3. The coherent topology.

**Definition 5.6.** ⚙️ A category $\mathcal{C}$ is *precoherent* if the collection of finite effective epimorphic families forms a coverage. In other words, if for any finite effective epimorphic family $(\pi_i : X_i \to B)_{i \in I}$ and any morphism $f: B' \to B$, there exists a finite effective epimorphic family $(\pi'_j : X'_j \to B')_{j \in I'}$, such that for each $j \in I'$, the composition $f \circ \pi'_j$ factors through $\pi_i$ for some $i \in I$. In this case, we call this coverage the *coherent coverage* on $\mathcal{C}$, and the Grothendieck topology generated by this coverage is called the *coherent topology* on $\mathcal{C}$.

In MATHLIB, we define a predicate **Precoherent** ⚙️ on categories:

```c
class Precoherent : Prop where
pullback {B1 B2 : C} (f : B2 → B1) :
  ∀ (α : Type) [Finite α] (X1 : α → C) (π1 : (a : α) → (X1 a → B1)),
  EffectiveEpiFamily X1 π1 →
∃ (β : Type) (_ : Finite β) (X2 : β → C) (π2 : (b : β) → (X2 b → B2)),
  EffectiveEpiFamily X2 π2 ∧
∃ (i : β → α) (ι : (b : β) → (X2 b → X1 (i b))),
  ∀ (b : β), ι b ≫ π1 _ = π2 _ ≫ f
```

Then the definition of the coherent topology follows ⚙️:
def coherentCoverage [Precoherent C] : Coverage C where
covering B := { S | ∃ (α : Type) (_ : Finite α) (X : α → C) (π : (a : α) → (X a → B)) },
S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π }
pullback := by ...

def coherentTopology [Precoherent C] : GrothendieckTopology C :=
Coverage.toGrothendieck _ <| coherentCoverage C

**Remark 5.7.** The notion of a precoherent category naturally arose through the formalization process, and was forced upon us by the “MATHLIB philosophy” where definitions are often phrased in the most general way (see §2.2). Indeed, the condition that $\mathcal{C}$ is a precoherent category is precisely the minimal axiom needed to ensure that what we call the *coherent coverage* above is indeed a coverage. A similar approach was taken to define the notion of a *preregular* category. For example, we do not require the existence of pullbacks required in the definition of *regular* and *coherent* categories as in [Joh02, A1.3] and [Joh02, A1.4] respectively.

Due to our weaker assumptions, several of our results about the regular and coherent topology strengthen existing standard results. For example, [Joh02, Example C.2.1.12 (d)] states that the coherent topology on a *coherent* category is subcanonical, which we extend in Proposition 6.8 below to *precoherent* categories. The analogous statement for the regular topology on a regular category can be found in [Lur18, Corollary B.3.6], and is extended to preregular categories in Proposition 6.1 below. In Proposition 6.10 (respectively Lemma 6.2), we explicitly characterize the covering sieves in the coherent (respectively regular) topology on a precoherent (respectively preregular) category. Under stronger assumptions on the category, this result can be found in [Lur18, Definition B.5.1 and Proposition B.5.2] (respectively in [Joh02, C.2.1.12 (c)]).

## 5.4. The coherent topology on a regular extensive category.

**Proposition 5.8.** ☑ Let $\mathcal{C}$ be a category which is preregular and finitary extensive. Then $\mathcal{C}$ is precoherent.

*Proof.* Since $\mathcal{C}$ is finitary extensive, Lemmas 4.8 and 4.9 imply that finite effective epimorphic families in $\mathcal{C}$ are precisely those which induce an effective epimorphism on the coproduct.

Let $(f_i : X_i \to X)_{i \in I}$ be a finite effective epimorphic family and let $g: Y \to X$ be a morphism. Since the morphism $\coprod_i X_i \to X$ is an effective epimorphism, the fact that $\mathcal{C}$ is preregular ensures the existence of a diagram

<figure><img src="image_9.png" /></figure>

in which $h: Z \to Y$ is an effective epimorphism.

Now, the fact that $\mathcal{C}$ is extensive ensures that the family $(Z \times_{\coprod_i X_i} X_i \to Z)_{i \in I}$ exhibits $Z$ as a coproduct in the sense that the canonical map

$$ \coprod_i Z \times_{\coprod_i X_i} X_i \to Z $$

is an isomorphism. Therefore, the composition

$$ \coprod_i Z \times_{\coprod_i X_i} X_i \to Y $$

is an effective epimorphism, and therefore the family $(Z \times_{\coprod_i X_i} X_i \to Y)_{i \in I}$ works as the desired effective epimorphic family. $\square$

It is obvious that the union of two coverages is a coverage. This allows us to state:

**Proposition 5.9.** ☑ Let $\mathcal{C}$ be a category which is preregular and finitary extensive. The union of the regular and extensive coverages generates the coherent topology.
*Proof.* Denote by $\mathcal{T}$ the topology generated by the union of the regular and extensive coverages. Note that the regular and extensive coverages are both contained in the coherent coverage, hence $\mathcal{T}$ is contained in the coherent topology, so it suffices to show that the coherent topology is contained in $\mathcal{T}$.

Let $X$ be an object of $\mathcal{C}$ and let $S$ be a covering sieve on $X$ for the coherent topology: in other words, $S$ is generated by a finite effective epimorphic family $(f_i: X_i \to X)_{i \in I}$. We want to show that $S$ is a $\mathcal{T}$-covering sieve. Denote by

$$f: \coprod_{i \in I} X_i \to X$$

the map induced by the $f_i$ and for each $j \in I$, let

$$\iota_j: X_j \to \coprod_{i \in I} X_i$$

be the coprojection. For each $j$,

$$f \circ \iota_j = f_j \in S, \text{ so } \iota_j \in f^*S.$$

Therefore, the sieve $T$ generated by the family $(\iota_i)_i$ is contained in $f^*S$. Since the presieve generated by the family $(\iota_i)_i$ is a covering presieve of the coproduct in the extensive coverage, $T$ is a $\mathcal{T}$-covering sieve and hence by Lemma 3.12, $f^*S$ is a $\mathcal{T}$-covering sieve of $\coprod_i X_i$. By Lemma 4.8, $f$ is an effective epimorphism, and hence the sieve $S_f$ generated by the singleton presieve $\{f\}$ is a $\mathcal{T}$-covering sieve. Now by axiom GT-3) for Grothendieck topologies, it suffices to show that $g^*S$ is a $\mathcal{T}$-covering sieve for every $g$ in $S_f$. Given such a $g = f \circ h$, we have $g^*S = h^*(f^*S)$ which is a $\mathcal{T}$-covering sieve because $f^*S$ is. $\square$

## 6. SHEAVES

**6.1. Regular sheaves.** Let $\mathcal{C}$ be a preregular category (see Definition 5.1).

**Proposition 6.1.** *The regular topology on $\mathcal{C}$ is subcanonical*^4.

*Proof.* We need to show that each presheaf of the form $h_W = \operatorname{Hom}(\-, W)$ with $W$ an object of $\mathcal{C}$ is a sheaf. By Proposition 3.15, it is enough to check that $h_W$ is a sheaf for each family consisting of a single effective epimorphism. Noting that a singleton family is effective epimorphic if and only if it consists of an effective epimorphism, this is now clear from Lemma 4.7. $\square$

**Lemma 6.2.** *A sieve in $\mathcal{C}$ is a covering sieve for the regular topology if and only if it contains an effective epimorphism.*

*Proof.* The proof is a simpler version of the proof of Proposition 6.10 below. The reader can easily take that proof and replace effective epimorphic families by effective epimorphisms, thereby filling in this proof (the key is to prove that effective epimorphisms in preregular categories are stable under composition). $\square$

**Lemma 6.3.** *Suppose $\mathcal{C}$ has kernel pairs of effective epimorphisms. Then a presheaf $F$ on $\mathcal{C}$ is a sheaf for the regular topology if and only if for every effective epimorphism $\pi: X \to B$, the diagram*

$$(\text{EqCond}) \qquad F(B) \xrightarrow{F(\pi)} F(X) \mathrel{\substack{\longrightarrow \\ \longleftarrow}} F(X \times_B X)$$

is an equalizer (the two parallel morphisms being given by the projections in the pullback).

*Proof.* This follows from the fact that a presheaf is a sheaf for the regular topology if and only if it is a sheaf for every family consisting of a single effective epimorphism, and the characterization (discussed in Remark 3.5) of the sheaf condition in the case where the relevant pullbacks exist. $\square$

**Proposition 6.4.** *Suppose every object in $\mathcal{C}$ is projective$^5$. Then every presheaf on $\mathcal{C}$ is a sheaf for the regular topology.*

*Proof.* Since every object is projective, every sieve generated by an epimorphism is the top sieve, for which every presheaf is a sheaf. $\square$

<footnote n="4">⁴A Grothendieck topology is called *subcanonical* if every representable presheaf is a sheaf. By *representable*, we mean a presheaf of the form $\operatorname{Hom}(\-, W)$ for some object $W$ of $\mathcal{C}$.</footnote>

<footnote n="5">⁵An object $P$ is *projective* if every morphism out of $P$ lifts along every epimorphism with the same target.</footnote>
**6.2. Extensive sheaves.** Let $\mathcal{C}$ be a finitary extensive category (see Definition 5.2).

**Proposition 6.5.** ☑ A presheaf on $\mathcal{C}$ is a sheaf with respect to the extensive topology if and only if it preserves finite products.

*Proof.* This is proved in [Lur18, Proposition B.4.5] (there, the extensive topology is defined only for categories with pullbacks, but the proof remains valid in our setting since only pullbacks along coprojections of finite coproducts are used). Our formalization follows the same ideas used *ibid*.

**Proposition 6.6.** ☑ The extensive topology on $\mathcal{C}$ is subcanonical.

*Proof.* Since $\operatorname{Hom}(-, W)$ preserves limits, this follows from Proposition 6.5

**Proposition 6.7.** ☑ Let $X$ be an object of $\mathcal{C}$ and $S$ a sieve on $X$. Then $S$ is a covering sieve for the extensive topology on $\mathcal{C}$ if and only if it contains a family of morphisms $(f_i : X_i \to X)_{i \in I}$ which exhibit $X$ as a coproduct of the $X_i$.

*Proof.* The proof is a simpler version of the proof of Proposition 6.10 below. The reader can easily take that proof and replace effective epimorphic families by families of morphisms exhibiting the target as a coproduct, thereby filling in this proof.

**6.3. Coherent sheaves.**

**Proposition 6.8.** ☑ Let $\mathcal{C}$ be a precoherent category (see Definition 5.6). The coherent topology on $\mathcal{C}$ is subcanonical.

*Proof.* We need to show that each presheaf of the form $h_W = \operatorname{Hom}(-, W)$ with $W$ an object of $\mathcal{C}$ is a sheaf. By Proposition 3.15, it is enough to check that $h_W$ is a sheaf for each finite effective epimorphic family, and this follows from Lemma 4.7.

**Remark 6.9.** If $\mathcal{C}$ is finitary extensive and preregular (and hence precoherent), then Proposition 6.8 implies Proposition 6.6 and Proposition 6.1, because the coherent topology is finer than the extensive and regular one. On the other hand, being precoherent might not in general imply being finitary extensive or preregular (for example, when $\mathcal{C}$ does not have finite coproducts) and this is why we proved Proposition 6.6 and Proposition 6.1 separately.

**Proposition 6.10.** ☑ Let $\mathcal{C}$ be a precoherent category. A sieve in $\mathcal{C}$ is a covering sieve for the coherent topology if and only if it contains a finite effective epimorphic family.

Before proving Proposition 6.10 we provide some preliminary results.

**Lemma 6.11.** ☑ If a sieve $S$ contains a finite effective epimorphic family, then $S$ is a covering sieve for the coherent topology.

*Proof.* Let $(\pi_i : X_i \to X)_{i \in I}$ be a finite effective epimorphic family contained in $S$. By definition, the sieve $S_0$ generated by the family $(\pi_i)_{i \in I}$ is a covering sieve for the coherent topology, and since $S$ contains the family $(\pi_i)_{i \in I}$, it contains $S_0$. Lemma 3.12 yields the conclusion.

**Lemma 6.12.** ☑ Assume that $\mathcal{C}$ is precoherent and that $(\pi_i : X_i \to B)_{i \in I}$ is a finite effective epimorphic family, and suppose that for each $i \in I$, we are given a finite effective epimorphic family $(\pi_{i,j} : Y_{i,j} \to X_i)_{j \in J_i}$. Then the induced collection $(\varpi_{i,j} = \pi_i \circ \pi_{i,j} : Y_{i,j} \to B)_{i \in I, j \in J_i}$ is an effective epimorphic family.

*Proof.* By Lemma 4.7, a family is effective epimorphic if and only if for each object $W$ the presheaf $h_W$ is a sheaf for the sieve generated by this family. Thus, since the coherent topology is subcanonical by Proposition 6.8, it is enough to show that the sieve $S$ generated by the family $(\varpi_{i,j})_{i \in I, j \in J_i}$ is a covering sieve for the coherent topology.

By and GT-3) of Definition 3.11, it is enough to check that $f^*S$ is a covering sieve for every map $f$ in the sieve generated by $(\pi_i)_{i \in I}$ (which is a covering sieve by Lemma 6.11). In fact, by GT-2), it is enough to check that each $\pi_i^*S$ is a covering sieve. Since $\pi_i^*S$ contains the finite effective epimorphic family $(\pi_{i,j})_{j \in I_j}$, it is a covering sieve for the coherent topology by Lemma 6.11.
**Proof of Proposition 6.10.** Let $\mathcal{T}$ denote the collection of sieves in $\mathcal{C}$ that contain a finite effective epimorphic family. By Lemma 6.11, we know that $\mathcal{T}$ is contained in the coherent topology. Our goal is to show that they are equal, so it remains to show that $\mathcal{T}$ contains the coherent topology. By definition, the coherent topology is the smallest Grothendieck topology whose associated coverage contains the coherent coverage. Therefore, it suffices to show that

a) the collection $\mathcal{T}$ forms a Grothendieck topology and

b) the coverage associated to $\mathcal{T}$ contains the coherent coverage.

Once a) is established, point b) is immediate from the definitions of $\mathcal{T}$ and of the associated coverage (Definition 3.13). It remains to show a) by checking the conditions of Definition 3.11. Condition GT-1) is immediate, since for every object $X$ of $\mathcal{C}$, the identity on $X$ forms a finite effective epimorphic family. Condition GT-2) is a consequence of the precoherence assumption: Let $f: X \to Y$ be a morphism and let $S$ be a sieve on $Y$ that is contained in $\mathcal{T}$, i.e. that contains a finite effective epimorphic family $(\pi_i: Y_i \to Y)_{i \in I}$. Then the condition of being precoherent (see Definition 5.6) provides an effective epimorphic family $(\pi'_j: X_j \to X)_{j \in I'}$ that is contained in the pullback sieve $f^*S$. Finally, we address GT-3). Let $S, R$ be sieves on $Y$ with $S \in \mathcal{T}$ such that for every $f: X \to Y \in S$, the pullback sieve $f^*R$ is in $\mathcal{T}$. Then we have a finite effective epimorphic family $(f_i: X_i \to Y)_{i \in I}$ contained in $S$, and for each $i \in I$, a finite effective epimorphic family $(g_{i,j}: X_{i,j} \to X_i)_{j \in J_i}$ contained in $f_i^*R$. By Lemma 6.12, the finite family $(f_i \circ g_{i,j}: X_{i,j} \to Y)_{i \in I, j \in J_i}$ is effective epimorphic. By Definition 3.10 of the pullback sieve, the composition $f_i \circ g_{i,j}$ factors through some morphism in $R$, hence lies in $R$ for each pair $(i, j)$. Thus the whole family $(f_i \circ g_{i,j})_{i \in I, j \in J_i}$ is contained in $R$, showing that $R \in \mathcal{T}$. This finishes the proof of Condition GT-3). $\square$

**Proposition 6.13.** ☐ Let $\mathcal{C}$ be a preregular, finitary extensive category with pullbacks of kernel pairs. A presheaf on $\mathcal{C}$ is a sheaf for the coherent topology if and only if it satisfies the equalizer condition (EqCond) of Lemma 6.3, and preserves finite products.

*Proof.* It is easy to see that a presheaf is a sheaf for the topology generated by a union of coverages if and only if it is a sheaf for every covering presieve of both coverages ☐. The result now follows by combining Proposition 5.9 with Lemma 6.3 and Proposition 6.5. $\square$

**Proposition 6.14.** ☐ Let $\mathcal{C}$ be a preregular, finitary extensive category in which every object is projective. A presheaf on $\mathcal{C}$ is a sheaf for the coherent topology if and only if it preserves finite products.

*Proof.* As in the proof of Proposition 6.13, the result follows by combining Proposition 6.4 with Proposition 6.5. $\square$

**Proposition 6.15.** ☐ Let $\mathcal{C}$ be a category and let $F: \mathcal{C} \to \mathcal{D}$ be a fully faithful functor into a precoherent category $\mathcal{D}$ such that

1) $F$ preserves and reflects finite effective epimorphic families.

2) For every object $Y$ of $\mathcal{D}$, there exists an object $X$ of $\mathcal{C}$ and an effective epimorphism $F(X) \to Y$.

Then the following holds:

a) $\mathcal{C}$ is precoherent.

b) Let $G$ be a sheaf for the coherent topology on $\mathcal{D}$. The presheaf $G \circ F^{\text{op}}$ is a sheaf for the coherent topology on $\mathcal{C}$.

c) Precomposition with $F$ induces an equivalence between the categories of sheaves for the coherent topology on $\mathcal{C}$ and on $\mathcal{D}$.

Before proving Proposition 6.15, we need to fix some terminology and state some preliminary results. These preliminaries were already in MATHLIB, and we simply state them here without proof. The results can be extracted from [SGA72, Exposé III], but the approach ibid. differs slightly from the one in MATHLIB.

**Definition 6.16.** Let $\mathcal{C}$ and $\mathcal{D}$ be two categories, both endowed with a Grothendieck topology, and let $F: \mathcal{C} \to \mathcal{D}$ be a functor. Fix an object $X$ in $\mathcal{C}$ and an object $Y$ in $\mathcal{D}$.

a) Given a sieve $S$ on $X$, the functor-pushforward of $S$ along $F$ is the sieve $F_*S$ on $F(X)$ consisting of those morphisms $f: Y \to F(X)$ that factor through $F(g)$ for some morphism $g: Z \to X$ in $S$. ☐

b) Given a sieve $S$ on $F(X)$, the functor-pullback of $S$ along $F$ is the sieve $F^*S$ on $X$ consisting of those arrows $f$ such that $F(f)$ belongs to $S$. ☐
c) The F-image sieve is the sieve $S_Y^F$ on $Y$ consisting of those morphisms to $Y$ that factor through an object of the form $F(X)$ for some $X$ in $\mathcal{C}$. ☐

We omit the verification that Definition 6.16 is actually defining sieves (one needs to check that they are downwards closed). This verification was formalized in MATHLIB, and each point of Definition 6.16 contains the corresponding external link.

**Definition 6.17.** In the same setting of Definition 6.16, denote by $\mathcal{T}$ the topology on $\mathcal{C}$ and by $\mathcal{T}'$ that on $\mathcal{D}$.

a) We say that $F$ is continuous if for every $\mathcal{T}'$-sheaf $P$ on $\mathcal{D}$, the presheaf $P \circ F^{\text{op}}$ on $\mathcal{C}$ is a $\mathcal{T}$-sheaf ☐. In particular, if $F$ is continuous it induces a functor

$$F^*: \mathrm{Sh}_{\mathcal{T}'}(\mathcal{D}) \to \mathrm{Sh}_{\mathcal{T}}(\mathcal{C}).$$

b) We say that $F$ is cocontinuous if for every object $U$ of $\mathcal{C}$ and every $\mathcal{T}'$-covering sieve $S$ on $F(U)$, the functor-pullback $F^*S$ is a $\mathcal{T}$-covering sieve of $U$. ☐

c) We say that $F$ is cover-dense if for every object $Y$ of $\mathcal{D}$, the F-image sieve $S_Y^F$ is a $\mathcal{T}'$-covering sieve. ☐

**Remark 6.18.** Observe that in point c) of Definition 6.17 the topology $\mathcal{T}$ on $\mathcal{C}$ plays no role. Hence, to speak of cover-dense functors one only needs a Grothendieck topology on the target.

**Proposition 6.19.** ☐ ☐ In the setting of Definition 6.17, suppose that $F$ is continuous and cocontinuous. Then we have an adjunction $F^* \dashv F_*$.$\blacksquare$ If $F$ is also fully faithful and cover-dense, then this adjunction is an adjoint equivalence of categories.

**Definition 6.20.** ☐ Let $\mathcal{C}$ and $\mathcal{D}$ be categories, let $\mathcal{T}'$ be a Grothendieck topology on $\mathcal{D}$ and let $F: \mathcal{C} \to \mathcal{D}$ be a fully faithful cover-dense functor. Define a Grothendieck topology $\mathcal{T}$ on $\mathcal{C}$ as follows: we declare that a sieve $S$ on an object $X$ in $\mathcal{C}$ is a $\mathcal{T}$-covering sieve if and only if the functor-pushforward sieve $F_*S$ is a $\mathcal{T}'$-covering sieve of $F(X)$ (see ☐ for a proof of the fact that this indeed defines a Grothendieck topology). This is called the topology induced by $F$.

**Lemma 6.21.** ☐ Let $\mathcal{C}$ and $\mathcal{D}$ be categories, let $\mathcal{T}'$ a Grothendieck topology on $\mathcal{D}$ and let $F: \mathcal{C} \to \mathcal{D}$ be a fully faithful cover-dense functor. Equip $\mathcal{C}$ with the induced topology. Then $F$ is continuous and cocontinuous.

*Proof of Proposition 6.15.* To show that $\mathcal{C}$ is precoherent, let $(\pi_i: X_i \to B)_i$ be a finite effective epimorphic family in $\mathcal{C}$ and let $f: B' \to B$ be any morphism. The family $F(\pi_i)$ is finite effective epimorphic (in $\mathcal{D}$) by condition 1): then, the hypothesis that $\mathcal{D}$ is precoherent, applied to the morphism $F(f): F(B') \to F(B)$, provides a finite effective epimorphic family $\varpi_j: Y_j \to F(B')$ whose components factor through some of the $F(\pi_i)$. By condition 2) there exist objects $(X'_j)_j$ in $\mathcal{C}$ together with effective epimorphisms $\varphi_j: F(X'_j) \to Y_j$, that combine into an effective epimorphic family $F(X'_j) \to F(B')$ thanks to Lemma 6.12; moreover, the morphisms in this family are of the form $F(\pi'_j)$ for suitable $\pi'_j: X'_j \to B'$ because $F$ is fully faithful. Applying again condition 1), this family $(\pi'_j)_j$ is finite effective epimorphic; that, for each $j$, the morphism $\pi'_j$ factors through some of the $\pi_i$ follows from the equivalent statement for the components of $\varpi_j$, combined once more with the full faithfulness of $F$. This establishes point a).

We claim that the topology on $\mathcal{C}$ induced by $F$ is the coherent topology. It suffices to show that given an object $X$ of $\mathcal{C}$, a sieve $S$ on $X$ is a covering for the induced topology if and only if it contains a finite effective epimorphic family. Suppose first that $S$ contains a finite effective epimorphic family $(\pi_i: Y_i \to X)_i$. By condition 1), the family $(F(\pi_i))_i$ is finite effective epimorphic, and is clearly contained in $F_*S$. Hence $F_*S$ is a covering sieve of $F(X)$ with respect to the coherent topology on $\mathcal{D}$ by Proposition 6.10, which means that $S$ is a covering sieve with for the induced topology (see Definition 6.20). For the other direction, suppose that $S$ is a covering sieve for the induced topology: as for the first implication, this is equivalent to the condition that $F_*S$ contains a finite effective epimorphic family $(\pi_i: Z_i \to F(X))_i$. Condition 2) ensures that for every $i$, there is an effective epimorphism of the form $f_i: F(Y_i) \to Z_i$; moreover, since $\mathcal{C}$ is precoherent, we can apply Lemma 6.12 to obtain that the family $(\pi_i \circ f_i: F(Y_i) \to F(X))_i$ is effective epimorphic. Since $F$ is full and reflects finite effective epimorphic families by condition 1), this family can be pulled back to a finite effective epimorphic family $(Y_i \to X)_i$ contained in $F^*(F_*S)$. We conclude thanks to Proposition 6.19.

Endowing $\mathcal{D}$ with the coherent topology, point b) is now immediate from Lemma 6.21 (see Definition 6.17).
To finish the proof, we pass to point c), again endowing $\mathcal{D}$ with the coherent topology. By Proposition 6.19, it suffices to prove that $F$ is cover-dense, continuous and cocontinuous. By Lemma 6.21 and the above discussion, it suffices to prove that $F$ is cover-dense. By Proposition 6.10, it suffices to show that for every object $Y$ of $\mathcal{D}$, the $F$-image sieve $S_Y^F$ contains an effective epimorphism. Condition 2) ensures the existence of an object $X$ in $\mathcal{C}$ and of an effective epimorphism $F(X) \to Y$, that, by definition of the $F$-image sieve, belongs to $S_Y^F$. $\square$

**Remark 6.22.** A finite-coproduct preserving functor between finitary extensive categories preserves (resp. reflects) finite effective epimorphic families if and only if it preserves (resp. reflects) effective epimorphisms. This is because finite effective epimorphic families in extensive categories are precisely those that induce effective epimorphisms on the coproduct (see Lemmas 4.8 and 4.9). This observation yields variants (see for instance $\surd$) of Proposition 6.15 in the case where the target is preregular and finitary extensive and the functor preserves certain pullbacks and coproducts, or when the target category is already finitary extensive.

## 7. CONDENSED MATHEMATICS

We can now introduce condensed sets and prove the main theorems from our general categorical results. We begin with the following result:

**Proposition 7.1.** *The categories *CompHaus*, *Profinite* and *Stonean* are preregular and finitary extensive.*

*Proof.* $\surd \surd \surd \surd \surd \surd$ Let $\mathcal{C}$ denote any of the categories *CompHaus*, *Profinite* or *Stonean*. Note that the effective epimorphisms in $\mathcal{C}$ are precisely the continuous surjections (Proposition 4.13). These also coincide with the epimorphisms, by Lemma 4.10. Given the explicit description of pullbacks in *Profinite* and *CompHaus*, we immediately obtain that effective epimorphisms can be pulled back, and therefore *Profinite* and *CompHaus* are preregular. To see that *Stonean* is preregular, we use the fact that every object in *Stonean* is projective, and hence every epimorphism can be pulled back to the identity.

We also need to show that $\mathcal{C}$ is finitary extensive. In *MATHLIB* it was already proved that the category of all topological spaces is finitary extensive, and that given a functor $F: \mathcal{C} \to \mathcal{D}$ to a finitary extensive category which preserves and reflects finite coproducts, preserves pullbacks along coprojections in finite coproducts and reflects pullbacks, if $\mathcal{C}$ has finite coproducts and pullbacks along coprojections, then $\mathcal{C}$ is finitary extensive. To see that $\mathcal{C}$ together with its inclusion functor to the category of topological spaces has these properties, the only point which needs clarification is the case for pullbacks in *Stonean*. We know that *Stonean* does not have all pullbacks, but in the very special case of coprojections in finite coproducts, it does. Indeed, these are clopen embeddings, in which case the pullback is identified with the preimage of the image of the embedding. $\square$

**Definition 7.2.** $\surd$ A condensed set is a sheaf for the coherent topology on *CompHaus*. (We refer the reader to Definition 5.6 for the definition of coherent topology.)

**Remark 7.3.** Thanks to Theorem 7.7 below, a condensed set can be defined as a sheaf for the coherent topology on *Profinite* or *Stonean*.

**Theorem 7.4.** $\surd \surd$

a) When $\mathcal{C}$ is *CompHaus* or *Profinite*, a presheaf $X: \mathcal{C}^{\mathrm{op}} \to \mathrm{Set}$ is a sheaf for the coherent topology on $\mathcal{C}$ if and only if it satisfies the following two conditions:

1) $X$ preserves finite products: in other words, for every finite family $(T_i)$ of object of $\mathcal{C}$, the natural map

$$X(\coprod_i T_i) \to \prod_i X(T_i)$$

is a bijection.

2) For every surjection $\pi: S \to T$ in $\mathcal{C}$, the diagram

$$X(T) \xrightarrow{X(\pi)} X(S) \longrightarrow X(S \times_T S)$$

is an equalizer (the two parallel morphisms being given by the projections in the pullback).
b) A presheaf $X$: Stonean$^{OP}$ → Set is a sheaf for the coherent topology on Stonean if and only if it preserves finite products: in other words, for every finite family $(T_i)$ of object of $\mathcal{C}$, the natural map

$$X(\coprod_i T_i) \to \prod_i X(T_i)$$

is a bijection.

*Proof.* In the case when $\mathcal{C}$ is CompHaus or Profinite, it has all pullbacks and we obtain the characterization from Proposition 6.13. In the case of Stonean, since every object is projective, we obtain the characterization from Proposition 6.14. □

**Remark 7.5.** A detailed proof of Theorem 7.4 is given in [Asg21, Theorems 1.2.17 and 1.2.18].

**Remark 7.6.** A condition similar to the one in point a) of Theorem 7.4 above holds true when $\mathcal{C}$ is Stonean as well, except that condition a)-1) must be modified slightly (for example, using 1-hypercovers) due to the fact that Stonean does not have pullbacks. The content of b) is that this analogous condition turns out to be vacuously true in Stonean.

**Theorem 7.7.** ☞ ☞ The inclusion functors Profinite → CompHaus and Stonean → CompHaus induce equivalences of categories between the categories of sheaves for the coherent topology on CompHaus, Profinite, and Stonean.

*Proof.* We are going to apply Proposition 6.15. We spell out the case of Stonean here, the other one being similar. It is clear that the inclusion functor preserves and reflects effective epimorphisms (by the characterization of effective epimorphisms as continuous surjections). Verifying the other condition in the theorem amounts to proving that CompHaus has enough projectives. Given a compact Hausdorff space $S$, denote by $S^\delta$ the set $S$ equipped with the discrete topology. Then the Stone-Čech compactification $\beta S^\delta$ is a projective object with a continuous surjection $\beta S^\delta \to S$. □

## ACKNOWLEDGMENTS

This work began when the five authors gathered in Copenhagen for the Masterclass: Formalisation of Mathematics that took place in June 2023. We are grateful to Kevin Buzzard for the lectures he delivered jointly with one of the authors (A. T.) and to Boris Kjær who co-organized the masterclass with another author (D. A.). Financial support for the masterclass was provided by the Copenhagen Centre for Geometry and Topology (GeoTop) and D. A. acknowledges funding from GeoTop through grant CPH-GEOTOP-DNRF151. N. K. was supported by the Research Council of Norway grant 302277 – Orthogonal gauge duality and non-commutative geometry. F. N. was supported by a projet émergent from Labex MILYON/ANR-10-LABX-0070. A. T. is funded by NSERC discovery grant RGPIN-2019-04762.

All authors wish to express their gratitude to the whole MATHLIB community for their support and interest in this work, and in particular to Johan Commelin and to Joël Riou for reviewing and improving many pull requests related to the work presented here.

## REFERENCES

[Asg21] Dagur Asgeirsson, *The Foundations of Condensed Mathematics*, https://dagur.sites.ku.dk/files/2022/01/condensed-foundations.pdf, 2021, Master thesis.

[Asg24] __________, *Towards solid abelian groups: A formal proof of Nöbeling's theorem*, https://arxiv.org/abs/2309.07252v2, 2024.

[BH19] Clark Barwick and Peter Haine, *Pyknotic objects*, I. Basic notions*, https://arxiv.org/abs/1904.09966, 2019.

[Car19] Mario Carneiro, *The type theory of Lean*, https://github.com/digama0/lean-type-theory/releases, 2019, Master thesis.

[CLW93] Aurelio Carboni, Stephen Lack, and R.F.C. Walters, *Introduction to extensive and distributive categories*, Journal of Pure and Applied Algebra **84** (1993), no. 2, 145–158.

[CS22] Dustin Clausen and Peter Scholze, *Condensed mathematics and complex geometry*, https://people.mpim-bonn.mpg.de/scholze/Complex.pdf, 2022.
[CT+22] Johan Commelin, Adam Topaz, et al., *Liquid Tensor Experiment*, https://github.com/leanprover-community/lean-liquid, 2022.

[dMU21] Leonardo de Moura and Sebastian Ullrich, *The Lean 4 theorem prover and programming language, Automated deduction—CADE 28, Lecture Notes in Comput. Sci.*, vol. 12699, Springer, Cham, 2021, pp. 625–635. MR 4366655

[Gle58] Andrew M. Gleason, *Projective topological spaces*, Illinois J. Math. **2** (1958), 482–489. MR 121775

[Joh02] Peter T. Johnstone, *Sketches of an elephant: a topos theory compendium*. Vol. 2, Oxford Logic Guides, vol. 44, The Clarendon Press, Oxford University Press, Oxford, 2002. MR 2063092

[Lur18] Jacob Lurie, *Ultracategories*, https://www.math.ias.edu/~lurie/papers/Conceptual.pdf, 2018.

[mC20] The mathlib Community, *The lean mathematical library*, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (New York, NY, USA), CPP 2020, Association for Computing Machinery, 2020, p. 367–381.

[Sch19a] Peter Scholze, *Lectures on analytic geometry*, http://www.math.uni-bonn.de/people/scholze/Analytic.pdf, 2019.

[Sch19b] —, *Lectures on condensed mathematics*, https://www.math.uni-bonn.de/people/scholze/Condensed.pdf, 2019.

[Sch22] —, *Liquid tensor experiment*, Exp. Math. **31** (2022), no. 2, 349–354. MR 4458116

[SGA72] *Théorie des topos et cohomologie étale des schémas. Tome 1: Théorie des topos*, Lecture Notes in Mathematics, vol. 269, Springer-Verlag, Berlin-New York, 1972, Séminaire de Géométrie Algébrique du Bois-Marie 1963–1964 (SGA 4), Dirigé par M. Artin, A. Grothendieck, et J. L. Verdier. Avec la collaboration de N. Bourbaki, P. Deligne et B. Saint-Donat. MR 354652

(D. A.) **UNIVERSITY OF COPENHAGEN**

Email address: dagur@math.ku.dk

(R. B.) **INSTITUT DE MATHÉMATIQUES DE JUSSIEU-PARIS RIVE GAUCHE, UNIVERSITÉ PARIS-CITÉ**

Email address: riccardo.brasca@imj-prg.fr

(N. K.) **UNIVERSITY OF OSLO**

Email address: ntkuhn@posteo.net

(F. N.) **UNIVERSITÉ JEAN MONNET, CNRS, ECOLE CENTRALE DE LYON, INSA LYON, UNIVERSITE CLAUDE BERNARD LYON 1, ICJ UMR5208, 42023 SAINT-ETIENNE, FRANCE**

Email address: filippo.nuccio@univ-st-etienne.fr

(A. T.) **UNIVERSITY OF ALBERTA**

Email address: topaz@ualberta.ca