Could not include topos theory - contents
A logical morphism or logical functor is a homomorphism between elementary toposes that preserves the structure of a topos as a context for logic: a functor which preserves all the elementary topos structure, including in particular power objects, but not necessarily any infinitary structure (such as present additionally in a sheaf topos).
Since all the elementary topos structure follows from having finite limits and power objects, it suffices to define a logical functor to preserve these, up to isomorphism. It then follows that it is also a locally cartesian closed functor, a Heyting functor, etc.
for the exponential object. Write
This exhibits as a power object for .
But both can be combined:
This appears as (Johnstone, cor. 2.2.10).
For a logical functor, we have by definition a diagram
In particular, a logical functor preserves the truth of all sentences in the internal logic. If it is moreover conservative, then it also reflects the truth of such sentences. For example, the transfer principle? of nonstandard analysis can be stated as the fact that a certain functor is logical and conservative.
The difference between geometric and logical functors between toposes is, in a certain sense, a categorification of the difference between a homomorphism of frames and a homomorphism of Heyting algebras. When the latter are complete, these are the same objects with the same isomorphisms but different morphisms.
However, while frame homomorphisms naturally categorified by geometric functors, a more precise categorification of Heyting algebra homomorphisms would be Heyting functors, which preserve the internal first-order logic, but not the higher-order logic as logical functors do.
This appears as (Johnstone, scholium 2.3.9).
By prop. 1.
The following is the main source of examples of atomic geometric morphisms.
The inverse image is given by pullback along the given morphism.
When considering the internal logic of a given topos relations, predicates/propositions about variables of type are subobjects of . Application of function symbols to such expressions corresponds to pullback along the morphism representing the function symbol. The above says that this is, indeed, a logical operation .
More generally, for any small category the inclusion
into the presheaf topos is logical.
Section A2.1 in
Section IV.2, page 170 of