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,CA, B, C\dots, function symbols f,:ABf, \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

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

where PP and QQ are formulae, and xx 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 PP and QQ, 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 OT\mathcal{O}_T — we see that the entailment relation xyx \vdash y equips the objects of OT\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

xiF(i)=i(xF(i)) 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 XX, 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 XX can be called the classifying space of the theory TT, since points of XX correspond to models of TT, and the specialisation preorder on XX 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 omissions1, a category satisfying these assumptions is exactly a Grothendieck topos, and every topos classifies a particular theory, in the sense that, letting GG and E\ca{E} be topoi, a geometric morphism GEG \to \ca{E} is equivalent to an E\ca{E}-model in GG.

That begs a question: What theory do presheaf topoi PSh(C)\psh(\ca{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:CEF : \ca{C} \to \ca{E} is one whose left Kan extension along the Yoneda embedding \yo (i.e. its realisation) is left exact. The theorem is almost tautological then: Letting FF be a functor, the nerve-realisation adjunction Lan(F)hom(F(),)\Lan_\yo(F) \dashv \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)

    : {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:CPSh(D)f : \ca{C} \to \psh(\ca{D}) has an inverse image f:PSh(D)Cf^* : \psh(\ca{D}) \to \ca{C}, which we can turn into a functor DC\ca{D} \to \ca{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:DCF : \ca{D} \to \ca{C} can be recovered as the composite Lan(F)\Lan_\yo(F) \circ \yo, because \yo is a fully faithful functor.

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

  1. Disjointness of coproducts and effectivity of congruences.↩︎