Exact cofiltered limits and related notions

[ScriptRaccoon]

This PR adds five new properties:

1. exact cofiltered limits

This is the dual of "exact filtered colimits", hence it makes sense to add this. (Also to properly decide if Set^op has exact filtered colimits, which was open.) I already added similar dualized properties before, notably "cocartesian cofiltered limits" (#84).

To decide this new property and to not repeat myself in the proofs, it is useful to check a weaker property:

2. epimorphisms are stable under cofiltered limits

So this has been added as well. Accordingly, I also added the dual:

3. monomorphisms are stable under filtered colimits

This is related to Grothendieck's axiom AB4, but also - in the finite case - very similar to the counital property. It also clarifies why for example Met does not have exact filtered colimits: it is because monomorphisms are not stable.

Of course, in many categories in practice (not their duals!) epis are not stable. For example, in the category of abelian groups, the epimorphisms $A^{\oplus \mathbb{N}} \to A^n$ for $n \geq 0$ yield the homomorphism $A^{\oplus \mathbb{N}} \to A^{\mathbb{N}}$ in the limit, which is clearly no epimorphism. To generalize this argument and not repeat myself in various additive categories, I have added yet another property:

4. coproducts inject into products (CIP)

This means that the category has zero morphisms, all products, all coproducts, and the natural morphism $\coprod_i X_i \to \prod_i X_i$ is a monomorphism. I have called this CIP, probably there is no official name.

And then we also have its dual:

5. coproducts surject onto products (CSP)

This has blown the PR a bit, but I think it is necessary to understand where the failure of exact cofiltered limits really comes from. In fact, not a single (!) manual property assignment has been made for "exact cofiltered limits", everything is deduced.

As usual, I have tried to decide the new properties for all categories. Here we also run into some interesting mathematics. For example, for Ban the failure of CSP is because the canonical map $\ell^1 \to \ell^\infty$ has no dense image.

The following unknowns remain:

• CIP: –
• CSP: Sh(X,Ab)
• filtered-colimit-stable monos: unknown forLRS, Sch
• cofiltered-limit-stable epis: Sh(X,Ab), LRS
• exact cofiltered limits: Sh(X,Ab), LRS

Surely, the category Sh(X,Ab) does not satisfy CSP for most spaces X. In these cases, we can deduce that epis are not stable under cofiltered limits, and then also that cofiltered limits are not exact. As with the other currently unknown properties of this category, it needs to be made precise which conditions on the space X are required exactly.

Thoughts: Maybe it is more natural to consider the property of having stable regular epimorphisms.

[ykawase5048]

It would be nice to add "locally finitely multi-presentable → filtered-colimit-stable mono".

Here is a proof: Every locally finitely multi-presentable category is a multi-reflective full subcategory of a presheaf category closed under filtered colimits (Adamek--Rosicky, 4.30). Since multi-reflective full subcategories are in general closed under connected limits (Adamek--Rosicky, Thm. 4.26), in particular, we can calculate not only filtered colimits but also kernel pairs as well as in a presheaf category.