Voir la source de Langage et concepts catégoriques pour les mathématiques et l’informatique

This is a wiki for a course at the MSTII "École doctorale" of Grenoble.

Students are encouraged to participate by extending the wiki, adding proofs, corrections for exercices etc. To be able to modify the wiki, you need to register (upper right corner). Please use your real name...


===News===

Courses are on wednesdays morning, 9'00 to 12'00 in room F218 at the "UFR IMAG".

* first course on the 25th of February: categories, functors, natural transformations.
* March 4. : monads, adjunctions.
* March 11. : limits and colimits.

==Basic Concepts==

===Categories===

{{Definition |
A concrete category is given by:
* a collection of sets ''with structure'',
* for any pair of such sets, a set of ''morphisms'' preserving the structure.
Morphisms should compose, and the identity should be a morphism.}}

This definition is a little informal, but here are some examples:
* '''Grp''': groups and group morphisms
* '''Top''': topological spaces and continuous functions
* '''Ring''': rings and rings morphisms
* '''Vect''': vectors spaces and linear maps
* '''CPO''': CPOs and continuous functions
* ...
* '''Set''': sets and functions ('''ie''' sets with no structures, and arbitrary functions)

Generalizing the definition, we obtain the official definition of category:

{{Definition |
A category <math>\mathcal{C}</math> is given by:
* a collection <math>\mathcal{C}_o</math> of ''objects'',  (notation: <math>A,B,C,X,Y,...</math>)
* for each pair <math>A,B</math> of objects, a collection <math>\mathcal{C}[A,B]</math> of ''morphisms from <math>A</math> to <math>B</math>'',  (notation <math> f : A\to B</math>)
* for any object <math>A</math>, a special morphism <math>i_A : A\to A</math>
* for all objects <math>A,B,C</math>, a composition <math>\circ : \mathcal{C}[B,C] \times \mathcal{C}[A,B] \to \mathcal{C}[A,C]</math>,
such that:
* <math>f \in \mathcal{C}[A,B] \implies f\circ i_A = i_B\circ f = f</math>
* <math>f\circ(g\circ h) = (f\circ g)\circ h</math> whenever it makes sense.
}}

All concrete categories are categories, and here are some examples that are not obviously concrete:
* '''Graph''': graphs and graph morphisms
* '''Rel''': sets and relations
* '''Set×Set''': pairs of sets, pairs of functions
* '''Set<math>^{op}</math>''': opposite of '''Set'''
* '''P''', whenever ('''P''',<) is a preorder (at most one morphism between objects)
* '''M''', whenever ('''M''',e,×) is a monoid (a single object)

We sometimes write <math>gf</math> instead of <math>g \circ f</math>.

In a given category <math>\mathcal{C}</math>, there are analogues of the notions of injective and surjective functions in '''Set'''. We will see that on concrete categories, they are actually slightly more general. The idea of injectivity gives rise to ''monomorphisms'', and surjectivity gives rise to ''epimorphisms''.

{{Definition |

A morphism <math>f \colon A \to B</math> is a ''monomorphism'' iff for all object <math>C</math> and morphisms <math>g,h \colon C \to A</math>, we have <math>fg = fh</math> implies <math>g = h</math>.

The morphism <math>f</math> is an ''epimorphism'' when it is a monomorphism in <math>\mathcal{C}^{op}</math>. Explicitly, when for all object <math>C</math> and morphisms <math>g,h \colon B \to C</math>, we have <math>gf = hf</math> implies <math>g = h</math>.

  isomorphism
}}


<u>Exercice</u>
# Prove that in '''Set''', epic is equivalent to surjective and monic is equivalent to injective.
# Prove the same thing in '''Ab''', the category of commutative groups. (One thing is not obvious.)
# Prove the same thing in '''Grp''', the category of (non necessarily commutative) groups. (One thing is not obvious at all.)
# Prove that <math>i : \mathbf{Z} \to \mathbf{Q}</math> is an epimorphism in the category of rings with multiplicative neutral. (Note that it is not surjective.)
# In '''Set''', we saw that ''f'' is a monic iff <math>\forall x,y : 1 \to A, f\circ x = f\circ y \implies x=y</math>, where 1 is any singleton set. Can you find a set ''C'' such that ''f'' is epic iff <math>\forall p,q : B \to C, p\circ f = j\circ f \implies p=q</math>?
# In '''Group''', can you find an object playing a role similar to 1, ''ie'' a group ''G'' s.t. ''f'' is monic iff <math>\forall x,y : G \to A, f\circ x = f\circ y \implies x=y</math>. (We saw that we cannot use the singleton group ({e},e,×) to do that...)

