Documentation Verification Report

Coequalizer

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

Statistics

Metric	Count
Definitions `bottomMap`, `topMap`, `π`, `beckAlgebraCoequalizer`, `beckAlgebraCofork`, `beckCoequalizer`, `beckCofork`, `beckSplitCoequalizer`	8
Theorems `bottomMap_f`, `condition`, `topMap_f`, `π_f`, `beckAlgebraCofork_pt`, `beckAlgebraCofork_ι_app`, `beckCoequalizer_desc`, `beckCofork_pt`, `beckCofork_π`, `instIsReflexivePairAlgebraTopMapBottomMap`	10
Total	18

CategoryTheory.Monad

Definitions

Name	Category	Theorems
`beckAlgebraCoequalizer` 📖	CompOp	—
`beckAlgebraCofork` 📖	CompOp	2 math math: `beckAlgebraCofork_pt`, `beckAlgebraCofork_ι_app`
`beckCoequalizer` 📖	CompOp	2 math math: `beckCoequalizer_desc`, `MonadicityInternal.comparisonAdjunction_unit_f`
`beckCofork` 📖	CompOp	4 math math: `beckCoequalizer_desc`, `beckCofork_pt`, `MonadicityInternal.comparisonAdjunction_unit_f`, `beckCofork_π`
`beckSplitCoequalizer` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`beckAlgebraCofork_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `Algebra` `Algebra.eilenbergMoore` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `free` `toFunctor` `Algebra.A` `FreeCoequalizer.topMap` `FreeCoequalizer.bottomMap` `beckAlgebraCofork`	—	—
`beckAlgebraCofork_ι_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `Algebra` `Algebra.eilenbergMoore` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `free` `toFunctor` `Algebra.A` `FreeCoequalizer.topMap` `FreeCoequalizer.bottomMap` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.ι` `beckAlgebraCofork` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.comp` `FreeCoequalizer.π`	—	—
`beckCoequalizer_desc` 📖	mathematical	—	`CategoryTheory.Limits.IsColimit.desc` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `toFunctor` `Algebra.A` `CategoryTheory.Functor.map` `Algebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `μ` `beckCofork` `beckCoequalizer` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.id` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingParallelPair.one` `η` `CategoryTheory.Limits.Cofork.π`	—	—
`beckCofork_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Functor.obj` `toFunctor` `Algebra.A` `CategoryTheory.Functor.map` `Algebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `μ` `beckCofork`	—	—
`beckCofork_π` 📖	mathematical	—	`CategoryTheory.Limits.Cofork.π` `CategoryTheory.Functor.obj` `toFunctor` `Algebra.A` `CategoryTheory.Functor.map` `Algebra.a` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `μ` `beckCofork`	—	—
`instIsReflexivePairAlgebraTopMapBottomMap` 📖	mathematical	—	`CategoryTheory.IsReflexivePair` `Algebra` `Algebra.eilenbergMoore` `CategoryTheory.Functor.obj` `free` `toFunctor` `Algebra.A` `FreeCoequalizer.topMap` `FreeCoequalizer.bottomMap`	—	`CategoryTheory.IsReflexivePair.mk'` `Algebra.Hom.ext'` `CategoryTheory.Functor.map_comp` `Algebra.unit` `CategoryTheory.Functor.map_id` `right_unit`

CategoryTheory.Monad.FreeCoequalizer

Definitions

Name	Category	Theorems
`bottomMap` 📖	CompOp	5 math math: `condition`, `CategoryTheory.Monad.beckAlgebraCofork_pt`, `bottomMap_f`, `CategoryTheory.Monad.beckAlgebraCofork_ι_app`, `CategoryTheory.Monad.instIsReflexivePairAlgebraTopMapBottomMap`
`topMap` 📖	CompOp	5 math math: `condition`, `CategoryTheory.Monad.beckAlgebraCofork_pt`, `CategoryTheory.Monad.beckAlgebraCofork_ι_app`, `CategoryTheory.Monad.instIsReflexivePairAlgebraTopMapBottomMap`, `topMap_f`
`π` 📖	CompOp	3 math math: `condition`, `π_f`, `CategoryTheory.Monad.beckAlgebraCofork_ι_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bottomMap_f` 📖	mathematical	—	`CategoryTheory.Monad.Algebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.free` `CategoryTheory.Monad.toFunctor` `CategoryTheory.Monad.Algebra.A` `bottomMap` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.μ`	—	—
`condition` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.instCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.free` `CategoryTheory.Monad.toFunctor` `CategoryTheory.Monad.Algebra.A` `topMap` `π` `bottomMap`	—	`CategoryTheory.Monad.Algebra.Hom.ext` `CategoryTheory.Monad.Algebra.assoc`
`topMap_f` 📖	mathematical	—	`CategoryTheory.Monad.Algebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.free` `CategoryTheory.Monad.toFunctor` `CategoryTheory.Monad.Algebra.A` `topMap` `CategoryTheory.Functor.map` `CategoryTheory.Monad.Algebra.a`	—	—
`π_f` 📖	mathematical	—	`CategoryTheory.Monad.Algebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.free` `CategoryTheory.Monad.Algebra.A` `π` `CategoryTheory.Monad.Algebra.a`	—	—

---

← Back to Index