Documentation Verification Report

Colimits

📁 Source: Mathlib/Algebra/Category/MonCat/Colimits.lean

Statistics

Metric	Count
Definitions `Prequotient`, `coconeFun`, `coconeMorphism`, `colimit`, `colimitCocone`, `colimitIsColimit`, `colimitSetoid`, `descFun`, `descFunLift`, `descMorphism`, `instInhabitedColimitType`, `instInhabitedPrequotient`, `monoidColimitType`	13
Theorems `cocone_naturality`, `cocone_naturality_components`, `hasColimits_monCat`, `quot_mul`, `quot_one`	5
Total	18

MonCat.Colimits

Definitions

Name	Category	Theorems
`Prequotient` 📖	CompData	2 math math: `quot_one`, `quot_mul`
`coconeFun` 📖	CompOp	—
`coconeMorphism` 📖	CompOp	2 math math: `cocone_naturality_components`, `cocone_naturality`
`colimit` 📖	CompOp	2 math math: `cocone_naturality_components`, `cocone_naturality`
`colimitCocone` 📖	CompOp	—
`colimitIsColimit` 📖	CompOp	—
`colimitSetoid` 📖	CompOp	2 math math: `quot_one`, `quot_mul`
`descFun` 📖	CompOp	—
`descFunLift` 📖	CompOp	—
`descMorphism` 📖	CompOp	—
`instInhabitedColimitType` 📖	CompOp	—
`instInhabitedPrequotient` 📖	CompOp	—
`monoidColimitType` 📖	CompOp	2 math math: `quot_one`, `quot_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cocone_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `MonCat` `CategoryTheory.Category.toCategoryStruct` `MonCat.instCategory` `CategoryTheory.Functor.obj` `colimit` `CategoryTheory.Functor.map` `coconeMorphism`	—	`MonCat.hom_ext` `MonoidHom.ext`
`cocone_naturality_components` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `MonCat` `MonCat.instCategory` `colimit` `MonCat.carrier` `CategoryTheory.ConcreteCategory.hom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonCat.str` `MonoidHom.instFunLike` `MonCat.instConcreteCategoryMonoidHomCarrier` `coconeMorphism` `CategoryTheory.Functor.map`	—	`cocone_naturality`
`hasColimits_monCat` 📖	mathematical	—	`CategoryTheory.Limits.HasColimits` `MonCat` `MonCat.instCategory`	—	—
`quot_mul` 📖	mathematical	—	`Prequotient` `colimitSetoid` `Prequotient.mul` `ColimitType` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `monoidColimitType`	—	—
`quot_one` 📖	mathematical	—	`Prequotient` `colimitSetoid` `Prequotient.one` `ColimitType` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `monoidColimitType`	—	—

---

← Back to Index