Langage et concepts catégoriques pour les mathématiques et l’informatique

De Wiki du LAMA (UMR 5127)
Aller à la navigation Aller à la recherche

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 | 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 is given by:

  • a collection of objects, (notation: )
  • for each pair of objects, a collection of morphisms from to , (notation )
  • for any object , a special morphism
  • for all objects , a composition ,

such that:

  • 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: 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 instead of .

In a given category , 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 is a monomorphism iff for all object and morphisms , we have implies .

The morphism is an epimorphism when it is a monomorphism in . Explicitly, when for all object and morphisms , we have implies .

 isomorphism


Exercice

  1. Prove that in Set, epic is equivalent to surjective and monic is equivalent to injective.
  2. Prove the same thing in Ab, the category of commutative groups. (One thing is not obvious.)
  3. Prove the same thing in Grp, the category of (non necessarily commutative) groups. (One thing is not obvious at all.)
  4. Prove that is an epimorphism in the category of rings with multiplicative neutral. (Note that it is not surjective.)
  5. In Set, we saw that f is a monic iff , where 1 is any singleton set. Can you find a set C such that f is epic iff ?
  6. In Group, can you find an object playing a role similar to 1, ie a group G s.t. f is monic iff . (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 from a category to a category , noted , is given by:

  • a map which sends every object of to an object in , and
  • a map which sends every morphism in , to a morphism in ,

such that:

  • preserves identities, i.e., , and
  • preserves composition: .


Exercice

  1. Take a functor , three morphisms in , and , , . When , can we say something interesting about , and ?
  2. Do functors preserve monomorphisms? Do functors preserve epimorphisms?
  3. 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.

Answer

  1. No, since and may not even compose! This is the case when has type , and , with collapsing and (i.e., ).
  2. Functors in general do not preserve mono- nor epimorphisms. We build a counter-example for monomorphisms. Let be the category with two objects and , and exactly one morphism . This is a preorder, so is monic. Now take with two objects and , exactly one morphism , and one extra morphism , different from the identity. Because of , yet , is not monic in . The functor which sends to , to and in to in , does not preserve monomorphisms.
  3. In general, the answer is (again) no. For monos, take for example the functor which sends to the identity. Yet, when is faithful, then is monic (or epic).

Definition. A functor is faithful when, for any two morphisms , implies ( is injective on morphisms).

Definition. A functor is full when, for any two objects , if is a morphism , then there exists with ( is surjective on morphisms).


Exercice

Find an "interesting" functor from Set to Group.

Answer Let be the functor which sends:

  • every set to the free group generated by , and
  • every function to a group morphism defined by: .


Exercice

If is a locally small category and A one of its objects, let . Show that this operation from objects of to sets can be extended into a contravariant functor to Set.

Answer Let be a morphism in , then is expected to be a function from the set to the set . We can take, for any morphism : .

This extends to a contravariant functor, since and .

Natural Transformations

Definition. Let and be two functors . A natural transformation from to is given by:

  • a morphism in for every object in ,
  • such that, for any morphism , we have .


Exercice

If is the set of permutation of a (finite) set X; and the set of its linear orderings, we have where . Thus, there is a bijection (iso in Set) between P(X) and L(X).

  1. Show that we can extend P and L to functors from B to Set, where B is the category of finite sets and bijections,
  2. Show that there can be no natural transformation from P to L,
  3. Conclude that there is no natural isomorphism between P and L.

Adjunctions

About Limits and Colimits

One of the main thrusts of category theory is to define concepts by their properties rather than by explicit construction. In general this is just called abstraction, but in good cases, concepts are defined by their properties, at least canonically if not uniquely.

The chief example of this is binary products in Set. The product of two sets and is generally thought of as the set of pairs with and . But strictly speaking, or rather set-theoretically speaking, one has to construct it by cautious use of the axioms of Zermelo-Fraenkel set theory.

Instead, in any category , for any objects and categorists put:

Definition. A product of and is an object with arrows

such that for any object and arrows

there exists a unique arrow making the diagram

Universal property of product

commute, i.e., and .


The standard constructions in Set all have this property, and all the non-standard ones you can think of also do, e.g., the set of pairs with and .

Conversely, any set with this property is as good as any other construction of .

Products are determined canonically by this property property. We will give a more precise meaning to this in later lectures; for now we just state:


Lemma.


For any other product

of

and , there is a unique isomorphism pair such that the diagrams

Prod-iso.png and Prod-iso-2.png

commute.


First examples and definition

So-called free constructions in algebra: monoid, group, etc

Their universal property, the underlying functor

The isomorphism between hom-sets

Its naturality

Definition

On to the definition with and

The simplicity behind definitions:2-categories and adjunctions therein

Definition of 2-categories

String diagrams

CAT as a 2-category

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

and in logic

Sets/graphs and categories

Monads and resolutions

Definition of a monad

String diagrams

Every adjunction yields a monad

Example of monoids again: resolutions

Monadic adjunctions

The category of resolutions

Eilenberg-Moore is terminal

Kleisli is initial

Monadic adjunctions

Algebraic theories

Properties

Composing adjunctions

Preservation of limits/colimits

Freyd's existence theorem

Beck's monadicity theorem

Limites and Colimits

Limits

Example. Cartesian product.

Definition. Binary product.

Theorem. The product of X and Y, if it exists, is unique up to isomorphism. (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.

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 what Wikipedia has to say on category theory.