Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Catégorie de Kleisli
Résumé
In , a Kleisli category is a naturally associated to any T. It is equivalent to the category of free . The Kleisli category is one of two extremal solutions to the question Does every monad arise from an ? The other extremal solution is the . Kleisli categories are named for the mathematician Heinrich Kleisli.
Let 〈T, η, μ〉 be a over a category C. The Kleisli category of C is the category CT whose objects and morphisms are given by
That is, every morphism f: X → T Y in C (with codomain TY) can also be regarded as a morphism in CT (but with codomain Y). Composition of morphisms in CT is given by
where f: X → T Y and g: Y → T Z. The identity morphism is given by the monad unit η:
An alternative way of writing this, which clarifies the category in which each object lives, is used by Mac Lane. We use very slightly different notation for this presentation. Given the same monad and category as above, we associate with each object in a new object , and for each morphism in a morphism . Together, these objects and morphisms form our category , where we define
Then the identity morphism in is
Composition of Kleisli arrows can be expressed succinctly by means of the extension operator (–)# : Hom(X, TY) → Hom(TX, TY). Given a monad 〈T, η, μ〉 over a category C and a morphism f : X → TY let
Composition in the Kleisli category CT can then be written
The extension operator satisfies the identities:
where f : X → TY and g : Y → TZ. It follows trivially from these properties that Kleisli composition is associative and that ηX is the identity.
In fact, to give a monad is to give a Kleisli triple 〈T, η, (–)#〉, i.e.
A function ;
For each object in , a morphism ;
For each morphism in , a morphism
such that the above three equations for extension operators are satisfied.
Kleisli categories were originally defined in order to show that every monad arises from an adjunction. That construction is as follows.
Let 〈T, η, μ〉 be a monad over a category C and let CT be the associated Kleisli category.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.