EquivMon

📁 Source: Mathlib/CategoryTheory/Monad/EquivMon.lean

Statistics

Metric	Count
Definitions instMonObjFunctor, monToMonad, monadMonEquiv, monadToMon, ofMon, toMon	6
Theorems monToMonad_map_toNatTrans, monToMonad_obj, monadMonEquiv_counitIso_hom_app_hom, monadMonEquiv_counitIso_inv_app_hom, monadMonEquiv_functor, monadMonEquiv_inverse, monadMonEquiv_unitIso_hom_app_toNatTrans_app, monadMonEquiv_unitIso_inv_app_toNatTrans_app, monadToMon_map_hom, monadToMon_obj, mul_def, ofMon_obj, ofMon_η, ofMon_μ, one_def, toMon_X, toMon_mon	17
Total	23

CategoryTheory.Monad

Definitions

Name	Category	Theorems
instMonObjFunctor 📖	CompOp	3 math math: mul_def, toMon_mon, one_def
monToMonad 📖	CompOp	7 math math: monadMonEquiv_unitIso_inv_app_toNatTrans_app, monadMonEquiv_counitIso_hom_app_hom, monToMonad_obj, monToMonad_map_toNatTrans, monadMonEquiv_inverse, monadMonEquiv_counitIso_inv_app_hom, monadMonEquiv_unitIso_hom_app_toNatTrans_app
monadMonEquiv 📖	CompOp	6 math math: monadMonEquiv_unitIso_inv_app_toNatTrans_app, monadMonEquiv_counitIso_hom_app_hom, monadMonEquiv_inverse, monadMonEquiv_counitIso_inv_app_hom, monadMonEquiv_functor, monadMonEquiv_unitIso_hom_app_toNatTrans_app
monadToMon 📖	CompOp	7 math math: monadMonEquiv_unitIso_inv_app_toNatTrans_app, monadMonEquiv_counitIso_hom_app_hom, monadToMon_obj, monadToMon_map_hom, monadMonEquiv_counitIso_inv_app_hom, monadMonEquiv_functor, monadMonEquiv_unitIso_hom_app_toNatTrans_app
ofMon 📖	CompOp	5 math math: ofMon_η, monToMonad_obj, monToMonad_map_toNatTrans, ofMon_μ, ofMon_obj
toMon 📖	CompOp	4 math math: monadToMon_obj, monadToMon_map_hom, toMon_mon, toMon_X

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
monToMonad_map_toNatTrans 📖	mathematical	—	CategoryTheory.MonadHom.toNatTrans ofMon CategoryTheory.Functor.map CategoryTheory.Mon CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Monad CategoryTheory.instCategoryMonad monToMonad CategoryTheory.Mon.Hom.hom	—	—
monToMonad_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Monad CategoryTheory.instCategoryMonad monToMonad ofMon	—	—
monadMonEquiv_counitIso_hom_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Monad CategoryTheory.instCategoryMonad monToMonad monadToMon CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso monadMonEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
monadMonEquiv_counitIso_inv_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Monad CategoryTheory.instCategoryMonad monToMonad monadToMon CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso monadMonEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
monadMonEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Monad CategoryTheory.Mon CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory CategoryTheory.instCategoryMonad CategoryTheory.Mon.instCategory monadMonEquiv monadToMon	—	—
monadMonEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Monad CategoryTheory.Mon CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory CategoryTheory.instCategoryMonad CategoryTheory.Mon.instCategory monadMonEquiv monToMonad	—	—
monadMonEquiv_unitIso_hom_app_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app toFunctor CategoryTheory.Functor.obj CategoryTheory.Monad CategoryTheory.instCategoryMonad CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Mon CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory CategoryTheory.Mon.instCategory monadToMon monToMonad CategoryTheory.MonadHom.toNatTrans CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso monadMonEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
monadMonEquiv_unitIso_inv_app_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app toFunctor CategoryTheory.Functor.obj CategoryTheory.Monad CategoryTheory.instCategoryMonad CategoryTheory.Functor.comp CategoryTheory.Mon CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory CategoryTheory.Mon.instCategory monadToMon monToMonad CategoryTheory.Functor.id CategoryTheory.MonadHom.toNatTrans CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso monadMonEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
monadToMon_map_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory toMon CategoryTheory.Functor.map CategoryTheory.Monad CategoryTheory.instCategoryMonad CategoryTheory.Mon CategoryTheory.Mon.instCategory monadToMon CategoryTheory.MonadHom.toNatTrans	—	—
monadToMon_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Monad CategoryTheory.instCategoryMonad CategoryTheory.Mon CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory CategoryTheory.Mon.instCategory monadToMon toMon	—	—
mul_def 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory toFunctor instMonObjFunctor μ	—	—
ofMon_obj 📖	mathematical	—	CategoryTheory.Functor.obj toFunctor ofMon CategoryTheory.Mon.X CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory	—	—
ofMon_η 📖	mathematical	—	η ofMon CategoryTheory.MonObj.one CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory CategoryTheory.Mon.X CategoryTheory.Mon.mon	—	—
ofMon_μ 📖	mathematical	—	μ ofMon CategoryTheory.MonObj.mul CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory CategoryTheory.Mon.X CategoryTheory.Mon.mon	—	—
one_def 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory toFunctor instMonObjFunctor η	—	—
toMon_X 📖	mathematical	—	CategoryTheory.Mon.X CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory toMon toFunctor	—	—
toMon_mon 📖	mathematical	—	CategoryTheory.Mon.mon CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory toMon instMonObjFunctor	—	—

---

← Back to Index