Documentation Verification Report

Equalizer

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

Statistics

Metric	Count
Definitions `bottomMap`, `topMap`, `ι`, `beckCoalgebraEqualizer`, `beckCoalgebraFork`, `beckEqualizer`, `beckFork`, `beckSplitEqualizer`	8
Theorems `bottomMap_f`, `condition`, `topMap_f`, `ι_f`, `beckCoalgebraFork_pt`, `beckCoalgebraFork_π_app`, `beckEqualizer_lift`, `beckFork_pt`, `beckFork_ι`, `instIsCoreflexivePairCoalgebraTopMapBottomMap`	10
Total	18

CategoryTheory.Comonad

Definitions

Name	Category	Theorems
`beckCoalgebraEqualizer` 📖	CompOp	—
`beckCoalgebraFork` 📖	CompOp	2 math math: `beckCoalgebraFork_pt`, `beckCoalgebraFork_π_app`
`beckEqualizer` 📖	CompOp	2 math math: `ComonadicityInternal.comparisonAdjunction_counit_f`, `beckEqualizer_lift`
`beckFork` 📖	CompOp	4 math math: `ComonadicityInternal.comparisonAdjunction_counit_f`, `beckEqualizer_lift`, `beckFork_ι`, `beckFork_pt`
`beckSplitEqualizer` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`beckCoalgebraFork_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `Coalgebra` `Coalgebra.eilenbergMoore` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `cofree` `Coalgebra.A` `toFunctor` `CofreeEqualizer.topMap` `CofreeEqualizer.bottomMap` `beckCoalgebraFork`	—	—
`beckCoalgebraFork_π_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `Coalgebra` `Coalgebra.eilenbergMoore` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.parallelPair` `cofree` `Coalgebra.A` `toFunctor` `CofreeEqualizer.topMap` `CofreeEqualizer.bottomMap` `CategoryTheory.Limits.Cone.π` `beckCoalgebraFork` `CategoryTheory.Limits.WalkingParallelPair.zero` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CofreeEqualizer.ι` `CategoryTheory.Limits.WalkingParallelPair.one` `CategoryTheory.CategoryStruct.comp`	—	—
`beckEqualizer_lift` 📖	mathematical	—	`CategoryTheory.Limits.IsLimit.lift` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `toFunctor` `Coalgebra.A` `CategoryTheory.Functor.map` `Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `δ` `beckFork` `beckEqualizer` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelPair.zero` `CategoryTheory.Functor.id` `CategoryTheory.Limits.Fork.ι` `ε`	—	—
`beckFork_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `toFunctor` `Coalgebra.A` `CategoryTheory.Functor.map` `Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `δ` `beckFork`	—	—
`beckFork_ι` 📖	mathematical	—	`CategoryTheory.Limits.Fork.ι` `CategoryTheory.Functor.obj` `toFunctor` `Coalgebra.A` `CategoryTheory.Functor.map` `Coalgebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `δ` `beckFork`	—	—
`instIsCoreflexivePairCoalgebraTopMapBottomMap` 📖	mathematical	—	`CategoryTheory.IsCoreflexivePair` `Coalgebra` `Coalgebra.eilenbergMoore` `CategoryTheory.Functor.obj` `cofree` `Coalgebra.A` `toFunctor` `CofreeEqualizer.topMap` `CofreeEqualizer.bottomMap`	—	`CategoryTheory.IsCoreflexivePair.mk'` `Coalgebra.Hom.ext'` `CategoryTheory.Functor.map_comp` `Coalgebra.counit` `CategoryTheory.Functor.map_id` `right_counit`

CategoryTheory.Comonad.CofreeEqualizer

Definitions

Name	Category	Theorems
`bottomMap` 📖	CompOp	5 math math: `CategoryTheory.Comonad.beckCoalgebraFork_pt`, `CategoryTheory.Comonad.instIsCoreflexivePairCoalgebraTopMapBottomMap`, `condition`, `bottomMap_f`, `CategoryTheory.Comonad.beckCoalgebraFork_π_app`
`topMap` 📖	CompOp	5 math math: `CategoryTheory.Comonad.beckCoalgebraFork_pt`, `topMap_f`, `CategoryTheory.Comonad.instIsCoreflexivePairCoalgebraTopMapBottomMap`, `condition`, `CategoryTheory.Comonad.beckCoalgebraFork_π_app`
`ι` 📖	CompOp	3 math math: `ι_f`, `condition`, `CategoryTheory.Comonad.beckCoalgebraFork_π_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bottomMap_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.cofree` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Comonad.toFunctor` `bottomMap` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.δ`	—	—
`condition` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.instCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.cofree` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Comonad.toFunctor` `ι` `topMap` `bottomMap`	—	`CategoryTheory.Comonad.Coalgebra.Hom.ext` `CategoryTheory.Comonad.Coalgebra.coassoc`
`topMap_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.cofree` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Comonad.toFunctor` `topMap` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra.a`	—	—
`ι_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.cofree` `CategoryTheory.Comonad.Coalgebra.A` `ι` `CategoryTheory.Comonad.Coalgebra.a`	—	—

---

← Back to Index