Monadicity

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

Statistics

Metric	Count
Definitions CreatesColimitOfIsSplitPair, out, HasCoequalizerOfIsSplitPair, comparisonAdjunction, comparisonLeftAdjointHomEquiv, comparisonLeftAdjointObj, counitCoequalizerOfReflectsCoequalizer, counitCofork, leftAdjointComparison, unitCofork, unitColimitOfPreservesCoequalizer, PreservesColimitOfIsReflexivePair, PreservesColimitOfIsSplitPair, ReflectsColimitOfIsSplitPair, createsGSplitCoequalizersOfMonadic, instCreatesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfCreatesColimitOfIsSplitPair, instCreatesColimitWalkingParallelPairParallelPairOfIsSplitPairOfCreatesColimitOfIsSplitPair, monadicOfCreatesGSplitCoequalizers, monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms, monadicOfHasPreservesReflectsGSplitCoequalizers, monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms	21
Theorems out, comparisonAdjunction_counit, comparisonAdjunction_counit_app, comparisonAdjunction_unit_f, comparisonAdjunction_unit_f_aux, comparisonLeftAdjointHomEquiv_apply_f, comparisonLeftAdjointHomEquiv_symm_apply, counitCofork_pt, counitCofork_ι_app, instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA, main_pair_G_split, main_pair_reflexive, unitCofork_pt, unitCofork_π, out, out, out, instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair, instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair, instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair, instPreservesColimitWalkingParallelPairParallelPairOfIsReflexivePairOfPreservesColimitOfIsReflexivePair, instPreservesColimitWalkingParallelPairParallelPairOfIsSplitPairOfPreservesColimitOfIsSplitPair, instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair, instReflectsColimitWalkingParallelPairParallelPairOfIsSplitPairOfReflectsColimitOfIsSplitPair	24
Total	45

CategoryTheory.Monad

Definitions

Name	Category	Theorems
CreatesColimitOfIsSplitPair 📖	CompData	—
HasCoequalizerOfIsSplitPair 📖	CompData	—
PreservesColimitOfIsReflexivePair 📖	CompData	—
PreservesColimitOfIsSplitPair 📖	CompData	—
ReflectsColimitOfIsSplitPair 📖	CompData	—
createsGSplitCoequalizersOfMonadic 📖	CompOp	—
instCreatesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfCreatesColimitOfIsSplitPair 📖	CompOp	—
instCreatesColimitWalkingParallelPairParallelPairOfIsSplitPairOfCreatesColimitOfIsSplitPair 📖	CompOp	—
monadicOfCreatesGSplitCoequalizers 📖	CompOp	—
monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms 📖	CompOp	—
monadicOfHasPreservesReflectsGSplitCoequalizers 📖	CompOp	—
monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair 📖	mathematical	—	CategoryTheory.Limits.HasCoequalizer CategoryTheory.Functor.obj toFunctor CategoryTheory.Adjunction.toMonad Algebra.A CategoryTheory.Functor.map Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit	—	HasCoequalizerOfIsSplitPair.out MonadicityInternal.main_pair_G_split
instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Functor.obj toFunctor CategoryTheory.Adjunction.toMonad Algebra.A CategoryTheory.Functor.map Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit	—	PreservesColimitOfIsReflexivePair.out MonadicityInternal.main_pair_reflexive
instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Functor.obj toFunctor CategoryTheory.Adjunction.toMonad Algebra.A CategoryTheory.Functor.map Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit	—	PreservesColimitOfIsSplitPair.out MonadicityInternal.main_pair_G_split
instPreservesColimitWalkingParallelPairParallelPairOfIsReflexivePairOfPreservesColimitOfIsReflexivePair 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair	—	PreservesColimitOfIsReflexivePair.out
instPreservesColimitWalkingParallelPairParallelPairOfIsSplitPairOfPreservesColimitOfIsSplitPair 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair	—	PreservesColimitOfIsSplitPair.out
instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair 📖	mathematical	—	CategoryTheory.Limits.ReflectsColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Functor.obj toFunctor CategoryTheory.Adjunction.toMonad Algebra.A CategoryTheory.Functor.map Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit	—	ReflectsColimitOfIsSplitPair.out MonadicityInternal.main_pair_G_split
instReflectsColimitWalkingParallelPairParallelPairOfIsSplitPairOfReflectsColimitOfIsSplitPair 📖	mathematical	—	CategoryTheory.Limits.ReflectsColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair	—	ReflectsColimitOfIsSplitPair.out

