Aside. Category theory [dt-002A]
DefinitionCategory [dm-000G]
A category Cconsists of a collection of things (objects) and a collection of arrows between these things (morphisms). If there is a morphism A \xrightarrow {f} B and a morphism B \xrightarrow {g} C, we also have the composed morphism A \xrightarrow {g \circ f} C. This composition operator must be associative. Additionally each object X has an identity morphism X \xrightarrow {\mathsf {id}_X} X, such that for an arrow X \xrightarrow {a} Y, a \circ \mathsf {id}_X = \mathsf {id}_Y \circ a = a.
ExampleThe category \mathbf {Set} [dm-000H]
ExampleThe category \mathbf {Rel} [dm-000I]
ExampleThe category \mathbf {Cpo} [dt-002B]
The category \mathbf {Cpo} is the category where the objects are cpos, the morphisms are continuous functions between these cpos, composition is function composition ((g \circ f)(x) \triangleq g(f(x))) and identity is just the identity function \lambda x. x.
DefinitionFunctor [dm-000J]
A functor F from a category \mathbf {C} to a category \mathbf {D} consists of an object mapping that maps objects of \mathbf {C} to objects of \mathbf {D}, and a morphism mapping that maps morphisms of \mathbf {C} to morphisms of \mathbf {D} such that:
- For each A \xrightarrow {m} B in \mathbf {C}, we have a morphism F(A) \xrightarrow {F(m)} F(B) in \mathbf {D}.
- For each object A in \mathbf {C}, the equation F(\mathsf {id}_A) = \mathsf {id}_{F(A)} holds in \mathbf {D}.
- For a pair of morphism A \xrightarrow {f} B \xrightarrow {g} C in \mathbf {C}, the equation F (g \circ f) = F(g) \circ F(f) holds in \mathbf {D}.
ExampleThe category \mathbf {Cat} [dm-000K]
The category \mathbf {Cat} is the category where the objects are themselves (small) categories, the morphisms are structure-preserving maps between these categories, i.e., functors.
Commutative diagrams [dm-000L]
When working in a category, we can state many theorems compactly using commutative diagrams, such as this diagram for products:
