Algebra

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

Statistics

Metric	Count
Definitions A, comp, f, id, a, eilenbergMoore, instCategoryStruct, isoMk, adj, cofree, forget, Algebra, A, comp, f, id, instInhabited, a, eilenbergMoore, instCategoryStruct, isoMk, adj, algebraEquivOfIsoMonads, algebraFunctorOfMonadHom, algebraFunctorOfMonadHomComp, algebraFunctorOfMonadHomEq, algebraFunctorOfMonadHomId, forget, free, instInhabitedAlgebra	30
Theorems ext, ext', ext'_iff, ext_iff, h, h_assoc, coassoc, coassoc_assoc, comp_eq_comp, comp_f, counit, counit_assoc, id_eq_id, id_f, isoMk_hom_f, isoMk_inv_f, adj_counit, adj_unit, algebra_epi_of_epi, algebra_mono_of_mono, coalgebra_iso_of_iso, cofree_map_f, cofree_obj_A, cofree_obj_a, forget_faithful, forget_map, forget_obj, forget_reflects_iso, instIsLeftAdjointCoalgebraForget, ext, ext', ext'_iff, ext_iff, h, h_assoc, assoc, assoc_assoc, comp_eq_comp, comp_f, id_eq_id, id_f, isoMk_hom_f, isoMk_inv_f, unit, unit_assoc, adj_counit, adj_unit, algebraEquivOfIsoMonads_counitIso, algebraEquivOfIsoMonads_functor, algebraEquivOfIsoMonads_inverse, algebraEquivOfIsoMonads_unitIso, algebraFunctorOfMonadHomComp_hom_app_f, algebraFunctorOfMonadHomComp_inv_app_f, algebraFunctorOfMonadHomEq_hom_app_f, algebraFunctorOfMonadHomEq_inv_app_f, algebraFunctorOfMonadHomId_hom_app_f, algebraFunctorOfMonadHomId_inv_app_f, algebraFunctorOfMonadHom_map_f, algebraFunctorOfMonadHom_obj_A, algebraFunctorOfMonadHom_obj_a, algebra_epi_of_epi, algebra_equiv_of_iso_monads_comp_forget, algebra_iso_of_iso, algebra_mono_of_mono, forget_faithful, forget_map, forget_obj, forget_reflects_iso, free_map_f, free_obj_A, free_obj_a, instIsRightAdjointAlgebraForget	72
Total	102

CategoryTheory.Comonad

Definitions

Name	Category	Theorems
adj 📖	CompOp	6 math math: CategoryTheory.Adjunction.adjToComonadIso_inv_toNatTrans_app, CategoryTheory.instEssSurjCoalgebraToComonadAdjComparison, CategoryTheory.Adjunction.adjToComonadIso_hom_toNatTrans_app, adj_counit, adj_unit, CategoryTheory.instFullCoalgebraToComonadAdjComparison
cofree 📖	CompOp	18 math math: CategoryTheory.Adjunction.adjToComonadIso_inv_toNatTrans_app, beckCoalgebraFork_pt, CofreeEqualizer.topMap_f, instIsCoreflexivePairCoalgebraTopMapBottomMap, cofree_obj_A, CategoryTheory.instEssSurjCoalgebraToComonadAdjComparison, cofree_map_f, CategoryTheory.Adjunction.adjToComonadIso_hom_toNatTrans_app, adj_counit, left_comparison, CofreeEqualizer.ι_f, CategoryTheory.Over.star_map_left, cofree_obj_a, CofreeEqualizer.condition, CofreeEqualizer.bottomMap_f, adj_unit, beckCoalgebraFork_π_app, CategoryTheory.instFullCoalgebraToComonadAdjComparison
forget 📖	CompOp	28 math math: CategoryTheory.Adjunction.adjToComonadIso_inv_toNatTrans_app, ForgetCreatesLimits'.liftedCone_π_app_f, forget_map, ForgetCreatesLimits'.γ_app, forget_faithful, CategoryTheory.comp_comparison_forget_hasColimit, ForgetCreatesColimits'.newCocone_ι_app, ForgetCreatesLimits'.newCone_pt, CategoryTheory.instEssSurjCoalgebraToComonadAdjComparison, ForgetCreatesColimits'.γ_app, comparisonForget_inv_app, CategoryTheory.Adjunction.adjToComonadIso_hom_toNatTrans_app, adj_counit, comparisonForget_hom_app, ForgetCreatesLimits'.newCone_π, ForgetCreatesColimits'.coconePoint_a, forget_obj, ForgetCreatesColimits'.liftedCoconeIsColimit_desc_f, ForgetCreatesLimits'.conePoint_A, ForgetCreatesColimits'.coconePoint_A, forget_additive, ForgetCreatesLimits'.commuting, ForgetCreatesLimits'.liftedConeIsLimit_lift_f, ForgetCreatesColimits'.liftedCocone_ι_app_f, adj_unit, instIsLeftAdjointCoalgebraForget, CategoryTheory.instFullCoalgebraToComonadAdjComparison, forget_reflects_iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adj_counit 📖	mathematical	—	CategoryTheory.Adjunction.counit Coalgebra Coalgebra.eilenbergMoore forget cofree adj CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app toFunctor ε CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Coalgebra.A Coalgebra.a CategoryTheory.Functor.map Coalgebra.Hom.f CategoryTheory.Category.id_comp	—	CategoryTheory.Category.id_comp
adj_unit 📖	mathematical	—	CategoryTheory.Adjunction.unit Coalgebra Coalgebra.eilenbergMoore forget cofree adj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.obj Coalgebra.A Coalgebra.a Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp toFunctor CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id Coalgebra.Hom.f CategoryTheory.NatTrans.app ε Coalgebra.Hom	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
algebra_epi_of_epi 📖	mathematical	—	CategoryTheory.Epi Coalgebra Coalgebra.eilenbergMoore	—	CategoryTheory.Functor.epi_of_epi_map CategoryTheory.Functor.reflectsEpimorphisms_of_faithful forget_faithful
algebra_mono_of_mono 📖	mathematical	—	CategoryTheory.Mono Coalgebra Coalgebra.eilenbergMoore	—	CategoryTheory.Functor.mono_of_mono_map CategoryTheory.Functor.reflectsMonomorphisms_of_faithful forget_faithful
coalgebra_iso_of_iso 📖	mathematical	—	CategoryTheory.IsIso Coalgebra Coalgebra.eilenbergMoore	—	CategoryTheory.IsIso.eq_inv_comp Coalgebra.Hom.h_assoc CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id Coalgebra.Hom.ext' CategoryTheory.IsIso.inv_hom_id
cofree_map_f 📖	mathematical	—	Coalgebra.Hom.f CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp δ CategoryTheory.Functor.map Coalgebra Coalgebra.eilenbergMoore cofree	—	—
cofree_obj_A 📖	mathematical	—	Coalgebra.A CategoryTheory.Functor.obj Coalgebra Coalgebra.eilenbergMoore cofree toFunctor	—	—
cofree_obj_a 📖	mathematical	—	Coalgebra.a CategoryTheory.Functor.obj Coalgebra Coalgebra.eilenbergMoore cofree CategoryTheory.NatTrans.app toFunctor CategoryTheory.Functor.comp δ	—	—
forget_faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful Coalgebra Coalgebra.eilenbergMoore forget	—	Coalgebra.Hom.ext'
forget_map 📖	mathematical	—	CategoryTheory.Functor.map Coalgebra Coalgebra.eilenbergMoore forget Coalgebra.Hom.f	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj Coalgebra Coalgebra.eilenbergMoore forget Coalgebra.A	—	—
forget_reflects_iso 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms Coalgebra Coalgebra.eilenbergMoore forget	—	coalgebra_iso_of_iso
instIsLeftAdjointCoalgebraForget 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Coalgebra Coalgebra.eilenbergMoore forget	—	—