CategoryTheory.Monad.CreatesColimitOfIsSplitPair

Definitions

Name	Category	Theorems
out 📖	CompOp	—

CategoryTheory.Monad.HasCoequalizerOfIsSplitPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	CategoryTheory.Limits.HasCoequalizer	—	—

CategoryTheory.Monad.MonadicityInternal

Definitions

Name	Category	Theorems
comparisonAdjunction 📖	CompOp	4 math math: comparisonAdjunction_unit_f, comparisonAdjunction_unit_f_aux, comparisonAdjunction_counit, comparisonAdjunction_counit_app
comparisonLeftAdjointHomEquiv 📖	CompOp	3 math math: comparisonLeftAdjointHomEquiv_apply_f, comparisonLeftAdjointHomEquiv_symm_apply, comparisonAdjunction_counit
comparisonLeftAdjointObj 📖	CompOp	3 math math: comparisonLeftAdjointHomEquiv_apply_f, comparisonLeftAdjointHomEquiv_symm_apply, comparisonAdjunction_counit
counitCoequalizerOfReflectsCoequalizer 📖	CompOp	—
counitCofork 📖	CompOp	3 math math: counitCofork_pt, counitCofork_ι_app, comparisonAdjunction_counit_app
leftAdjointComparison 📖	CompOp	4 math math: comparisonAdjunction_unit_f, comparisonAdjunction_unit_f_aux, comparisonAdjunction_counit, comparisonAdjunction_counit_app
unitCofork 📖	CompOp	3 math math: unitCofork_π, comparisonAdjunction_unit_f, unitCofork_pt
unitColimitOfPreservesCoequalizer 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comparisonAdjunction_counit 📖	mathematical	CategoryTheory.Limits.HasCoequalizer CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Adjunction.toMonad CategoryTheory.Monad.Algebra.A CategoryTheory.Functor.map CategoryTheory.Monad.Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit	CategoryTheory.Monad.Algebra CategoryTheory.Monad.Algebra.eilenbergMoore leftAdjointComparison CategoryTheory.Monad.comparison comparisonAdjunction CategoryTheory.Adjunction.leftAdjointOfEquiv comparisonLeftAdjointObj comparisonLeftAdjointHomEquiv DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Limits.Cofork.IsColimit.homIso CategoryTheory.Limits.colimit.cocone CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Limits.colimit.isColimit CategoryTheory.Adjunction.homEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Monad.Algebra.Hom.f	—	—
comparisonAdjunction_counit_app 📖	mathematical	CategoryTheory.Limits.HasCoequalizer CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Adjunction.toMonad CategoryTheory.Monad.Algebra.A CategoryTheory.Functor.map CategoryTheory.Monad.Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit	CategoryTheory.Monad.Algebra CategoryTheory.Monad.Algebra.eilenbergMoore CategoryTheory.Monad.comparison leftAdjointComparison comparisonAdjunction CategoryTheory.Limits.colimit.desc CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA counitCofork	—	CategoryTheory.Limits.coequalizer.hom_ext instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA CategoryTheory.Adjunction.homEquiv_counit CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Limits.coequalizer.desc.congr_simp CategoryTheory.Limits.colimit.ι_desc
comparisonAdjunction_unit_f 📖	mathematical	CategoryTheory.Limits.HasCoequalizer CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Adjunction.toMonad CategoryTheory.Monad.Algebra.A CategoryTheory.Functor.map CategoryTheory.Monad.Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit	CategoryTheory.Monad.Algebra.Hom.f CategoryTheory.Monad.Algebra CategoryTheory.Monad.Algebra.eilenbergMoore leftAdjointComparison CategoryTheory.Monad.comparison CategoryTheory.Adjunction.unit comparisonAdjunction CategoryTheory.Limits.IsColimit.desc CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Monad.μ CategoryTheory.Monad.beckCofork CategoryTheory.Monad.beckCoequalizer unitCofork	—	CategoryTheory.Limits.Cofork.IsColimit.hom_ext CategoryTheory.Limits.Cofork.IsColimit.π_desc comparisonAdjunction_unit_f_aux CategoryTheory.Adjunction.homEquiv_naturality_left CategoryTheory.Limits.coequalizer.condition CategoryTheory.Adjunction.homEquiv_naturality_right CategoryTheory.Adjunction.homEquiv_unit CategoryTheory.Category.assoc CategoryTheory.Adjunction.right_triangle_components_assoc
comparisonAdjunction_unit_f_aux 📖	mathematical	CategoryTheory.Limits.HasCoequalizer CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Adjunction.toMonad CategoryTheory.Monad.Algebra.A CategoryTheory.Functor.map CategoryTheory.Monad.Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit	CategoryTheory.Monad.Algebra.Hom.f CategoryTheory.Monad.Algebra CategoryTheory.Monad.Algebra.eilenbergMoore leftAdjointComparison CategoryTheory.Monad.comparison CategoryTheory.Adjunction.unit comparisonAdjunction DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coequalizer EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv CategoryTheory.Limits.coequalizer.π	—	CategoryTheory.Category.comp_id
comparisonLeftAdjointHomEquiv_apply_f 📖	mathematical	—	CategoryTheory.Monad.Algebra.Hom.f CategoryTheory.Adjunction.toMonad CategoryTheory.Functor.obj CategoryTheory.Monad.Algebra CategoryTheory.Monad.Algebra.eilenbergMoore CategoryTheory.Monad.comparison DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct comparisonLeftAdjointObj CategoryTheory.Monad.Algebra.instCategoryStruct EquivLike.toFunLike Equiv.instEquivLike comparisonLeftAdjointHomEquiv CategoryTheory.Monad.Algebra.A CategoryTheory.Adjunction.homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Monad.Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit CategoryTheory.Limits.Cofork.IsColimit.homIso CategoryTheory.Limits.colimit.cocone CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Limits.colimit.isColimit	—	—
comparisonLeftAdjointHomEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Monad.Algebra CategoryTheory.Adjunction.toMonad CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Monad.Algebra.instCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Monad.Algebra.eilenbergMoore CategoryTheory.Monad.comparison CategoryTheory.Category.toCategoryStruct comparisonLeftAdjointObj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm comparisonLeftAdjointHomEquiv CategoryTheory.Monad.Algebra.A CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Monad.Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit CategoryTheory.Limits.Cofork.IsColimit.homIso CategoryTheory.Limits.colimit.cocone CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Limits.colimit.isColimit CategoryTheory.Adjunction.homEquiv CategoryTheory.Monad.Algebra.Hom.f	—	—
counitCofork_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit counitCofork	—	—
counitCofork_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.Adjunction.counit CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι counitCofork Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	—	CategoryTheory.Adjunction.counit_naturality
instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA 📖	mathematical	CategoryTheory.Limits.HasCoequalizer CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Adjunction.toMonad CategoryTheory.Monad.Algebra.A CategoryTheory.Functor.map CategoryTheory.Monad.Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit	CategoryTheory.Limits.HasColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair	—	—
main_pair_G_split 📖	mathematical	—	CategoryTheory.Functor.IsSplitPair CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Adjunction.toMonad CategoryTheory.Monad.Algebra.A CategoryTheory.Functor.map CategoryTheory.Monad.Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit	—	—
main_pair_reflexive 📖	mathematical	—	CategoryTheory.IsReflexivePair CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Adjunction.toMonad CategoryTheory.Monad.Algebra.A CategoryTheory.Functor.map CategoryTheory.Monad.Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit	—	CategoryTheory.IsReflexivePair.mk' CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_id CategoryTheory.Monad.Algebra.unit CategoryTheory.Adjunction.left_triangle_components
unitCofork_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Adjunction.toMonad CategoryTheory.Monad.Algebra.A CategoryTheory.Functor.map CategoryTheory.Monad.Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit unitCofork CategoryTheory.Limits.coequalizer	—	—
unitCofork_π 📖	mathematical	—	CategoryTheory.Limits.Cofork.π CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Adjunction.toMonad CategoryTheory.Monad.Algebra.A CategoryTheory.Functor.map CategoryTheory.Monad.Algebra.a CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit unitCofork CategoryTheory.Limits.coequalizer CategoryTheory.Limits.coequalizer.π	—	—

CategoryTheory.Monad.PreservesColimitOfIsReflexivePair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair	—	—

CategoryTheory.Monad.PreservesColimitOfIsSplitPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair	—	—

CategoryTheory.Monad.ReflectsColimitOfIsSplitPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	CategoryTheory.Limits.ReflectsColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair	—	—

---

← Back to Index