open import Algebra.Prelude open import Cat.Diagram.Colimit.Base open import Cat.Diagram.Limit.Finite open import Cat.Functor.Everything open import Cat.Diagram.Initial open import Cat.Instances.Comma open import Topoi.Base import Cat.Functor.Reasoning as Functor-kit import Cat.Reasoning module Topoi.Classifying.Diaconescu where

# Diaconescu’s theorem🔗

Let
$\Sigma$
be a **signature** consisting of sorts
$A, B, C\dots$,
function symbols
$f, \dots : A \to B$,
and relation symbols
$~, \dots$.
We can build a **logical theory** on top of this signature
by imposing **axioms** of the form

$P \vdash_{x} Q\text{,}$

where $P$ and $Q$ are formulae, and $x$ is a context consisting of variables typed with sorts from the signature. Depending on the signature and on what connectives are used to build up the formulae $P$ and $Q$, our logical theory can fit within several frameworks:

If our formulae can be presented using only $\land$, $\top$, and the equality relation $=$, then our logic is called

**cartesian logic**, and our theory a**cartesian theory**.**Regular logic**is obtained by augmenting cartesian logic with the quantifier $\exists$.**Coherent logic**is obtained by augmenting regular logic with disjunction $\lor$ and falsity $\bot$.**Geometric logic**is obtained by augmenting coherent logic with*infinitary*disjunction $\bigvee$.

In addition to the qualifiers above, if our signature has
**no** sorts, then our theory will be called a
“propositional theory”: A theory built up of
$\land, \bigvee, \top, \bot, \exists$
on a signature with no sorts is called a **propositional geometric
theory**.

Let the contexts of such a theory be denoted by $\mathcal{O}_T$ — we see that the entailment relation $x \vdash y$ equips the objects of $\mathcal{O}_T$ with a preorder structure, with the conjunctions providing meets and the (infinitary) disjunctions providing joins. Additionally, in this proset, the distributive law

$x \land \bigvee_i F(i) = \bigvee_i (x \land F(i))$

holds. We call such a structure a *frame*, and we can see that
that a frame determines a topological space
$X$,
by letting the opens of the topology be the elements of the frame (the
points come for free as filters satisfying a certain condition). This
space
$X$
can be called the **classifying space** of the theory
$T$,
since points of
$X$
correspond to models of
$T$,
and the specialisation preorder on
$X$
corresponds to homomorphism of models.

If our theory is *not* propositional, however, a topological
space won’t cut it, since there can be more than one homomorphism
between two given models! Most geometric theories (the theory of groups,
the theory of (local) rings, the theory of fields, the theory of an
object) are *not* propositional, so they won’t have useful
classifying spaces in this sense. If we relax the requirement that
specialisation be a preorder and allow a *set* of model
homomorphisms, the structure we get is a category satisfying certain
completeness and exactness properties:

The meets our frame used to have are now finite limits, and the
infinitary disjunctions are colimits; The infinite
distributive law corresponds to the statement that the pullback functors preserve
colimits, which follows from the pullback functors having right adjoints
(i.e. the category is locally
cartesian closed). Up to a couple of small omissions^{1}, a
category satisfying these assumptions is exactly a **Grothendieck
topos**, and every topos classifies a particular theory, in
the sense that, letting
$G$
and
$\mathcal{E}$
be topoi, a geometric morphism
$G \to \mathcal{E}$
is equivalent to an
$\mathcal{E}$-model
in
$G$.

That begs a question: What theory do presheaf topoi
${{\mathrm{PSh}}}(\mathcal{C})$
classify? Most presheaf topoi (e.g. the topos of quivers, the topos of
simplicial sets, the topos of sets) are *very far* from being
logically inspired: Most of those are conceived as being categories of
*geometric* objects! The answer is given by **Diaconescu’s
theorem**:

A presheaf topos classifies the flat functors on its site.

A **flat functor**
$F : \mathcal{C} \to \mathcal{E}$
is one whose left Kan extension along
the Yoneda embedding
${よ}$
(i.e. its realisation) is left exact. The
theorem is almost tautological then: Letting
$F$
be a functor, the nerve-realisation adjunction
$\operatorname{Lan}_{よ}(F) \dashv {\mathbf{Hom}}(F(-), -)$
is 75% of the way to being a geometric morphism, with
flatness *definitionally* guaranteeing that the left adjoint is
lex.

Flat : {D : Precategory κ κ} → Functor D C → Type _ Flat F = is-lex (Realisation colim F) Diaconescu : {D : Precategory κ κ} (F : Functor D C) → Flat F → Geom[ C , PSh κ D ] Inv[ Diaconescu F F-flat ] = Realisation colim F Dir[ Diaconescu F F-flat ] = Nerve F Diaconescu F F-flat .Inv-lex = F-flat Diaconescu F F-flat .Inv⊣Dir = Realisation⊣Nerve colim F

Conversely, any given geometric morphism $f : \mathcal{C} \to {{\mathrm{PSh}}}(\mathcal{D})$ has an inverse image $f^* : {{\mathrm{PSh}}}(\mathcal{D}) \to \mathcal{C}$, which we can turn into a functor $\mathcal{D} \to \mathcal{C}$ by precomposing with the Yoneda embedding:

Diaconescu⁻¹ : ∀ {D : Precategory κ κ} → Geom[ C , PSh κ D ] → Functor D C Diaconescu⁻¹ f = Inv[ f ] F∘ よ _

A standard fact about the computation of left Kan extensions as colimits tells us that any functor (flat or not) $F : \mathcal{D} \to \mathcal{C}$ can be recovered as the composite $\operatorname{Lan}_{よ}(F) \circ {よ}$, because ${よ}$ is a fully faithful functor.

Diaconescu-invl : Diaconescu⁻¹ (Diaconescu F flat) DC.≅ F Diaconescu-invl = ff-lan-ext colim (よ D) F (よ-is-fully-faithful D)