Triposes as a generalization of localic geometric morphisms

In Hyland et al. (1980), Hyland, Johnstone and Pitts introduced the notion of tripos for the purpose of organizing the construction of realizability toposes in a way that generalizes the construction of localic toposes from complete Heyting algebras. In Pitts (2002), one finds a generalization of this notion eliminating an unnecessary assumption of Hyland et al. (1980). The aim of this paper is to characterize triposes over a base topos ${\cal S}$ in terms of so-called constant objects functors from ${\cal S}$ to some elementary topos. Our characterization is slightly different from the one in Pitts’s PhD Thesis (Pitts, 1981) and motivated by the fibered view of geometric morphisms as described in Streicher (2020). In particular, we discuss the question whether triposes over Set giving rise to equivalent toposes are already equivalent as triposes.

Local External/Internal Symmetry of Smooth Manifolds and Lack of Tovariance in Physics

Category theory allows one to treat logic and set theory as internal to certain categories. What is internal to SET is 2-valued logic with classical Zermelo–Fraenkel set theory, while for general toposes it is typically intuitionistic logic and set theory. We extend symmetries of smooth manifolds with atlases defined in Set towards atlases with some of their local maps in a topos T . In the case of the Basel topos and R 4 , the local invariance with respect to the corresponding atlases implies exotic smoothness on R 4 . The smoothness structures do not refer directly to Casson handless or handle decompositions, which may be potentially useful for describing the so far merely putative exotic R 4 underlying an exotic S 4 (should it exist). The tovariance principle claims that (physical) theories should be invariant with respect to the choice of topos with natural numbers object and geometric morphisms changing the toposes. We show that the local T -invariance breaks tovariance even in the weaker sense.

Flat functors and classifying toposes

This chapter develops a general theory of extensions of flat functors along geometric morphisms of toposes; the attention is focused in particular on geometric morphisms between presheaf toposes induced by embeddings of categories and on geometric morphisms to the classifying topos of a geometric theory induced by a small category of set-based models of the latter. A number of general results of independent interest are established on the way, including developments on colimits of internal diagrams in toposes and a way of representing flat functors by using a suitable internalized version of the Yoneda lemma. These general results will be instrumental for establishing in Chapter 6 the main theorem characterizing the class of geometric theories classified by a presheaf topos and for applying it.

Expansions and faithful interpretations

This chapter introduces the concept of expansion of a geometric theory and develops some basic theory about it; it proves in particular that expansions of geometric theories induce geometric morphisms between the respective classifying toposes and that conversely every geometric morphism to the classifying topos of a geometric theory can be seen as arising from an expansion of that theory. The notion of hyperconnected-localic factorization of a geometric morphism is then investigated and shown to admit a natural description in the context of geometric theories. Further, the preservation, by ‘faithful interpretations’ of theories, of each of the conditions in the characterization theorem for theories of presheaf type established in Chapter 6 is discussed, leading to results of the form ‘under appropriate conditions, a geometric theory in which a theory of presheaf type faithfully interprets is again of presheaf type’.

Principal bundles as Frobenius adjunctions with application to geometric morphisms

Using a suitable notion of principalG-bundle, defined relative to an arbitrary cartesian category, it is shown that principal bundles can be characterised as adjunctions that stably satisfy Frobenius reciprocity. The result extends from internal groups to internal groupoids. Since geometric morphisms can be described as certain adjunctions that are stably Frobenius, as an application it is proved that all geometric morphisms, from a localic topos to a bounded topos, can be characterised as principal bundles.

Regular functors and relative realisability categories

The relative realisability toposes introduced by Awodey, Birkedal and Scott in Awodey et al. (2002) satisfy a universal property involving regular functors to other categories. We use this universal property to define what relative realisability categories are when they are based on categories other than the topos of sets. This paper explains the property and gives a construction for relative realisability categories that works for arbitrary base Heyting categories. The universal property also provides some new geometric morphisms to relative realisability toposes.

Pointed Torsors

This paper gives a characterization of homotopy fibres of inverse image maps on groupoids of torsors that are induced by geometric morphisms, in terms of both pointed torsors and pointed cocycles, suitably defined. Cocycle techniques are used to give a complete description of such fibres, when the underlying geometric morphism is the canonical stalk on the classifying topos of a profinite group G. If the torsors in question are defined with respect to a constant group H, then the path components of the fibre can be identified with the set of continuous maps from the profinite group G to the group H. More generally, when H is not constant, this set of path components is the set of continuous maps from a pro-object in sheaves of groupoids to H, which pro-object can be viewed as a “Grothendieck fundamental groupoid”.