===Functors===

Informally, a functor is a map between two categories which somehow preserves the structure of categories (namely, composition).

{{Definition |
A functor <math>F</math> from a category <math>\mathcal{C}</math> to a category <math>\mathcal{D}</math>, noted <math>F \colon \mathcal{C} \to \mathcal{D}</math>, is given by:
* a map which sends every object <math>A</math> of <math>\mathcal{C}</math> to an object <math>FA</math> in <math>\mathcal{D}</math>, and
* a map which sends every morphism <math>f \colon A \to B</math> in <math>\mathcal{C}</math>, to a morphism <math>Ff</math> in <math>\mathcal{D}[FA, FB]</math>,
such that:
* <math>F</math> preserves identities, i.e., <math>F(id_A) = id_{FA}</math>, and
* <math>F</math> preserves composition: <math>F(f \circ g) = F(f) \circ F(g)</math>.
}}

<u>Exercice</u>
# Take a functor <math>F \colon \mathcal{C} \to \mathcal{D}</math>, <math>f, g, h</math> three morphisms in <math>\mathcal{C}</math>, and <math>f' = Ff</math>, <math>g' = Fg</math>, <math>h' = Fh</math>. When <math>h' = f' \circ g'</math>, can we say something interesting about <math>f</math>, <math>g</math> and <math>h</math>?
# Do functors preserve monomorphisms? Do functors preserve epimorphisms?
# Let ''F'' be a functor and ''F(f) = g'', if ''g'' is a mono (resp. epi), is ''f'' a mono (resp. epi)?
If not, try to find some simple and natural condition on the functor to make that true.

<u>Answer</u>
# No, since <math>f</math> and <math>g</math> may not even compose! This is the case when <math>f</math> has type <math>A \to B</math>, and <math>g \colon C \to D</math>, with <math>F</math> collapsing <math>D</math> and <math>A</math> (i.e., <math>FA = FD</math>).
# Functors in general do not preserve mono- nor epimorphisms. We build a counter-example for monomorphisms. Let <math>\mathbf{2}</math> be the category with two objects <math>\star</math> and <math>\bullet</math>, and exactly one morphism <math>m \colon \star \to \bullet</math>. This is a preorder, so <math>m</math> is monic. Now take <math>\mathcal{C}</math> with two objects <math>\star</math> and <math>\bullet</math>, exactly one morphism <math>m \colon \star \to \bullet</math>, and one extra morphism <math>n \colon \star \to \star</math>, different from the identity. Because of <math>n \neq id_\star</math>, yet <math>m \circ n = m \circ id</math>, <math>m</math> is not monic in <math>\mathcal{C}</math>. The functor which sends <math>\star</math> to <math>\star</math>, <math>\bullet</math> to <math>\bullet</math> and <math>m</math> in <math>\mathbf{2}</math> to <math>m</math> in <math>\mathcal{C}</math>, does not preserve monomorphisms.
# In general, the answer is (again) no. For monos, take for example the functor <math>\mathcal{C} \to \mathbf{2}</math> which sends <math>n</math> to the identity. Yet, when <math>F</math> is ''faithful'', then <math>f</math> is monic (or epic).

{{Definition |
A functor <math>F</math> is faithful when, for any two morphisms <math>f, g</math>, <math>Ff = Fg</math> implies <math>f=g</math> (<math>F</math> is injective on morphisms).
}}
{{Definition |
A functor <math>F</math> is full when, for any two objects <math>A, B</math>, if <math>g</math> is a morphism <math>FA \to FB</math>, then there exists <math>f \colon A \to B</math> with <math>Ff = g</math> (<math>F</math> is surjective on morphisms).
}}

