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_η_app (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] {α : Type u} (a✝ : α) :
    (ofTypeMonad m).η.app α a✝ = pure a✝
    source
    @[simp]
    theorem CategoryTheory.ofTypeMonad_obj (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] (a✝ : Type u) :
    (ofTypeMonad m).obj a✝ = m a✝
    source
    @[simp]
    theorem CategoryTheory.ofTypeMonad_μ_app (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] {α : Type u} (a : m (m α)) :
    (ofTypeMonad m).μ.app α a = joinM a
    source
    @[simp]
    theorem CategoryTheory.ofTypeMonad_map (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) (a✝ : m X✝) :
    (ofTypeMonad m).map f a✝ = f <$> a✝
    source
    def CategoryTheory.eq (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.eq_functor_obj (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] (X : KleisliCat m) :
      (eq m).functor.obj X = X
      source
      @[simp]
      theorem CategoryTheory.eq_functor_map (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] {X✝ Y✝ : KleisliCat m} (f : X✝ ⟶ Y✝) (a✝ : X✝) :
      (eq m).functor.map f a✝ = f a✝
      source
      @[simp]
      theorem CategoryTheory.eq_unitIso (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] :
      (eq m).unitIso = NatIso.ofComponents (fun (X : KleisliCat m) => Iso.refl X) ⋯
      source
      @[simp]
      theorem CategoryTheory.eq_counitIso (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] :
      (eq m).counitIso = NatIso.ofComponents (fun (X : Kleisli (ofTypeMonad m)) => Iso.refl X) ⋯
      source
      @[simp]
      theorem CategoryTheory.eq_inverse_map (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] {X✝ Y✝ : Kleisli (ofTypeMonad m)} (f : X✝ ⟶ Y✝) (a✝ : X✝) :
      (eq m).inverse.map f a✝ = f a✝
      source
      @[simp]
      theorem CategoryTheory.eq_inverse_obj (m : Type u → Type u) [_root_.Monad m] [LawfulMonad m] (X : Kleisli (ofTypeMonad m)) :
      (eq m).inverse.obj X = X