CategoryTheory.Comonad.Coalgebra

Definitions

Name	Category	Theorems
A 📖	CompOp	48 math math: CategoryTheory.Comonad.beckCoalgebraFork_pt, comp_f, CategoryTheory.Comonad.CofreeEqualizer.topMap_f, CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone_ι_app, CategoryTheory.Comonad.instIsCoreflexivePairCoalgebraTopMapBottomMap, CategoryTheory.Comonad.cofree_obj_A, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_neg_f, CategoryTheory.Comonad.ComonadicityInternal.unitFork_ι, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair, Hom.h, coassoc, CategoryTheory.Comonad.adj_counit, CategoryTheory.coalgebraToOver_obj, CategoryTheory.Coreflective.instIsIsoAppCounitCoreflectorAdjunctionA, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_nsmul_f, Hom.h_assoc, coassoc_assoc, CategoryTheory.Comonad.ComonadicityInternal.main_pair_coreflexive, CategoryTheory.Comonad.CofreeEqualizer.ι_f, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zsmul_f, CategoryTheory.overToCoalgebra_obj_A, CategoryTheory.Comonad.forget_obj, CategoryTheory.coalgebraToOver_map, counit_assoc, id_f, CategoryTheory.Comonad.beckEqualizer_lift, CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint_A, CategoryTheory.Comonad.comparison_obj_A, CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint_A, CategoryTheory.Comonad.beckFork_ι, CategoryTheory.Comonad.beckFork_pt, CategoryTheory.Comonad.CofreeEqualizer.condition, counit, CategoryTheory.coalgebraEquivOver_unitIso, CategoryTheory.Comonad.ComonadicityInternal.main_pair_F_cosplit, CategoryTheory.Comonad.instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair, CategoryTheory.Comonad.ForgetCreatesLimits'.commuting, CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair, CategoryTheory.Comonad.CofreeEqualizer.bottomMap_f, CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_add_f, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_sub_f, CategoryTheory.Comonad.adj_unit, CategoryTheory.Comonad.beckCoalgebraFork_π_app, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zero_f
a 📖	CompOp	34 math math: CategoryTheory.Comonad.comparison_obj_a, CategoryTheory.Comonad.CofreeEqualizer.topMap_f, CategoryTheory.Comonad.ForgetCreatesLimits'.γ_app, CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone_ι_app, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair, CategoryTheory.Comonad.ComonadicityInternal.unitFork_ι, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair, Hom.h, CategoryTheory.Comonad.ForgetCreatesColimits'.γ_app, coassoc, CategoryTheory.Comonad.adj_counit, CategoryTheory.coalgebraToOver_obj, Hom.h_assoc, coassoc_assoc, CategoryTheory.Comonad.ComonadicityInternal.main_pair_coreflexive, CategoryTheory.Comonad.CofreeEqualizer.ι_f, CategoryTheory.Comonad.cofree_obj_a, CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint_a, CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint_a, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f, CategoryTheory.coalgebraToOver_map, counit_assoc, CategoryTheory.Comonad.beckEqualizer_lift, CategoryTheory.Comonad.beckFork_ι, CategoryTheory.Comonad.beckFork_pt, CategoryTheory.overToCoalgebra_obj_a, counit, CategoryTheory.Comonad.ComonadicityInternal.main_pair_F_cosplit, CategoryTheory.Comonad.instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair, CategoryTheory.Comonad.ForgetCreatesLimits'.commuting, CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair, CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt, CategoryTheory.Comonad.adj_unit, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply
eilenbergMoore 📖	CompOp	79 math math: CategoryTheory.Adjunction.adjToComonadIso_inv_toNatTrans_app, CategoryTheory.Comonad.comparison_faithful_of_faithful, CategoryTheory.ComonadicLeftAdjoint.eqv, CategoryTheory.comp_comparison_hasColimit, CategoryTheory.Comonad.comparison_obj_a, CategoryTheory.Comonad.beckCoalgebraFork_pt, CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone_pt, CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone_π_app_f, CategoryTheory.Comonad.CofreeEqualizer.topMap_f, CategoryTheory.Comonad.forget_map, CategoryTheory.Comonad.ForgetCreatesLimits'.γ_app, CategoryTheory.coalgebraEquivOver_functor, CategoryTheory.Comonad.forget_faithful, CategoryTheory.comp_comparison_forget_hasColimit, CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone_ι_app, CategoryTheory.Comonad.instIsCoreflexivePairCoalgebraTopMapBottomMap, CategoryTheory.Coreflective.comparison_full, CategoryTheory.Comonad.ForgetCreatesLimits'.newCone_pt, CategoryTheory.Comonad.cofree_obj_A, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_neg_f, isoMk_hom_f, CategoryTheory.Comonad.coalgebra_iso_of_iso, CategoryTheory.instEssSurjCoalgebraToComonadAdjComparison, CategoryTheory.Comonad.cofree_map_f, CategoryTheory.Comonad.ForgetCreatesColimits'.γ_app, CategoryTheory.Comonad.comparisonForget_inv_app, CategoryTheory.Adjunction.adjToComonadIso_hom_toNatTrans_app, CategoryTheory.overToCoalgebra_map_f, CategoryTheory.Comonad.adj_counit, CategoryTheory.Comonad.comparisonForget_hom_app, CategoryTheory.Comonad.ForgetCreatesLimits'.newCone_π, CategoryTheory.coalgebraToOver_obj, CategoryTheory.Comonad.left_comparison, CategoryTheory.coalgebraEquivOver_counitIso, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_nsmul_f, CategoryTheory.instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison, CategoryTheory.Comonad.comparison_map_f, CategoryTheory.Comonad.CofreeEqualizer.ι_f, CategoryTheory.Over.star_map_left, CategoryTheory.Comonad.cofree_obj_a, CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint_a, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zsmul_f, CategoryTheory.overToCoalgebra_obj_A, CategoryTheory.Comonad.forget_obj, CategoryTheory.Comonad.forget_creates_limits_of_comonad_preserves, CategoryTheory.coalgebraToOver_map, CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit_desc_f, CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint_A, CategoryTheory.Comonad.comparison_obj_A, CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint_A, CategoryTheory.Comonad.forget_additive, CategoryTheory.coalgebraEquivOver_inverse, CategoryTheory.overToCoalgebra_obj_a, CategoryTheory.Comonad.CofreeEqualizer.condition, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit, isoMk_inv_f, CategoryTheory.coalgebraEquivOver_unitIso, CategoryTheory.Comonad.algebra_epi_of_epi, CategoryTheory.Comonad.ForgetCreatesLimits'.commuting, CategoryTheory.Comonad.algebra_mono_of_mono, CategoryTheory.Comonad.CofreeEqualizer.bottomMap_f, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_add_f, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_sub_f, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_unit_app, CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit_lift_f, CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone_ι_app_f, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f_aux, CategoryTheory.Comonad.adj_unit, CategoryTheory.Comonad.beckCoalgebraFork_π_app, CategoryTheory.Comonad.instIsLeftAdjointCoalgebraForget, CategoryTheory.instFullCoalgebraToComonadAdjComparison, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zero_f, CategoryTheory.Comonad.forget_reflects_iso, CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone_pt, CategoryTheory.Comonad.hasColimit_of_comp_forget_hasColimit, CategoryTheory.Coreflective.comparison_essSurj
instCategoryStruct 📖	CompOp	7 math math: comp_f, id_eq_id, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f, id_f, CategoryTheory.Comonad.CofreeEqualizer.condition, comp_eq_comp, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply
isoMk 📖	CompOp	3 math math: isoMk_hom_f, isoMk_inv_f, CategoryTheory.coalgebraEquivOver_unitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coassoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct A CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor CategoryTheory.Functor.comp a CategoryTheory.NatTrans.app CategoryTheory.Comonad.δ CategoryTheory.Functor.map	—	—
coassoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct A CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Comonad.δ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coassoc
comp_eq_comp 📖	mathematical	—	Hom.comp CategoryTheory.CategoryStruct.comp CategoryTheory.Comonad.Coalgebra instCategoryStruct	—	—
comp_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.comp CategoryTheory.Comonad.Coalgebra instCategoryStruct CategoryTheory.Category.toCategoryStruct A	—	—
counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct A CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor CategoryTheory.Functor.id a CategoryTheory.NatTrans.app CategoryTheory.Comonad.ε CategoryTheory.CategoryStruct.id	—	—
counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct A CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor a CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Comonad.ε	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' counit
id_eq_id 📖	mathematical	—	Hom.id CategoryTheory.CategoryStruct.id CategoryTheory.Comonad.Coalgebra instCategoryStruct	—	—
id_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.id CategoryTheory.Comonad.Coalgebra instCategoryStruct CategoryTheory.Category.toCategoryStruct A	—	—
isoMk_hom_f 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct A CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor CategoryTheory.CategoryStruct.comp a CategoryTheory.Functor.map CategoryTheory.Iso.hom	Hom.f CategoryTheory.Comonad.Coalgebra eilenbergMoore isoMk	—	—
isoMk_inv_f 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct A CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor CategoryTheory.CategoryStruct.comp a CategoryTheory.Functor.map CategoryTheory.Iso.hom	Hom.f CategoryTheory.Iso.inv CategoryTheory.Comonad.Coalgebra eilenbergMoore isoMk	—	—

CategoryTheory.Comonad.Coalgebra.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	1 math math: CategoryTheory.Comonad.Coalgebra.comp_eq_comp
f 📖	CompOp	32 math math: CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone_π_app_f, CategoryTheory.Comonad.Coalgebra.comp_f, CategoryTheory.Comonad.CofreeEqualizer.topMap_f, CategoryTheory.Comonad.forget_map, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_neg_f, CategoryTheory.Comonad.Coalgebra.isoMk_hom_f, h, CategoryTheory.Comonad.cofree_map_f, CategoryTheory.overToCoalgebra_map_f, CategoryTheory.Comonad.adj_counit, ext_iff, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_nsmul_f, h_assoc, CategoryTheory.Comonad.comparison_map_f, CategoryTheory.Comonad.CofreeEqualizer.ι_f, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zsmul_f, CategoryTheory.coalgebraToOver_map, CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit_desc_f, CategoryTheory.Comonad.Coalgebra.id_f, CategoryTheory.Comonad.Coalgebra.isoMk_inv_f, CategoryTheory.Comonad.CofreeEqualizer.bottomMap_f, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_add_f, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_sub_f, CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit_lift_f, CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone_ι_app_f, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f_aux, CategoryTheory.Comonad.adj_unit, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zero_f, ext'_iff
id 📖	CompOp	1 math math: CategoryTheory.Comonad.Coalgebra.id_eq_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	f	—	—	—
ext' 📖	—	f	—	—	ext
ext'_iff 📖	mathematical	—	f	—	ext'
ext_iff 📖	mathematical	—	f	—	ext
h 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comonad.Coalgebra.A CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor CategoryTheory.Comonad.Coalgebra.a CategoryTheory.Functor.map f	—	—
h_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comonad.Coalgebra.A CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor CategoryTheory.Comonad.Coalgebra.a CategoryTheory.Functor.map f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h

CategoryTheory.Monad

Definitions

Name	Category	Theorems
Algebra 📖	CompData	97 math math: ForgetCreatesColimits.commuting, algebra_iso_of_iso, ForgetCreatesColimits.liftedCocone_pt, free_map_f, forget_reflects_iso, ForgetCreatesLimits.liftedConeIsLimit_lift_f, algebra_mono_of_mono, left_comparison, algebraFunctorOfMonadHom_obj_A, algebraFunctorOfMonadHomId_inv_app_f, forget_creates_colimits_of_monad_preserves, CategoryTheory.comp_comparison_forget_hasLimit, algebraPreadditive_homGroup_sub_f, algebraEquivOfIsoMonads_inverse, algebraFunctorOfMonadHomId_hom_app_f, algebraEquivOfIsoMonads_unitIso, ForgetCreatesLimits.conePoint_a, FreeCoequalizer.condition, Algebra.comp_eq_comp, algebraFunctorOfMonadHomEq_hom_app_f, ForgetCreatesColimits.γ_app, Algebra.id_f, ForgetCreatesLimits.newCone_π_app, algebraPreadditive_homGroup_add_f, CategoryTheory.instFullAlgebraToMonadAdjComparison, comparisonForget_hom_app, algebraFunctorOfMonadHomComp_hom_app_f, MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, Algebra.isoMk_inv_f, comparison_obj_a, beckAlgebraCofork_pt, adj_counit, adj_unit, ForgetCreatesLimits.liftedCone_pt, algebraFunctorOfMonadHomEq_inv_app_f, CategoryTheory.algebraEquivUnder_inverse, CategoryTheory.underToAlgebra_obj_A, algebraEquivOfIsoMonads_functor, CategoryTheory.instEssSurjAlgebraToMonadAdjComparison, hasLimit_of_comp_forget_hasLimit, algebra_equiv_of_iso_monads_comp_forget, comparison_obj_A, free_obj_a, ForgetCreatesColimits.coconePoint_A, CategoryTheory.instFaithfulAlgebraToMonadComparison, forget_faithful, algebraPreadditive_homGroup_zsmul_f, ForgetCreatesColimits.newCocone_pt, MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, CategoryTheory.Adjunction.adjToMonadIso_inv_toNatTrans_app, MonadicityInternal.comparisonAdjunction_unit_f, free_obj_A, FreeCoequalizer.π_f, algebraEquivOfIsoMonads_counitIso, FreeCoequalizer.bottomMap_f, Algebra.id_eq_id, algebra_epi_of_epi, CategoryTheory.algebraEquivUnder_unitIso, algebraPreadditive_homGroup_zero_f, CategoryTheory.underToAlgebra_obj_a, CategoryTheory.algebraToUnder_obj, algebraFunctorOfMonadHom_obj_a, MonadicityInternal.comparisonAdjunction_unit_f_aux, MonadicityInternal.comparisonAdjunction_counit, forget_map, algebraPreadditive_homGroup_nsmul_f, CategoryTheory.algebraEquivUnder_counitIso, CategoryTheory.Reflective.comparison_full, CategoryTheory.comp_comparison_hasLimit, instIsRightAdjointAlgebraForget, ForgetCreatesLimits.conePoint_A, algebraFunctorOfMonadHomComp_inv_app_f, beckAlgebraCofork_ι_app, comparisonForget_inv_app, forget_additive, comparison_map_f, CategoryTheory.underToAlgebra_map_f, ForgetCreatesColimits.liftedCocone_ι_app_f, ForgetCreatesLimits.γ_app, CategoryTheory.MonadicRightAdjoint.eqv, algebraPreadditive_homGroup_neg_f, CategoryTheory.Under.costar_map_left, CategoryTheory.Adjunction.adjToMonadIso_hom_toNatTrans_app, Algebra.isoMk_hom_f, ForgetCreatesLimits.liftedCone_π_app_f, CategoryTheory.Reflective.comparison_essSurj, CategoryTheory.instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison, forget_obj, CategoryTheory.algebraToUnder_map, instIsReflexivePairAlgebraTopMapBottomMap, Algebra.comp_f, CategoryTheory.algebraEquivUnder_functor, MonadicityInternal.comparisonAdjunction_counit_app, ForgetCreatesColimits.liftedCoconeIsColimit_desc_f, algebraFunctorOfMonadHom_map_f, FreeCoequalizer.topMap_f, ForgetCreatesColimits.newCocone_ι
adj 📖	CompOp	6 math math: CategoryTheory.instFullAlgebraToMonadAdjComparison, adj_counit, adj_unit, CategoryTheory.instEssSurjAlgebraToMonadAdjComparison, CategoryTheory.Adjunction.adjToMonadIso_inv_toNatTrans_app, CategoryTheory.Adjunction.adjToMonadIso_hom_toNatTrans_app
algebraEquivOfIsoMonads 📖	CompOp	4 math math: algebraEquivOfIsoMonads_inverse, algebraEquivOfIsoMonads_unitIso, algebraEquivOfIsoMonads_functor, algebraEquivOfIsoMonads_counitIso
algebraFunctorOfMonadHom 📖	CompOp	14 math math: algebraFunctorOfMonadHom_obj_A, algebraFunctorOfMonadHomId_inv_app_f, algebraEquivOfIsoMonads_inverse, algebraFunctorOfMonadHomId_hom_app_f, algebraEquivOfIsoMonads_unitIso, algebraFunctorOfMonadHomEq_hom_app_f, algebraFunctorOfMonadHomComp_hom_app_f, algebraFunctorOfMonadHomEq_inv_app_f, algebraEquivOfIsoMonads_functor, algebra_equiv_of_iso_monads_comp_forget, algebraEquivOfIsoMonads_counitIso, algebraFunctorOfMonadHom_obj_a, algebraFunctorOfMonadHomComp_inv_app_f, algebraFunctorOfMonadHom_map_f
algebraFunctorOfMonadHomComp 📖	CompOp	4 math math: algebraEquivOfIsoMonads_unitIso, algebraFunctorOfMonadHomComp_hom_app_f, algebraEquivOfIsoMonads_counitIso, algebraFunctorOfMonadHomComp_inv_app_f
algebraFunctorOfMonadHomEq 📖	CompOp	4 math math: algebraEquivOfIsoMonads_unitIso, algebraFunctorOfMonadHomEq_hom_app_f, algebraFunctorOfMonadHomEq_inv_app_f, algebraEquivOfIsoMonads_counitIso
algebraFunctorOfMonadHomId 📖	CompOp	4 math math: algebraFunctorOfMonadHomId_inv_app_f, algebraFunctorOfMonadHomId_hom_app_f, algebraEquivOfIsoMonads_unitIso, algebraEquivOfIsoMonads_counitIso
forget 📖	CompOp	29 math math: ForgetCreatesColimits.commuting, forget_reflects_iso, ForgetCreatesLimits.liftedConeIsLimit_lift_f, CategoryTheory.comp_comparison_forget_hasLimit, ForgetCreatesLimits.conePoint_a, ForgetCreatesColimits.γ_app, ForgetCreatesLimits.newCone_π_app, CategoryTheory.instFullAlgebraToMonadAdjComparison, comparisonForget_hom_app, adj_counit, adj_unit, CategoryTheory.instEssSurjAlgebraToMonadAdjComparison, algebra_equiv_of_iso_monads_comp_forget, ForgetCreatesColimits.coconePoint_A, forget_faithful, ForgetCreatesColimits.newCocone_pt, CategoryTheory.Adjunction.adjToMonadIso_inv_toNatTrans_app, forget_map, instIsRightAdjointAlgebraForget, ForgetCreatesLimits.conePoint_A, comparisonForget_inv_app, forget_additive, ForgetCreatesColimits.liftedCocone_ι_app_f, ForgetCreatesLimits.γ_app, CategoryTheory.Adjunction.adjToMonadIso_hom_toNatTrans_app, ForgetCreatesLimits.liftedCone_π_app_f, forget_obj, ForgetCreatesColimits.liftedCoconeIsColimit_desc_f, ForgetCreatesColimits.newCocone_ι
free 📖	CompOp	18 math math: free_map_f, left_comparison, FreeCoequalizer.condition, CategoryTheory.instFullAlgebraToMonadAdjComparison, beckAlgebraCofork_pt, adj_counit, adj_unit, CategoryTheory.instEssSurjAlgebraToMonadAdjComparison, free_obj_a, CategoryTheory.Adjunction.adjToMonadIso_inv_toNatTrans_app, free_obj_A, FreeCoequalizer.π_f, FreeCoequalizer.bottomMap_f, beckAlgebraCofork_ι_app, CategoryTheory.Under.costar_map_left, CategoryTheory.Adjunction.adjToMonadIso_hom_toNatTrans_app, instIsReflexivePairAlgebraTopMapBottomMap, FreeCoequalizer.topMap_f
instInhabitedAlgebra 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adj_counit 📖	mathematical	—	CategoryTheory.Adjunction.counit Algebra Algebra.eilenbergMoore free forget adj CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.obj Algebra.A Algebra.a Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp toFunctor CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.NatTrans.app η Algebra.Hom.f Algebra.Hom	—	CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
adj_unit 📖	mathematical	—	CategoryTheory.Adjunction.unit Algebra Algebra.eilenbergMoore free forget adj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app toFunctor η CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Algebra.Hom.f Algebra.A CategoryTheory.Functor.map Algebra.a CategoryTheory.Category.comp_id	—	CategoryTheory.Category.comp_id
algebraEquivOfIsoMonads_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Algebra Algebra.eilenbergMoore algebraEquivOfIsoMonads CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp algebraFunctorOfMonadHom CategoryTheory.Iso.hom CategoryTheory.Monad CategoryTheory.instCategoryMonad CategoryTheory.Iso.inv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.id CategoryTheory.Iso.symm algebraFunctorOfMonadHomComp CategoryTheory.CategoryStruct.id algebraFunctorOfMonadHomEq algebraFunctorOfMonadHomId	—	—
algebraEquivOfIsoMonads_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Algebra Algebra.eilenbergMoore algebraEquivOfIsoMonads algebraFunctorOfMonadHom CategoryTheory.Iso.inv CategoryTheory.Monad CategoryTheory.instCategoryMonad	—	—
algebraEquivOfIsoMonads_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Algebra Algebra.eilenbergMoore algebraEquivOfIsoMonads algebraFunctorOfMonadHom CategoryTheory.Iso.hom CategoryTheory.Monad CategoryTheory.instCategoryMonad	—	—
algebraEquivOfIsoMonads_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Algebra Algebra.eilenbergMoore algebraEquivOfIsoMonads CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id algebraFunctorOfMonadHom CategoryTheory.CategoryStruct.id CategoryTheory.Monad CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMonad CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Iso.hom CategoryTheory.Iso.symm algebraFunctorOfMonadHomId CategoryTheory.CategoryStruct.comp algebraFunctorOfMonadHomEq algebraFunctorOfMonadHomComp	—	—
algebraFunctorOfMonadHomComp_hom_app_f 📖	mathematical	—	Algebra.Hom.f CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore algebraFunctorOfMonadHom CategoryTheory.CategoryStruct.comp CategoryTheory.Monad CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMonad CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category algebraFunctorOfMonadHomComp Algebra.A CategoryTheory.Iso.refl	—	—
algebraFunctorOfMonadHomComp_inv_app_f 📖	mathematical	—	Algebra.Hom.f CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore CategoryTheory.Functor.comp algebraFunctorOfMonadHom CategoryTheory.CategoryStruct.comp CategoryTheory.Monad CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMonad CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category algebraFunctorOfMonadHomComp Algebra.A CategoryTheory.Iso.refl	—	—
algebraFunctorOfMonadHomEq_hom_app_f 📖	mathematical	—	Algebra.Hom.f CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore algebraFunctorOfMonadHom CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category algebraFunctorOfMonadHomEq Algebra.A CategoryTheory.Iso.refl	—	—
algebraFunctorOfMonadHomEq_inv_app_f 📖	mathematical	—	Algebra.Hom.f CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore algebraFunctorOfMonadHom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category algebraFunctorOfMonadHomEq Algebra.A CategoryTheory.Iso.refl	—	—
algebraFunctorOfMonadHomId_hom_app_f 📖	mathematical	—	Algebra.Hom.f CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore algebraFunctorOfMonadHom CategoryTheory.CategoryStruct.id CategoryTheory.Monad CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMonad CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category algebraFunctorOfMonadHomId Algebra.A CategoryTheory.Iso.refl	—	—
algebraFunctorOfMonadHomId_inv_app_f 📖	mathematical	—	Algebra.Hom.f CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore CategoryTheory.Functor.id algebraFunctorOfMonadHom CategoryTheory.CategoryStruct.id CategoryTheory.Monad CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMonad CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category algebraFunctorOfMonadHomId Algebra.A CategoryTheory.Iso.refl	—	—
algebraFunctorOfMonadHom_map_f 📖	mathematical	—	Algebra.Hom.f Algebra.A CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.MonadHom.toNatTrans Algebra.a CategoryTheory.Functor.map Algebra Algebra.eilenbergMoore algebraFunctorOfMonadHom	—	—
algebraFunctorOfMonadHom_obj_A 📖	mathematical	—	Algebra.A CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore algebraFunctorOfMonadHom	—	—
algebraFunctorOfMonadHom_obj_a 📖	mathematical	—	Algebra.a CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore algebraFunctorOfMonadHom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct toFunctor Algebra.A CategoryTheory.NatTrans.app CategoryTheory.MonadHom.toNatTrans	—	—
algebra_epi_of_epi 📖	mathematical	—	CategoryTheory.Epi Algebra Algebra.eilenbergMoore	—	CategoryTheory.Functor.epi_of_epi_map CategoryTheory.Functor.reflectsEpimorphisms_of_faithful forget_faithful
algebra_equiv_of_iso_monads_comp_forget 📖	mathematical	—	CategoryTheory.Functor.comp Algebra Algebra.eilenbergMoore algebraFunctorOfMonadHom forget	—	—
algebra_iso_of_iso 📖	mathematical	—	CategoryTheory.IsIso Algebra Algebra.eilenbergMoore	—	CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.Category.assoc Algebra.Hom.h Algebra.Hom.ext' CategoryTheory.IsIso.hom_inv_id CategoryTheory.IsIso.inv_hom_id
algebra_mono_of_mono 📖	mathematical	—	CategoryTheory.Mono Algebra Algebra.eilenbergMoore	—	CategoryTheory.Functor.mono_of_mono_map CategoryTheory.Functor.reflectsMonomorphisms_of_faithful forget_faithful
forget_faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful Algebra Algebra.eilenbergMoore forget	—	Algebra.Hom.ext'
forget_map 📖	mathematical	—	CategoryTheory.Functor.map Algebra Algebra.eilenbergMoore forget Algebra.Hom.f	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore forget Algebra.A	—	—
forget_reflects_iso 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms Algebra Algebra.eilenbergMoore forget	—	algebra_iso_of_iso
free_map_f 📖	mathematical	—	Algebra.Hom.f CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp μ CategoryTheory.Functor.map Algebra Algebra.eilenbergMoore free	—	—
free_obj_A 📖	mathematical	—	Algebra.A CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore free toFunctor	—	—
free_obj_a 📖	mathematical	—	Algebra.a CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore free CategoryTheory.NatTrans.app CategoryTheory.Functor.comp toFunctor μ	—	—
instIsRightAdjointAlgebraForget 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint Algebra Algebra.eilenbergMoore forget	—	—

CategoryTheory.Monad.Algebra

Definitions

Name	Category	Theorems
A 📖	CompOp	67 math math: CategoryTheory.Monad.ForgetCreatesColimits.commuting, unit_assoc, CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_A, Hom.h, CategoryTheory.Monad.algebraFunctorOfMonadHomId_inv_app_f, CategoryTheory.Monad.algebraPreadditive_homGroup_sub_f, CategoryTheory.Monad.beckCoequalizer_desc, Compactum.instT2SpaceA, CategoryTheory.Monad.algebraFunctorOfMonadHomId_hom_app_f, assoc_assoc, CategoryTheory.Monad.FreeCoequalizer.condition, CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair, CategoryTheory.Monad.algebraFunctorOfMonadHomEq_hom_app_f, id_f, CategoryTheory.Monad.ForgetCreatesLimits.newCone_π_app, CategoryTheory.Monad.algebraPreadditive_homGroup_add_f, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair, Compactum.cl_eq_closure, CategoryTheory.Monad.algebraFunctorOfMonadHomComp_hom_app_f, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, Compactum.instCompactSpaceA, CategoryTheory.Monad.beckAlgebraCofork_pt, CategoryTheory.Monad.adj_counit, CategoryTheory.Monad.adj_unit, Compactum.le_nhds_of_str_eq, Compactum.lim_eq_str, CategoryTheory.Monad.algebraFunctorOfMonadHomEq_inv_app_f, CategoryTheory.Monad.MonadicityInternal.unitCofork_π, CategoryTheory.underToAlgebra_obj_A, assoc, CategoryTheory.Monad.comparison_obj_A, CategoryTheory.Monad.beckCofork_pt, CategoryTheory.Monad.instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair, CategoryTheory.Monad.ForgetCreatesColimits.coconePoint_A, CategoryTheory.Monad.algebraPreadditive_homGroup_zsmul_f, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, CategoryTheory.Monad.free_obj_A, CategoryTheory.Monad.FreeCoequalizer.π_f, CategoryTheory.Monad.FreeCoequalizer.bottomMap_f, Compactum.continuous_of_hom, CategoryTheory.algebraEquivUnder_unitIso, CategoryTheory.Monad.algebraPreadditive_homGroup_zero_f, CategoryTheory.algebraToUnder_obj, CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_a, CategoryTheory.Monad.beckCofork_π, CategoryTheory.Monad.algebraPreadditive_homGroup_nsmul_f, CategoryTheory.Monad.MonadicityInternal.unitCofork_pt, CategoryTheory.Monad.ForgetCreatesLimits.conePoint_A, CategoryTheory.Monad.algebraFunctorOfMonadHomComp_inv_app_f, CategoryTheory.Monad.beckAlgebraCofork_ι_app, Compactum.str_hom_commute, CategoryTheory.Monad.algebraPreadditive_homGroup_neg_f, CategoryTheory.Monad.MonadicityInternal.main_pair_G_split, CategoryTheory.Monad.MonadicityInternal.main_pair_reflexive, CategoryTheory.Monad.forget_obj, CategoryTheory.algebraToUnder_map, CategoryTheory.Monad.instIsReflexivePairAlgebraTopMapBottomMap, comp_f, unit, Compactum.isClosed_iff, Compactum.isClosed_cl, Hom.h_assoc, CategoryTheory.Reflective.instIsIsoAppUnitReflectorAdjunctionA, Compactum.join_distrib, CategoryTheory.Monad.algebraFunctorOfMonadHom_map_f, CategoryTheory.Monad.FreeCoequalizer.topMap_f
a 📖	CompOp	36 math math: CategoryTheory.Monad.ForgetCreatesColimits.commuting, CategoryTheory.Monad.ForgetCreatesColimits.coconePoint_a, unit_assoc, Hom.h, CategoryTheory.Monad.beckCoequalizer_desc, assoc_assoc, CategoryTheory.Monad.ForgetCreatesLimits.conePoint_a, CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair, CategoryTheory.Monad.ForgetCreatesColimits.γ_app, CategoryTheory.Monad.ForgetCreatesLimits.newCone_π_app, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, CategoryTheory.Monad.comparison_obj_a, CategoryTheory.Monad.adj_counit, CategoryTheory.Monad.adj_unit, CategoryTheory.Monad.MonadicityInternal.unitCofork_π, assoc, CategoryTheory.Monad.beckCofork_pt, CategoryTheory.Monad.instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair, CategoryTheory.Monad.free_obj_a, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, CategoryTheory.Monad.FreeCoequalizer.π_f, CategoryTheory.underToAlgebra_obj_a, CategoryTheory.algebraToUnder_obj, CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_a, CategoryTheory.Monad.beckCofork_π, CategoryTheory.Monad.MonadicityInternal.unitCofork_pt, CategoryTheory.Monad.ForgetCreatesLimits.γ_app, CategoryTheory.Monad.MonadicityInternal.main_pair_G_split, CategoryTheory.Monad.MonadicityInternal.main_pair_reflexive, CategoryTheory.algebraToUnder_map, unit, Hom.h_assoc, CategoryTheory.Monad.algebraFunctorOfMonadHom_map_f, CategoryTheory.Monad.FreeCoequalizer.topMap_f
eilenbergMoore 📖	CompOp	93 math math: CategoryTheory.Monad.ForgetCreatesColimits.commuting, CategoryTheory.Monad.algebra_iso_of_iso, CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_pt, CategoryTheory.Monad.free_map_f, CategoryTheory.Monad.forget_reflects_iso, CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit_lift_f, CategoryTheory.Monad.algebra_mono_of_mono, CategoryTheory.Monad.left_comparison, CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_A, CategoryTheory.Monad.algebraFunctorOfMonadHomId_inv_app_f, CategoryTheory.Monad.forget_creates_colimits_of_monad_preserves, CategoryTheory.comp_comparison_forget_hasLimit, CategoryTheory.Monad.algebraPreadditive_homGroup_sub_f, CategoryTheory.Monad.algebraEquivOfIsoMonads_inverse, CategoryTheory.Monad.algebraFunctorOfMonadHomId_hom_app_f, CategoryTheory.Monad.algebraEquivOfIsoMonads_unitIso, CategoryTheory.Monad.ForgetCreatesLimits.conePoint_a, CategoryTheory.Monad.FreeCoequalizer.condition, CategoryTheory.Monad.algebraFunctorOfMonadHomEq_hom_app_f, CategoryTheory.Monad.ForgetCreatesColimits.γ_app, CategoryTheory.Monad.ForgetCreatesLimits.newCone_π_app, CategoryTheory.Monad.algebraPreadditive_homGroup_add_f, CategoryTheory.instFullAlgebraToMonadAdjComparison, CategoryTheory.Monad.comparisonForget_hom_app, CategoryTheory.Monad.algebraFunctorOfMonadHomComp_hom_app_f, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, isoMk_inv_f, CategoryTheory.Monad.comparison_obj_a, CategoryTheory.Monad.beckAlgebraCofork_pt, CategoryTheory.Monad.adj_counit, CategoryTheory.Monad.adj_unit, CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_pt, CategoryTheory.Monad.algebraFunctorOfMonadHomEq_inv_app_f, CategoryTheory.algebraEquivUnder_inverse, CategoryTheory.underToAlgebra_obj_A, CategoryTheory.Monad.algebraEquivOfIsoMonads_functor, CategoryTheory.instEssSurjAlgebraToMonadAdjComparison, CategoryTheory.Monad.hasLimit_of_comp_forget_hasLimit, CategoryTheory.Monad.algebra_equiv_of_iso_monads_comp_forget, CategoryTheory.Monad.comparison_obj_A, CategoryTheory.Monad.free_obj_a, CategoryTheory.Monad.ForgetCreatesColimits.coconePoint_A, CategoryTheory.instFaithfulAlgebraToMonadComparison, CategoryTheory.Monad.forget_faithful, CategoryTheory.Monad.algebraPreadditive_homGroup_zsmul_f, CategoryTheory.Monad.ForgetCreatesColimits.newCocone_pt, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, CategoryTheory.Adjunction.adjToMonadIso_inv_toNatTrans_app, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f, CategoryTheory.Monad.free_obj_A, CategoryTheory.Monad.FreeCoequalizer.π_f, CategoryTheory.Monad.algebraEquivOfIsoMonads_counitIso, CategoryTheory.Monad.FreeCoequalizer.bottomMap_f, CategoryTheory.Monad.algebra_epi_of_epi, CategoryTheory.algebraEquivUnder_unitIso, CategoryTheory.Monad.algebraPreadditive_homGroup_zero_f, CategoryTheory.underToAlgebra_obj_a, CategoryTheory.algebraToUnder_obj, CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_a, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit, CategoryTheory.Monad.forget_map, CategoryTheory.Monad.algebraPreadditive_homGroup_nsmul_f, CategoryTheory.algebraEquivUnder_counitIso, CategoryTheory.Reflective.comparison_full, CategoryTheory.comp_comparison_hasLimit, CategoryTheory.Monad.instIsRightAdjointAlgebraForget, CategoryTheory.Monad.ForgetCreatesLimits.conePoint_A, CategoryTheory.Monad.algebraFunctorOfMonadHomComp_inv_app_f, CategoryTheory.Monad.beckAlgebraCofork_ι_app, CategoryTheory.Monad.comparisonForget_inv_app, CategoryTheory.Monad.forget_additive, CategoryTheory.Monad.comparison_map_f, CategoryTheory.underToAlgebra_map_f, CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_ι_app_f, CategoryTheory.Monad.ForgetCreatesLimits.γ_app, CategoryTheory.MonadicRightAdjoint.eqv, CategoryTheory.Monad.algebraPreadditive_homGroup_neg_f, CategoryTheory.Under.costar_map_left, CategoryTheory.Adjunction.adjToMonadIso_hom_toNatTrans_app, isoMk_hom_f, CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_π_app_f, CategoryTheory.Reflective.comparison_essSurj, CategoryTheory.instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison, CategoryTheory.Monad.forget_obj, CategoryTheory.algebraToUnder_map, CategoryTheory.Monad.instIsReflexivePairAlgebraTopMapBottomMap, CategoryTheory.algebraEquivUnder_functor, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit_app, CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit_desc_f, CategoryTheory.Monad.algebraFunctorOfMonadHom_map_f, CategoryTheory.Monad.FreeCoequalizer.topMap_f, CategoryTheory.Monad.ForgetCreatesColimits.newCocone_ι
instCategoryStruct 📖	CompOp	7 math math: CategoryTheory.Monad.FreeCoequalizer.condition, comp_eq_comp, id_f, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, id_eq_id, comp_f
isoMk 📖	CompOp	3 math math: isoMk_inv_f, CategoryTheory.algebraEquivUnder_unitIso, isoMk_hom_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Monad.toFunctor A CategoryTheory.NatTrans.app CategoryTheory.Monad.μ a CategoryTheory.Functor.map	—	—
assoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor A CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Monad.μ a CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' assoc
comp_eq_comp 📖	mathematical	—	Hom.comp CategoryTheory.CategoryStruct.comp CategoryTheory.Monad.Algebra instCategoryStruct	—	—
comp_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.comp CategoryTheory.Monad.Algebra instCategoryStruct CategoryTheory.Category.toCategoryStruct A	—	—
id_eq_id 📖	mathematical	—	Hom.id CategoryTheory.CategoryStruct.id CategoryTheory.Monad.Algebra instCategoryStruct	—	—
id_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.id CategoryTheory.Monad.Algebra instCategoryStruct CategoryTheory.Category.toCategoryStruct A	—	—
isoMk_hom_f 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor A CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Iso.hom a	Hom.f CategoryTheory.Monad.Algebra eilenbergMoore isoMk	—	—
isoMk_inv_f 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor A CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Iso.hom a	Hom.f CategoryTheory.Iso.inv CategoryTheory.Monad.Algebra eilenbergMoore isoMk	—	—
unit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id A CategoryTheory.Monad.toFunctor CategoryTheory.NatTrans.app CategoryTheory.Monad.η a CategoryTheory.CategoryStruct.id	—	—
unit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct A CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Monad.η a	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' unit

