Documentation Verification Report

Presentation

📁 Source: Mathlib/CategoryTheory/Limits/Presentation.lean

Statistics

Metric	Count
Definitions `Presentation`, `changeDiag`, `cocone`, `colimit`, `diag`, `isColimit`, `map`, `ofIso`, `reindex`, `self`, `ι`, `LimitPresentation`, `changeDiag`, `cone`, `diag`, `isLimit`, `limit`, `map`, `ofIso`, `reindex`, `self`, `π`, `Presentation`, `Presentation`	24
Theorems `changeDiag_diag`, `changeDiag_ι`, `hasColimit`, `map_diag`, `map_ι`, `ofIso_diag`, `ofIso_ι`, `reindex_diag`, `reindex_ι`, `self_diag`, `self_ι`, `w`, `w_assoc`, `changeDiag_diag`, `changeDiag_π`, `hasLimit`, `map_diag`, `map_π`, `ofIso_diag`, `ofIso_π`, `reindex_diag`, `reindex_π`, `self_diag`, `self_π`, `w`, `w_assoc`	26
Total	50

Algebra

Definitions

Name	Category	Theorems
`Presentation` 📖	CompData	1 math math: `Presentation.exists_presentation_fin`

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`LimitPresentation` 📖	CompData	—

CategoryTheory.Limits.ColimitPresentation

Definitions

Name	Category	Theorems
`changeDiag` 📖	CompOp	2 math math: `changeDiag_ι`, `changeDiag_diag`
`cocone` 📖	CompOp	—
`colimit` 📖	CompOp	1 math math: `CategoryTheory.ObjectProperty.ColimitOfShape.colimit_toColimitPresentation`
`diag` 📖	CompOp	20 math math: `CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_obj`, `changeDiag_ι`, `map_diag`, `map_ι`, `self_diag`, `Total.Hom.w`, `CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj`, `w_assoc`, `Total.Hom.comp_hom`, `Total.Hom.w_assoc`, `CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_map`, `reindex_ι`, `ofIso_ι`, `hasColimit`, `w`, `reindex_diag`, `ofIso_diag`, `comp_hom`, `id_hom`, `changeDiag_diag`
`isColimit` 📖	CompOp	—
`map` 📖	CompOp	2 math math: `map_diag`, `map_ι`
`ofIso` 📖	CompOp	3 math math: `ofIso_ι`, `CategoryTheory.ObjectProperty.ColimitOfShape.ofIso_toColimitPresentation`, `ofIso_diag`
`reindex` 📖	CompOp	3 math math: `reindex_ι`, `reindex_diag`, `CategoryTheory.ObjectProperty.ColimitOfShape.reindex_toColimitPresentation`
`self` 📖	CompOp	2 math math: `self_diag`, `self_ι`
`ι` 📖	CompOp	12 math math: `CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_obj`, `changeDiag_ι`, `map_ι`, `Total.Hom.w`, `w_assoc`, `Total.Hom.w_assoc`, `CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_map`, `reindex_ι`, `ofIso_ι`, `w`, `bind_ι_app`, `self_ι`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`changeDiag_diag` 📖	mathematical	—	`diag` `changeDiag`	—	—
`changeDiag_ι` 📖	mathematical	—	`ι` `changeDiag` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `diag` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const` `CategoryTheory.Iso.hom`	—	—
`hasColimit` 📖	mathematical	—	`CategoryTheory.Limits.HasColimit` `diag`	—	—
`map_diag` 📖	mathematical	—	`diag` `CategoryTheory.Functor.obj` `map` `CategoryTheory.Functor.comp`	—	—
`map_ι` 📖	mathematical	—	`ι` `CategoryTheory.Functor.obj` `map` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `diag` `CategoryTheory.Functor.const` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.constComp`	—	—
`ofIso_diag` 📖	mathematical	—	`diag` `ofIso`	—	—
`ofIso_ι` 📖	mathematical	—	`ι` `ofIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `diag` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	—	—
`reindex_diag` 📖	mathematical	—	`diag` `reindex` `CategoryTheory.Functor.comp`	—	—
`reindex_ι` 📖	mathematical	—	`ι` `reindex` `CategoryTheory.Functor.whiskerLeft` `diag` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const`	—	—
`self_diag` 📖	mathematical	—	`diag` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `PUnit.instCompleteBooleanAlgebra` `self` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const`	—	—
`self_ι` 📖	mathematical	—	`ι` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `PUnit.instCompleteBooleanAlgebra` `self` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const`	—	—
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `diag` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `ι`	—	`CategoryTheory.NatTrans.naturality` `CategoryTheory.Category.comp_id`
`w_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `diag` `CategoryTheory.Functor.map` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.NatTrans.app` `ι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`

