<h1> CatsCheatSheet </h1>

This project is to contain a listing of common theorems in elementary category theory.

The repo contains other articles I've written on Category Theory; which may be read in a blog-format at: https://alhassy.github.io/blog/categories/#categorytheory

The listing sheet, as PDF, can be found here, while below is an unruly html rendition.

This reference sheet is built around the system https://github.com/alhassy/CheatSheet

Table of Contents

1. Categories
2. “Gluing” Morphisms Together
3. Functors
4. Naturality
5. Adjunctions
6. Constant Combinators
7. Monics and Epics
8. Isos
9. Skolemisation
10. Initiality
11. Colimits
12. Limits
13. Sums
14. Products
15. Finitary Sums and Products
16. Mixing products and coproducts
17. References
18. To Read
19. Monoidal and Closed Categories
20. Enrichment & Internal Algebraic Structures

<a id="org190f6a8"></a>

Categories

A category 𝒞 consists of a collection of “objects” (\Obj, 𝒞), a collection of “(homo)morphisms” (\Hom_𝒞(a,b)) for any (a,b : \Obj,𝒞) —also denoted “(a ,\to_𝒞, b)”—, an operation (\Id) associating a morphism (\Idₐ : \Hom(a,a)) to each object (a), and a dependently-typed “composition” operation (_∘_ : ∀{A , B , C : \Obj} → \Hom(B,C) → \Hom(A,B) → \Hom(A,C)) that is required to be associative with (\Id) as identity.

It is convenient to define a pair of operations (\src, \tgt) from morphisms to objects as follows:

\begin{flalign*} f : X \to_𝒞 Y \quad\equiv\quad \mathsf{src}; f = X ;\land; \mathsf{tgt}; f = Y && \tag*{$\src,\tgt$-Definition} \label{src-tgt-Definition} \end{flalign*}

Instead of (\Hom_𝒞) we can instead assume primitive a ternary relation (_:_→_𝒞_) and regain (\Hom_𝒞) precisely when the relation is functional in its last two arguments: \eqn{type-Unique}{f : A \to_𝒞 B ;;\land;; f : A' \to_𝒞 B' ;\implies; A=A' ;\land; B=B'} When this condition is dropped, we obtain a pre-category; e.g., the familiar Sets is a pre-category that is usually treated as a category by making morphisms contain the information about their source and target: ((A, f, B) : A → B) rather than just (f). \newline This is sometimes easier to give than Hom! C.f. Alg(F). \room

Here's an equivalence-preserving property that is useful in algebraic calculations,

Examples:

• Linear Algebra: Matrices with real number values determine a category whose objects are the natural numbers, morphisms (n → m) are (n × m) matrices, (\Id) is the identity matrix, and composition is matrix multiplication.

• Each preorder determines a category: The objects are the elements and there is a morphism (a → b) named, say, “((a, b))”, precisely when (a \leq b); composition boils down to transitivity of (\leq).

• Each monoid ((M, ⊕, e)) gives rise to a category: The objects and the arrows are both the elements of(M), and (k : m → n ;≡; k ⊕ m = n). E.g., ((ℕ, ×, 1)) gives rise to a category whose products are gcd's and so properties of products are thus gcd theorems!

• Each digraph determines a category: The objects are the nodes and the paths are the morphisms typed with their starting and ending node. Composition is catenation of paths and identity is the empty path.

• Suppose we have an `interface', in the programming sense, of constant, function, and relation symbols —this is also called a signature.

  Let 𝒯 be any collection of sentences in the first-order language of signature (\Sigma). Then we can define a category (\mathsf{Mod},𝒯) whose objects are implementations of interface (\Sigma) satisfying constraints 𝒯, and whose morphisms are functions that preserve the (\Sigma) structure. Ignoring constraints 𝒯 gives us `functor algebras'.

  Particular examples include monoids and structure-preserving maps between them; likewise digraphs, posets, rings, etc and their homomorphisms.

\room

Even when morphisms are functions, the objects need not be sets: Sometimes the objects are operations —with an appropriate definition of typing for the functions. The categories of F-algebras are an example of this.

<a id="org417a0df"></a>

“Gluing” Morphisms Together

Traditional function application is replaced by the more generic concept of functional composition suggested by morphism-arrow chaining:

