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’.