nLab logical functor

Contents

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Contents

Idea

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

If instead a topos is regarded as a context for geometry or specifically geometric logic, then the notion of homomorphism preserving this is that of a geometric morphism.

Definition

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.

Definition

Let \mathcal{E} be an elementary topos. Write Ω\Omega \in \mathcal{E} for the subobject classifier. For each object AA \in \mathcal{E} write

PAΩ A P A \coloneqq \Omega^A

for the exponential object. Write

APA×A \in_A \hookrightarrow P A \times A

for the subobject classified by the evaluation map ev:PA×AΩev : P A \times A \to \Omega.

This exhibits PAP A as a power object for AA.

Definition

A functor F:F : \mathcal{E} \to \mathcal{F} between elementary toposes is called a logical morphism if

  1. FF preserves finite limits;

  2. for every object AA \in \mathcal{E}

The notion of logical functors between toposes is in contrast to geometric morphisms between toposes: the former preserve the structure of an elementary topos, the latter those of a sheaf topos.

But both can be combined:

Definition

A geometric morphism whose inverse image is a logical functor is called an atomic geometric morphism.

Remark

The other case, that the direct image of a geometric morphism is a logical functor is not of interest. See cor. below.

Properties

General

Proposition

A logical functor has a left adjoint precisely if it has a right adjoint.

This appears as (Johnstone, cor. A2.2.10).

Proof

For F:F : \mathcal{E} \to \mathcal{F} a logical functor, we have by definition a diagram

op F op op P P F \array{ \mathcal{E}^{op} &\stackrel{F^{op}}{\to}& \mathcal{F}^{op} \\ {}^{\mathllap{P}}\downarrow &\swArrow_{\simeq}& \downarrow^{\mathrlap{P}} \\ \mathcal{E} &\stackrel{F}{\to}& \mathcal{F} }

in Cat. This satisfies the assumptions of the adjoint lifting theorem and hence FF has a right adjoint precisely if F opF^{op} does. But a right adjoint of F opF^{op} is a left adjoint of FF, and vice versa.

Proposition

If a logical functor F:F : \mathcal{E} \to \mathcal{F} has a left adjoint LL, then LL preserves monomorphisms, and indeed induces a bijection between subobjects of AA\in \mathcal{F} and subobjects of LAL A\in \mathcal{E}.

Proof

Since F(Ω )=Ω F(\Omega_{\mathcal{E}}) = \Omega_{\mathcal{F}}, we have a bijection

Sub (A)(A,Ω )(LA,Ω )Sub (LA). Sub_{\mathcal{F}}(A) \cong \mathcal{F}(A,\Omega_{\mathcal{F}}) \cong \mathcal{E}(L A,\Omega_{\mathcal{E}}) \cong Sub_{\mathcal{E}}(L A).

It remains to check that this bijection is implemented by the action of LL, which can be done with partial map classifiers; see (Johnstone, Lemma A2.4.8).

Proposition

For a logical functor F:F : \mathcal{E} \to \mathcal{F} having a left adjoint LL, the following are equivalent:

  1. The induced functor L:/L1L':\mathcal{F} \to \mathcal{E}/L 1 is an equivalence of categories, i.e. the adjunction LFL\dashv F can be identified with the pullback adjunction /B\mathcal{E}/B \rightleftarrows \mathcal{E} for some BB (namely L1L1).
  2. LL is conservative.
  3. LL is faithful.
  4. LL preserves equalizers.
  5. LL preserves pullbacks.

This appears as (Johnstone, Prop. A2.3.8).

Proof

The left adjoint of pullback has all the other properties. Any pullback-preserving functor preserves equalizers. An equalizer-preserving functor is faithful as soon as it reflects invertibility of monomorphisms, which follows from Proposition above. A faithful functor reflects monos and epis, hence is conservative once its domain is balanced.

Finally, if LL is conservative then so is LL', and its right adjoint FF' (given by FF followed by pullback along η:1FL1\eta : 1 \to F L 1) is also logical, hence cartesian closed. Thus, LFL'\dashv F' is a Hopf adjunction for the cartesian monoidal structures, and LL' preserves the terminal object. Now the counit of LFL'\dashv F' can be factored as

LFAL(1×FA)L1×A1×AA L' F' A \cong L'(1\times F' A) \xrightarrow{\cong} L' 1 \times A \cong 1\times A\cong A

so it is an isomorphism. By the triangle identity, L(η)L'(\eta) is an isomorphism, but LL' is conservative, hence the unit η\eta is also an isomorphism, and LFL'\dashv F' is an equivalence.

This appears as (Johnstone, cor. A2.2.10).

Corollary

If a logical functor is right adjoint to a left exact functor, then it is an equivalence of categories.

This appears as (Johnstone, scholium 2.3.9).

Preserved structures

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.

Relation to geometric morphisms

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.

Proposition

A logical functor is the direct image of a geometric morphism precisely if it is an equivalence.

Proof

Since by definition the direct image of a geometric morphism has a left adjoint that preserves finite limits.

But logical inverse images are of interest. Recall from def. above that a geometric morphism with logical inverse image is called an atomic geometric morphism.

Proof

By prop. .

The following is the main source of examples of atomic geometric morphisms.

Proposition

The inverse image of any base change geometric morphism, hence in particular of any etale geometric morphism, is a logical morphism.

Proof

The inverse image is given by pullback along the given morphism.

Remark

When considering the internal logic of a given topos \mathcal{E} relations, predicates/propositions about variables of type AobA \in ob \mathcal{E} are subobjects of AA. 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.

Examples

References

Section A2.1 in

Section IV.2, page 170 of

Last revised on November 16, 2022 at 06:16:51. See the history of this page for a list of all contributions to it.