In Borceux and Bourn's book "Mal'cev, Protomodular, Homological and Semi-Abelian Categories", the authors introduce two similar metatheorems that are used throughout the book to greatly simplify many proofs. Contrary to the well-known metatheorems resulting from embedding theorems such as Freyd-Mitchell's or Barr's, which pose strict conditions to the categories they can be applied to, but then allow to transfer large amounts of statements to easier categories, these metatheorems pose strict conditions to the structure of the statements, but can be applied to very general types of categories (arbitrary categories for the first metatheorem, and pointed categories for the second).
For those who don't have immediate access to the book, here are both theorems:
Let $\mathcal{P}$ be a statement of the form $\varphi \Rightarrow \psi$, where $\varphi$ and $\psi$ can be expressed as conjunctions of properties in the following list:
- (just for pointed categories) some arrow is a zero arrow;
- some finite diagram is commutative;
- some morphism is a monomorphism;
- some morphism is an isomorphism;
- some finite diagram is a limit diagram
- some arrow $f: A \to B$ factors (of course, uniquely) through some specified monomorphism $s: S \hookrightarrow B$.
If this statement $\mathcal{P}$ is valid in the category of (pointed) sets, it is valid in every (pointed) category.
The proof proceeds via the Yoneda embedding, and then asserts that each of the above statements is valid in a presheaf category iff it is valid pointwise (i.e. in $\mathbf{Set}$ or $\mathbf{Set}_*$ respectively).
My problem is though, that in the proof the demanded structure of the statement $\mathcal{P}$ (implication of conjunctions) is ignored. It is only mentioned that the Yoneda embedding "preserves and reflects all ingredients which appear in $\mathcal{P}$" (i.e. the items on the list), and that "... all the properties listed in our statement are valid in $[\mathcal{E}^\text{op}, \mathbf{Set}]$ precisely when they are valid pointwise in $\mathbf{Set}$."
Even more irritatingly, the authors note afterwards, that "the list of properties in our metatheorem is not exhaustive. A better way to express the metatheorem would have been to state it for Horn sentences and the "unique existential quantifier $\exists!$", but we do not want to enter those considerations here.".
More generally, I wonder why I can't find this metatheorem anywhere else, since it is so useful. Is there an alternative formulation, e.g. via the internal logic of categories, which I do not recognize as equivalent yet?
Thus my questions are the following:
- How does a complete proof of the metatheorem proceed?
- How does the "better way" noted above work? Is there another source that elaborates this?
- Is there a more systematic way to formulate the theorems?