Adjunction

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

Statistics

Metric	Count
Definitions adjToComonadIso, adjToMonadIso, counitAsIsoOfIso, fullyFaithfulLOfCompIsoId, fullyFaithfulROfCompIsoId, toComonad, toMonad, unitAsIsoOfIso, comparison, comparisonForget, ComonadicLeftAdjoint, R, adj, comparison, comparisonForget, MonadicRightAdjoint, L, adj, comonadicAdjunction, comonadicOfCoreflective, comonadicRightAdjoint, instComonadicLeftAdjointCoalgebraForget, instMonadicRightAdjointAlgebraForget, monadicAdjunction, monadicLeftAdjoint, monadicOfReflective	26
Theorems adjToComonadIso_hom_toNatTrans_app, adjToComonadIso_inv_toNatTrans_app, adjToMonadIso_hom_toNatTrans_app, adjToMonadIso_inv_toNatTrans_app, isIso_counit_of_iso, isIso_unit_of_iso, toComonad_coe, toComonad_δ, toComonad_ε, toMonad_coe, toMonad_η, toMonad_μ, comparisonForget_hom_app, comparisonForget_inv_app, comparison_faithful_of_faithful, comparison_map_f, comparison_obj_A, comparison_obj_a, left_comparison, eqv, comparison_essSurj, comparison_full, instIsIsoAppCounitCoreflectorAdjunctionA, comparisonForget_hom_app, comparisonForget_inv_app, comparison_map_f, comparison_obj_A, comparison_obj_a, left_comparison, eqv, comparison_essSurj, comparison_full, instIsIsoAppUnitReflectorAdjunctionA, instEssSurjAlgebraToMonadAdjComparison, instEssSurjCoalgebraToComonadAdjComparison, instFaithfulAlgebraToMonadComparison, instFullAlgebraToMonadAdjComparison, instFullCoalgebraToComonadAdjComparison, instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison, instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison, instIsLeftAdjointOfComonadicLeftAdjoint, instIsRightAdjointOfMonadicRightAdjoint, δ_iso_of_coreflective, μ_iso_of_reflective	44
Total	70

CategoryTheory

Definitions

