topos theory

Contents

Definition

Let $C$ be a coherent category. Write $\tau C$ for the category whose objects are pairs $\left(X,F\right)$ where $X$ is an object of $C$ and $F$ is a prime filter on ${\mathrm{Sub}}_{C}\left(X\right)$. This is the full subcategory of the category of filters? of $C$ spanned by the prime filters. Jet ${J}_{p}$ be the Grothendieck topology on $\tau C$ induced from the coherent topology on the category of filters.

As defined by Makkai, the topos of types $T\left(C\right)$ of $C$ is the sheaf topos

$T\left(C\right):={\mathrm{Sh}}_{{J}_{p}}\left(\tau C\right)\phantom{\rule{thinmathspace}{0ex}}.$\mathbf{T}(C) := Sh_{J_p}(\tau C) \,.

Note: The word “types” here has nothing to do with type theory. Instead, refers to the notion of type in model theory.

Properties

In terms of the coherent hyperdoctrine

Let $C$ be a coherent category. The canonical extension ${𝒮}_{C}^{\delta }$ of its coherent hyperdoctrine ${𝒮}_{C}$ is naturally an internal locale in the presheaf topos $\left[{C}^{\mathrm{op}},\mathrm{Set}\right]$ (as well as in the sheaf topos ${\mathrm{Sh}}_{\mathrm{coh}}\left(C\right)$ for the coherent topology on $C$).

The topos of types is equivalent to the topos of internal sheaves over this internal locale.

$T\left(C\right)\simeq \mathrm{Sh}\left({𝒮}_{C}^{\delta }\right)\phantom{\rule{thinmathspace}{0ex}}.$\mathbf{T}(C) \simeq Sh(\mathcal{S}_C^\delta) \,.

This is due to (Coumans, theorem 25).

In particular this implies that there is a localic geometric morphism

$T\left(C\right)\to {\mathrm{Sh}}_{\mathrm{coh}}\left(C\right)\phantom{\rule{thinmathspace}{0ex}}.$\mathbf{T}(C) \to Sh_{coh}(C) \,.

Let $\mathrm{Mod}\left(C\right)\simeq {\mathrm{Func}}_{\mathrm{coh}}\left(C,\mathrm{Set}\right)$ be the category of models of the coherent theory given by $C$ in Set.

There is a full subcategory $𝒦↪\mathrm{Mod}\left(C\right)$ such that the Yoneda extension of the evaluation map $\mathrm{ev}:C\to \mathrm{Func}\left(𝒦,\mathrm{Set}\right)$ is the inverse image of a geometric morphism

${\varphi }_{\mathrm{ev}}:{\mathrm{Set}}^{𝒦}\to {\mathrm{Sh}}_{\mathrm{coh}}\left(C\right)\phantom{\rule{thinmathspace}{0ex}}.$\phi_{ev} : Set^{\mathcal{K}} \to Sh_{coh}(C) \,.

The hyperconnected / localic factorization of this morphism is through the topos of types of $C$:

${\varphi }_{\mathrm{ev}}:{\mathrm{Set}}^{𝒦}\stackrel{\mathrm{hyperconn}.}{\to }T\left(C\right)\stackrel{\mathrm{localic}}{\to }{\mathrm{Sh}}_{\mathrm{coh}}\left(C\right)\phantom{\rule{thinmathspace}{0ex}}.$\phi_{ev} : Set^{\mathcal{K}} \stackrel{hyperconn.}{\to} \mathbf{T}(C) \stackrel{localic}{\to} Sh_{coh}(C) \,.

This is (Coumans, theorem 39).

References

The notion was introduced in

• Michael Makkai, The topos of types, Logic Year 1979-80 (Proc. Seminars and Conf. Math. Logic, Univ. Connecticut, Storrs, Conn., 1979/80), Lecture Notes in Math. 859, Springer, Berlin (1981) pp. 157-201, doi.

The relation to canonical extension is made explicit in

• Dion Coumans, Generalizing canonical extensions to the categorical setting, pdf, to appear in Annals of Pure and Applied Logic

Revised on July 24, 2012 04:01:55 by Zoran Škoda (190.26.78.124)