CategoryTheory.Monad.Algebra.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	1 math math: CategoryTheory.Monad.Algebra.comp_eq_comp
f 📖	CompOp	40 math math: CategoryTheory.Monad.free_map_f, CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit_lift_f, h, CategoryTheory.Monad.algebraFunctorOfMonadHomId_inv_app_f, CategoryTheory.Monad.algebraPreadditive_homGroup_sub_f, CategoryTheory.Monad.algebraFunctorOfMonadHomId_hom_app_f, ext_iff, CategoryTheory.Monad.algebraFunctorOfMonadHomEq_hom_app_f, CategoryTheory.Monad.Algebra.id_f, CategoryTheory.Monad.algebraPreadditive_homGroup_add_f, CategoryTheory.Monad.algebraFunctorOfMonadHomComp_hom_app_f, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, CategoryTheory.Monad.Algebra.isoMk_inv_f, CategoryTheory.Monad.adj_counit, CategoryTheory.Monad.adj_unit, CategoryTheory.Monad.algebraFunctorOfMonadHomEq_inv_app_f, CategoryTheory.Monad.algebraPreadditive_homGroup_zsmul_f, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f, CategoryTheory.Monad.FreeCoequalizer.π_f, CategoryTheory.Monad.FreeCoequalizer.bottomMap_f, CategoryTheory.Monad.algebraPreadditive_homGroup_zero_f, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit, CategoryTheory.Monad.forget_map, CategoryTheory.Monad.algebraPreadditive_homGroup_nsmul_f, CategoryTheory.Monad.algebraFunctorOfMonadHomComp_inv_app_f, CategoryTheory.Monad.comparison_map_f, CategoryTheory.underToAlgebra_map_f, CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_ι_app_f, CategoryTheory.Monad.algebraPreadditive_homGroup_neg_f, CategoryTheory.Monad.Algebra.isoMk_hom_f, CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_π_app_f, CategoryTheory.algebraToUnder_map, CategoryTheory.Monad.Algebra.comp_f, ext'_iff, CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit_desc_f, h_assoc, CategoryTheory.Monad.algebraFunctorOfMonadHom_map_f, CategoryTheory.Monad.FreeCoequalizer.topMap_f
id 📖	CompOp	1 math math: CategoryTheory.Monad.Algebra.id_eq_id
instInhabited 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	f	—	—	—
ext' 📖	—	f	—	—	ext
ext'_iff 📖	mathematical	—	f	—	ext'
ext_iff 📖	mathematical	—	f	—	ext
h 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Monad.Algebra.A CategoryTheory.Functor.map f CategoryTheory.Monad.Algebra.a	—	—
h_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Monad.Algebra.A CategoryTheory.Functor.map f CategoryTheory.Monad.Algebra.a	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h

---

← Back to Index