Name	Category	Theorems
ComonadicLeftAdjoint 📖	CompData	—
MonadicRightAdjoint 📖	CompData	—
comonadicAdjunction 📖	CompOp	3 math math: comp_comparison_hasColimit, comp_comparison_forget_hasColimit, instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison
comonadicOfCoreflective 📖	CompOp	1 math math: rightAdjoint_preservesInitial_of_coreflective
comonadicRightAdjoint 📖	CompOp	4 math math: comp_comparison_hasColimit, comp_comparison_forget_hasColimit, instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison, rightAdjoint_preservesInitial_of_coreflective
instComonadicLeftAdjointCoalgebraForget 📖	CompOp	—
instMonadicRightAdjointAlgebraForget 📖	CompOp	—
monadicAdjunction 📖	CompOp	3 math math: comp_comparison_forget_hasLimit, comp_comparison_hasLimit, instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison
monadicLeftAdjoint 📖	CompOp	4 math math: comp_comparison_forget_hasLimit, leftAdjoint_preservesTerminal_of_reflective, comp_comparison_hasLimit, instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison
monadicOfReflective 📖	CompOp	1 math math: leftAdjoint_preservesTerminal_of_reflective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEssSurjAlgebraToMonadAdjComparison 📖	mathematical	—	Functor.EssSurj Monad.Algebra Adjunction.toMonad Monad.Algebra.eilenbergMoore Monad.free Monad.forget Monad.adj Monad.comparison	—	Category.comp_id Monad.adj_unit Monad.Algebra.unit Functor.map_id Category.id_comp Monad.adj_counit Monad.Algebra.assoc
instEssSurjCoalgebraToComonadAdjComparison 📖	mathematical	—	Functor.EssSurj Comonad.Coalgebra Adjunction.toComonad Comonad.Coalgebra.eilenbergMoore Comonad.forget Comonad.cofree Comonad.adj Comonad.comparison	—	Category.id_comp Comonad.adj_counit Comonad.Coalgebra.counit Functor.map_id Category.comp_id Comonad.adj_unit Comonad.Coalgebra.coassoc
instFaithfulAlgebraToMonadComparison 📖	mathematical	—	Functor.Faithful Monad.Algebra Adjunction.toMonad Monad.Algebra.eilenbergMoore Monad.comparison	—	Functor.map_injective
instFullAlgebraToMonadAdjComparison 📖	mathematical	—	Functor.Full Monad.Algebra Monad.Algebra.eilenbergMoore Adjunction.toMonad Monad.free Monad.forget Monad.adj Monad.comparison	—	Functor.map_id Category.id_comp Monad.adj_counit Monad.Algebra.Hom.h
instFullCoalgebraToComonadAdjComparison 📖	mathematical	—	Functor.Full Comonad.Coalgebra Comonad.Coalgebra.eilenbergMoore Adjunction.toComonad Comonad.forget Comonad.cofree Comonad.adj Comonad.comparison	—	Functor.map_id Category.comp_id Comonad.adj_unit Comonad.Coalgebra.Hom.h
instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison 📖	mathematical	—	Functor.IsEquivalence Monad.Algebra Adjunction.toMonad monadicLeftAdjoint monadicAdjunction Monad.Algebra.eilenbergMoore Monad.comparison	—	MonadicRightAdjoint.eqv
instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison 📖	mathematical	—	Functor.IsEquivalence Comonad.Coalgebra Adjunction.toComonad comonadicRightAdjoint comonadicAdjunction Comonad.Coalgebra.eilenbergMoore Comonad.comparison	—	ComonadicLeftAdjoint.eqv
instIsLeftAdjointOfComonadicLeftAdjoint 📖	mathematical	—	Functor.IsLeftAdjoint	—	Adjunction.isLeftAdjoint
instIsRightAdjointOfMonadicRightAdjoint 📖	mathematical	—	Functor.IsRightAdjoint	—	Adjunction.isRightAdjoint
δ_iso_of_coreflective 📖	mathematical	—	IsIso Functor Functor.category Comonad.toFunctor Adjunction.toComonad coreflector coreflectorAdjunction Functor.comp Comonad.δ	—	Functor.isIso_whiskerRight Functor.isIso_whiskerLeft Adjunction.unit_isIso_of_L_fully_faithful Coreflective.toFull Coreflective.toFaithful
μ_iso_of_reflective 📖	mathematical	—	IsIso Functor Functor.category Functor.comp Monad.toFunctor Adjunction.toMonad reflector reflectorAdjunction Monad.μ	—	Functor.isIso_whiskerRight Functor.isIso_whiskerLeft Adjunction.counit_isIso_of_R_fully_faithful Reflective.toFull Reflective.toFaithful

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
adjToComonadIso 📖	CompOp	2 math math: adjToComonadIso_inv_toNatTrans_app, adjToComonadIso_hom_toNatTrans_app
adjToMonadIso 📖	CompOp	2 math math: adjToMonadIso_inv_toNatTrans_app, adjToMonadIso_hom_toNatTrans_app
counitAsIsoOfIso 📖	CompOp	—
fullyFaithfulLOfCompIsoId 📖	CompOp	—
fullyFaithfulROfCompIsoId 📖	CompOp	—
toComonad 📖	CompOp	32 math math: adjToComonadIso_inv_toNatTrans_app, CategoryTheory.Comonad.comparison_faithful_of_faithful, CategoryTheory.ComonadicLeftAdjoint.eqv, CategoryTheory.comp_comparison_hasColimit, CategoryTheory.Comonad.comparison_obj_a, CategoryTheory.comp_comparison_forget_hasColimit, CategoryTheory.Coreflective.comparison_full, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair, toComonad_δ, CategoryTheory.Comonad.ComonadicityInternal.unitFork_ι, toComonad_ε, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair, CategoryTheory.instEssSurjCoalgebraToComonadAdjComparison, CategoryTheory.Comonad.comparisonForget_inv_app, adjToComonadIso_hom_toNatTrans_app, CategoryTheory.Comonad.comparisonForget_hom_app, CategoryTheory.Comonad.left_comparison, CategoryTheory.Coreflective.instIsIsoAppCounitCoreflectorAdjunctionA, CategoryTheory.instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison, CategoryTheory.Comonad.comparison_map_f, CategoryTheory.Comonad.ComonadicityInternal.main_pair_coreflexive, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f, CategoryTheory.δ_iso_of_coreflective, CategoryTheory.Comonad.comparison_obj_A, CategoryTheory.Comonad.ComonadicityInternal.main_pair_F_cosplit, CategoryTheory.Comonad.instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair, toComonad_coe, CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair, CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt, CategoryTheory.instFullCoalgebraToComonadAdjComparison, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply, CategoryTheory.Coreflective.comparison_essSurj
toMonad 📖	CompOp	32 math math: CategoryTheory.Monad.left_comparison, CategoryTheory.comp_comparison_forget_hasLimit, CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair, CategoryTheory.instFullAlgebraToMonadAdjComparison, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair, CategoryTheory.Monad.comparisonForget_hom_app, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, CategoryTheory.Monad.comparison_obj_a, toMonad_η, CategoryTheory.Monad.MonadicityInternal.unitCofork_π, toMonad_μ, CategoryTheory.instEssSurjAlgebraToMonadAdjComparison, CategoryTheory.Monad.comparison_obj_A, CategoryTheory.Monad.instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair, CategoryTheory.instFaithfulAlgebraToMonadComparison, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, adjToMonadIso_inv_toNatTrans_app, CategoryTheory.Monad.MonadicityInternal.unitCofork_pt, CategoryTheory.Reflective.comparison_full, CategoryTheory.comp_comparison_hasLimit, CategoryTheory.Monad.comparisonForget_inv_app, CategoryTheory.Monad.comparison_map_f, toMonad_coe, CategoryTheory.μ_iso_of_reflective, CategoryTheory.MonadicRightAdjoint.eqv, adjToMonadIso_hom_toNatTrans_app, CategoryTheory.Monad.MonadicityInternal.main_pair_G_split, CategoryTheory.Reflective.comparison_essSurj, CategoryTheory.Monad.MonadicityInternal.main_pair_reflexive, CategoryTheory.instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison, CategoryTheory.Reflective.instIsIsoAppUnitReflectorAdjunctionA
unitAsIsoOfIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjToComonadIso_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comonad.toFunctor toComonad CategoryTheory.Comonad.Coalgebra CategoryTheory.Comonad.Coalgebra.eilenbergMoore CategoryTheory.Comonad.forget CategoryTheory.Comonad.cofree CategoryTheory.Comonad.adj CategoryTheory.ComonadHom.toNatTrans CategoryTheory.Iso.hom CategoryTheory.Comonad CategoryTheory.instCategoryComonad adjToComonadIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
adjToComonadIso_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comonad.toFunctor toComonad CategoryTheory.Comonad.Coalgebra CategoryTheory.Comonad.Coalgebra.eilenbergMoore CategoryTheory.Comonad.forget CategoryTheory.Comonad.cofree CategoryTheory.Comonad.adj CategoryTheory.ComonadHom.toNatTrans CategoryTheory.Iso.inv CategoryTheory.Comonad CategoryTheory.instCategoryComonad adjToComonadIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
adjToMonadIso_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Monad.toFunctor toMonad CategoryTheory.Monad.Algebra CategoryTheory.Monad.Algebra.eilenbergMoore CategoryTheory.Monad.free CategoryTheory.Monad.forget CategoryTheory.Monad.adj CategoryTheory.MonadHom.toNatTrans CategoryTheory.Iso.hom CategoryTheory.Monad CategoryTheory.instCategoryMonad adjToMonadIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
adjToMonadIso_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Monad.toFunctor toMonad CategoryTheory.Monad.Algebra CategoryTheory.Monad.Algebra.eilenbergMoore CategoryTheory.Monad.free CategoryTheory.Monad.forget CategoryTheory.Monad.adj CategoryTheory.MonadHom.toNatTrans CategoryTheory.Iso.inv CategoryTheory.Monad CategoryTheory.instCategoryMonad adjToMonadIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
isIso_counit_of_iso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	CategoryTheory.Iso.isIso_hom
isIso_unit_of_iso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	—	CategoryTheory.Iso.isIso_hom
toComonad_coe 📖	mathematical	—	CategoryTheory.Comonad.toFunctor toComonad CategoryTheory.Functor.comp	—	—
toComonad_δ 📖	mathematical	—	CategoryTheory.Comonad.δ toComonad CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerLeft unit	—	—
toComonad_ε 📖	mathematical	—	CategoryTheory.Comonad.ε toComonad counit	—	—
toMonad_coe 📖	mathematical	—	CategoryTheory.Monad.toFunctor toMonad CategoryTheory.Functor.comp	—	—
toMonad_η 📖	mathematical	—	CategoryTheory.Monad.η toMonad unit	—	—
toMonad_μ 📖	mathematical	—	CategoryTheory.Monad.μ toMonad CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerLeft counit	—	—

