Epilogue: Theorems in Category Theory
FC03 — Riehl, Category Theory in Context.
This chapter contains 7 definitions, 4 theorems, 2 constructions and 1 other statements.
Nobody has checked this chapter against Lean yet, so the statements below say nothing about whether they are formalized.
Definition: A symmetric monoidal category has a bifunctor ⊗, unit object, and natural…
A symmetric monoidal category has a bifunctor ⊗, unit object, and natural symmetry, associativity, and unit isomorphisms satisfying coherence; a monoidal category omits symmetry.
Named comparison
Finite-product and finite-coproduct categories are symmetric monoidal; Mod_R has ⊕ and, for commutative R, ⊗_R; chain complexes have the graded tensor product.
Theorem E.2.2
Mac Lane–Kelly coherence: every formal diagram in a symmetric monoidal category built from associators, unitors, and symmetries commutes.
Construction: The unit interval I=[0,1] defines paths
The unit interval I=[0,1] defines paths; composable paths p,q compose through the homeomorphism δ:I≅I∨I followed by p∨q.
Definition: A bipointed space is a space with two distinct closed designated endpoints
A bipointed space is a space with two distinct closed designated endpoints; morphisms preserve the two endpoints, and X∨X is formed by gluing the right point of one copy to the left point of the other.
Theorem E.3.1
Freyd–Leinster: the unit interval (I,0,1) is the terminal bipointed space equipped with a bipointed map X→X∨X; equivalently it is the terminal coalgebra for X↦X∨X.
Definition: A Grothendieck topos is a reflective full subcategory of a presheaf category…
A Grothendieck topos is a reflective full subcategory of a presheaf category whose reflector preserves finite limits; equivalently it is a category of sheaves on a small site.
Theorem E.4.1
Giraud: E is a Grothendieck topos iff it is locally small; has finite limits; has all small coproducts, disjoint and universal; equivalence relations have universal coequalizers; every equivalence relation is effective and every epi a coequalizer; and E has a separating set.
Definitions/comparisons
A coproduct is disjoint when its injections are monic with pairwise-initial pullbacks; a colimit is universal when stable under pullback; an effective equivalence relation is a kernel pair.
Definition E.5.1
A category is abelian if it has a zero object 0, that is both initial and terminal, it has all binary products and binary coproducts, it has all kernels and cokernels, defined respectively to be the equalizer and coequalizer of a map \(f \colon A \to B\) with the zero map \(A 0 B ,\) and all monomorphisms and epimorphisms arise as kernels or cokernels, respectively.
Construction/terminology
In an abelian category finite products and coproducts coincide as biproducts/direct sums; hom-sets are canonically abelian groups and composition is bilinear.
Definition: The image of f is ker(coker f), equivalently coker(ker f)
The image of f is ker(coker f), equivalently coker(ker f); a composable sequence is exact when ker f_n = im f_{n+1}.
Definition: A functor between abelian categories is exact when it preserves exact…
A functor between abelian categories is exact when it preserves exact sequences, equivalently when it is both left and right exact.
Theorem E.5.2
Freyd–Mitchell: every small abelian category A admits an exact fully faithful functor A↪Mod_R for some ring R, embedding A as a full subcategory.