Documentation Verification Report

Comonadicity

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

Statistics

Metric	Count
Definitions `comparisonAdjunction`, `comparisonRightAdjointHomEquiv`, `comparisonRightAdjointObj`, `counitFork`, `counitLimitOfPreservesEqualizer`, `rightAdjointComparison`, `unitEqualizerOfCoreflectsEqualizer`, `unitFork`, `CreatesLimitOfIsCosplitPair`, `out`, `HasEqualizerOfIsCosplitPair`, `PreservesLimitOfIsCoreflexivePair`, `PreservesLimitOfIsCosplitPair`, `ReflectsLimitOfIsCosplitPair`, `comonadicOfCreatesFSplitEqualizers`, `comonadicOfHasPreservesCoreflexiveEqualizersOfReflectsIsomorphisms`, `comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms`, `comonadicOfHasPreservesReflectsFSplitEqualizers`, `createsFSplitEqualizersOfComonadic`, `instCreatesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfCreatesLimitOfIsCosplitPair`, `instCreatesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfCreatesLimitOfIsCosplitPair`	21
Theorems `comparisonAdjunction_counit`, `comparisonAdjunction_counit_f`, `comparisonAdjunction_counit_f_aux`, `comparisonAdjunction_unit_app`, `comparisonRightAdjointHomEquiv_apply`, `comparisonRightAdjointHomEquiv_symm_apply_f`, `counitFork_pt`, `instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA`, `main_pair_F_cosplit`, `main_pair_coreflexive`, `unitFork_pt`, `unitFork_ι`, `unitFork_π_app`, `out`, `out`, `out`, `out`, `instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair`, `instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair`, `instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair`, `instPreservesLimitWalkingParallelPairParallelPairOfIsCoreflexivePairOfPreservesLimitOfIsCoreflexivePair`, `instPreservesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfPreservesLimitOfIsCosplitPair`, `instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair`, `instReflectsLimitWalkingParallelPairParallelPairOfIsCosplitPairOfReflectsLimitOfIsCosplitPair`	24
Total	45

CategoryTheory.Comonad

Definitions

