module Topoi.Base where

# Grothendieck topoiπ

Topoi are an abstraction introduced by Alexander Grothendieck in the
1960s as a generalisation of topological
spaces, suitable for his work in algebraic geometry. Later (in the
work of William Lawvere, and even later Myles Tierney), topoi found a
new life as βcategories with a nice internal logicβ, which mirrors that
of the category
$\mathbf{Sets}$.
Perhaps surprisingly, every Grothendieck topos is also a topos in their
logical conception (called **elementary**); Since
elementary topoi are very hard to come by predicatively, we formalise a
particular incarnation of Grothendieckβs notion here.

Grothendieck described his topoi by first defining a notion of
*site*, which generalises the (poset of) open subsets of a
topological space, and then describing what βsheaves on a siteβ should
be, the corresponding generalisation of sheaves on a space. Instead of
directly defining the notion of site, we will leave it implicitly, and
define a **topos** as follows:

A **topos**
$\mathcal{T}$
is a full subcategory of
a presheaf
category
$[\mathcal{C}^{\mathrm{op}},\mathbf{Sets}]$
(the category
$\mathcal{C}$
is part of the definition) such that the inclusion functor
$\iota : \mathcal{T} \hookrightarrow [\mathcal{C}^{\mathrm{op}},\mathbf{Sets}]$
admits a left adjoint,
and this left adjoint preserves finite
limits. We summarise this situation in the diagram below, where
βlexβ (standing for β**l**eft **ex**actβ) is
old-timey speak for βfinite limit preservingβ.

In type theory, we must take care about the specific universes in which everything lives. Now, much of Grothendieck topos theory generalises to arbitrary βbaseβ topoi, via the use of bounded geometric morphisms, but the βmainβ definition talks about $\mathbf{Sets}$-topoi. In particular, every universe $\kappa$ generates a theory of $\mathbf{Sets}_\kappa$-topoi, the categories of $\kappa$-small sheaves on $\kappa$-small sites.

Fix a universe level
$\kappa$,
and consider the category
$\mathbf{Sets}_\kappa$:
A topos
$\mathcal{T}$
might be a large category (i.e.Β it might have a space of objects
$o$
with
$o > \kappa$),
but it is *essentially locally small*, since it admits a
fully-faithful functor into
$[\mathcal{C}^{\mathrm{op}},\mathbf{Sets}_\kappa]$,
which have homs at level
$\kappa$.
Hence, even if we allowed the category
$\mathcal{T}$
to have
$\mathbf{Hom}$s
at a level
$\ell$,
we would have no more information there than fits in
$\kappa$.

For this reason, a topos $\mathcal{C}$ only has two levels: The level $o$ of its objects, and the level $\kappa$ of the category of Sets relative to which $\mathcal{C}$ is a topos.

record Topos {o} ΞΊ (π£ : Precategory o ΞΊ) : Type (lsuc (o β ΞΊ)) where field site : Precategory ΞΊ ΞΊ ΞΉ : Functor π£ (PSh ΞΊ site) has-ff : is-fully-faithful ΞΉ L : Functor (PSh ΞΊ site) π£ L-lex : is-lex L Lβ£ΞΉ : L β£ ΞΉ module ΞΉ = Functor ΞΉ module L = Functor L module Lβ£ΞΉ = _β£_ Lβ£ΞΉ

## As generalised spacesπ

Iβll echo here the standard definition of topological space, but due
to personal failings I canβt motivate it. A **topological
space**
$(X, \tau)$
consists of a set of *points*
$X$,
and a *topology*
$\tau$,
a subset of its powerset which is closed
under arbitrary unions and finite intersections.

Letβs reword that using category-theoretic language: Recall that the
powerset of
$X$
is the poset
$[X,\mathbf{Props}]$.
It is β being a functor category into a complete and cocomplete (thin)
category β *also* complete and cocomplete, so all joins and
finite meets (unions and intersections) exist; Furthermore, the
distributive law

$S \cap \left(\bigcup_i F_i\right) = \bigcup_i (S \cap F_i)$

holds for any subset
$S$
and family of subsets
$F$.
A lattice satisfying these properties
(finite meets, arbitrary joins, the distributive law) is called a
**frame**. A map of frames
$f : A \to B$
is defined to be a map of their underlying sets preserving finite meets
and arbitrary joins β by abstract nonsense, this is the same as a
function
$f^* : A \to B$
which preserves finite meets and has a right adjoint
$f_* : B \to A$^{1}.

