Documentation

Mathlib.CategoryTheory.Monad.Types

Convert from Monad (i.e. Lean's Type-based monads) to CategoryTheory.Monad #

This allows us to use these monads in category theory.

source
def CategoryTheory.ofTypeMonad (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] :
Monad (Type u)

A lawful Control.Monad gives a category theory Monad on the category of types.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.ofTypeMonad_obj (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] (x : Type u) :
    (ofTypeMonad m).obj x = m x
    source
    @[simp]
    theorem CategoryTheory.ofTypeMonad_μ_app (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] (X : Type u) :
    (ofTypeMonad m).μ.app X = TypeCat.ofHom joinM
    source
    @[simp]
    theorem CategoryTheory.ofTypeMonad_map (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) :
    (ofTypeMonad m).map f = TypeCat.ofHom (_root_.Functor.map ⇑(TypeCat.Hom.hom f))
    source
    @[simp]
    theorem CategoryTheory.ofTypeMonad_η_app (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] (X : Type u) :
    (ofTypeMonad m).η.app X = TypeCat.ofHom pure
    source
    def CategoryTheory.kleisliCatEquivKleisli (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] :
    KleisliCat m ≌ Kleisli (ofTypeMonad m)

    The Kleisli category of a Control.Monad is equivalent to the Kleisli category of its category-theoretic version, provided the monad is lawful.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.kleisliCatEquivKleisli_functor_obj_of (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] (X : KleisliCat m) :
      ((kleisliCatEquivKleisli m).functor.obj X).of = X
      source
      @[simp]
      theorem CategoryTheory.kleisliCatEquivKleisli_inverse_obj (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] (X : Kleisli (ofTypeMonad m)) :
      (kleisliCatEquivKleisli m).inverse.obj X = X.of
      source
      @[simp]
      theorem CategoryTheory.kleisliCatEquivKleisli_inverse_map (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] {X✝ Y✝ : Kleisli (ofTypeMonad m)} (f : X✝ ⟶ Y✝) (x : X✝.of) :
      (kleisliCatEquivKleisli m).inverse.map f x = (ConcreteCategory.hom f.of) x
      source
      @[simp]
      theorem CategoryTheory.kleisliCatEquivKleisli_counitIso (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] :
      (kleisliCatEquivKleisli m).counitIso = NatIso.ofComponents (fun (X : Kleisli (ofTypeMonad m)) => Iso.refl X) ⋯
      source
      @[simp]
      theorem CategoryTheory.kleisliCatEquivKleisli_unitIso (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] :
      (kleisliCatEquivKleisli m).unitIso = NatIso.ofComponents (fun (X : KleisliCat m) => Iso.refl X) ⋯
      source
      @[simp]
      theorem CategoryTheory.kleisliCatEquivKleisli_functor_map_of (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] {X✝ Y✝ : KleisliCat m} (f : X✝ ⟶ Y✝) :
      ((kleisliCatEquivKleisli m).functor.map f).of = TypeCat.ofHom f
      source
      @[deprecated CategoryTheory.kleisliCatEquivKleisli (since := "2026-04-16")]
      def CategoryTheory.eq (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] :
      KleisliCat m ≌ Kleisli (ofTypeMonad m)

      Alias of CategoryTheory.kleisliCatEquivKleisli.

      The Kleisli category of a Control.Monad is equivalent to the Kleisli category of its category-theoretic version, provided the monad is lawful.

      Equations
      Instances For