CategoryTheory.Comonad

Definitions

Name	Category	Theorems
comparison 📖	CompOp	21 math math: comparison_faithful_of_faithful, CategoryTheory.ComonadicLeftAdjoint.eqv, CategoryTheory.comp_comparison_hasColimit, comparison_obj_a, CategoryTheory.comp_comparison_forget_hasColimit, CategoryTheory.Coreflective.comparison_full, ComonadicityInternal.comparisonAdjunction_counit_f, CategoryTheory.instEssSurjCoalgebraToComonadAdjComparison, comparisonForget_inv_app, comparisonForget_hom_app, left_comparison, CategoryTheory.instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison, comparison_map_f, ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f, comparison_obj_A, ComonadicityInternal.comparisonAdjunction_counit, ComonadicityInternal.comparisonAdjunction_unit_app, ComonadicityInternal.comparisonAdjunction_counit_f_aux, CategoryTheory.instFullCoalgebraToComonadAdjComparison, ComonadicityInternal.comparisonRightAdjointHomEquiv_apply, CategoryTheory.Coreflective.comparison_essSurj
comparisonForget 📖	CompOp	2 math math: comparisonForget_inv_app, comparisonForget_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comparisonForget_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp Coalgebra CategoryTheory.Adjunction.toComonad Coalgebra.eilenbergMoore comparison forget CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category comparisonForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
comparisonForget_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp Coalgebra CategoryTheory.Adjunction.toComonad Coalgebra.eilenbergMoore comparison forget CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category comparisonForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
comparison_faithful_of_faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful Coalgebra CategoryTheory.Adjunction.toComonad Coalgebra.eilenbergMoore comparison	—	CategoryTheory.Functor.map_injective
comparison_map_f 📖	mathematical	—	Coalgebra.Hom.f CategoryTheory.Adjunction.toComonad CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit Coalgebra Coalgebra.eilenbergMoore comparison	—	—
comparison_obj_A 📖	mathematical	—	Coalgebra.A CategoryTheory.Adjunction.toComonad CategoryTheory.Functor.obj Coalgebra Coalgebra.eilenbergMoore comparison	—	—
comparison_obj_a 📖	mathematical	—	Coalgebra.a CategoryTheory.Adjunction.toComonad CategoryTheory.Functor.obj Coalgebra Coalgebra.eilenbergMoore comparison CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit	—	—
left_comparison 📖	mathematical	—	CategoryTheory.Functor.comp Coalgebra CategoryTheory.Adjunction.toComonad Coalgebra.eilenbergMoore comparison cofree	—	—