<u>Exercice</u>

Find an "interesting" functor from '''Set''' to '''Group'''.

<u>Answer</u>
Let <math>F</math> be the functor which sends:
* every set <math>X</math> to the free group generated by <math>X</math>, and
* every function <math>f \colon X \to Y</math> to a group morphism defined by: <math>Ff(x_1^{\alpha_1}\times\dots\times x_k^{\alpha_k})=f(x_1)^{\alpha_1} \times \dots \times f(x_k)^{\alpha_k}</math>.


<u>Exercice</u>

If <math>\mathcal{C}</math> is a locally small category and ''A'' one of its objects, let <math>Y_A : X \mapsto \mathcal{C}[X,A]</math>. Show that this operation from objects of <math>\mathcal{C}</math> to sets can be extended into a contravariant functor <math>\mathcal{C}</math> to '''Set'''.

<u>Answer</u>
Let <math>f\colon X \to Y</math> be a morphism in <math>\mathcal{C}</math>, then <math>Y_A(f)</math> is expected to be a function from the set <math>\mathcal{C}[Y, A]</math> to the set <math>\mathcal{C}[X, A]</math>. We can take, for any morphism <math>m \in \mathcal{C}[Y,A]</math>: <math>Y_A(f)(m) = m \circ f</math>.

This extends <math>Y_A</math> to a contravariant functor, since <math>Y_A(id_X) = id_{\mathcal{C}[X, A]}</math> and <math>Y_A(f \circ g)(m) = m \circ (f \circ g) = (m \circ f) \circ g = (Y_A(g) \circ Y_A(f))(m)</math>.

===Natural Transformations===

{{Definition |
Let <math>F</math> and <math>G</math> be two functors <math>\mathcal{C} \to \mathcal{D}</math>. A natural transformation <math>\alpha</math> from <math>F</math> to <math>G</math> is given by:
* a morphism <math>\alpha_A \colon FA \to GA</math> in <math>\mathcal{D}</math> for every object <math>A</math> in <math>\mathcal{C}</math>,
* such that, for any morphism <math>f \colon A \to B</math>, we have <math>Gf \circ \alpha_A = \alpha_B \circ Ff</math>.
}}

<u>Exercice</u>

If <math>P(X)</math> is the set of permutation of a (finite) set ''X''; and <math>L(X)</math> the set of its linear orderings, we have <math>\#(L(X)) = \#(L(X)) = n!</math> where <math>n = \#(X)</math>. Thus, there is a bijection (iso in '''Set''') between ''P(X)'' and ''L(X)''.
# Show that we can extend ''P'' and ''L'' to functors from '''B''' to '''Set''', where '''B''' is the category of finite sets and bijections,
# Show that there can be no natural transformation from ''P'' to ''L'',
# Conclude that there is no natural isomorphism between ''P'' and ''L''.


==Adjunctions and Monads==

===2-categories and their diagrammatic calculus===

This part is just to make the definitions of monads and adjunctions
easier: we do not give the full details, and only intend to provide a
few intuitions.

{{Definition | A ''2-category'' is like a category: it has objects and
morphisms between them. But it also has ''2-cells'', which are
'morphisms between morphisms': 
[[Image:2-cat-1.png|center|A 2-cell]] 
These
2-cells must compose vertically and horizontally, satisfying the
''interchange law'':
[[Image:2-cat-inter.png|center|Interchange law]]
}}

There is a more comfortable representation than the '2-diagrams' above.
In pictures:
[[Image:Poincare.png|center|String diagram example]]
In words, the idea is to consider:
* objects as background colors, 
* morphisms as vertical frontiers between them, and
* 2-cells as labelled dots.

Then, both compositions correspond to horizontal and vertical
juxtaposition, respectively.  For example, the interchange law
corresponds to the two ways of parsing:
[[Image:interchange.png|center|Interchange law in a string diagram]]

There are technical subtleties hidden behind this nice diagrammatic
calculus, but we will stick to bare intuitions for now.

===Cat as a 2-category===

The prime example of a 2-category is of course Cat, the category of (small) categories. It has:
* objects: small categories,
* morphisms: functors,
* 2-cells: natural transformations.

