nLab conceptual completeness

Redirected from "strong conceptual completeness".
Contents

Contents

Idea

In any context it is interesting to ask when a contravariant hom-functor Hom(,X)\operatorname{Hom}(-,X) reflects isomorphisms, i.e. if homming into an object is enough to distinguish isomorphism classes. In a 22-categorical setting, the analogous question is if homming into an object reflects equivalences.

Definition

Conceptual completeness refers to the result of Makkai and Reyes that in the 22-category Pretop\mathbf{Pretop} of pretoposes, the hom-2-functor Hom Pretop(,Set):Pretop opCAT\operatorname{Hom}_{\mathbf{Pretop}}(-,\mathbf{Set}) : \mathbf{Pretop}^{op} \to \mathbf{CAT} reflects equivalences. More explicitly:

Theorem

[Conceptual completeness] Let F:P 1P 2F : P_1 \to P_2 be a pretopos morphism. If the functor

F:Hom Pretop(P 2,Set)Hom Pretop(P 1,Set) - \circ F : \operatorname{Hom}_{\mathbf{Pretop}}(P_2, \mathbf{Set}) \to \operatorname{Hom}_{\mathbf{Pretop}}(P_1,\mathbf{Set})

is an equivalence of categories, then so is FF.

From a logical point of view, recall that pretoposes can be conceived as syntactic categories of coherent theories (up to elimination of imaginaries), so that a pretopos morphism P 1P 2P_1 \to P_2 corresponds to an interpretation of the theory P 1P_1 into the theory P 2P_2, or equivalently to a model of the theory P 1P_1 inside the category P 2P_2; in particular, a pretopos morphism into SetSet is therefore a model of the source theory. In these terms, conceptual completeness states that if an interpretation T 1T 2T_1 \to T_2 between two coherent theories induces an equivalence between the categories of models Mod(T 2)Mod(T 1)\operatorname{Mod}(T_2) \to \operatorname{Mod}(T_1), then T 1T_1 and T 2T_2 are bi-interpretable up to elimination of imaginaries, i.e. T 1 eqT_1^{eq} and T 2 eqT_2^{eq} are bi-interpretable.

Makkai duality states that Hom Pretop(,X)\operatorname{Hom}_{\mathbf{Pretop}}(-,X) factors through the 22-category of ultracategories (categories equipped with ultraproduct functors?) (which also contains Set\mathbf{Set}) and that Hom Pretop(,Set)\operatorname{Hom}_{\mathbf{Pretop}}(-,\mathbf{Set}) is left-adjoint to Hom Ult(,Set)\mathbf{Hom}_{\mathbf{Ult}}(-,\mathbf{Set}).

Furthermore, the unit of this adjunction is an equivalence, so that a pretopos TT is equivalent to the category of ultrafunctors (ultraproduct-preserving functors) from Mod(T)\mathbf{Mod}(T) to Set\mathbf{Set}, i.e. any ultrafunctor Mod(T)Set\mathbf{Mod}(T) \to \mathbf{Set} is induced by taking points in models of some definable set XTX \in T.

This means: when viewed as a functor to the 22-category of ultracategories instead, Hom Pretop(,Set)\operatorname{Hom}_{\mathbf{Pretop}}(-,\mathbf{Set}) creates equivalences also, so that the pretopos/theory TT can be reconstructed up to bi-interpretability from its ultracategory of models. This is what is known as strong conceptual completeness.

Remarks

In his AMS monograph on duality and definability in first-order logic, Makkai refined the above reconstruction result to work with just the (ultra) core of the ultracategory of models of TT. Awodey and his students replace the ultracategory structure on this groupoid with a related topology instead; this is the “spectral groupoid” which forms the basis of the logical scheme approach.

Examples

(Maybe I’ll add some explicit computations later.)

References

An approach which reframes conceptual completeness in terms of logical schemes is adopted in section 4.4 of

For the (,1)(\infty, 1)-analog of conceptual completeness, see section A.9 of

Last revised on July 17, 2025 at 09:05:37. See the history of this page for a list of all contributions to it.