mjhjmtu

Isbell gave, in Two set-theoretic theorems in categories (1964), a necessary criterion for categories to be concretisable (i.e. to admit some faithful functor into sets). Freyd, in Concreteness (1973), showed that Isbell’s criterion is also sufficient.

My question is: Has anyone ever used Isbell’s criterion to check that a category is concretisable?

I’m interested not only in seeing the theorem is formally invoked in print, to show some category is concretisable — though of course that would be a perfect answer, if it’s happened. What I’m also interested in, and suspect is more likely to have occurred, is if anyone’s found the criterion useful as a heuristic for checking whether a category is concretisable, in a situation where one wants it to be concrete but finding a suitable functor is not totally trivial. (I’m imagining a situation similar to the adjoint functor theorems: they give very useful quick heuristics for guessing whether adjoints exist, but if they suggest an adjoint does exist, usually there’s an explicit construction as well, so they’re used as heuristics much more often than they’re formally invoked in print.)

What I’m not so interested in is uses of the criterion to confirm that an expected non-concretisable category is indeed non-concretisable — I’m after cases where it’s used in expectation of a positive answer.

An inverse category can be defined as a category where every $f$ admits a unique regular inverse, i.e. a map $g$ such that $fgf=f$ and $gfg=g$. In [1], Kastl proves that any locally small inverse category admits a faithful functor into $PInj$, the category of sets and partial injections. The proof first verifies Isbell's criterion, obtaining a faithful functor to $Set$ and then one proves a general result giving rise to a faithful functor to $PInj$.

[1] J. Kastl. Inverse categories. Studien zur Algebra und ihre Anwendungen, 7:51–
60, 1979.

I did this once with the category of schemes in response to this question, with help from Laurent Moret-Bailly. But then Zhen Lin Low pointed out there's an obvious concretizing functor. Maybe it wasn't so obvious until we were sure it was there, though. So I suppose this falls under the "useful heuristic" category. In practice, the Isbell-Freyd criterion translated the problem into something more concrete (pardon the pun!) which an algebraic geometer had a sense for how to answer. At the time, I didn't know enough algebraic geometry to answer this question on my own, so translating it into more geometric language which I could ask somebody else was an essential step for me.

It helped that, as Ivan Di Liberti points out in the comments, the criterion is especially simple in a finitely-complete category.

[Answer converted from a comment by Jiří Rosický on another answer.]

Isbell’s criterion is used directly in Libor Barto’s paper Accessible set functors are universal (pdf), Section 4, to show that the category of “accessible set functors” (i.e. accessible endofunctors on $mathrmSet$) is concretisable. A slightly different argument, based on the simpler criterion “regular-well-powered” for the finitely complete case, is used for this same example in Remarks 5.5–6 of Adámek–Rosičký How nice are free completions of categories? (arXiv:1806.02524)