mathlib3 documentation

category_theory.monad.types

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This allows us to use these monads in category theory.

source
@[simp]
theorem category_theory.of_type_monad_μ_app (m : Type u → Type u) [monad m] [is_lawful_monad m] {α : Type u} (a : m (m α)) :
(category_theory.of_type_monad m).μ.app α a = mjoin a
source
def category_theory.of_type_monad (m : Type u → Type u) [monad m] [is_lawful_monad m] :
category_theory.monad (Type u)

A lawful control.monad gives a category theory monad on the category of types.

Equations
source
@[simp]
theorem category_theory.of_type_monad_coe (m : Type u → Type u) [monad m] [is_lawful_monad m] :
↑(category_theory.of_type_monad m) = category_theory.of_type_functor m
source
@[simp]
theorem category_theory.of_type_monad_η_app (m : Type u → Type u) [monad m] [is_lawful_monad m] {α : Type u} (ᾰ : α) :
(category_theory.of_type_monad m).η.app α ᾰ = has_pure.pure ᾰ
source
def category_theory.eq (m : Type u → Type u) [monad m] [is_lawful_monad m] :
category_theory.Kleisli m ≌ category_theory.kleisli (category_theory.of_type_monad 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
source
@[simp]
theorem category_theory.eq_inverse_obj (m : Type u → Type u) [monad m] [is_lawful_monad m] (X : category_theory.kleisli (category_theory.of_type_monad m)) :
(category_theory.eq m).inverse.obj X = X
source
@[simp]
theorem category_theory.eq_counit_iso (m : Type u → Type u) [monad m] [is_lawful_monad m] :
(category_theory.eq m).counit_iso = category_theory.nat_iso.of_components (λ (X : category_theory.kleisli (category_theory.of_type_monad m)), category_theory.iso.refl X) _
source
@[simp]
theorem category_theory.eq_functor_obj (m : Type u → Type u) [monad m] [is_lawful_monad m] (X : category_theory.Kleisli m) :
(category_theory.eq m).functor.obj X = X
source
@[simp]
theorem category_theory.eq_inverse_map (m : Type u → Type u) [monad m] [is_lawful_monad m] (X Y : category_theory.kleisli (category_theory.of_type_monad m)) (f : X ⟶ Y) (ᾰ : X) :
(category_theory.eq m).inverse.map f ᾰ = f ᾰ
source
@[simp]
theorem category_theory.eq_functor_map (m : Type u → Type u) [monad m] [is_lawful_monad m] (X Y : category_theory.Kleisli m) (f : X ⟶ Y) (ᾰ : X) :
(category_theory.eq m).functor.map f ᾰ = f ᾰ
source
@[simp]
theorem category_theory.eq_unit_iso (m : Type u → Type u) [monad m] [is_lawful_monad m] :
(category_theory.eq m).unit_iso = category_theory.nat_iso.of_components (λ (X : category_theory.Kleisli m), category_theory.iso.refl X) _