Can we define geometric morphisms (between ETCS categories) elementarily?

2010-10-20T00:05:25Z

The ETCS axioms give conditions on a category for it to be a category of sets. These axioms can be written out in first order language, resulting in a finite axiomatisation of the category of sets. Given a model of ZFC one can form the associated category of sets and this will satisfy the axioms. On the other hand, the axioms do not require a priori defined sets. (The existence of a model of the ETCS axioms then is probably on par with the assuption there exists a model of the ZFC axioms) The appropriate definition of map between ETCS categories is a geometric morphism.

Is it possible to define geometric morphisms elementarily? In first order language?

Then one can define the category of ETCS categories and consider the relations between models. This is related to my previous question.

Answer by Peter LeFanu Lumsdaine for Can we define geometric morphisms (between ETCS categories) elementarily?

2010-10-20T01:37:48Z

Yes, it is possible. Precisely, we can write down a first-order theory for which a model is a pair of ETCS-models and a geometric morphism between them (am I right in thinking this is what you're asking for?).

To do this, on top of axiomatising “a pair of models of ETCS”, you add some extra function symbols for the adjunction. The conditions of functoriality, etc. are easily written algebraically; the adjunction can be expressed in various ways, of which the simplest to write down is probably the triangle-inequalities form. “Preserving finite limits”, when you write it out, is also just a scheme of first-order conditions; if you want to reduce it to a finite axiomatisation, note that it's enough to ask for preservation of finite products and equalisers (by the usual proof that all finite limits can be constructed from these).

This said, I disagree somewhat with an implicit premise of your question. You say: “Then one can define the category of ETCS categories…” But to do this, you don't need to show that geometric morphisms can be defined in first-order terms. To talk about “the category of ETCS categories”, you already need to be working in a meta-theory with some sort of notion of set or similar (eg types, etc.); and so don't need the definitions of the morphisms to be first-order.

The foundational advantage of a first-order axiomatisation of widgets is that you can then study a single widget without needing any meta-theory. But to study the collection of all widgets (as a category or whatever else), you still need a meta-theory.

Can we define geometric morphisms (between ETCS categories) elementarily? - MathOverflow

Can we define geometric morphisms (between ETCS categories) elementarily?

Answer by Peter LeFanu Lumsdaine for Can we define geometric morphisms (between ETCS categories) elementarily?