Whenever we have two morphisms such that the target type of one of them, say (g : B ← A) is the same as the source type of the other, say (f : C ← B) then “(f) after (g)”, their composite morphism, (f ∘ g : C ← A) can be defined. It “glues” (f) and (g) together, “sequentially”:

Composition is the basis for gluing morphisms together to build more complex morphisms. However, not every two morphisms can be glued together by composition.

\room

Types provide the interface for putting morphisms together to obtain more complex functions.

\room

A split arises wherever two morphisms do not compose but share the same source.

• Since they share the same source, their outputs can be paired: (c ↦ (f, c, g, c)).
• This duplicates the input so that the functions can be executed in “parallel” on it.

\room

A product appears when there is no explicit relationship between the types of the morphisms.

• We regard their sources as projections of a product, whence they can be seen as splits.
• This ((c, d) ↦ (f, c, g, d)) corresponds to the “parallel” application of (f) and (g), each with its own input.

\room

An either arises wherever two morphisms do not compose but share the same target.

• Apply (f) if the input is from the “(A) side” or apply (g) if it is from the “(B) side”.
• This is a “case analysis” of the input with branches being either (f) or (g).

\room

A sum appears when there is no explicit relationship between the types of the morphisms.

• We regard their targets as injections into a sum, whence they can be seen as eithers.

\room

A transpose arises when we need to combine a binary morphism with a unary morphism.

• I.e., it arises when a composition chain is interrupted by an extra product argument.
• Express (f) as a C-indexed family, (f_c : A → B), of morphisms such that applying a function at any index behaves like (f); i.e., (f_c , a = f(c, a)). Each (f_c) can now be composed with (g). Let (\transpose{(;)}) denote the operation (f ↦ f_c).

\vspace{-0.5em}

\vspace{1em}

<a id="org42710d1"></a>

Functors

A functor F : 𝒜 → ℬ is a pair of mappings, denoted by one name, from the objects, and morphisms, of 𝒜 to those of ℬ such that it respects the categorical structure:

\vspace{1em}

The two axioms are equivalent to the single statement that functors distribute over finite compositions, with (\Id) being the empty composition: [ F(f_0 ∘ \cdots ∘ f_{n-1}) ;=; F, f_0 ∘ \cdots ∘ F, f_{n-1} ]

Use of Functors.

• In the definition of a category, “objects” are “just things” for which no internal structure is observable by categorical means —composition, identities, morphisms, typing. Functors form the tool to deal with “structured” objects.

  Indeed in 𝒮ℯ𝓉 the aspect of a structure is that it has “constituents”, and that it is possible to apply a function to all the individual constituents; this is done by F f : F A → F B.

• For example, let (\bin A = A × A) and (\bin f = (x, y) ↦ (f, x, f, y)). So (\bin) is or represents the structure of pairs; (\bin, A) is the set of pairs of A, and (\bin, f) is the function that applies f to each constituent of a pair.

  • A binary operation on A is then just a function (\bin A → A); in the same sense we obtain F-ary operations.

• Also, Seq is or represents the structure of sequences; Seq A is the structure of sequences over A, and Seq f is the function that applies f to each constituent of a sequence.

• Even though F A is still just an object, a thing with no observable internal structure, the functor properties enable to exploit the “structure” of F A by allowing us to “apply” an f to each “constituent” by using F f.

\vspace{1em}

Category (𝒜lℊ(F))

• For a functor F : 𝒜 → 𝒟, this category has F-algebras, F-ary operations in 𝒟 as, objects — i.e., objects are 𝒟-arrows (F, A → A) — and F-homomorphisms as morphisms, and it inherits composition and identities from 𝒟.

  Note that category axiom \eqref{unique-Type} is not fulfilled since a function can be a homomorphism between several distinct operations. However, we pretend it is a category in the way discussed earlier, and so the carrier of an algebra is fully determined by the operation itself, so that the operation itself can be considered the algebra.

  <div class="org-center"> *\ref{comp-Homomorhism} renders a semantic property as a syntactic condition!* </div>

\vspace{1em}

• A contravariant functor 𝒞 → 𝒟 is just a functor 𝒞ᵒᵖ → 𝒟.
• A bifunctor from 𝒞 to 𝒟 is just a functor 𝒞² → 𝒟.

<a id="orgd826582"></a>

Naturality

A natural transformation is nothing but a structure preserving map between functors. “Structure preservation” makes sense, here, since we've seen already that a functor is, or represents, a structure that objects might have.

\room

As discussed