On the definition of "exact filtered colimits"

[ykawase5048]

The implication finitely accessible" ==> "filtered-colimit-stable monos is discussed in #297 (comment).
I think this would be a corollary of the following more general fact: in any κ-accessible category $A$, κ-filtered colimits commute with existing κ-limits.
This follows from the properties below satisfied by the canonical embedding $A\to Set^{A_{κ}^{op}}$ to the presheaf category over the full subcategory of κ-presentables:

• It is closed under κ-filtered colimits.
• It preserves any existing limits in $A$.
• It reflects limits.

This suggests us to remove the assumption on the existence of finite limits (perhaps also filtered colimits?) from the definition of exact filtered colimits.

I also think it would be best to cite a source that explicitly states this basic fact, but I haven't been able to find one for now.

[ScriptRaccoon]

The problems of removing finite limits or filtered colimits from "exact filtered colimits":

1. Which property do we remove? And why? (If one, why not the other?)
2. The equivalent formulations of the property do not hold anymore*.
3. We might end up having three different non-equivalent properties (all of which need a separate entry).
4. (lazy and weak point, but still want to mention it) We need to decide the property for lots of categories which are currently decided.

*In general, what does "limits of shape I commute with colimits of shape J" mean? Do we start with a bifunctor? What are the exact assumptions?

Similar remarks apply to other properties where other properties are assumed.

[ScriptRaccoon]

The discussion also applies to "filtered-colimit-stable monos" which currently requires filtered colimits to exist, but one might argue again to remove this assumption. Here I definitely agree, and only the "lazy point" remains. We then need to decide the property for 23 categories where it is currently decided.

And of course, the dual properties are affected as well.

[ykawase5048]

@ScriptRaccoon
The main reason I suggested removing the assumption of finite limits is actually much more concrete.

When I looked at the list of categories satisfying finitely accessible ∧ ¬exact filtered colimits in CatDat, I noticed that several categories appear there simply because they do not have finite limits. For example, the category of fields is on the list, even though the basic fact "pullbacks commute with filtered colimits in the category of fields" is still true. From a mathematical point of view, this feels rather weird to me, independently of any structural considerations about the database.

On the other hand, I only mentioned removing the assumption of filtered colimits for consistency. In fact, I am not particularly convinced that we should do that, since I don't have any motivating example for now.

Remark. If we were to weaken the assumptions in the way I suggested, I think the three equivalent definitions currently used on the exact filtered colimits page would only need minor adjustments: in (1), the domain category would have to be restricted, while in (2) and (3), one would simply add "whenever the (co)limits exist."

[ScriptRaccoon]

About the definiton of exact filtered colimits:

(1) says that for every finite category $I$ the functor $lim : [I,C] \to C$ preserves filtered colimits. You are saying that we simply need to adjust the domain of this functor, presumably to diagrams that have a limit. But I assume that we don't want to consider filtered colimits in this subcategory. I guess we still want to consider filtered colimits in $[I,C]$. But the problem is that these do not have to be computed point-wise. It is true when $C$ has filtered colimits. This inconvenience has led me (and others) to add the assumption that filtered colimits exist. Without this assumption, any form of equivalence to (2) or (3) is not available, I am afraid.

With (2), where we talk about $colim : [J,C] \to C$, there are similar problems.

(3) Here we have a diagram $X : I \times J \to C$, where $I$ is finite and $J$ is filtered, and assert that the canonical morphism

$\alpha : ~colim_j lim_i X(i,j) \to lim_i colim_j X(i,j)$

is an isomorphism. For this to make sense, we need to say that all the involved limits and colimits exist. Maybe this is the best definition since it is very concrete and avoids functor categories.

So I guess the definition (3') would be: When $I$ is finite and $J$ is filtered, and $X : I \times J \to C$ is a diagram such that (a) for every $i \in I$ the colimit $colim_j X(i,j)$ exists, (b) the limit $lim_i colim_j X(i,j)$ exists, (c) for every $j \in J$ the limit $lim_i X(i,j)$ exists, (d) the colimit $colim_j lim_i X(i,j)$ exists, then the canonical morphism $\alpha$ is an isomorphism.

This is very ugly. And how am I supposed to check if this is true in categories with few filtered colimits or few finite limits? For example, how should we check this in FinSet? Suddenly, this is not trivial anymore. What might be useful is that the inclusion functor FinSet → Set is cocontinuous (see here); this result is not formal.

This is my main issue with the extension of the definition to arbitrary categories. We do not just demand that colimits and limits interact in a good way. In the end, we also need to understand precisely which colimits and which limits exist.

EDIT: Also, it is not clear if (c) and (d) should be assumed. I think some authors assume (c) or (d).