nLab functor

Redirected from "internal functor".
Contents

Contents

Idea

So, for CC, DD two categories, a functor F:CDF \colon C \to D consists of

  1. a component-function of the classes of objects;

    F 0:Obj(C)Obj(D)F_0 \colon Obj(C) \to Obj(D)

  • a component-function of sets of morphisms

    F 1:Mor(C)Mor(D)F_1 \colon Mor(C) \to Mor(D)

    or equivalently:

    for each pair x,yObj(C)x,y \in Obj(C) of objects, a component-function

    (1)F x,y:C(x,y)D(F(x),F(y)) F_{x,y} \;\colon\; C(x,y) \xrightarrow{\;\;} D(F(x), F(y))

    between hom-sets;

such that:

  • it respects source and target of morphisms: F 1F_1 coincides with F 0F_0 on source and target objects;

  • it respects identity morphisms: F(id X)=id F(X)F(id_X) = id_{F(X)};

  • it respects composition: the image of the composite of two morphisms under FF is the composite of their images.

These last two properties are the decisive ones of a functor; they are called the functoriality conditions. These are a direct generalization of the notion of homomorphism (of monoids, groups, algebras, etc.) to the case that there are more objects. As a slogan:

The notion of functor is a horizontal categorification of that of homomorphism.

Definition

External definition

A functor FF from a category CC to a category DD is a map sending each object xCx \in C to an object F(x)DF(x) \in D and each morphism f:xyf : x \to y in CC to morphism F(f):F(x)F(y)F(f) : F(x) \to F(y) in DD, such that

  • FF preserves composition: F(gf)=F(g)F(f)F(g\circ f) = F(g)\circ F(f) whenever the left-hand side is well-defined,

  • FF preserves identity morphisms: for each object xCx \in C, F(1 x)=1 F(x)F(1_x) = 1_{F(x)}.

Or equivalently, since compositions gf=gfg f = g\circ f (commuting triangles) and identities 1 x1_x (commuting loops) are both simple commuting diagrams, we can combine the above conditions to the single statement

Given morphisms f:XYf \colon X\to Y, g:YZg \colon Y\to Z, and h:XZh \colon X\to Z, declaring the triangle commutes amounts to declaring

h=gf.h = g\circ f.

In this case, for F:CDF:C\to D to preserve the commutative triangle means

F(h)=F(g)F(f)F(h) = F(g)\circ F(f)

as depicted below

Preserving commuting triangles means FF preserves compositions.

Given morphisms f:XYf:X\to Y, g:YZg:Y\to Z, and h:ZXh:Z\to X, declaring the loop commutes amounts to declaring

1 X=hgf.1_X = h\circ g\circ f.

In this case, for F:CDF:C\to D to preserve the commutative loop means

F(1 X)=F(h)F(g)F(f)F(1_X) = F(h)\circ F(g)\circ F(f)

as depicted below

However, it means more than that. Since any commutative loop is equal to the identity morphism, we must also have

1 F(X)=F(h)F(g)F(f)1_{F(X)} = F(h)\circ F(g)\circ F(f)

implying

F(1 X)=1 F(X).F(1_X) = 1_{F(X)}.

Preserving commuting loops means FF preserves identity morphisms.

Another equivalent way to say this is that a functor F:CDF : C \to D is precisely a morphism of simplicial sets N(F):N(C)N(D)N(F) : N(C) \to N(D) between the nerves of these categories

  • the objects of CC and DD are the 0-cells of N(C)N(C) and N(D)N(D), so N(F) 0:N(F) 0N(F) 0N(F)_0 : N(F)_0 \to N(F)_0 maps objects of CC to objects of DD;

  • the morphisms of CC and DD are the 1-cells of N(C)N(C) and N(D)N(D), so N(F) 1:N(F) 1N(F) 1N(F)_1 : N(F)_1 \to N(F)_1 maps morphisms of CC to objects of DD;

  • the identity morphisms of CC and DD are the degenerate 1-cells of N(C)N(C) and N(D)N(D), so the fact that N(F)N(F) respects degeneracy maps means that FF respects identities;

  • the commuting triangles of CC and DD are the 2-cells of N(C)N(C) and N(D)N(D), so the fact that N(F)N(F) maps 2-cells to 2-cells means that it respects commuting triangles, hence that it respects composition.

See nerve for more details on this.

The functors between two categories CC and DD form themselves a category, the functor category [C,D][C,D], whose morphisms are natural transformations. Equipped with these functor categories as hom-objects, we have a 22-category Cat of categories, functors and natural transformations. In other words, functors are morphisms in CatCat.

Internal definition