We can prove that a topology $\tau$ on $X$ is the same thing as a subframe of its powerset $[X,\mathbf{Props}]$ β a collection of subsets of $X$, closed under finite meets and arbitrary joins.

Now, the notion of βtoposβ as a generalisation of that of
βtopological spaceβ is essentially self-evident: A topos
$\mathcal{T}$
is a sub-topos of a presheaf category
$[\mathcal{C}^{\mathrm{op}},\mathbf{Sets}]$.
We have essentially categorified βsubframeβ into βsubtoposβ, and
$\mathbf{Props}$
into
$\mathbf{Sets}$.
Note that, while this seems circular (βa topos is a sub-topos ofβ¦β), the
notion of subtopos β or rather, of **geometric embedding**
β makes no mention of actual topoi, and makes sense for any pair of
categories.

## As categories of spacesπ

Another perspective on topoi is that they are *categories of*
spaces, rather than spaces themselves. We start by looking at presheaf
topoi,
$[\mathcal{C}^{\mathrm{op}},\mathbf{Sets}]$.
The coyoneda lemma tells us
that every presheaf is a colimit of representables, which can be
restated in less abstract terms by saying that *presheaves are
instructions for gluing together objects of
$\mathcal{C}$.*
The objects of
$\mathcal{C}$
are then interpreted as βprimitive shapesβ, and the maps in
$\mathcal{C}$
are interpreted as βmaps to glue againstβ.

Letβs make this more concrete by considering an example: Take
$\mathcal{C} = \bull \rightrightarrows \bull$,
the category with two points β letβs call them
$V$
and
$E$
β and two arrows
$s, t : V \to E$.
A presheaf
$F$
on this category is given by a set
$F_0(V)$,
a set
$F_0(E)$,
and two functions
$F_1(s), F_1(t) : F_0(E) \to F_0(V)$.
We call
$F_0(V)$
the vertex set, and
$F_0(E)$
the edge set. Indeed, a presheaf on this category is a *directed
multigraph*, and maps between presheaves *preserve
adjacency*.

Our statement about βgluing primitive shapesβ now becomes the rather pedestrian statement βgraphs are made up of vertices and edgesβ. For instance, the graph $\bull \to \bull \to \bull$ can be considered as a disjoint union of two edges, which is then glued together in a way such that the target of the first is the source of the second. The maps $s, t : V \to E$ exhibit the two ways that a vertex can be considered βpart ofβ an edge.

## As βlogically niceβ categoriesπ

The definition of topos implies that any topos $\mathcal{T}$ enjoys many of the same categorical properties of the category $\mathbf{Sets}$ (see below). Topoi are complete and cocomplete, cartesian closed (even locally so) β colimits are stable under pullback, coproducts are disjoint, and equivalence relations are effective.

These properties, but *especially* local cartesian closure,
imply that the internal logic of a topos is an incredibly nice form of
type theory. Dependent sums and products exist, there is an object of
natural numbers, the poset of subobjects of any object is a complete lattice (even a Heyting algebra),
including existential and universal quantification. Effectivity of
congruences means that two points in a quotient are identified if, and
only if, they are related by the congruence.

In fact, this is essentially the *definition of* a topos. The
actual definition, as a lex reflective subcategory of
a presheaf category, essentially ensures that the category
$\mathcal{T}$
inherits the nice logical properties of
$\mathbf{Sets}$
(through the presheaf category, which is *also* very nice
logically).

As was implicitly mentioned above, for a topos
$L : \mathcal{T} \xrightleftarrows[]{} \mathrm{PSh}(\mathcal{C})$,
we call the category
$\mathcal{C}$
the **site of definition**. Objects in
$\mathcal{T}$
are called **sheaves**, and the functor
$L$
is called **sheafification**. Maps between topoi are called
**geometric morphisms**, and will be defined below. We
denote the 2-category of topoi, geometric morphisms and natural
transformations by
$\mathfrak{Topos}$,
following Johnstone. When
$\mathrm{PSh}(\mathcal{C})$
is regarded as a topos unto itself, rather than an indirection in the
definition of a sheaf topos, we call it the **topos of
$\mathcal{C}$-sets**.

