Inverse image functor of a geometric morphism
ID: inverse-image-functor-of-a-geometric-morphism
The inverse image is a finite-limit-preserving left adjoint with right adjoint . It preserves arbitrary colimits, and hence images as well as finite limits. These properties preserve the interpretation of geometric formulas. It need not preserve Heyting implication or every universal quantifier.
New to topics? Read the docs here!