On stability of exactness properties under the pro-completion (Q2217538)

This paper is concerned with the question which properties of the given category carry over to its pro-completion. If \(C\)\ is a small finitely complete category, its pro-completion is no other than its free cofiltered limit completion, which is given by the restricted Yoneda embedding \[ C\hookrightarrow\mathbf{Lex}(C,\mathbf{Set})^{\mathrm{op}} \] where \(\mathbf{Lex}(C,\mathbf{Set})\) is the category of finite limit preserving functors from \(C\)\ to \(\mathbf{Set}\). Many so-called \textit{exactness properties} have been shown to be stable under this construction, say, being regular [\textit{M. Barr}, J. Pure Appl. Algebra 41, 113--137 (1986; Zbl 0606.18004)], coregular [\textit{B. Day} and \textit{R. Street}, J. Pure Appl. Algebra 58, No. 3, 227--233 (1989; Zbl 0677.18009)], additive [\textit{B. Day} and \textit{R. Street}, J. Pure Appl. Algebra 63, No. 3, 225--229 (1990; Zbl 0705.18006)], abelian [loc. cit.], exact Mal'tsev with pushouts [\textit{F. Borceux} and \textit{M. C. Pedicchio}, J. Pure Appl. Algebra 135, No. 1, 9--22 (1999; Zbl 0926.18003)], coregular co-Mal'tsev [\textit{M. Gran} and \textit{M. C. Pedicchio}, Theory Appl. Categ. 8, 1--15 (2001; Zbl 0970.18008)], coextensive with pushouts [\textit{A. Carboni} et al., J. Pure Appl. Algebra 161, No. 1--2, 65--90 (2001; Zbl 0982.18006)] and extensive [loc. cit.]. The principal objective in this paper consisting of six sections is to establish a general stability theorem (Theorem 2.2) subsuming not only the said ones but also properties of being semi-abelian, regular, Mal'tsev, coherent with finite products and so on. In some sense, the authors' approach to establishing the general stability theorem is analogous to the approach exploited in the particular said cases, though the generality brings in heavy technicalities, which are tackled in use of \(2\)-categorical calculus of natural transformations. Indeed, the proof of Theorem 2.2 is relegated to \S 4 after preliminaries for the proof of the stability theorem in \S 3, being divided into 29 steps. As is expected, the authors make use of a generalization of the set-based case of a lemma from [\textit{B. Day} and \textit{R. Street}, J. Pure Appl. Algebra 58, No. 3, 227--233 (1989; Zbl 0677.18009)] called the \textit{uniformity lemma}, whose proof occupies a substantial part in the proof of the general stability theorem, relying on classical results regarding pro-completion [\textit{P. Gabriel} and \textit{F. Ulmer}, Lokal präsentierbare Kategorien. (Locally presentable categories). Berlin-Heidelberg-New York: Springer-Verlag (1971; Zbl 0225.18004); \textit{M. Artin} et al., Séminaire de géométrie algébrique du Bois-Marie 1963--1964. Théorie des topos et cohomologie étale des schémas. (SGA 4). Un séminaire dirigé par M. Artin, A. Grothendieck, J. L. Verdier. Avec la collaboration de N. Bourbaki, P. Deligne, B. Saint-Donat. Tome 1: Théorie des topos. Exposés I à IV. 2e éd. Berlin-Heidelberg-New York: Springer-Verlag (1972; Zbl 0234.00007)]. The authors' approach to formalizing the definition of an exactness property is based on the theory of \textit{sketches} due to \textit{C. Ehresmann} [Bul. Inst. Politeh. Iaşi, N. Ser. 14(18), No. 1--2, 1--14 (1968; Zbl 0196.03102)]. The present approach to exactness properties is not intended to cover all properties of a category of interest, being to be thought of as formalization of the so-called \textit{first-order} exactness properties so that such a higher-order exactness property as existence of enough projectives is out of consideration. It should be noted that the authors' stability theorem claims that not all but only certain first-order exactness properties are stable under the pro-completion, a notably exception being the exactness property of a morphism to be the truth morphism for a subobject classifier. The stability theorem claims under certain conditions that, given a functorial verification of \(\alpha\vdash\beta\) for an \(\mathcal{X}\)-structure \(F\) in \(C\), there exists a functorial verification of \(\alpha\vdash\beta\)\ for the image \(\mathbf{y}F\) of \(F\) under the (restricted) Yoneda embedding \[ \mathbf{y}:C\hookrightarrow\mathbf{Lex}(C,\mathbf{Set})^{\mathrm{op}} \] Furthermore, the functorial verification of \(\alpha\vdash\beta\)\ for \(\mathbf{y}F\) can be chosen so that it is \textit{coherent} with the functorial verification of \(\alpha\vdash\beta\) for \(F\), as addressed in \S 5. \S 6 is concerned with concluding remarks.