# Examplesπ

The βtrivialβ example of topoi is the category
$\mathbf{Sets}$,
which is equivalently the category
$[*^{\mathrm{op}},\mathbf{Sets}]$
of presheaves on the terminal
category. This is, in fact, the terminal object in
the 2-category
$\mathfrak{Topos}$
of topoi (morphisms are described below), so we denote it by
`π`

.

π : β {ΞΊ} β Topos ΞΊ (Sets ΞΊ) π {ΞΊ} = sets where open Topos open Functor open _β£_ open is-lex

The inclusion functor $\mathbf{Sets} \hookrightarrow \mathrm{PSh}(*)$ is given by the βconstant presheafβ functor, which sends each set $X$ to the constant functor with value $X$.

incl : Functor (Sets ΞΊ) (PSh ΞΊ (Lift-cat ΞΊ ΞΊ β€Cat)) incl .Fβ x .Fβ _ = x incl .Fβ x .Fβ _ f = f incl .Fβ x .F-id = refl incl .Fβ x .F-β f g = refl incl .Fβ f = NT (Ξ» _ β f) (Ξ» _ _ _ β refl) incl .F-id = Nat-path Ξ» _ β refl incl .F-β f g = Nat-path Ξ» _ β refl sets : Topos ΞΊ (Sets ΞΊ) sets .site = Lift-cat ΞΊ ΞΊ β€Cat sets .ΞΉ = incl

This functor is fully faithful since a natural transformation between presheaves on the point is entirely determined by its component at.. well, the point. Hence, the map $\eta \mapsto \eta_*$ exhibits an inverse to the inclusion functorβs action on morphisms, which is sufficient (and necessary) to conclude fully-faithfulness.

sets .has-ff {x} {y} = is-isoβis-equiv isic where open is-iso isic : is-iso (incl .Fβ {x} {y}) isic .inv nt = Ξ· nt _ isic .rinv nt i .Ξ· _ = Ξ· nt _ isic .rinv nt i .is-natural _ _ f j x = y .is-tr _ _ (Ξ» j β nt .Ξ· _ x) (Ξ» j β nt .is-natural _ _ f j x) i j isic .linv x i = x

The βsheafificationβ left adjoint is given by evaluating a presheaf $F$ at its sole section $F(*)$, and similarly by evaluating a natural transformation $\eta : F \Rightarrow G$ at its one component $\eta_* : F(*) \to G(*)$.

sets .L .Fβ F = Fβ F _ sets .L .Fβ nt = Ξ· nt _ sets .L .F-id = refl sets .L .F-β f g = refl

## These functors actually define an adjoint equivalence of categories, $L$ is continuous and, in particular, lex. Rather than appealing to that theorem, though, we define the preservation of finite limits directly for efficiency concerns.