Vertical composition of 2-cells is the obvious notion of composition
of natural transformations.

Define the horizontal composition:
[[Image:vert-comp.png|center|Vertical composition]] 
by <center><math>
(\beta \bullet \alpha)_a = f' (f (a)) \xrightarrow{f' (\alpha_a)} f' (g (a)) 
\xrightarrow{\beta_{g (a)}} g' (g (a)) </math></center>
or equivalently
 <center><math>
(\beta \bullet \alpha)_a = f' (f (a)) \xrightarrow{\beta_{f (a)}} g' (f (a)) 
\xrightarrow{g' (\alpha_a)} g' (g (a)).</math></center>
The two coincide by naturality. Observe that what we have actually done is:
* define ''whiskering'', i.e., composing with an identity, both to the left and to the right, and 
* observe that the two ways of defining horizontal composition from whiskering coincide.
This yields an equivalent definition of 2-categories.


==Monads==

*''Free'' constructions in algebra: monoid, group, etc

*Definition of a monad
*Eilenberg-Moore's category of algebras
*Kleisli's category of free algebras
*The category of resolutions of a monad
===Adjunctions===

*Definition with <math>\eta</math>
*Definition with hom-sets
*Definition with <math>\eta</math> and <math>\epsilon</math>
*Adjunctions in a 2-category

===Other basic examples===

*Discussion: any syntax defines the free something
* The issue of variable binding.
*Adjunction between partial orders = Galois connection
*<math>\times</math> and <math>\Rightarrow</math> in logic
*Sets/graphs and categories

===Properties===

*Composition
*Preservation of limits/colimits
*Freyd's existence theorem, the locally presentable case
*Beck's monadicity theorem
==Limits and Colimits==

===Limits===

'''Example.''' Cartesian product.

{{ Definition | Binary product.}}

'''Theorem.''' ''The product of X and Y, if it exists, is unique up to isomorphism.'' (with proof)

'''Examples.''' Set, Grp, Ab, Part.

'''Examples.''' Preorder, Subset(E), Prop with entailment.

{{ Definition | Diagram. Cone. Limit.}}

'''Example.''' Limits in Set.

'''Examples.''' Shape of diagrams for products, pullbacks, equalizers.

'''Example.''' Monos as pullbacks.

'''Theorem.''' ''The limit of a diagram d, if it exists, is unique up to isomorphism.''

'''Theorem.''' ''A category with "all" products and equalizers has "all" limits.''

'''Theorem.''' ''A category with a terminal object and all binary products and all equalizers has all finite limits.''

===Colimits===

{{ Definition | Cocone. Colimit.}}

'''Examples.''' Sums in Set, Grp, Ab.

'''Examples.''' Shape of diagrams for sums, initial objects, pushouts, coequalizers.

'''Example.''' Epis as pushouts.

'''Theorem.''' ''The colimit of a diagram d, if it exists, is unique up to isomorphism.''

'''Example.''' The most general unifier (of two terms) is a coequalizer in the "category of substitutions".
 
'''Theorem.''' ''A category with "all" sums and coequalizers has "all" colimits.''

'''Theorem.''' ''A category with an initial object and all binary sums and all coequalizers has all finite colimits.''

===Limits, colimits and adjunctions===

'''Theorem.''' ''A right adjoint preserves limits. A left adjoint preserves colimits.'' (with proof of existence)

'''Example.''' The adjunction between Set and Grp

===Sums and products===

A category is ''distributive'' if the canonical map from AxB+AxC to Ax(B+C) is an isomorphism.

A category is ''extensive'' if the canonical functor + from C/A x C/B to C/(A+B) is an equivalence. 

'''Example.''' "if..then..else.." from B=1+1 and extensivity.
 
==Monoidal categories==

===Definition and graphical calculus===

* Definition
* Graphical calculus
* The 2-category of monoidal categories, strong monoidal functors, and monoidal transformations
* Coherence and its many definitions

===From planar to symmetric monoidal categories===

A teaser for the whole enchilada of variations on monoidal structure.

* Braided 
* Balanced
* Symmetric
* Compact closed
* Traced monoidal categories and the Int/GoI construction

===Monoidal categories for linear logic===

* Linear logic 
** Sequent calculus
** Intuitionnistic variant
** Proof nets

* Symmetric monoidal closed categories

* Star-autonomous categories
** Symmetric monoidal closed category with a dualising object
** Symmetric monoidal category <math>\mathcal{C}</math> with:
*** a full and faithful contravariant endofunctor <math>\mathcal{C}^{op} \xrightarrow{(-)^*} \mathcal{C} </math>, and
*** an isomorphism <center><math>\mathcal{C} (A \otimes B, C^*) \cong \mathcal{C} (A, (B \otimes C)^*).</math></center>

* Trimble-Hughes' free star-autonomous category
** Split star-autonomy
** The free star-autonomous category as a category of proof nets
** Trimble rewiring

===Perspectives===

* Premonoidal categories and side effects
* Products and coproducts
* Monoidal 2-categories, monoidal double categories.

==Presheaves and sheaves==

===Yoneda===

*A few presheaf categories <math>\hat{\mathcal{C}} := \mathcal{C}^{op} \to \mathbf{Set}</math>:
**<math>\mathcal{C}</math> is a graph (no composition): graphs.
**<math>\mathcal{C}</math> is a preorder: Kripke-style modal logic.
**<math>\mathcal{C}</math> is an order: presheaves on a topological space.
**<math>\mathcal{C}</math> is free: presheaves on an algebraic theory.

*Representable presheaves <math>yA(B) := \mathcal{C}(B, A)</math>, and their meaning in each of the examples.

*The Yoneda lemma: for any object <math>A</math> of <math>\mathcal{C}</math>, and presheaf <math>F</math>, there is an isomorphism
<center><math>F (A) \cong \hat{\mathcal{C}} (yA, F),</math></center>
natural in <math>A</math> and <math>F</math>.

*A consequence: <math>y</math> is a 'full embedding', or how <math>\mathcal{C}</math> is a full subcategory of <math>\hat{\mathcal{C}}</math>.

*Presheaves as a colimit completion
**The Grothendieck construction, or the category of elements of a presehaf.
**Example: graphs.
**Every presheaf is a colimit of representables.
**Example: graphs.
**The universal property of <math>y</math>.

===Topos structure===

*Limits and colimits in functor categories.
*Exponentials. If it exists, the exponential <math>G^F</math> must satisfy, for any object <math>A</math> of <math>\mathcal{C}</math>:<center><math>\begin{array}{lcl}
G^F(A) & \cong & \hat{\mathcal{C}} (yA, G^F) \\
& \cong & \hat{\mathcal{C}} (yA \times F, G).
\end{array}
</math>
</center>
Taking this as a definition indeed yields an exponential.
*Computation of the exponential in '''Gph'''.
*The very special presheaf <math>\Omega</math>.
*The isomorphism <center><math>\mathit{Sub}(F) \cong \hat{\mathcal{C}} (F, \Omega). </math>
</center>
*The official definition of a subobject classifier and a topos.

===Sheaves===

*Sheaves on a space, a few examples and counterexamples:
**functions, 
**continuous functions,
**bounded functions.
*The <math>(\cdot)^+</math> construction and its convergence in two steps. The counterexample of constant presheaves.
*Sheaves on a site. Example of sheaves for the dense topology on an algebraic theory and its coincidence with the double negation topology.

==Sketches (esquisses)==

===Linear sketches===

<span style="font-style: italic;">"A linear sketch is a generator for
a category"</span>

<span style="font-weight: bold;">Examples.</span> 
Linear sketch for graphs, for sets, for a split
mono-epi.

<span style="font-weight: bold;">Definition.</span> A linear sketch is
a graph with some potential idenitites and composed arrows

<span style="font-weight: bold;">Definition.</span> The category of
models of a linear sketch S in a category C, Mod(S,C), or Mod(S) when C
is Set.

<span style="font-weight: bold;">Note.</span> The set-valued models of
S are the presheaves over F(S)^op

<span style="font-weight: bold;">Theorem.</span> A linear sketch has a
terminal model, made of singletons, and an initial model, made of empty
sets.

<span style="font-weight: bold;">Definition.</span> The category of
linear sketches LinearSk and the underlying functor U:Cat-&gt;LinearSk

<span style="font-weight: bold;">Theorem.</span> There is a left
adjoint to U, F:LinearSk-&gt;Cat. F(S) is the category generated by S

<span style="font-weight: bold;">Example.</span> "Implementation of
Bool by Nat" : fractions of morphisms of linear sketches

<span style="font-weight: bold;">Definition.</span> The Yoneda
contravariant model of S with values in Mod(S)

===Limit sketches===

<span style="font-style: italic;">"A limit sketch is a generator for a
category with limits"</span>

<span style="font-weight: bold;">Examples. </span>Limit sketch
for monoids, "for naturals".

<span style="font-weight: bold;">Definition.</span> A limit sketch is a
linear sketch with some potential limits

<span style="font-weight: bold;">Definition.</span> The category of
models of a limit sketch S in a category C, Mod(S,C), or Mod(S) when C
is Set.

<span style="font-weight: bold;">Theorem.</span> A limit sketch has a
terminal model, made of singletons, and an initial model, made of the
closed terms.

<span style="font-weight: bold;">Definition.</span> The category of
limit sketches LimSk and the underlying functor U:LimCat-&gt;LimSk

<span style="font-weight: bold;">Theorem. </span>There is a left
adjoint to U, F:LimSk-&gt;LimCat. F(S) is the category with chosen
limits generated by S

<span style="font-weight: bold;">Theorem.</span> There is still a
Yoneda contravariant model of S with values in Mod(S)

===Sketches===

<span style="font-weight: bold;"></span><span
style="font-style: italic;">"A sketch is a generator for a category
with limits and colimits"</span>

<span style="font-weight: bold;">Example.</span> Sketch for
fields.

<span style="font-weight: bold;">Definition.</span> A sketch is a limit
sketch with some potential colimits

<span style="font-weight: bold;">Definition.</span> The category of
models of a sketch S in a category C, Mod(S,C), or Mod(S) when C is
Set.

<span style="font-weight: bold;">Note.</span> A sketch has no terminal
model and no initial model, in general.

<span style="font-weight: bold;">Theorem.</span> [Guitart-Lair] A
sketch with only discrete potential colimits has an initial family of
models.

<span style="font-weight: bold;">Definition.</span> The category of
sketches LimSk and the underlying functor U:LimColimCat-&gt;Sk

<span style="font-weight: bold;">Theorem.</span> There is a left
adjoint to U, F:Sk-&gt;LimColimCat. F(S) is the category with chosen
limits and colimits generated by S

<span style="font-weight: bold;">Remark. </span>The proof of this
theorem (and the previous similar ones) can be done by first
constructing a limit sketch E1 for Sk, a limit sketch E2 for
LimColimCat, and a morphism of limit sketches P:E1-&gt;E2, and then
applying Ehresmann's theorem below, which is a fundadmental <span
style="font-weight: bold;">theorem about limit sketches</span>. 

<span style="font-weight: bold;">Theorem.</span> [Ehresmann]. For each
morphism of limit sketches P:E1-&gt;E2 there is an adjunction (F,U)
where U:Mod(E2)-&gt;Mod(E1) is the composition by P.

<span style="font-weight: bold;">Note.</span> There is no Yoneda
contravariant model of S with values in Mod(S)

===Sketches and logic===

<span style="font-style: italic;">"A sketch is an alternative to a
logical theory"</span>

From the point of view of (set-valued) models: 

finite products sketches &lt;-&gt; equational logic 

finite limits sketches &lt;-&gt; a logic strictly more expressive than
the logic of universal Horn theories

sketches&nbsp; &lt;-&gt;&nbsp; first order logic 

Generalization of sketches to higher order logic?

==Course Complements, references==

One of the best books about category theory is
* Saunder MacLane, ''"Categories for the Working Mathematician"''.
It is a little "dry", in the sense that learning categories from it is not the easiest task on earth, but it still is one of the best references.

I haven't really read it carefully, but here is [http://en.wikipedia.org/wiki/Category_theory what Wikipedia has to say on category theory].