nLab functor category

Functor categories

Functor categories

Definition

Given categories CC and DD, the functor category – written D CD^C or [C,D][C,D] – is the category whose

In homotopy type theory

Discussion in homotopy type theory.

Note: the HoTT book calls a internal category in HoTT a “precategory” and a univalent category a “category”, but here we shall refer to the standard terminology of “category” and “univalent category” respectively.

For categories A,BA,B, there is a category B AB^A, called the functor category, defined by

Proof. We define (1 F) a1 Fa(1_F)_a \equiv 1_{F a}. Naturality follows by the unit axioms of a category. For γ:FG\gamma : F \to G and δ:GH\delta : G \to H, we define (δγ) aδ aγ a(\delta \circ \gamma)_a \equiv \delta_a \circ \gamma_a. Naturality follows by associativity. Similarly, the unit and associativity laws for B AB^A follow from those for BB. \square

We define a natural isomorphism to be an isomorphism in B AB^A.

Usage

Functor categories serve as the hom-categories in the strict 2-category Cat.

In the context of enriched category theory the functor category is generalized to the enriched functor category.

In the absence of the axiom of choice (including many internal situations), the appropriate notion to use is often instead the anafunctor category.

Properties

Limits and colimits and closure

If DD has limits or colimits of a certain shape, then so does [C,D][C,D] and they are computed pointwise. (However, if DD is not complete, then other limits in [C,D][C,D] can exist “by accident” without being pointwise.)

If CC is small and DD is cartesian closed and complete, then [C,D][C,D] is cartesian closed. See at cartesian closed category for a proof.

Accessibility and local presentability

Functor categories enjoy the following accessibility and local presentability properties, as explained by Zhen Lin Low at nForum.

  • κ\kappa-accessible functors from a κ\kappa-accessible category to any accessible category form an accessible category. (It is not so easy to say what the accessibility rank is here.)

  • κ\kappa-accessible functors from a κ\kappa-accessible category to any locally λ\lambda-presentable category form a locally λ\lambda-presentable category.

  • Cocontinuous functors between locally presentable categories form a locally presentable category. More precisely, if CC and DD are locally κ\kappa-presentable, then so is [C,D][C,D].

  • Continuous accessible functors between locally presentable categories form the opposite of a locally presentable category. More precisely, if CC and DD are locally κ\kappa-presentable, then so is [C,D] rmop[C,D]^{\rm op}.

Indeed, the point is this: given a κ\kappa-accessible category 𝒞Ind κ(𝒜)\mathcal{C} \simeq Ind^\kappa (\mathcal{A}) (𝒜\mathcal{A} essentially small), the category of κ\kappa-accessible functors 𝒞𝒟\mathcal{C} \to \mathcal{D} (for arbitrary 𝒟\mathcal{D}; here by “κ\kappa-accessible” we mean simply “preserves κ\kappa-filtered colimits”) is naturally equivalent to the category of all 𝒜𝒟\mathcal{A} \to \mathcal{D}. It should be well known that:

  1. If 𝒟\mathcal{D} is accessible, then so is [𝒜,𝒟][\mathcal{A}, \mathcal{D}].

  2. If 𝒟\mathcal{D} is locally λ\lambda-presentable, then so is [𝒜,𝒟][\mathcal{A}, \mathcal{D}].

  3. Colimit-preserving functors out of a locally κ\kappa-presentable category are κ\kappa-accessible.

  4. A right adjoint between locally κ\kappa-presentable categories is κ\kappa-accessible if and only if its left adjoint is strongly κ\kappa-accessible (i.e. preserves κ\kappa-presentable objects as well as κ\kappa-filtered colimits); and every limit-preserving accessible functor between locally presentable categories is a right adjoint.

Statements 1 and 2 are proved in [Adamek and Rosick, Locally presentable and accessible categories], statement 3 is obvious, and statement 4 is a straightforward exercise. Thus the claims follow.

In general, accessible functors between accessible categories do not form an accessible category due to size issues. The best one can hope for is a class-accessible category. Let 𝒞\mathcal{C} be an accessible category that is not essentially small. Consider the category 𝒜\mathcal{A} of all accessible functors 𝒞Set\mathcal{C} \to \mathbf{Set}. This is the same as the smallest full replete subcategory of [𝒞,Set][\mathcal{C}, \mathbf{Set}] containing all representable functors and closed under small colimits. In particular, 𝒜\mathcal{A} is accessible if and only if 𝒜\mathcal{A} locally presentable. We claim 𝒜\mathcal{A} is not accessible.

Indeed, suppose 𝒜\mathcal{A} has a small generating family, say 𝒢\mathcal{G}. Then for some regular cardinal κ\kappa, every member of 𝒢\mathcal{G} is κ\kappa-accessible. So consider 𝒞(X,)\mathcal{C} (X, -) for some object XX that is not κ\kappa-presentable. (Such an XX exists because 𝒞\mathcal{C} is not essentially small.) Since 𝒢\mathcal{G} generates, there is a small diagram of κ\kappa-accessible functors whose colimit is 𝒞(X,)\mathcal{C} (X, -). But then 𝒞(X,)\mathcal{C} (X, -) is a retract of a κ\kappa-accessible functor and hence κ\kappa-accessible: a contradiction. That said, 𝒜\mathcal{A} is a class-locally presentable category.

In homotopy type theory

Lemma 9.2.4