CategoryTheory.ComonadicLeftAdjoint

Definitions

Name	Category	Theorems
R 📖	CompOp	1 math math: eqv
adj 📖	CompOp	1 math math: eqv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqv 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.Comonad.Coalgebra CategoryTheory.Adjunction.toComonad R adj CategoryTheory.Comonad.Coalgebra.eilenbergMoore CategoryTheory.Comonad.comparison	—	—

CategoryTheory.Coreflective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comparison_essSurj 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.Comonad.Coalgebra CategoryTheory.Adjunction.toComonad CategoryTheory.coreflector CategoryTheory.coreflectorAdjunction CategoryTheory.Comonad.Coalgebra.eilenbergMoore CategoryTheory.Comonad.comparison	—	instIsIsoAppCounitCoreflectorAdjunctionA CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Category.assoc CategoryTheory.Adjunction.counit_naturality CategoryTheory.Adjunction.left_triangle_components_assoc CategoryTheory.Category.comp_id CategoryTheory.whisker_eq CategoryTheory.Comonad.Coalgebra.counit
comparison_full 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Comonad.Coalgebra CategoryTheory.Adjunction.toComonad CategoryTheory.Comonad.Coalgebra.eilenbergMoore CategoryTheory.Comonad.comparison	—	CategoryTheory.Comonad.Coalgebra.Hom.ext' CategoryTheory.Functor.map_preimage
instIsIsoAppCounitCoreflectorAdjunctionA 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.coreflector CategoryTheory.Comonad.Coalgebra.A CategoryTheory.Adjunction.toComonad CategoryTheory.coreflectorAdjunction CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit	—	CategoryTheory.Adjunction.counit_naturality CategoryTheory.counit_obj_eq_map_counit CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_id CategoryTheory.Comonad.Coalgebra.counit

