Product category and its projection functors

Depends on

• Category, object, morphism, domain, codomain, identity, composition, and hom-collection
• Covariant functor, identity functor, composite functor, and contravariant functor

Used by

• Iterated ends may be taken in either order Corollary
• Dinatural transformation between functors on CᵒᵖtimesC Definition
• Ends and coends with parameters Definition
• Monoidal category Definition
• Strict 2-category Definition
• The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category Definition
• The tensor product of a presheaf and a covariant set-valued functor Definition
• The twisted arrow category and its projection to CᵒᵖtimesC Definition
• Wedges and cowedges, and the categories they form Definition
• Fubini checked by hand on a product of two walking arrows Example
• The distributive and exponential laws of sets are natural isomorphisms Example
• A wedge on a product index category is exactly a family dinatural in each variable separately Lemma
• A small product of preadditive categories is preadditive Proposition
• Composing a dinatural transformation with a natural transformation on either side gives a dinatural transformation Proposition
• The end of a functor made mute in its contravariant variable is the ordinary limit of that functor Proposition
• A category with finite products is monoidal Theorem
• A coend is a colimit weighted by the hom-bifunctor, and an end a limit weighted by it Theorem
• A family into a parametrised end is natural, or dinatural, in the parameter exactly when its composite with the counit is Theorem
• Dinatural transformations do not compose in general Theorem
• Fubini: an end over a product index category and the two iterated ends exist together and agree Theorem
• Iterated small limits commute: either order is canonically isomorphic to the limit over the product category Theorem
• The hom-assignment C(-,-):CᵒᵖtimesCtoSet is a bifunctor Theorem
• The twisted arrow category is the category of elements of the hom-bifunctor Theorem

Dependency tree · two levels

5 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

• Emily Riehl, Category Theory in Context, Chapter 1 (standard reference, not scraped)