3
$\begingroup$

I'm now reading the proof of Mitchell's embedding theorem proved in the book of Swan 'Algebraic K-Theory'.

Now I'm trying to understand the sentence

'It is well known that for a small abelian category $A$, the functor category from $A$ to the category $Ab$ of abelian groups is well powered, right complete, and has injective envelopes.'

To understand the well-poweredness, I tried to understand that for a functor $F$, $\{ F(X) \}_{X \in \mathrm{obj}(A)}$ is a set.

I guess the relevant axiom in the set theory is the 'Axiom of Replacement' and it seems that the axiom is understood to be natural because if a collection of elements of a class is indexed by a set, then the collection is also a set because the cardinality of the collection is bounded by the index set. With this explanation, $\{ F(X) \}_{X \in \mathrm{obj}(A)}$ must be a set.

But in the textbooks of set theory, there is a mention of the definable property (more precisely definable in the formal first order language) in the axiom of replacement.

So my question is

In the category theory, do we implicitly assume that a functor is definable? or if not the argument using the cardinality is formal enough?

(By the way, If you can also briefly explain the sentence of the Swan's book, then that would be also a great help! as I'm not meant to be a specialist in this field.)

$\endgroup$

3 Answers 3

7
$\begingroup$

For category theory, rather than using ZFC as the background theory, one usually works with an axiomatic system that treats classes a little more simply, like NBG. In NBG, the axiom of replacement has no definability requirement for class functions.

If you want to stick with ZFC, then yes you are implicitly assuming that functors are class functions, and hence are definable from first-order formulas in the language (possibly with set parameters).

I personally like to work with ZFC + an axiom of universes. In this view, one may take every category to be contained in a universe. Thus, every functor is actually a set, and hence definable (using that set as a parameter).

$\endgroup$
2
8
$\begingroup$

In the Axiom of Replacement, the "definition" involved is allowed to use parameters, i.e. it is allowed to refer to specific sets. In this case, the functor $F$ is a set, and so your definition using Replacement is allowed to refer to $F$.

(Note that if $A$ were not small, then it would not be possible for a functor on $A$ to be a set (though in some special cases it may be possible to "encode" such functors with sets). In that case, working in ZFC, it would not be possible to quantify over such functors at all and formulate a theorem such as the one you refer to. Instead, you would need to work in a set theory that can refer to "large" objects as described in Pace Nielsen's answer.)

$\endgroup$
2
  • $\begingroup$ Eric, I think the issue is justifying that $F$ is indeed a set in the first place. In general, a functor between categories is not a set. So by what principle can you assert that $F$ is a set when the domain is a small category? If you use an axiom of replacement to do so, that doesn't let you a priori claim that $F$ is definable; for the axiom of replacement requires that you have definability before using it. $\endgroup$ Commented Dec 20, 2020 at 5:40
  • $\begingroup$ In other words, you can't take $F$ to be a parameter before you know it is a set. $\endgroup$ Commented Dec 23, 2020 at 22:15
6
$\begingroup$

Another way to formalise functors from a small category $A$ to a large concrete category $C$ is to define it as a function $El(F) \to Ob(A)$, where the preimage of $a\in Ob(A)$ is precisely the underlying set of the value of $F$ at $a$, together with some more data specifying the effect of arrows (plus a functoriality condition). In one sense this is defining away the problem, but in fact such an approach is necessary when dealing with these kind of functors in other settings.

For functors to $\mathbf{Ab}$, you would specify that the fibres of $El(F) \to Ob(A)$ are equipped with an abelian group structure, and that the functoriality data respects that.

In this way, no universes are needed, and the data is, informally, exactly what you think it should be.

$\endgroup$
10
  • $\begingroup$ "In one sense this is defining away the problem, but in fact such an approach is necessary when dealing with these kind of functors in other settings." I'm intrigued, and at a loss for why this would be necessary. I would have thought that in all settings, the functor category was defined in the same way, regardless of whether the domain category is small or not. $\endgroup$ Commented Dec 20, 2020 at 5:50
  • 1
    $\begingroup$ OK, try this: Take an arbitrary topos $E$ with nno as "the" category of constructive sets. This is just a construction of first order logic, so there is no [I]ZF[C] metatheory, so like ETCS but without classical logic baked in. A small category is then an internal category $C$ in $E$. Ask yourself what a functor $C\to E$ can even be. One definition that makes sense is that of an internal diagram (there is also an option using fibred categories), and this is what I was alluding to. $\endgroup$
    – David Roberts
    Commented Dec 20, 2020 at 8:01
  • $\begingroup$ David, I think you misunderstood my question. Let $C$ and $D$ be arbitrary categories. As I understand it, the functor category $D^C$ always exists (whether or not $C$ and $D$ are small). I find it strange that it would be necessary to use a different definition of this functor category when $C$ is small. $\endgroup$ Commented Dec 20, 2020 at 22:50
  • $\begingroup$ @Pace Well, if you are in ZFC and both $C$ and $D$ are large (and so are given as classes defined by formulae), what is the class of objects of $D^C$? It would require having a class of functions between a pair of proper classes. Even taking NBG as foundation, so you don't need a formula to define a proper class, there is still no such class. It's not so much smallness, but how foundations handle large categories. $\endgroup$
    – David Roberts
    Commented Dec 21, 2020 at 2:12
  • 1
    $\begingroup$ @gualterio In this formalism, a functor $F\colon A \to \mathbf{Ab}$ is given by the following data: a function $p\colon El(F) \to Obj(A)$ and specified abelian group structure on each $F(a) := p^{-1}(a)$; a function $f\colon s^*El(F) \to t^*El(F)$ over $Mor(A)$ respecting the abelian group structures, where $s,t\colon Mor(A) \to Obj(A)$ are the source and target functions, and $s^*,t^*$ denote pullbacks. Additionally, $f$ satisfies a functoriality condition: $m^*f$ is the composite of $pr_1^*f$ and $pr_2^*f$, for $m,pr_1,pr_2 \colon Mor(A)\times_{Obj(A)} Mor(A) \to Mor(A)$. $\endgroup$
    – David Roberts
    Commented Dec 23, 2020 at 0:34

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .