Basic

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

Statistics

Metric	Count
Definitions Comonad, id, instInhabited, toFunctor, transport, δ, ε, ComonadHom, toNatTrans, mk, toNatIso, id, instInhabited, toFunctor, transport, η, μ, MonadHom, toNatTrans, mk, toNatIso, coeComonad, coeMonad, comonadToFunctor, instCategoryComonad, instCategoryMonad, instInhabitedComonadHom, instInhabitedMonadHom, instQuiverComonad, instQuiverMonad, monadToFunctor	31
Theorems coassoc, coassoc_assoc, counit_naturality, counit_naturality_assoc, delta_naturality, delta_naturality_assoc, id_map, id_obj, id_δ_app, id_ε_app, isSplitEpi_iff_isIso_counit, left_counit, left_counit_assoc, map_counit_app, right_counit, right_counit_assoc, app_δ, app_δ_assoc, app_ε, app_ε_assoc, ext, ext', ext'_iff, ext_iff, id_toNatTrans, mk_hom_toNatTrans, mk_inv_toNatTrans, toNatIso_hom, toNatIso_inv, assoc, id_map, id_obj, id_η_app, id_μ_app, isSplitMono_iff_isIso_unit, left_unit, left_unit_assoc, map_unit_app, mu_naturality, mu_naturality_assoc, right_unit, right_unit_assoc, unit_naturality, unit_naturality_assoc, app_η, app_η_assoc, app_μ, app_μ_assoc, comp_toNatTrans, ext, ext', ext'_iff, ext_iff, id_toNatTrans, mk_hom_toNatTrans, mk_inv_toNatTrans, toNatIso_hom, toNatIso_inv, comonadToFunctor_map, comonadToFunctor_mapIso_comonad_iso_mk, comonadToFunctor_obj, comp_toNatTrans, instFaithfulComonadFunctorComonadToFunctor, instFaithfulMonadFunctorMonadToFunctor, instReflectsIsomorphismsComonadFunctorComonadToFunctor, instReflectsIsomorphismsMonadFunctorMonadToFunctor, monadToFunctor_map, monadToFunctor_mapIso_monad_iso_mk, monadToFunctor_obj	69
Total	100

CategoryTheory

Definitions

Name	Category	Theorems
Comonad 📖	CompData	13 math math: Adjunction.adjToComonadIso_inv_toNatTrans_app, ComonadIso.toNatIso_inv, ComonadIso.toNatIso_hom, comonadToFunctor_mapIso_comonad_iso_mk, comonadToFunctor_obj, ComonadHom.id_toNatTrans, comp_toNatTrans, Adjunction.adjToComonadIso_hom_toNatTrans_app, ComonadIso.mk_hom_toNatTrans, comonadToFunctor_map, instReflectsIsomorphismsComonadFunctorComonadToFunctor, ComonadIso.mk_inv_toNatTrans, instFaithfulComonadFunctorComonadToFunctor
ComonadHom 📖	CompData	—
MonadHom 📖	CompData	—
coeComonad 📖	CompOp	—
coeMonad 📖	CompOp	—
comonadToFunctor 📖	CompOp	7 math math: ComonadIso.toNatIso_inv, ComonadIso.toNatIso_hom, comonadToFunctor_mapIso_comonad_iso_mk, comonadToFunctor_obj, comonadToFunctor_map, instReflectsIsomorphismsComonadFunctorComonadToFunctor, instFaithfulComonadFunctorComonadToFunctor
instCategoryComonad 📖	CompOp	13 math math: Adjunction.adjToComonadIso_inv_toNatTrans_app, ComonadIso.toNatIso_inv, ComonadIso.toNatIso_hom, comonadToFunctor_mapIso_comonad_iso_mk, comonadToFunctor_obj, ComonadHom.id_toNatTrans, comp_toNatTrans, Adjunction.adjToComonadIso_hom_toNatTrans_app, ComonadIso.mk_hom_toNatTrans, comonadToFunctor_map, instReflectsIsomorphismsComonadFunctorComonadToFunctor, ComonadIso.mk_inv_toNatTrans, instFaithfulComonadFunctorComonadToFunctor
instCategoryMonad 📖	CompOp	31 math math: Monad.monadMonEquiv_unitIso_inv_app_toNatTrans_app, MonadIso.toNatIso_hom, instReflectsIsomorphismsMonadFunctorMonadToFunctor, Monad.algebraFunctorOfMonadHomId_inv_app_f, Monad.algebraEquivOfIsoMonads_inverse, Monad.monadMonEquiv_counitIso_hom_app_hom, MonadHom.comp_toNatTrans, Monad.algebraFunctorOfMonadHomId_hom_app_f, Monad.algebraEquivOfIsoMonads_unitIso, Monad.monadToMon_obj, monadToFunctor_obj, Monad.monToMonad_obj, MonadIso.mk_hom_toNatTrans, Monad.algebraFunctorOfMonadHomComp_hom_app_f, Monad.monadToMon_map_hom, MonadIso.toNatIso_inv, Monad.algebraEquivOfIsoMonads_functor, Adjunction.adjToMonadIso_inv_toNatTrans_app, Monad.monToMonad_map_toNatTrans, Monad.algebraEquivOfIsoMonads_counitIso, monadToFunctor_mapIso_monad_iso_mk, Monad.monadMonEquiv_inverse, monadToFunctor_map, instFaithfulMonadFunctorMonadToFunctor, Monad.algebraFunctorOfMonadHomComp_inv_app_f, Monad.monadMonEquiv_counitIso_inv_app_hom, MonadIso.mk_inv_toNatTrans, Monad.monadMonEquiv_functor, Adjunction.adjToMonadIso_hom_toNatTrans_app, Monad.monadMonEquiv_unitIso_hom_app_toNatTrans_app, MonadHom.id_toNatTrans
instInhabitedComonadHom 📖	CompOp	—
instInhabitedMonadHom 📖	CompOp	—
instQuiverComonad 📖	CompOp	—
instQuiverMonad 📖	CompOp	—
monadToFunctor 📖	CompOp	7 math math: MonadIso.toNatIso_hom, instReflectsIsomorphismsMonadFunctorMonadToFunctor, monadToFunctor_obj, MonadIso.toNatIso_inv, monadToFunctor_mapIso_monad_iso_mk, monadToFunctor_map, instFaithfulMonadFunctorMonadToFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comonadToFunctor_map 📖	mathematical	—	Functor.map Comonad instCategoryComonad Functor Functor.category comonadToFunctor ComonadHom.toNatTrans	—	—
comonadToFunctor_mapIso_comonad_iso_mk 📖	mathematical	CategoryStruct.comp Category.toCategoryStruct Functor.obj Comonad.toFunctor Functor.id NatTrans.app Iso.hom Functor Functor.category Comonad.ε Functor.comp Comonad.δ Functor.map	Functor.mapIso Comonad instCategoryComonad comonadToFunctor	—	Iso.ext NatTrans.ext'
comonadToFunctor_obj 📖	mathematical	—	Functor.obj Comonad instCategoryComonad Functor Functor.category comonadToFunctor Comonad.toFunctor	—	—
comp_toNatTrans 📖	mathematical	—	ComonadHom.toNatTrans CategoryStruct.comp Comonad Category.toCategoryStruct instCategoryComonad Functor Functor.category Comonad.toFunctor	—	—
instFaithfulComonadFunctorComonadToFunctor 📖	mathematical	—	Functor.Faithful Comonad instCategoryComonad Functor Functor.category comonadToFunctor	—	ComonadHom.ext'
instFaithfulMonadFunctorMonadToFunctor 📖	mathematical	—	Functor.Faithful Monad instCategoryMonad Functor Functor.category monadToFunctor	—	MonadHom.ext'
instReflectsIsomorphismsComonadFunctorComonadToFunctor 📖	mathematical	—	Functor.ReflectsIsomorphisms Comonad instCategoryComonad Functor Functor.category comonadToFunctor	—	Iso.isIso_hom ComonadHom.app_ε ComonadHom.app_δ
instReflectsIsomorphismsMonadFunctorMonadToFunctor 📖	mathematical	—	Functor.ReflectsIsomorphisms Monad instCategoryMonad Functor Functor.category monadToFunctor	—	Iso.isIso_hom MonadHom.app_η MonadHom.app_μ
monadToFunctor_map 📖	mathematical	—	Functor.map Monad instCategoryMonad Functor Functor.category monadToFunctor MonadHom.toNatTrans	—	—
monadToFunctor_mapIso_monad_iso_mk 📖	mathematical	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.id Monad.toFunctor NatTrans.app Monad.η Iso.hom Functor Functor.category Functor.comp Monad.μ Functor.map	Functor.mapIso Monad instCategoryMonad monadToFunctor	—	Iso.ext NatTrans.ext'
monadToFunctor_obj 📖	mathematical	—	Functor.obj Monad instCategoryMonad Functor Functor.category monadToFunctor Monad.toFunctor	—	—

CategoryTheory.Comonad

Definitions

Name	Category	Theorems
id 📖	CompOp	4 math math: id_δ_app, id_ε_app, id_map, id_obj
instInhabited 📖	CompOp	—
toFunctor 📖	CompOp	72 math math: CategoryTheory.Adjunction.adjToComonadIso_inv_toNatTrans_app, beckCoalgebraFork_pt, CategoryTheory.ComonadIso.toNatIso_inv, CofreeEqualizer.topMap_f, right_counit_assoc, ForgetCreatesLimits'.γ_app, CategoryTheory.ComonadIso.toNatIso_hom, ForgetCreatesColimits'.newCocone_ι_app, coassoc, instIsCoreflexivePairCoalgebraTopMapBottomMap, CategoryTheory.ComonadHom.app_ε, ForgetCreatesLimits'.newCone_pt, cofree_obj_A, counit_naturality, instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair, CategoryTheory.comonadToFunctor_obj, CategoryTheory.ComonadHom.id_toNatTrans, delta_naturality_assoc, isSplitEpi_iff_isIso_counit, CategoryTheory.comp_toNatTrans, ComonadicityInternal.unitFork_ι, CategoryTheory.ComonadHom.app_ε_assoc, instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair, CategoryTheory.prodComonad_obj, left_counit, Coalgebra.Hom.h, cofree_map_f, ForgetCreatesColimits'.γ_app, CategoryTheory.ComonadHom.app_δ_assoc, Coalgebra.coassoc, CategoryTheory.prodComonad_map, CategoryTheory.Adjunction.adjToComonadIso_hom_toNatTrans_app, adj_counit, CategoryTheory.Cokleisli.Adjunction.fromCokleisli_map, ForgetCreatesLimits'.newCone_π, map_counit_app, CategoryTheory.ComonadIso.mk_hom_toNatTrans, CategoryTheory.coalgebraToOver_obj, coassoc_assoc, Coalgebra.Hom.h_assoc, Coalgebra.coassoc_assoc, delta_naturality, ComonadicityInternal.main_pair_coreflexive, cofree_obj_a, CategoryTheory.ComonadHom.app_δ, counit_naturality_assoc, CategoryTheory.ComonadHom.ext_iff, CategoryTheory.coalgebraToOver_map, Coalgebra.counit_assoc, CategoryTheory.δ_iso_of_coreflective, right_counit, CategoryTheory.ComonadIso.mk_inv_toNatTrans, CategoryTheory.ComonadHom.ext'_iff, beckEqualizer_lift, beckFork_ι, beckFork_pt, CofreeEqualizer.condition, id_map, Coalgebra.counit, ComonadicityInternal.main_pair_F_cosplit, instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair, ForgetCreatesLimits'.commuting, CategoryTheory.Adjunction.toComonad_coe, id_obj, instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair, CofreeEqualizer.bottomMap_f, CategoryTheory.Cokleisli.Adjunction.fromCokleisli_obj, left_counit_assoc, ComonadicityInternal.counitFork_pt, adj_unit, beckCoalgebraFork_π_app, CategoryTheory.Cokleisli.Adjunction.toCokleisli_map
transport 📖	CompOp	—
δ 📖	CompOp	24 math math: right_counit_assoc, CategoryTheory.prodComonad_δ_app, coassoc, ComonadicityInternal.comparisonAdjunction_counit_f, delta_naturality_assoc, CategoryTheory.Adjunction.toComonad_δ, left_counit, cofree_map_f, id_δ_app, CategoryTheory.ComonadHom.app_δ_assoc, Coalgebra.coassoc, CategoryTheory.Cokleisli.Adjunction.fromCokleisli_map, coassoc_assoc, Coalgebra.coassoc_assoc, delta_naturality, cofree_obj_a, CategoryTheory.ComonadHom.app_δ, CategoryTheory.δ_iso_of_coreflective, right_counit, beckEqualizer_lift, beckFork_ι, beckFork_pt, CofreeEqualizer.bottomMap_f, left_counit_assoc
ε 📖	CompOp	19 math math: CategoryTheory.prodComonad_ε_app, right_counit_assoc, CategoryTheory.ComonadHom.app_ε, counit_naturality, isSplitEpi_iff_isIso_counit, CategoryTheory.ComonadHom.app_ε_assoc, CategoryTheory.Adjunction.toComonad_ε, left_counit, adj_counit, map_counit_app, counit_naturality_assoc, Coalgebra.counit_assoc, right_counit, beckEqualizer_lift, id_ε_app, Coalgebra.counit, left_counit_assoc, adj_unit, CategoryTheory.Cokleisli.Adjunction.toCokleisli_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coassoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.comp CategoryTheory.NatTrans.app δ CategoryTheory.Functor.map	—	—
coassoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp δ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coassoc
counit_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app ε	—	CategoryTheory.NatTrans.naturality
counit_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id ε	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' counit_naturality
delta_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app δ	—	CategoryTheory.NatTrans.naturality
delta_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' delta_naturality
id_map 📖	mathematical	—	CategoryTheory.Functor.map toFunctor id	—	—
id_obj 📖	mathematical	—	CategoryTheory.Functor.obj toFunctor id	—	—
id_δ_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id δ id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
id_ε_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id ε id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
isSplitEpi_iff_isIso_counit 📖	mathematical	—	CategoryTheory.IsSplitEpi CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app ε CategoryTheory.IsIso	—	CategoryTheory.Functor.map_id CategoryTheory.IsSplitEpi.id CategoryTheory.Functor.map_comp map_counit_app counit_naturality CategoryTheory.IsSplitEpi.of_iso
left_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app δ ε CategoryTheory.CategoryStruct.id	—	—
left_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp δ CategoryTheory.Functor.id ε	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' left_counit
map_counit_app 📖	mathematical	—	CategoryTheory.Functor.map toFunctor CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.NatTrans.app ε	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.NatIso.isIso_app_of_isIso right_counit left_counit
right_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app δ CategoryTheory.Functor.map ε CategoryTheory.CategoryStruct.id	—	—
right_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp δ CategoryTheory.Functor.map CategoryTheory.Functor.id ε	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' right_counit

CategoryTheory.ComonadHom

Definitions

Name	Category	Theorems
toNatTrans 📖	CompOp	13 math math: CategoryTheory.Adjunction.adjToComonadIso_inv_toNatTrans_app, app_ε, id_toNatTrans, CategoryTheory.comp_toNatTrans, app_ε_assoc, app_δ_assoc, CategoryTheory.Adjunction.adjToComonadIso_hom_toNatTrans_app, CategoryTheory.ComonadIso.mk_hom_toNatTrans, CategoryTheory.comonadToFunctor_map, app_δ, ext_iff, CategoryTheory.ComonadIso.mk_inv_toNatTrans, ext'_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor CategoryTheory.Functor.comp CategoryTheory.NatTrans.app toNatTrans CategoryTheory.Comonad.δ CategoryTheory.Functor.map	—	—
app_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor CategoryTheory.NatTrans.app toNatTrans CategoryTheory.Functor.comp CategoryTheory.Comonad.δ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_δ
app_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app toNatTrans CategoryTheory.Comonad.ε	—	—
app_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor CategoryTheory.NatTrans.app toNatTrans CategoryTheory.Functor.id CategoryTheory.Comonad.ε	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_ε
ext 📖	—	CategoryTheory.NatTrans.app CategoryTheory.Comonad.toFunctor toNatTrans	—	—	—
ext' 📖	—	CategoryTheory.NatTrans.app CategoryTheory.Comonad.toFunctor toNatTrans	—	—	ext
ext'_iff 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comonad.toFunctor toNatTrans	—	ext'
ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comonad.toFunctor toNatTrans	—	ext
id_toNatTrans 📖	mathematical	—	toNatTrans CategoryTheory.CategoryStruct.id CategoryTheory.Comonad CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryComonad CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Comonad.toFunctor	—	—

CategoryTheory.ComonadIso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—
toNatIso 📖	CompOp	2 math math: toNatIso_inv, toNatIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom_toNatTrans 📖	mathematical	—	CategoryTheory.ComonadHom.toNatTrans CategoryTheory.Iso.hom CategoryTheory.Comonad CategoryTheory.instCategoryComonad CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Comonad.toFunctor	—	—
mk_inv_toNatTrans 📖	mathematical	—	CategoryTheory.ComonadHom.toNatTrans CategoryTheory.Iso.inv CategoryTheory.Comonad CategoryTheory.instCategoryComonad CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Comonad.toFunctor	—	—
toNatIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Comonad.toFunctor toNatIso CategoryTheory.Functor.map CategoryTheory.Comonad CategoryTheory.instCategoryComonad CategoryTheory.comonadToFunctor	—	—
toNatIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Comonad.toFunctor toNatIso CategoryTheory.Functor.map CategoryTheory.Comonad CategoryTheory.instCategoryComonad CategoryTheory.comonadToFunctor	—	—

CategoryTheory.Monad

Definitions

Name	Category	Theorems
id 📖	CompOp	4 math math: id_η_app, id_μ_app, id_obj, id_map
instInhabited 📖	CompOp	—
toFunctor 📖	CompOp	79 math math: ForgetCreatesColimits.commuting, monadMonEquiv_unitIso_inv_app_toNatTrans_app, CategoryTheory.MonadIso.toNatIso_hom, free_map_f, mul_def, Algebra.unit_assoc, CategoryTheory.MonadHom.app_μ, Algebra.Hom.h, beckCoequalizer_desc, CategoryTheory.MonadHom.comp_toNatTrans, CategoryTheory.Kleisli.Adjunction.toKleisli_map, isSplitMono_iff_isIso_unit, Algebra.assoc_assoc, FreeCoequalizer.condition, CategoryTheory.monadToFunctor_obj, instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair, instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair, ForgetCreatesColimits.γ_app, ForgetCreatesLimits.newCone_π_app, instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair, CategoryTheory.MonadIso.mk_hom_toNatTrans, left_unit, id_obj, beckAlgebraCofork_pt, adj_counit, adj_unit, assoc, unit_naturality, MonadicityInternal.unitCofork_π, mu_naturality, CategoryTheory.MonadIso.toNatIso_inv, mu_naturality_assoc, CategoryTheory.MonadHom.ext_iff, CategoryTheory.MonadHom.app_η_assoc, CategoryTheory.MonadHom.app_μ_assoc, Algebra.assoc, map_unit_app, beckCofork_pt, instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair, free_obj_a, CategoryTheory.MonadHom.app_η, ForgetCreatesColimits.newCocone_pt, CategoryTheory.Adjunction.adjToMonadIso_inv_toNatTrans_app, CategoryTheory.ofTypeMonad_map, free_obj_A, FreeCoequalizer.bottomMap_f, algebraFunctorOfMonadHom_obj_a, beckCofork_π, CategoryTheory.Kleisli.Adjunction.fromKleisli_map, MonadicityInternal.unitCofork_pt, beckAlgebraCofork_ι_app, CategoryTheory.Kleisli.Adjunction.fromKleisli_obj, CategoryTheory.MonadHom.ext'_iff, ForgetCreatesLimits.γ_app, CategoryTheory.coprodMonad_map, CategoryTheory.Adjunction.toMonad_coe, ofMon_obj, CategoryTheory.μ_iso_of_reflective, right_unit, CategoryTheory.MonadIso.mk_inv_toNatTrans, unit_naturality_assoc, CategoryTheory.Adjunction.adjToMonadIso_hom_toNatTrans_app, MonadicityInternal.main_pair_G_split, toMon_X, MonadicityInternal.main_pair_reflexive, monadMonEquiv_unitIso_hom_app_toNatTrans_app, one_def, left_unit_assoc, instIsReflexivePairAlgebraTopMapBottomMap, Algebra.unit, CategoryTheory.MonadHom.id_toNatTrans, id_map, CategoryTheory.coprodMonad_obj, CategoryTheory.ofTypeMonad_obj, Algebra.Hom.h_assoc, algebraFunctorOfMonadHom_map_f, right_unit_assoc, FreeCoequalizer.topMap_f, ForgetCreatesColimits.newCocone_ι
transport 📖	CompOp	—
η 📖	CompOp	22 math math: id_η_app, ofMon_η, Algebra.unit_assoc, CategoryTheory.ofTypeMonad_η_app, beckCoequalizer_desc, CategoryTheory.Kleisli.Adjunction.toKleisli_map, isSplitMono_iff_isIso_unit, left_unit, adj_counit, adj_unit, CategoryTheory.Adjunction.toMonad_η, unit_naturality, CategoryTheory.MonadHom.app_η_assoc, map_unit_app, CategoryTheory.MonadHom.app_η, CategoryTheory.coprodMonad_η_app, right_unit, unit_naturality_assoc, one_def, left_unit_assoc, Algebra.unit, right_unit_assoc
μ 📖	CompOp	26 math math: free_map_f, mul_def, CategoryTheory.MonadHom.app_μ, beckCoequalizer_desc, CategoryTheory.coprodMonad_μ_app, id_μ_app, Algebra.assoc_assoc, CategoryTheory.ofTypeMonad_μ_app, left_unit, assoc, mu_naturality, mu_naturality_assoc, CategoryTheory.Adjunction.toMonad_μ, CategoryTheory.MonadHom.app_μ_assoc, Algebra.assoc, beckCofork_pt, free_obj_a, MonadicityInternal.comparisonAdjunction_unit_f, FreeCoequalizer.bottomMap_f, beckCofork_π, CategoryTheory.Kleisli.Adjunction.fromKleisli_map, ofMon_μ, CategoryTheory.μ_iso_of_reflective, right_unit, left_unit_assoc, right_unit_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app μ	—	—
id_map 📖	mathematical	—	CategoryTheory.Functor.map toFunctor id	—	—
id_obj 📖	mathematical	—	CategoryTheory.Functor.obj toFunctor id	—	—
id_η_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id η id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
id_μ_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id μ id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
isSplitMono_iff_isIso_unit 📖	mathematical	—	CategoryTheory.IsSplitMono CategoryTheory.Functor.obj CategoryTheory.Functor.id toFunctor CategoryTheory.NatTrans.app η CategoryTheory.IsIso	—	CategoryTheory.IsSplitMono.id CategoryTheory.Functor.map_id CategoryTheory.Functor.map_comp map_unit_app unit_naturality CategoryTheory.IsSplitMono.of_iso
left_unit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id toFunctor CategoryTheory.NatTrans.app η CategoryTheory.Functor.comp μ CategoryTheory.CategoryStruct.id	—	—
left_unit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.id η CategoryTheory.Functor.comp μ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' left_unit
map_unit_app 📖	mathematical	—	CategoryTheory.Functor.map toFunctor CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.NatTrans.app η	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.NatIso.isIso_app_of_isIso right_unit left_unit
mu_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp μ	—	CategoryTheory.NatTrans.naturality
mu_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp μ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mu_naturality
right_unit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app η CategoryTheory.Functor.comp μ CategoryTheory.CategoryStruct.id	—	—
right_unit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id η CategoryTheory.Functor.comp μ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' right_unit
unit_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.id η CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality
unit_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.id η CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_naturality

CategoryTheory.MonadHom

Definitions

Name	Category	Theorems
toNatTrans 📖	CompOp	19 math math: CategoryTheory.Monad.monadMonEquiv_unitIso_inv_app_toNatTrans_app, app_μ, comp_toNatTrans, CategoryTheory.MonadIso.mk_hom_toNatTrans, CategoryTheory.Monad.monadToMon_map_hom, ext_iff, app_η_assoc, app_μ_assoc, app_η, CategoryTheory.Adjunction.adjToMonadIso_inv_toNatTrans_app, CategoryTheory.Monad.monToMonad_map_toNatTrans, CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_a, CategoryTheory.monadToFunctor_map, ext'_iff, CategoryTheory.MonadIso.mk_inv_toNatTrans, CategoryTheory.Adjunction.adjToMonadIso_hom_toNatTrans_app, CategoryTheory.Monad.monadMonEquiv_unitIso_hom_app_toNatTrans_app, id_toNatTrans, CategoryTheory.Monad.algebraFunctorOfMonadHom_map_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_η 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Monad.toFunctor CategoryTheory.NatTrans.app CategoryTheory.Monad.η toNatTrans	—	—
app_η_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Monad.η toNatTrans	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_η
app_μ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Monad.toFunctor CategoryTheory.NatTrans.app CategoryTheory.Monad.μ toNatTrans CategoryTheory.Functor.map	—	—
app_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Monad.μ toNatTrans CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_μ
comp_toNatTrans 📖	mathematical	—	toNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Monad CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMonad CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monad.toFunctor	—	—
ext 📖	—	CategoryTheory.NatTrans.app CategoryTheory.Monad.toFunctor toNatTrans	—	—	—
ext' 📖	—	CategoryTheory.NatTrans.app CategoryTheory.Monad.toFunctor toNatTrans	—	—	ext
ext'_iff 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Monad.toFunctor toNatTrans	—	ext'
ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Monad.toFunctor toNatTrans	—	ext
id_toNatTrans 📖	mathematical	—	toNatTrans CategoryTheory.CategoryStruct.id CategoryTheory.Monad CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMonad CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monad.toFunctor	—	—

CategoryTheory.MonadIso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—
toNatIso 📖	CompOp	2 math math: toNatIso_hom, toNatIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom_toNatTrans 📖	mathematical	—	CategoryTheory.MonadHom.toNatTrans CategoryTheory.Iso.hom CategoryTheory.Monad CategoryTheory.instCategoryMonad CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monad.toFunctor	—	—
mk_inv_toNatTrans 📖	mathematical	—	CategoryTheory.MonadHom.toNatTrans CategoryTheory.Iso.inv CategoryTheory.Monad CategoryTheory.instCategoryMonad CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monad.toFunctor	—	—
toNatIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monad.toFunctor toNatIso CategoryTheory.Functor.map CategoryTheory.Monad CategoryTheory.instCategoryMonad CategoryTheory.monadToFunctor	—	—
toNatIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monad.toFunctor toNatIso CategoryTheory.Functor.map CategoryTheory.Monad CategoryTheory.instCategoryMonad CategoryTheory.monadToFunctor	—	—

---

← Back to Index