A natural transformation γ:FG\gamma : F \to G is an isomorphism in B AB^A if and only if each γ a\gamma_a is an isomorphism in BB.

Proof. If γ\gamma is an isomorphism, then we have δ:GF\delta : G \to F that is its inverse. By definition of composition in B AB^A, (δγ) aδ aγ a(\delta \gamma)_a \equiv \delta_a \gamma_a. Thus, δγ=1 F\delta \gamma = 1_F and γδ=1 G\gamma \delta=1_G imply that δ aγ a=1 Fa\delta_a \gamma_a = 1_{F a} and γ aδ a=1 Ga\gamma_a \delta_a = 1_{G a}, so γ a\gamma_a is an isomorphism.

Conversely, suppose each γ a\gamma_a is an isomorphism, with inverse called δ a\delta_a. We define a natural transformation δ:GF\delta : G \to F with components δ a\delta_a; for the naturality axiom we have

Ffδ a=δ bγ bFfδ a=δ bGfγ aδ a=δ bGfF f \circ \delta_a=\delta_b \circ \gamma_b \circ F f \circ \delta_a = \delta_b \circ G f \circ \gamma_a \circ \delta_a = \delta_b \circ G f

Now since composition and identity of natural transformations is determined on their components, we have γδ=1 G\gamma \delta=1_G and δγ1 F.\delta \gamma 1_F.\ \square

Theorem 9.2.5

If AA is a category and BB is a univalent category, then B AB^A is a univalent category.

Proof. Let F,G:ABF,G:A\to B; we must show that idtoiso:(F=G)(FG)idtoiso:({F}={G}) \to (F\cong G) is an equivalence.

To give an inverse to it, suppose γ:FG\gamma:F\cong G is a natural isomorphism. Then for any a:Aa:A, we have an isomorphism γ a:FaGa\gamma_a:F a \cong G a, hence an identity isotoid(γ a):Fa=Gaisotoid(\gamma_a):{F a}={G a}. By function extensionality, we have an identity γ¯:F 0= (A 0B 0)G 0\bar{\gamma}:{F_0}=_{(A_0\to B_0)}{G_0}.

Now since the last two axioms of a functor are mere propositions, to show that F=G{F}={G} it will suffice to show that for any a,b:Aa,b:A, the functions

F a,b:hom A(a,b)hom B(Fa,Fb) F_{a,b}:hom_A(a,b) \to hom_B(F a,F b)
G a,b:hom A(a,b)hom B(Ga,Gb) G_{a,b}:hom_A(a,b) \to hom_B(G a,G b)

become equal when transported? along γ¯\bar\gamma. By computation for function extensionality, when applied to aa, γ¯\bar\gamma becomes equal to isotoid(γ a)isotoid(\gamma_a).

This reference needs to be included. For now as transports are not yet written up I didn’t bother including a reference to the page univalent category. -Ali

But by [INCLUDE ME], transporting Ff:hom B(Fa,Fb)F f:hom_B(F a,F b) along isotoid(γ a)isotoid(\gamma_a) and isotoid(γ b)isotoid(\gamma_b) is equal to the composite γ bFfinv(γ a)\gamma_b\circ F f\circ \inv{(\gamma_a)}, which by naturality of γ\gamma is equal to GfG f.

This completes the definition of a function (FG)(F=G)(F\cong G) \to (F =G). Now consider the composite

(F=G)(FG)(F=G). (F= G) \to (F\cong G) \to (F =G).

Since hom-sets are sets, their identity types are mere propositions, so to show that two identities p,q:F=Gp,q:F =G are equal, it suffices to show that p= F 0=G 0qp =_{{F_0}={G_0}}{q}. But in the definition of γ¯\bar\gamma, if γ\gamma were of the form idtoiso(p)idtoiso(p), then γ a\gamma_a would be equal to idtoiso(p a)idtoiso(p_a) (this can easily be proved by induction on pp). Thus, isotoid(γ a)isotoid(\gamma_a) would be equal to p ap_a, and so by function extensionality we would have γ¯=p{\bar\gamma}={p}, which is what we need.

Finally, consider the composite

(FG)(F=G)(FG).(F\cong G)\to ( F = G) \to (F\cong G).

Since identity of natural transformations can be tested componentwise, it suffices to show that for each aa we have idtoiso(γ¯) a=γ a{idtoiso(\bar\gamma)_a}={\gamma_a}. But as observed above, we have idtoiso(γ¯) a=idtoiso((γ¯) a){idtoiso(\bar\gamma)_a}={idtoiso((\bar\gamma)_a)}, while (γ¯) a=isotoid(γ a){(\bar\gamma)_a}={isotoid(\gamma_a)} by computation for function extensionality. Since isotoidisotoid and idtoisoidtoiso are inverses, we have idtoiso(γ¯) a=γ a{idtoiso(\bar\gamma)_a}={\gamma_a} as desired. \square

Size issues

If CC and DD are small, then [C,D][C,D] is also small.

If CC is small and DD is locally small, then [C,D][C,D] is still locally small.

Even if CC and DD are locally small, if CC is not small, then [C,D][C,D] will usually not be locally small.

As a partial converse to the above, if CC and [C,Set][C,Set] are locally small, then CC must be essentially small; see Freyd & Street (1995).

References

Last revised on June 7, 2022 at 11:17:28. See the history of this page for a list of all contributions to it.