Documentation Verification Report

ColimitPresentation

📁 Source: Mathlib/CategoryTheory/Presentable/ColimitPresentation.lean

Statistics

Metric	Count
Definitions `ColimitPresentation`, `Total`, `base`, `comp`, `hom`, `mk`, `bind`, `instCategoryTotal`	8
Theorems `comp_base`, `comp_hom`, `ext`, `ext_iff`, `w`, `w_assoc`, `exists_hom_of_hom`, `bind_diag_map`, `bind_diag_obj`, `bind_ι_app`, `comp_base`, `comp_hom`, `id_base`, `id_hom`, `instIsFilteredTotalOfIsFinitelyPresentableObjDiag`, `instLocallySmallTotal`, `instNonemptyTotalOfIsFiltered`	17
Total	25

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`ColimitPresentation` 📖	CompData	—

CategoryTheory.Limits.ColimitPresentation

Definitions

Name	Category	Theorems
`Total` 📖	CompOp	10 math math: `bind_diag_obj`, `comp_base`, `bind_diag_map`, `instLocallySmallTotal`, `instNonemptyTotalOfIsFiltered`, `id_base`, `instIsFilteredTotalOfIsFinitelyPresentableObjDiag`, `comp_hom`, `id_hom`, `bind_ι_app`
`bind` 📖	CompOp	3 math math: `bind_diag_obj`, `bind_diag_map`, `bind_ι_app`
`instCategoryTotal` 📖	CompOp	9 math math: `bind_diag_obj`, `comp_base`, `bind_diag_map`, `instLocallySmallTotal`, `id_base`, `instIsFilteredTotalOfIsFinitelyPresentableObjDiag`, `comp_hom`, `id_hom`, `bind_ι_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind_diag_map` 📖	mathematical	`CategoryTheory.IsFiltered` `CategoryTheory.IsFinitelyPresentable` `CategoryTheory.Functor.obj` `diag`	`CategoryTheory.Functor.map` `Total` `instCategoryTotal` `bind` `Total.Hom.hom`	—	—
`bind_diag_obj` 📖	mathematical	`CategoryTheory.IsFiltered` `CategoryTheory.IsFinitelyPresentable` `CategoryTheory.Functor.obj` `diag`	`Total` `instCategoryTotal` `bind`	—	—
`bind_ι_app` 📖	mathematical	`CategoryTheory.IsFiltered` `CategoryTheory.IsFinitelyPresentable` `CategoryTheory.Functor.obj` `diag`	`CategoryTheory.NatTrans.app` `Total` `instCategoryTotal` `Total.Hom.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `ι` `bind` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`comp_base` 📖	mathematical	—	`Total.Hom.base` `CategoryTheory.CategoryStruct.comp` `Total` `CategoryTheory.Category.toCategoryStruct` `instCategoryTotal`	—	—
`comp_hom` 📖	mathematical	—	`Total.Hom.hom` `CategoryTheory.CategoryStruct.comp` `Total` `CategoryTheory.Category.toCategoryStruct` `instCategoryTotal` `CategoryTheory.Functor.obj` `diag`	—	—
`id_base` 📖	mathematical	—	`Total.Hom.base` `CategoryTheory.CategoryStruct.id` `Total` `CategoryTheory.Category.toCategoryStruct` `instCategoryTotal`	—	—
`id_hom` 📖	mathematical	—	`Total.Hom.hom` `CategoryTheory.CategoryStruct.id` `Total` `CategoryTheory.Category.toCategoryStruct` `instCategoryTotal` `CategoryTheory.Functor.obj` `diag`	—	—
`instIsFilteredTotalOfIsFinitelyPresentableObjDiag` 📖	mathematical	`CategoryTheory.IsFiltered` `CategoryTheory.IsFinitelyPresentable` `CategoryTheory.Functor.obj` `diag`	`Total` `instCategoryTotal`	—	`CategoryTheory.IsFiltered.toIsFilteredOrEmpty` `Total.exists_hom_of_hom` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Category.assoc` `Total.Hom.w` `Total.Hom.w_assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.IsFiltered.coeq_condition` `CategoryTheory.IsFinitelyPresentable.exists_eq_of_isColimit` `Total.Hom.ext` `Mathlib.Tactic.Reassoc.eq_whisker'` `instNonemptyTotalOfIsFiltered`
`instLocallySmallTotal` 📖	mathematical	—	`CategoryTheory.LocallySmall` `Total` `instCategoryTotal`	—	`small_of_injective` `small_prod` `CategoryTheory.instSmallHomOfLocallySmall`
`instNonemptyTotalOfIsFiltered` 📖	mathematical	`CategoryTheory.IsFiltered`	`Total`	—	`CategoryTheory.IsFiltered.nonempty`

CategoryTheory.Limits.ColimitPresentation.Total

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_hom_of_hom` 📖	mathematical	—	`Hom.base`	—	`CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit`

CategoryTheory.Limits.ColimitPresentation.Total.Hom

Definitions

Name	Category	Theorems
`base` 📖	CompOp	7 math math: `CategoryTheory.Limits.ColimitPresentation.Total.exists_hom_of_hom`, `CategoryTheory.Limits.ColimitPresentation.comp_base`, `ext_iff`, `w`, `CategoryTheory.Limits.ColimitPresentation.id_base`, `comp_base`, `w_assoc`
`comp` 📖	CompOp	2 math math: `comp_base`, `comp_hom`
`hom` 📖	CompOp	8 math math: `ext_iff`, `CategoryTheory.Limits.ColimitPresentation.bind_diag_map`, `w`, `comp_hom`, `w_assoc`, `CategoryTheory.Limits.ColimitPresentation.comp_hom`, `CategoryTheory.Limits.ColimitPresentation.id_hom`, `CategoryTheory.Limits.ColimitPresentation.bind_ι_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_base` 📖	mathematical	—	`base` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`comp_hom` 📖	mathematical	—	`hom` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.ColimitPresentation.diag`	—	—
`ext` 📖	—	`base` `hom`	—	—	—
`ext_iff` 📖	mathematical	—	`base` `hom`	—	`ext`
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.ColimitPresentation.diag` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.ColimitPresentation.ι` `CategoryTheory.Functor.map` `base` `hom`	—	—
`w_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.ColimitPresentation.diag` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.ColimitPresentation.ι` `CategoryTheory.Functor.map` `base` `hom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`

---

← Back to Index