%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Compilation of Facts about Category theory
%% 
%% I call them "mantras" for you have to repeat them a few times to let
%% them sink in. They are organized in 'circles' of somewhat increasing
%% difficulty. First card in each circle is the highest one.
%% 
%% They are taken from several references:
%% 
%% JS:  Personal Script from Jaap van Oostens lecture (Summer School in
%%      Semantics at BRICS, Århus, Denmark in May 1999 
%% VJO: Jaap van Oosten: Category Theory in Computer Science, BRICS lecture
%%      series BRICS-LS-95-1 (Issue May 1999)
%% CML: Colin McLarty: Elementary Categories, elementary toposes
%%	Oxford 1991
%% FB:  Francis Borceux: Encyclopedia of mathematics and its application,
%%	Categories (Mathematics), Cambridge UP, 1994
%% BP:  Benjamin Pierce: Basic Category Theory for the Computer Scientist,
%%	MIT Press. 1991
%% AHS: J. Ad{\'a}mek and H. Herrlich and G. E. Strecker: Abstract and
%%      Concrete Categories - the joy of cats; John Wiley and Sons, NY 1990
%% BW:  Michael Barr and Charles Wells: Category Theory for Computing Science,
%%	Prentice Hall, New York, 1990 
%% SML: Saunders Mac Lane: Categories for Working Mathematicians,
%%      Springer-Verlag, New York, 1971 
%%
%% Oliver Möller 
%%
%% begun:     10/05/1999
%% continued: 11/06/1999

%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Reorganized into more coherent circles
%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% ----------------------------------------
%% First Circle: Basics... epic, mono, iso
%% ----------------------------------------

BP22: A coequalizer provides the categorical analogue to the set-theoretic notion of equivalence classes.

JVO4: If ${\cal C}(X,Y)$ is always a set, $\cal C$ is locally small.

CML30: Equalizers - if existent - are determined up to isomorphism.

%% ---

CML50: Limits are equalizers of products.

BP22: An epic equalizer is an isomorphism.

BP17: Terminal objects are unique up to isomorphism.

%% ---

BP16: If $f$ is an isomorphism, then the inverse $f^{-1}$ is unique.

CML31: Every equalizer is monic.

JS1: Category theory is a method to organize mathematics.


%%% ======================================================================

%% ----------------------------------------
%% Second Circle: Limits and objects
%% ----------------------------------------

JS6b: In $Set^{{\cal C}^{op}}$ limits are computed pointwise.

JVO19: If a category has a terminal object and pullbacks, it has binary products and equalizers.

CML43: A category with all products and equalizers also has all pullbacks.

%% ---

BP16: There is a category containing an arrow that is epic and monic but not iso.

CML105: For $A$ object of $\cal C$, $h:f\rightarrow g$ of ${\cal C}/A$ is monic iff h is monic in $\cal C$.

CML23: If a category has a terminal object $\mathbf 1$, every object is its own product with $\mathbf 1$.

%% ---

BP27: The cones for a diagram form a category; the limit is the terminal object of this.

CML31: Coequalizers cannot be defined in terms of general elements.

CML17: An arrow is fully determined by its effects on generalized elements.


%%% ======================================================================

%% ----------------------------------------
%% Third Circle: Functors and natural transformations
%% ----------------------------------------


AHS26: If $G\circ F$ is an embedding, then so is $F$.

JVO7: A full and faithful functor reflects the property of being a terminal or initial object.

JVO13: A category is equivalent to a discrete category iff it is a groupoid and a preorder.

%% ---

JVO7: A faithful functor reflects epis and monos.

BW70: Every functor preserves isomorphism.

AHS78: Objects that represent the same functor are isomporphic.

%% ---

JVO8: A natural transformation between two functors $F,G:\cal C\rightarrow \cal D$ is a family $(\mu_C:FC\Rightarrow GC)_{C\in{\cal C}_0}$.

JVO9: An embedding is a functor which is full and faithful and injective on objects.

BP36: ``It should be observed that the whole concept of a category is essentially an auxillary one.''\\[1.2ex] \hspace*{1.9ex}\footnotesize \it (Eilenberg \& Mac Lane)\\ 

%%% ======================================================================

%% ----------------------------------------
%%  Fourth Circle: Around the Yoneda Lemma
%% ----------------------------------------

JVO9: (Yoneda Lemma) For $F$ of $Set^{{\cal C}^{op}}$, $C$ of $\cal C$ there is a bijection $f_{C,F}:$ $Set^{{\cal C}^{op}}(h_c,F)$ $\rightarrow F(C)$.

CML172: Natural numbers object:\\[2mm] $\begin{array}{ccccc} \mathbf1&\rightarrow&N&\rightarrow&N\\ &\searrow&\downarrow&&\downarrow\\ &&A&\rightarrow&A \end{array}$\\ 

BP35: There is a category with a terminal object and all products, but without exponentiation.

%% ---

AHS39: A subcategory $\cal C$ of $\cal D$ is full, if for all $A,B$: ${\cal C}(A,B)$ $\:=\:$ ${\cal D}(A,B)$.

AHS217: For each functor $T:$ ${\cal C}\rightarrow {\cal C}$, the forgetful functor of $\mathbf A \mathbf l \mathbf g$ $(T)$ creates limits.

JVO10: The functor $Y:{\cal C}\rightarrow \mbox{Set}^{{\cal C}^{op}}$ is full and faithful.

%% ---

BW108: The Yoneda Lemma is a generalization of Cayley's Theorem.

JVO4: For a category $\cal C$ and an object $C$, ${\cal C}/C$ is the slice category. Objects are arrows to $C$.

JS7b: ``A universal property is itself a reason to study it.''\\[1.2ex] \hspace*{6ex}\footnotesize \it (Jaap van Oosten)


%%% ======================================================================

%% ----------------------------------------
%%  Fifth Circle: Adjoints
%% ----------------------------------------

BW260: The right adjoint to the binary product functor describes the exponential. 

AHS300: If $G:\,{\cal C}\rightarrow{\cal C}$, ${\cal C}$ a poset and $G\adjoint G$, then $G$ is an isomorphism.

CML96: In a category with finite products, \mbox{--$\times A$} has a left adjoint iff $A$ is a terminal object.

%% ---

SML101: Let $F:\,{\cal C}\rightarrow{\cal D}$, $F\adjoint G$ and ${\overline F}:\,{\cal D}\rightarrow{\cal E}$, ${\overline F}\adjoint{\overline G}$. Then ${\overline F}F\adjoint G{\overline G}$.


SML93: Galois connections are adjoint pairs.

BW259: For every adjunction there exists a counit $\epsilon$.

%% ---

SML83: Any two left-adjoints of a functor are naturally isomorphic.

BP48: {A simple example for adjoints is\\[3mm] \hspace*{-0.5em}\small $\begin{array}{rll} S&\stackrel{i}{\longrightarrow}&U({\sl List}(S),\star,[\,]) \\[2mm] &\mbox{\tiny 1}\searrow&\downarrow\,U({\sl length}) \\[2mm] & &U(I\!\!N,+,0) \end{array}$\\ }

SML,V: The slogan is: ``Adjoint functors arise everywhere.''\\[1.2ex] \hspace*{1.5em}\footnotesize \it (Saunders Mac Lane)


%%% ======================================================================

%% ----------------------------------------
%%  Sixth Circle: CCC and Toposes
%% ----------------------------------------

CML121: In a topos, take $x:\mathbf1\rightarrow A$, $w:A\rightarrow\Omega$. Then $x\in^A$`$w$' iff $x\in w^*$.

JS5b: Theories in the simply typed $\lambda$-calculus correspond to cartesian closed categories.

JS8b: In a topos $\cal E$, one can interpret many-sorted predicate logic which also has constructors for subsets.

%% ---

CML123: For toposes $\cal E$, $\cal E'$ also $\cal E\times\cal E'$ is a topos.

CML114: In a topos, all monics are equalizers and all monic epics are iso.

JS5: Every monotone map of $X$ to a $\omega$-cpo factors uniquely through the limits of this cpo.

%% ---

JS5b: In cartesian closed categories, coproducts distribute over products.

BP43: The category {\bf Cat} is cartesian closed with $\cal A^B$ the functor category.

BP34: A cartesian closed category is a category with a terminal object, binary products and exponentiation.


%%% ======================================================================

%% ----------------------------------------
%%  Seventh Circle: The far side
%% ----------------------------------------

SML239: IF $G:\,$ ${\cal C}\rightarrow{\cal D}$ has a left adjoint $F$, $F$ preserves all right Kahn extensions which exist in $\cal C$.

BW273: Let $F:\,{\cal C}\rightarrow{\cal C}$ be a functor. If $(A,f)$ is initial in the category $(F:\,\cal C)$, then $f$ is an isomorphism.

SML162: For every monoidal $\cal C$, $A\in \cal C$ there is a unique morphism $\cal D\rightarrow \cal C$ of monoidal categories with (--)$\mapsto A$.

%% ---

AHS187: Each colimit is an extremal epi-sink.

AHS26: If $F:\cal C\rightarrow \cal D$ a full, faithful functor, $\forall$ $f:FA\rightarrow FB$ $\exists_1$ $g:A\rightarrow B$ with $Fg\:=\:f$.

FB97: If $F: \cal A \rightarrow \cal B$, $B$ in $\cal B$ and a reflection along $B$ exists, it is unique up to isomorphism.

%% ---

JS7: Each presheaf is a colimit of a representable presheaf.

CML19: If there is an inital object $\mathbf 0$ and an arrow $\mathbf1\rightarrow\mathbf0$ then $\mathbf0$ and $\mathbf1$ are zero objects.

CML39: Equivalent sub-objects have isomorphic domains.

%%% ======================================================================
%%% ======================================================================