CategoryTheory.Monad

Definitions

Name	Category	Theorems
comparison 📖	CompOp	21 math math: left_comparison, CategoryTheory.comp_comparison_forget_hasLimit, CategoryTheory.instFullAlgebraToMonadAdjComparison, comparisonForget_hom_app, MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, comparison_obj_a, CategoryTheory.instEssSurjAlgebraToMonadAdjComparison, comparison_obj_A, CategoryTheory.instFaithfulAlgebraToMonadComparison, MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, MonadicityInternal.comparisonAdjunction_unit_f, MonadicityInternal.comparisonAdjunction_unit_f_aux, MonadicityInternal.comparisonAdjunction_counit, CategoryTheory.Reflective.comparison_full, CategoryTheory.comp_comparison_hasLimit, comparisonForget_inv_app, comparison_map_f, CategoryTheory.MonadicRightAdjoint.eqv, CategoryTheory.Reflective.comparison_essSurj, CategoryTheory.instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison, MonadicityInternal.comparisonAdjunction_counit_app
comparisonForget 📖	CompOp	2 math math: comparisonForget_hom_app, comparisonForget_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comparisonForget_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp Algebra CategoryTheory.Adjunction.toMonad Algebra.eilenbergMoore comparison forget CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category comparisonForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
comparisonForget_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp Algebra CategoryTheory.Adjunction.toMonad Algebra.eilenbergMoore comparison forget CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category comparisonForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
comparison_map_f 📖	mathematical	—	Algebra.Hom.f CategoryTheory.Adjunction.toMonad CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit Algebra Algebra.eilenbergMoore comparison	—	—
comparison_obj_A 📖	mathematical	—	Algebra.A CategoryTheory.Adjunction.toMonad CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore comparison	—	—
comparison_obj_a 📖	mathematical	—	Algebra.a CategoryTheory.Adjunction.toMonad CategoryTheory.Functor.obj Algebra Algebra.eilenbergMoore comparison CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit	—	—
left_comparison 📖	mathematical	—	CategoryTheory.Functor.comp Algebra CategoryTheory.Adjunction.toMonad Algebra.eilenbergMoore comparison free	—	—

CategoryTheory.MonadicRightAdjoint

Definitions

Name	Category	Theorems
L 📖	CompOp	1 math math: eqv
adj 📖	CompOp	1 math math: eqv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqv 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.Monad.Algebra CategoryTheory.Adjunction.toMonad L adj CategoryTheory.Monad.Algebra.eilenbergMoore CategoryTheory.Monad.comparison	—	—

CategoryTheory.Reflective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comparison_essSurj 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.Monad.Algebra CategoryTheory.Adjunction.toMonad CategoryTheory.reflector CategoryTheory.reflectorAdjunction CategoryTheory.Monad.Algebra.eilenbergMoore CategoryTheory.Monad.comparison	—	instIsIsoAppUnitReflectorAdjunctionA CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Adjunction.unit_naturality_assoc CategoryTheory.Adjunction.right_triangle_components CategoryTheory.Category.comp_id CategoryTheory.Monad.Algebra.unit_assoc
comparison_full 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Monad.Algebra CategoryTheory.Adjunction.toMonad CategoryTheory.Monad.Algebra.eilenbergMoore CategoryTheory.Monad.comparison	—	CategoryTheory.Monad.Algebra.Hom.ext' CategoryTheory.Functor.map_preimage
instIsIsoAppUnitReflectorAdjunctionA 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Monad.Algebra.A CategoryTheory.Adjunction.toMonad CategoryTheory.reflector CategoryTheory.reflectorAdjunction CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit	—	CategoryTheory.Monad.Algebra.unit CategoryTheory.Adjunction.unit_naturality CategoryTheory.unit_obj_eq_map_unit CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_id

---

← Back to Index