CategoryTheory.Limits.LimitPresentation

Definitions

Name	Category	Theorems
`changeDiag` 📖	CompOp	2 math math: `changeDiag_π`, `changeDiag_diag`
`cone` 📖	CompOp	—
`diag` 📖	CompOp	15 math math: `hasLimit`, `CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj`, `w`, `changeDiag_π`, `changeDiag_diag`, `reindex_π`, `reindex_diag`, `ofIso_π`, `self_diag`, `map_π`, `map_diag`, `ofIso_diag`, `CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_obj`, `CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_map`, `w_assoc`
`isLimit` 📖	CompOp	—
`limit` 📖	CompOp	—
`map` 📖	CompOp	2 math math: `map_π`, `map_diag`
`ofIso` 📖	CompOp	3 math math: `ofIso_π`, `CategoryTheory.ObjectProperty.LimitOfShape.ofIso_toLimitPresentation`, `ofIso_diag`
`reindex` 📖	CompOp	3 math math: `reindex_π`, `reindex_diag`, `CategoryTheory.ObjectProperty.LimitOfShape.reindex_toLimitPresentation`
`self` 📖	CompOp	2 math math: `self_π`, `self_diag`
`π` 📖	CompOp	9 math math: `w`, `self_π`, `changeDiag_π`, `reindex_π`, `ofIso_π`, `map_π`, `CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_obj`, `CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_map`, `w_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`changeDiag_diag` 📖	mathematical	—	`diag` `changeDiag`	—	—
`changeDiag_π` 📖	mathematical	—	`π` `changeDiag` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const` `diag` `CategoryTheory.Iso.inv`	—	—
`hasLimit` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit` `diag`	—	—
`map_diag` 📖	mathematical	—	`diag` `CategoryTheory.Functor.obj` `map` `CategoryTheory.Functor.comp`	—	—
`map_π` 📖	mathematical	—	`π` `CategoryTheory.Functor.obj` `map` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Functor.comp` `diag` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.constComp` `CategoryTheory.Functor.whiskerRight`	—	—
`ofIso_diag` 📖	mathematical	—	`diag` `ofIso`	—	—
`ofIso_π` 📖	mathematical	—	`π` `ofIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const` `diag` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv`	—	—
`reindex_diag` 📖	mathematical	—	`diag` `reindex` `CategoryTheory.Functor.comp`	—	—
`reindex_π` 📖	mathematical	—	`π` `reindex` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `diag`	—	—
`self_diag` 📖	mathematical	—	`diag` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `PUnit.instCompleteBooleanAlgebra` `self` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const`	—	—
`self_π` 📖	mathematical	—	`π` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `PUnit.instCompleteBooleanAlgebra` `self` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const`	—	—
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `diag` `CategoryTheory.NatTrans.app` `π` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.naturality`
`w_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `diag` `CategoryTheory.NatTrans.app` `π` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`

Module

Definitions

Name	Category	Theorems
`Presentation` 📖	CompData	—

SheafOfModules

Definitions

Name	Category	Theorems
`Presentation` 📖	CompData	—

---

← Back to Index