sets .L-lex .pres-β€ {T} psh-terminal set = contr (cent .Ξ· _) uniq where func = incl .Fβ set cent = psh-terminal func .centre uniq : β f β cent .Ξ· _ β‘ f uniq f = psh-terminal func .paths f' Ξ·β _ where f' : _ => _ f' .Ξ· _ = f f' .is-natural _ _ _ = funext Ξ» x β happly (sym (F-id T)) _ sets .L-lex .pres-pullback {P} {X} {Y} {Z} pb = pb' where open is-pullback pb' : is-pullback (Sets ΞΊ) _ _ _ _ pb' .square = pb .square Ξ·β _ pb' .universal {P'} {pβ' = pβ'} {pβ' = pβ'} p = Ξ· (pb .universal {P' = incl .Fβ P'} {pβ' = p1'} {pβ' = p2'} (Nat-path Ξ» _ β p)) _ where p1' : _ => _ p1' .Ξ· _ = pβ' p1' .is-natural x y f i o = F-id X (~ i) (pβ' o) p2' : _ => _ p2' .Ξ· _ = pβ' p2' .is-natural x y f i o = F-id Y (~ i) (pβ' o) pb' .pββuniversal = pb .pββuniversal Ξ·β _ pb' .pββuniversal = pb .pββuniversal Ξ·β _ pb' .unique {P'} {lim' = lim'} p1 p2 = pb .unique {lim' = l'} (Nat-path Ξ» _ β p1) (Nat-path Ξ» _ β p2) Ξ·β _ where l' : incl .Fβ P' => P l' .Ξ· _ = lim' l' .is-natural x y f i o = F-id P (~ i) (lim' o)

Similarly, we can construct the adjunction unit and counit by looking at components and constructing identity natural transformations.

sets .Lβ£ΞΉ .unit .Ξ· _ .Ξ· _ f = f sets .Lβ£ΞΉ .unit .Ξ· F .is-natural _ _ _ = F-id F sets .Lβ£ΞΉ .unit .is-natural _ _ _ = Nat-path Ξ» _ β refl sets .Lβ£ΞΉ .counit .Ξ· _ x = x sets .Lβ£ΞΉ .counit .is-natural _ _ _ = refl sets .Lβ£ΞΉ .zig = refl sets .Lβ£ΞΉ .zag = Nat-path Ξ» _ β refl

More canonical examples are given by any presheaf category, where
both the inclusion and sheafification functors are the identity.
Examples of presheaf topoi are abundant in abstract homotopy theory (the
categories of cubical and simplicial sets) β which also play an
important role in modelling homotopy *type* theory; Another
example of a presheaf topos is the category of *quivers*
(directed multigraphs).

Presheaf : β {ΞΊ} (C : Precategory ΞΊ ΞΊ) β Topos ΞΊ (PSh ΞΊ C) Presheaf {ΞΊ} C = psh where open Functor open Topos psh : Topos _ _ psh .site = C psh .ΞΉ = Id psh .has-ff = id-equiv psh .L = Id psh .L-lex .is-lex.pres-β€ c = c psh .L-lex .is-lex.pres-pullback pb = pb psh .Lβ£ΞΉ = adj where open _β£_ adj : Id β£ Id adj .unit = NT (Ξ» _ β idnt) Ξ» x y f β Nat-path Ξ» _ β refl adj .counit = NT (Ξ» _ β idnt) (Ξ» x y f β Nat-path Ξ» _ β refl) adj .zig = Nat-path Ξ» _ β refl adj .zag = Nat-path Ξ» _ β refl

# Properties of topoiπ

The defining property of a topos $\mathcal{T}$ is that it admits a geometric embedding into a presheaf category, meaning the adjunction $L : \mathcal{T} \xrightleftarrows[]{} \mathrm{PSh}(\mathcal{C}) : \iota$ is very special indeed: Since the right adjoint is fully faithful, the adjunction is monadic, meaning that it exhibits $\mathcal{T}$ as the category of algebras for a (lex, idempotent) monad: the βsheafification monadβ. This gives us completeness in $\mathcal{T}$ for βfreeβ (really, itβs because presheaf categories are complete, and those are complete because $\mathbf{Sets}$ is.)

module _ {o ΞΊ} {π£ : Precategory o ΞΊ} (T : Topos ΞΊ π£) where open Topos T Sheafify : Monad (PSh ΞΊ site) Sheafify = AdjunctionβMonad Lβ£ΞΉ Sheafify-monadic : is-monadic Lβ£ΞΉ Sheafify-monadic = is-reflectiveβis-monadic Lβ£ΞΉ has-ff Topos-is-complete : is-complete ΞΊ ΞΊ π£ Topos-is-complete = equivalenceβcomplete (is-equivalence.inverse-equivalence Sheafify-monadic) (Eilenberg-Moore-is-complete (Functor-cat-is-complete (Sets-is-complete {ΞΉ = ΞΊ} {ΞΊ} {ΞΊ})))

Furthermore, since $L$ preserves colimits (it is a left adjoint), then we can compute the colimit of some diagram $F : J \to \mathcal{T}$ as the colimit (in $\mathrm{PSh}(\mathcal{C})$) of $\iota F$ β which exists because $\mathbf{Sets}$ is cocomplete β then apply $L$ to get a colimiting cocone for $L \iota F$. But the counit of the adjunction $\varepsilon : L \iota \Rightarrow \operatorname{Id}_{}$ is a natural isomorphism, so we have a colimiting cocone for $F$.

Topos-is-cocomplete : is-cocomplete ΞΊ ΞΊ π£ Topos-is-cocomplete F = natural-isoβcolimit (Fβ-iso-id-l (is-reflectiveβcounit-iso Lβ£ΞΉ has-ff)) sheafified where psh-colim : Colimit (ΞΉ Fβ F) psh-colim = Functor-cat-is-cocomplete (Sets-is-cocomplete {ΞΉ = ΞΊ} {ΞΊ} {ΞΊ}) _ sheafified : Colimit ((L Fβ ΞΉ) Fβ F) sheafified = subst Colimit Fβ-assoc $ left-adjoint-colimit Lβ£ΞΉ psh-colim

Since the reflector is left exact, and
thus in particular preserves finite products, a theorem of Johnstone
(Elephant A4.3.1) implies the topos
$\mathcal{T}$
is an *exponential ideal* in
$\mathrm{PSh}(\mathcal{C})$:
If
$Y$
is a sheaf, and
$X$
is any presheaf, then the internal hom
$[X,Y]$
is a sheaf: topoi are cartesian
closed.

Since topoi are defined as embedding faithfully into a category of
presheaves, it follows that they have a small **generating
set**, in the same sense that representables generate presheaves:
In fact, the generating set of a Grothendieck topos is exactly the set
of representables of its site!

Elaborating, letting $\mathcal{T}$ be a topos, two maps $f, g : X \to Y \in \mathcal{T}$ are equal if and only if they are equal under $\iota$, i.e.Β as maps of presheaves. But it follows from the coyoneda lemma that maps of presheaves are equal if and only if they are equal on all representables. Consequently, two maps in a $\mathcal{T}$ are equal if and only if they agree on all generalised elements with domain the sheafification of a representable:

module _ {o β} {C : Precategory o β} (ct : Topos β C) where private module C = Cat.Reasoning C module ct = Topos ct module Site = Cat.Reasoning (ct.site) module PSh = Cat.Reasoning (PSh β ct.site) module ΞΉ = Functor (ct.ΞΉ) module L = Functor (ct.L) open _β£_ (ct.Lβ£ΞΉ) open Functor open _=>_

Representables-generate : β {X Y} {f g : C.Hom X Y} β ( β {A} (h : C.Hom (L.β (γβ ct.site A)) X) β f C.β h β‘ g C.β h ) β f β‘ g Representables-generate {f = f} {g} sep = fully-faithfulβfaithful {F = ct.ΞΉ} ct.has-ff $ Representables-generate-presheaf ct.site Ξ» h β ΞΉ.β f PSh.β h β‘β¨ mangle β©β‘ ΞΉ.β β f C.β counit.Ξ΅ _ C.β L.β h β PSh.β unit.Ξ· _ β‘β¨ ap! (sep _) β©β‘ ΞΉ.β (g C.β counit.Ξ΅ _ C.β L.β h) PSh.β unit.Ξ· _ β‘Λβ¨ mangle β©β‘Λ ΞΉ.β g PSh.β h β

where mangle : β {X Y} {f : C.Hom X Y} {Z} {h : PSh.Hom Z _} β ΞΉ.β f PSh.β h β‘ ΞΉ.β (f C.β counit.Ξ΅ _ C.β L.β h) PSh.β unit.Ξ· _ mangle {f = f} {h = h} = ΞΉ.β f PSh.β h β‘β¨ PSh.insertl zag β©β‘ ΞΉ.β (counit.Ξ΅ _) PSh.β β unit.Ξ· _ PSh.β ΞΉ.β f PSh.β h β β‘β¨ ap! (PSh.extendl (unit.is-natural _ _ _)) β©β‘ ΞΉ.β (counit.Ξ΅ _) PSh.β ΞΉ.β (L.β (ΞΉ.β f)) PSh.β β unit.Ξ· _ PSh.β h β β‘β¨ ap! (unit.is-natural _ _ _) β©β‘ ΞΉ.β (counit.Ξ΅ _) PSh.β β ΞΉ.β (L.β (ΞΉ.β f)) PSh.β ΞΉ.β (L.β h) PSh.β unit.Ξ· _ β β‘β¨ ap! (PSh.pulll (sym (ΞΉ.F-β _ _))) β©β‘ ΞΉ.β (counit.Ξ΅ _) PSh.β ΞΉ.β (L.β (ΞΉ.β f) C.β L.β h) PSh.β unit.Ξ· _ β‘β¨ PSh.pulll (sym (ΞΉ.F-β _ _)) β©β‘ ΞΉ.β β counit.Ξ΅ _ C.β L.β (ΞΉ.β f) C.β L.β h β PSh.β unit.Ξ· _ β‘β¨ ap! (C.extendl (counit.is-natural _ _ _)) β©β‘ ΞΉ.β (f C.β counit.Ξ΅ _ C.β L.β h) PSh.β unit.Ξ· _ β

Finally, the property of βbeing a toposβ is invariant under slicing. More specifically, since a given topos can be presented by different sites, a presentation $\mathcal{T} \xrightleftarrows[]{} \mathrm{PSh}(\mathcal{C})$ can be sliced under an object $X \in \mathcal{T}$ to present $\mathcal{T}/X$ as a sheaf topos, with site of definition $\mathrm{PSh}(\int \iota(X))$. This follows from a wealth of pre-existing theorems:

- A pair $L \dashv R$ of adjoint functors can be sliced under an object $X$, giving an adjunction $\Sigma \varepsilon L/R(X) \dashv R/X$; Slicing a functor preserves full-faithfulness and left exactness, hence slicing a geometric embedding gives a geometric embedding.

- The category $\mathrm{PSh}(\mathcal{C})/\iota(X)$ is equivalent to the category $\mathrm{PSh}(\int \iota(X))$, hence βbeing a presheaf topos is stable under slicingβ. Furthermore, this equivalence is part of an ambidextrous adjunction, hence both functors preserve limits.

- Dependent sum
$\Sigma f$
along an isomorphism is an equivalence of categories; But since a topos
is presented by a
*reflective*subcategory inclusion, the counit is an isomorphism.

module _ {o β} {C : Precategory o β} (T : Topos β C) (X : Precategory.Ob C) where private module C = Cat.Reasoning C module Co = Cat.Reasoning (Slice C X) module T = Topos T open Topos open Functor

We build the geometric embedding presenting $\mathcal{T}/X$ as a topos by composing the adjunctions $\varepsilon_!(L/\iota(X)) \dashv \iota/X$ and $F \dashv F^{-1}$ β where $F$ is the equivalence $\mathrm{PSh}(\mathcal{C})/X \to \mathrm{PSh}(\int X)$. The right adjoint is fully faithful because it composes two fully faithful functors (a slice of $\iota$ and an equivalence), the left adjoint preserves finite limits because it is a composite of two equivalences (hence two right adjoints) and a lex functor.

Slice-topos : Topos β (Slice C X) Slice-topos .site = β« T.site (T.ΞΉ.Fβ X) Slice-topos .ΞΉ = sliceβtotal Fβ Sliced (T.ΞΉ) X Slice-topos .has-ff = β-is-equiv (Sliced-ff {F = T.ΞΉ} (T.has-ff)) sliceβtotal-is-ff Slice-topos .L = (Ξ£f (T .Lβ£ΞΉ.counit.Ξ΅ _) Fβ Sliced (T.L) (T.ΞΉ.Fβ X)) Fβ totalβslice Slice-topos .L-lex = Fβ-is-lex (Fβ-is-lex (right-adjointβlex (is-equivalence.Fβ»ΒΉβ£F (Ξ£-iso-equiv (C.isoβinvertible (is-reflectiveβcounit-is-iso T.Lβ£ΞΉ T.has-ff))))) (Sliced-lex T.L-lex)) (right-adjointβlex (sliceβtotal-is-equiv .is-equivalence.Fβ£Fβ»ΒΉ)) Slice-topos .Lβ£ΞΉ = LFβ£GR (is-equivalence.Fβ»ΒΉβ£F sliceβtotal-is-equiv) (Sliced-adjoints T.Lβ£ΞΉ)

# Geometric morphismsπ

The definition of a topos as a generalisation of topological space
leads us to look for a categorification of βcontinuous mapβ to functors
between topoi. In the same way that a continuous function
$f : X \to Y$
may be seen as a homomorphism of frames
$f^* : O(Y) \to O(X)$,
with defining feature the preservation of finite meets and arbitrary
joins, we shall define a **geometric morphism**
$\mathfrak{Topos}(X,Y)$
to be a functor
$f^* : Y \to X$
which is left exact and admits a right adjoint.

Why the right adjoint? Well, right adjoints preserve
limits, but by duality, *left adjoints preserve colimits*.
This embodies the βarbitrary joinsβ part of a map of frames, whereas the
βfinite meetsβ come from left exactness.

private variable o β o' β' ΞΊ ΞΊ' ΞΊ'' s s' : Level E F G : Precategory o β lvl : β {o β o' β'} β Precategory o β β Precategory o' β' β Level lvl {o} {β} {o'} {β'} _ _ = o β β β β' β o'

record Geom[_,_] (E : Precategory o β) (F : Precategory o' β') : Type (lvl E F) where no-eta-equality field Inv[_] : Functor F E Dir[_] : Functor E F Inv-lex : is-lex Inv[_] Invβ£Dir : Inv[_] β£ Dir[_] open Geom[_,_] public

Computation establishes that the identity functor is left exact, and self adjoint, so it is in particular both the direct and inverse image parts of a geometric morphism $\mathcal{T} \to \mathcal{T}$.

Idg : Geom[ E , E ] Idg {E = E} = record { Inv[_] = Id ; Dir[_] = Id ; Inv-lex = lex ; Invβ£Dir = adj }

where module E = Cat.Reasoning E lex : is-lex Id lex .is-lex.pres-β€ f = f lex .is-lex.pres-pullback p = p adj : Id β£ Id adj ._β£_.unit .Ξ· _ = E.id adj ._β£_.unit .is-natural x y f = sym E.id-comm adj ._β£_.counit .Ξ· _ = E.id adj ._β£_.counit .is-natural x y f = sym E.id-comm adj ._β£_.zig = E.idl _ adj ._β£_.zag = E.idl _

Since adjunctions compose, geometric morphisms do, too. Observe that the composite of inverse images and the composite of direct images go in different directions! Fortunately, this matches the convention for composing adjunctions, where the functors βswap sidesβ: $LF \dashv GR$.

_Gβ_ : Geom[ F , G ] β Geom[ E , F ] β Geom[ E , G ] f Gβ g = mk where module f = Geom[_,_] f module g = Geom[_,_] g open is-lex mk : Geom[ _ , _ ] Inv[ mk ] = Inv[ g ] Fβ Inv[ f ] Dir[ mk ] = Dir[ f ] Fβ Dir[ g ] mk .Invβ£Dir = LFβ£GR f.Invβ£Dir g.Invβ£Dir

The composition of two left-exact functors is again left-exact, so thereβs no impediment to composition there, either.

mk .Inv-lex .pres-β€ term ob = g.Inv-lex .pres-β€ (f.Inv-lex .pres-β€ term) _ mk .Inv-lex .pres-pullback pb = g.Inv-lex .pres-pullback (f.Inv-lex .pres-pullback pb)

An important class of geometric morphism is the **geometric
embedding**, which weβve already met as the very definition of
`Topos`

. These are the geometric
morphisms with fully faithful direct image. These are *again*
closed under composition, so if we want to exhibit that a certain
category
$\mathcal{C}$
is a topos, it suffices to give a geometric embedding
$\mathcal{C} \to \mathcal{T}$,
where
$\mathcal{T}$
is some topos which is convenient for this application.

record Geom[_βͺ_] (E : Precategory o β) (F : Precategory o' β') : Type (lvl E F) where field morphism : Geom[ E , F ] has-ff : is-fully-faithful Dir[ morphism ] Geometric-embeddings-compose : Geom[ F βͺ G ] β Geom[ E βͺ F ] β Geom[ E βͺ G ] Geometric-embeddings-compose f g = record { morphism = f .morphism Gβ g .morphism ; has-ff = β-is-equiv (g .has-ff) (f .has-ff) } where open Geom[_βͺ_] Toposβgeometric-embedding : (T : Topos ΞΊ E) β Geom[ E βͺ PSh ΞΊ (T .Topos.site) ] Toposβgeometric-embedding T = emb where emb : Geom[ _ βͺ _ ] Inv[ emb .Geom[_βͺ_].morphism ] = T .Topos.L Dir[ emb .Geom[_βͺ_].morphism ] = T .Topos.ΞΉ emb .Geom[_βͺ_].morphism .Inv-lex = T .Topos.L-lex emb .Geom[_βͺ_].morphism .Invβ£Dir = T .Topos.Lβ£ΞΉ emb .Geom[_βͺ_].has-ff = T .Topos.has-ff

By the adjoint functor theorem, any map between posets which preserves arbitrary joins has a right adjoint; Conversely, every map which has a right adjoint preserves arbitrary joins.β©οΈ