If CC and DD are internal categories in some ambient category AA, then an internal functor F:CDF : C \to D is

  • a morphism of objects F 0:C 0D 0F_0 : C_0 \to D_0 in AA;

  • a morphisms of morphisms F 1:C 1D 1F_1 : C_1 \to D_1 in AA;

  • such that the following diagrams commute

    • respect for the source map: C 1 f 1 D 1 s s C 0 f 0 D 0 \array{ C_1 &\stackrel{f_1}{\to}& D_1 \\ \downarrow^s && \downarrow^s \\ C_0 &\stackrel{f_0}{\to}& D_0 } ;

    • respect for the target map: C 1 f 1 D 1 t t C 0 f 0 D 0 \array{ C_1 &\stackrel{f_1}{\to}& D_1 \\ \downarrow^t && \downarrow^t \\ C_0 &\stackrel{f_0}{\to}& D_0 } ;

    • respect for identities C 0 f 0 D 0 i i C 1 f 1 D 1 \array{ C_0 &\stackrel{f_0}{\to}& D_0 \\ \downarrow^i && \downarrow^i \\ C_1 &\stackrel{f_1}{\to}& D_1 } ;

    • respect for composition C 1× t,sC 1 f 1× t,sf 1 D 1× t,sD 1 C 1 f 1 D 1 \array{ C_1 \times_{t,s} C_1 &\stackrel{f_1\times_{t,s} f_1}{\to}& D_1 \times_{t,s} D_1 \\ \downarrow^{\circ} && \downarrow^{\circ} \\ C_1 &\stackrel{f_1}{\to}& D_1 } .

This reproduces the external definition of functors above for small categories, which are categories internal to Set

In many cases, this notion is too restrictive, and we should use internal anafunctors instead.

Enriched definition

In enriched category theory a functor maps not hom-sets but the given hom-objects to each other, in a way that respects their composition. This is described at

Profunctors

A generalization of the notion of enriched functor is the notion of profunctor.

Higher categorical functors

In higher category theory there are corresponding higher notions of functor, such as

In homotopy type theory

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

The definition of functor in homotopy type theory is a straightforward translation of the ordinary one. However, the notion of univalent category allows us to construct some such functors that in classical mathematics would require either the axiom of choice or the use of anafunctors.

Let AA and BB be categories. Informally, a functor F:ABF : A \to B consists of

  • A function F 0:A 0B 0F_0 : A_0 \to B_0
  • For each a,b:Aa,b:A, a function 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), generally also denoted FF.
  • For each a:Aa:A, we have F(1 a)=1 FaF(1_a)=1_{F a}.
  • For each a,b,c:Aa,b,c: A and f:hom A(a,b)f:hom_A(a,b) and g:hom A(b,c)g:hom_A(b,c), we have
F(gf)=FgFfF(g \circ f) = F g \circ F f

Formally, the type of functors from AA to BB is

Func(A,B) F 0:A 0B 0 F: a,b:Ahom A(a,b)hom B(Fa,Fb)( a:AF(1 a)=1 Fa)×( a,b,c:A f:hom A(a,b) g:hom A(b,c)F(gf)=FgFf) Func(A,B) \coloneqq \sum_{F_0:A_0\to B_0} \sum_{F:\prod_{a,b:A} hom_A(a,b) \to \hom_B(F a,F b)} \Big(\prod_{a:A} F(1_a) = 1_{F a}\Big) \times \Big( \prod_{a,b,c:A} \prod_{f:\hom_A(a,b)} \prod_{g:\hom_A(b,c)} F(g \circ f) = F g \circ F f\Big)

A formal definition in Coq can be found in Ahrens-Kapulkin-Shulman 13.

Properties

These properties come from the HoTT book.

By induction on identity, a functor also preserves idtoisoidtoiso (See category).

Composition of functors

For functors F:ABF:A\to B and G:BCG:B \to C, their composite GF:ACG \circ F : A \to C is given by

  • The composite (G 0F 0):A 0C 0(G_0 \circ F_0): A_0 \to C_0
  • For each a,b:Aa,b:A, the composite
    (G Fa,FbF a,b):hom A(a,b)hom C(GFa,GFb)(G_{F a, F b} \circ F_{a,b}):hom_A(a,b)\to hom_C(G F a, G F b)

Lemma 9.2.9 in HoTT book

Composition of functors is associative H(GF)=(HG)FH(G F)=(H G)F.

Proof: Since composition of functions is associative, this follows immediately for the actions on objects and on homs. And since hom-sets are sets, the rest of the data is automatic. \square

Lemma 9.2.10 in HoTT book

Lemma 9.2.9 is coherent, i.e. the following pentagon of equalities commutes:

(KH)(GF) ((KH)G)F K(H(GF)) (K(HG))F K((HG)F) \array{ && (K H)(G F) \\ & \nearrow && \searrow \\ ((K H) G) F && && K (H (G F)) \\ \downarrow && && \uparrow \\ (K(H G)) F && \longrightarrow && K( (H G) F) }

Types of functors

Specific types of functors are important in applications. See for instance

And for more background on this see stuff, structure, property.

Examples

Morphisms of monoids and groups

For A,BA,B monoids or G,HG, H groups, let BA,BB\mathbf{B}A, \mathbf{B}B, BG\mathbf{B}G, BH\mathbf{B}H be the corresponding one-object categories (as described at delooping). Then functors

BABB \mathbf{B}A \to \mathbf{B}B

