6.9. Makkai completeness
The preceding section recovers a coherent topos from its pretopos of coherent objects. Makkai completeness addresses the converse logical question: can this finitary syntax be recovered from its models? For a coherent topos \(T\), the models are its points, and the additional structure needed for reconstruction is given by ultraproducts.
Can we recover \(T\) from its category of points?
The category \(\Pt(T)\) alone does not contain enough information. For example, if \(T\) classifies local rings, then \(\Pt(T)\) is the category of local rings, but the purely categorical structure does not remember which constructions are first-order. Ultraproducts record this extra structure. The resulting completeness statement says that the theory, equivalently its coherent topos or pretopos, can be recovered from its category of models equipped with these operations.
An ultracategory is a category equipped with coherent ultraproduct operations: for every ultrafilter \(\Uu\) on a set \(I\), there is a functor
More precisely, let \(\mathrm{Stone}^{\mathrm{free}}\) denote the category of Stone–Čech compactifications of sets. The category \(\Cat^{\ultra}\) of ultracategories is the subcategory of \(\mathrm{LaxFun}((\mathrm{Stone}^{\mathrm{free}})\catop,\Cat)\) spanned by the lax functors \(F\) satisfying:
We have \(F(\beta I) \simeq \prod_I F(*)\).
Given \(f\colon \beta I \to \beta J\) and \(g\colon \beta J \to \beta K\), if \(f\) is induced by a map \(I \to J\), then \(f^* \circ g^* \simeq (g \circ f)^*\).
Theorem 6.136. (Makkai completeness)
The \(2\)-functor
is fully faithful.
The higher-categorical formulation in Theorem 6.136 is the version stated in the lectures. The available reference [Lurie 2018, Theorem 2.3.1 and Corollary 2.3.3] proves strong conceptual completeness and Makkai duality for small classical pretopoi, classical coherent topoi, and ordinary categories of set-valued models. In particular, that reference proves the restriction of the theorem to classical topoi and classical categories, but it does not by itself supply a proof of the displayed higher-categorical extension. We do not know a counterexample to the extension.
There is a pullback square
For \(\An\), every lax functor occurring here is automatically strict.
References
- Jacob Lurie. Ultracategories. 2018.