Name	Category	Theorems
`CreatesLimitOfIsCosplitPair` 📖	CompData	—
`HasEqualizerOfIsCosplitPair` 📖	CompData	—
`PreservesLimitOfIsCoreflexivePair` 📖	CompData	1 math math: `CategoryTheory.Functor.instPreservesLimitOfIsCoreflexivePairDiscreteObjWhiskeringLeftIncl`
`PreservesLimitOfIsCosplitPair` 📖	CompData	—
`ReflectsLimitOfIsCosplitPair` 📖	CompData	—
`comonadicOfCreatesFSplitEqualizers` 📖	CompOp	—
`comonadicOfHasPreservesCoreflexiveEqualizersOfReflectsIsomorphisms` 📖	CompOp	—
`comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms` 📖	CompOp	—
`comonadicOfHasPreservesReflectsFSplitEqualizers` 📖	CompOp	—
`createsFSplitEqualizersOfComonadic` 📖	CompOp	—
`instCreatesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfCreatesLimitOfIsCosplitPair` 📖	CompOp	—
`instCreatesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfCreatesLimitOfIsCosplitPair` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair` 📖	mathematical	—	`CategoryTheory.Limits.HasEqualizer` `CategoryTheory.Functor.obj` `Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `toFunctor` `CategoryTheory.Functor.map` `Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit`	—	`HasEqualizerOfIsCosplitPair.out` `ComonadicityInternal.main_pair_F_cosplit`
`instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `toFunctor` `CategoryTheory.Functor.map` `Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit`	—	`PreservesLimitOfIsCoreflexivePair.out` `ComonadicityInternal.main_pair_coreflexive`
`instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `toFunctor` `CategoryTheory.Functor.map` `Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit`	—	`PreservesLimitOfIsCosplitPair.out` `ComonadicityInternal.main_pair_F_cosplit`
`instPreservesLimitWalkingParallelPairParallelPairOfIsCoreflexivePairOfPreservesLimitOfIsCoreflexivePair` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair`	—	`PreservesLimitOfIsCoreflexivePair.out`
`instPreservesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfPreservesLimitOfIsCosplitPair` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair`	—	`PreservesLimitOfIsCosplitPair.out`
`instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair` 📖	mathematical	—	`CategoryTheory.Limits.ReflectsLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `toFunctor` `CategoryTheory.Functor.map` `Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit`	—	`ReflectsLimitOfIsCosplitPair.out` `ComonadicityInternal.main_pair_F_cosplit`
`instReflectsLimitWalkingParallelPairParallelPairOfIsCosplitPairOfReflectsLimitOfIsCosplitPair` 📖	mathematical	—	`CategoryTheory.Limits.ReflectsLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair`	—	`ReflectsLimitOfIsCosplitPair.out`

CategoryTheory.Comonad.ComonadicityInternal

Definitions

Name	Category	Theorems
`comparisonAdjunction` 📖	CompOp	4 math math: `comparisonAdjunction_counit_f`, `comparisonAdjunction_counit`, `comparisonAdjunction_unit_app`, `comparisonAdjunction_counit_f_aux`
`comparisonRightAdjointHomEquiv` 📖	CompOp	3 math math: `comparisonRightAdjointHomEquiv_symm_apply_f`, `comparisonAdjunction_counit`, `comparisonRightAdjointHomEquiv_apply`
`comparisonRightAdjointObj` 📖	CompOp	3 math math: `comparisonRightAdjointHomEquiv_symm_apply_f`, `comparisonAdjunction_counit`, `comparisonRightAdjointHomEquiv_apply`
`counitFork` 📖	CompOp	3 math math: `comparisonAdjunction_counit_f`, `unitFork_ι`, `counitFork_pt`
`counitLimitOfPreservesEqualizer` 📖	CompOp	—
`rightAdjointComparison` 📖	CompOp	4 math math: `comparisonAdjunction_counit_f`, `comparisonAdjunction_counit`, `comparisonAdjunction_unit_app`, `comparisonAdjunction_counit_f_aux`
`unitEqualizerOfCoreflectsEqualizer` 📖	CompOp	—
`unitFork` 📖	CompOp	3 math math: `unitFork_π_app`, `unitFork_pt`, `comparisonAdjunction_unit_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comparisonAdjunction_counit` 📖	mathematical	`CategoryTheory.Limits.HasEqualizer` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit`	`CategoryTheory.Adjunction.counit` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.comparison` `rightAdjointComparison` `comparisonAdjunction` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.rightAdjointOfEquiv` `comparisonRightAdjointObj` `comparisonRightAdjointHomEquiv` `CategoryTheory.Functor.id` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.CategoryStruct.id`	—	—
`comparisonAdjunction_counit_f` 📖	mathematical	`CategoryTheory.Limits.HasEqualizer` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit`	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Functor.comp` `rightAdjointComparison` `CategoryTheory.Comonad.comparison` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.counit` `comparisonAdjunction` `CategoryTheory.Limits.IsLimit.lift` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.Comonad.δ` `CategoryTheory.Comonad.beckFork` `CategoryTheory.Comonad.beckEqualizer` `counitFork`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Adjunction.homEquiv_counit`
`comparisonAdjunction_counit_f_aux` 📖	mathematical	`CategoryTheory.Limits.HasEqualizer` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit`	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Functor.comp` `rightAdjointComparison` `CategoryTheory.Comonad.comparison` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.counit` `comparisonAdjunction` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.equalizer` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.Adjunction.unit` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Limits.equalizer.ι`	—	`CategoryTheory.Category.id_comp`
`comparisonAdjunction_unit_app` 📖	mathematical	`CategoryTheory.Limits.HasEqualizer` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.comparison` `rightAdjointComparison` `CategoryTheory.Adjunction.unit` `comparisonAdjunction` `CategoryTheory.Limits.limit.lift` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA` `unitFork`	—	`CategoryTheory.Limits.equalizer.hom_ext` `instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA` `CategoryTheory.Adjunction.homEquiv_unit` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.equalizer.lift.congr_simp` `CategoryTheory.Limits.limit.lift_π`
`comparisonRightAdjointHomEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Comonad.Coalgebra.instCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.comparison` `CategoryTheory.Category.toCategoryStruct` `comparisonRightAdjointObj` `EquivLike.toFunLike` `Equiv.instEquivLike` `comparisonRightAdjointHomEquiv` `CategoryTheory.Limits.equalizer.lift` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Comonad.Coalgebra.Hom.f`	—	—
`comparisonRightAdjointHomEquiv_symm_apply_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.comparison` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `comparisonRightAdjointObj` `CategoryTheory.Comonad.Coalgebra.instCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `comparisonRightAdjointHomEquiv` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Limits.equalizer.ι` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit`	—	—
`counitFork_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit` `counitFork` `CategoryTheory.Limits.equalizer`	—	—
`instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA` 📖	mathematical	`CategoryTheory.Limits.HasEqualizer` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit`	`CategoryTheory.Limits.HasLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.unit`	—	—
`main_pair_F_cosplit` 📖	mathematical	—	`CategoryTheory.Functor.IsCosplitPair` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit`	—	—
`main_pair_coreflexive` 📖	mathematical	—	`CategoryTheory.IsCoreflexivePair` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit`	—	`CategoryTheory.IsCoreflexivePair.mk'` `CategoryTheory.Functor.map_comp` `CategoryTheory.Functor.map_id` `CategoryTheory.Comonad.Coalgebra.counit` `CategoryTheory.Adjunction.right_triangle_components`
`unitFork_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.unit` `unitFork`	—	—
`unitFork_ι` 📖	mathematical	—	`CategoryTheory.Limits.Fork.ι` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit` `counitFork` `CategoryTheory.Limits.equalizer` `CategoryTheory.Limits.equalizer.ι`	—	—
`unitFork_π_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Functor.id` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.map` `CategoryTheory.Adjunction.unit` `CategoryTheory.Limits.Cone.π` `unitFork` `CategoryTheory.Limits.WalkingParallelPair.zero` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.WalkingParallelPair.one` `CategoryTheory.CategoryStruct.comp`	—	—

CategoryTheory.Comonad.CreatesLimitOfIsCosplitPair

Definitions

Name	Category	Theorems
`out` 📖	CompOp	—

CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair

Theorems

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

CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair

Theorems

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

CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair

Theorems

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

CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair

Theorems

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

---

← Back to Index