are canonically in bijection with monoid homomorphisms ABA \to B and accordingly functors

BGBH \mathbf{B}G \to \mathbf{B}H

are canonically in bijection with group homomorphisms GHG \to H.

Representations

With BG\mathbf{B}G as above, functors on BG\mathbf{B}G with values in Vect are the same as linear representations of the group GG. In fact, we have a canonical isomorphism of categories

Funct(BG,Vect)Rep(G) Funct(\mathbf{B}G, Vect) \simeq Rep(G)

of the functor category with the representation category.

Linear Maps

Let BEnd(U)\mathbf{B} End(U) and BEnd(V)\mathbf{B} End(V) be one-object categories whose objects are each finite-dimensional vector space and whose morphisms are all of the linear endomorphisms on that space, i.e. one-object full subcategories of FinVectFin Vect.

Left Inverses

If the linear map F:UVF:U\to V has a left inverse, i.e.

F *F=1 U,F^*\circ F = 1_U,

where F *F^* is the preimage, then we can construct a functor

F *:BEnd(U)BEnd(V)F_*:\mathbf{B} End(U)\to\mathbf{B} End(V)

by defining its action on objects by

F *(U)=F *UF_*(U) = F_* U

where F *F_* on the right-hand side is the image and its action on endomorphisms by

F *(f)=FfF *.F_*(f) = F f F^*.

Composition follows immediately

F *(fg)=FfgF *=FfF *FgF *=F *(f)F *(g).F_*(f g) = F f g F^* = F f F^* F g F^* = F_*(f) F_*(g).

Identity morphisms are preserved since for any vector yy in F *UVF_*U\subset V, then

y=Fxy = F x

for some vector xx in UU and we have

F *(1 U)y=FF *y=FF *Fx=Fx=yF_*(1_U)y = F\circ F^* y = F\circ F^*\circ F x = F x = y

so that

F *(1 U)=1 F *(U)F_*(1_U) = 1_{F_*(U)}

as required. Hence, F *F_* is a functor.

Right Inverses

If the linear map F:UVF:U\to V has a right inverse, i.e.

FF *=1 V,F\circ F^* = 1_V,

where F *F^* is the preimage, then we can construct a functor

F *:BEnd(V)BEnd(U)F^*:\mathbf{B} End(V)\to\mathbf{B} End(U)

by defining its action on objects by

F *(V)=F *VF^*(V) = F^*V

where F *F^* on the right-hand side is preimage, and its action on endomorphisms by

F *(f)=F *fF.F^*(f) = F^* f F.

Composition follows immediately

F *(fg)=F *fgF=F *fFF *gF=F *(f)F *(g).F^*(f g) = F^* f g F = F^* f F F^* g F = F^*(f) F^*(g).

Identity morphisms are preserved since for any vector xx in F *VUF^*V\subset U, then

x=F *yx = F^*y

for some vector yy in VV and we have

F *(1 V)x=F *Fx=F *FF *y=F *y=xF^*(1_V)x = F^*\circ F x = F^*\circ F \circ F^* y = F^* y = x

so that

F *(1 V)=1 F *(V)F^*(1_V) = 1_{F^*(V)}

as required. Hence, F *F^* is a functor.

Presheaves

Functors F:CSetF : C \to Set with values in Set are also called presheaves. As such one calls them presheaves on the opposite category C opC^{op} of CC. See presheaf for more on this.

Functors and generalized elements

For CC a category, and XCX \in C an object, and UU any other object, a morphism x:UXx : U \to X may be regarded as a generalized element of XX, written xXx \in X (For this language applied to the category Set of sets see ETCS. For the general case see type theory).

The set of generalized elements of an object XCX \in C is thus the union of hom-sets UCHom C(U,X)\coprod_{U \in C} Hom_C(U,X).

While a morphism f:XYf : X \to Y in an arbitrary category CC need not at all come to us as a function of sets, it always induces a function of sets of generalized elements : it sends the generalized element x:UXx : U \to X of XX to the generalized element

f(x):UxXfY f(x) : U \stackrel{x}{\to} X \stackrel{f}{\to} Y

of YY, using the composition of the morphism ff with the morphism xx in CC.

In terms of this notation, the functoriality condition on a functor F:CDF : C \to D, which is

F(UxXfY)=F(U)F(x)F(X)F(f)F(Y) F(U \stackrel{x}{\to} X \stackrel{f}{\to} Y) = F(U) \stackrel{F(x)}{\to} F(X) \stackrel{F(f)}{\to} F(Y)

appears as

F(f(x))=F(f)(F(x)). F(f(x)) = F(f)(F(x)) \,.

This can be illustrated in the following diagram

which provides an alternative expression of the functoriality condition as simply a statement that commuting diagrams in CC map to commuting diagrams in DD.

basic properties of…

References

Textbook accounts:

See also the references at:

For functors in homotopy type theory

Coq code formalizing the concept of functors includes the following:

Formalization in cubical Agda:

Last revised on February 24, 2024 at 07:26:58. See the history of this page for a list of all contributions to it.