Documentation Verification Report

Colimits

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

Statistics

Metric	Count
Definitions `forget₂CreatesColimit`, `instCreatesColimitsOfShapeModuleCatForget₂LinearMapIdCarrierObjIsFG`	2
Theorems `instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG`, `instFiniteCarrierSigmaObjModuleCatOfFinite`, `instHasColimitsOfShapeOfFinCategory`, `instHasFiniteColimits`, `instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG`	5
Total	7

FGModuleCat

Definitions

Name	Category	Theorems
`forget₂CreatesColimit` 📖	CompOp	—
`instCreatesColimitsOfShapeModuleCatForget₂LinearMapIdCarrierObjIsFG` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG` 📖	mathematical	—	`Module.Finite` `ModuleCat.carrier` `CategoryTheory.Limits.colimit` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.Functor.comp` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat.isFG` `CategoryTheory.forget₂` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `CategoryTheory.FullSubcategory.concreteCategory` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.FullSubcategory.hasForget₂` `ModuleCat.HasColimit.instHasColimit` `AddCommGrpCat.hasColimit` `UnivLE.small` `univLE_of_max` `UnivLE.self` `AddCommGrpCat` `AddCommGrpCat.instCategory` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `ModuleCat.hasForgetToAddCommGroup`	—	`instFiniteCarrier` `Module.Finite.of_surjective` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize` `ModuleCat.hasColimitsOfSize` `AddCommGrpCat.hasColimitsOfSize` `univLE_of_max` `UnivLE.self` `ModuleCat.HasColimit.instHasColimit` `AddCommGrpCat.hasColimit` `UnivLE.small` `RingHomSurjective.ids` `instFiniteCarrierSigmaObjModuleCatOfFinite` `Finite.of_fintype` `ModuleCat.epi_iff_surjective` `CategoryTheory.Limits.colimitQuotientCoproduct_epi`
`instFiniteCarrierSigmaObjModuleCatOfFinite` 📖	mathematical	`Module.Finite` `ModuleCat.carrier` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule`	`CategoryTheory.Limits.sigmaObj` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.HasColimit.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `AddCommGrpCat.hasColimit` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Functor.comp` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.forget₂` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `ModuleCat.hasForgetToAddCommGroup`	—	`ModuleCat.HasColimit.instHasColimit` `AddCommGrpCat.hasColimit` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Module.Finite.equiv_iff` `Module.Finite.instDirectSum`
`instHasColimitsOfShapeOfFinCategory` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfShape` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG`	—	`CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape` `ModuleCat.hasColimitsOfShape` `AddCommGrpCat.hasColimitsOfShape` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`instHasFiniteColimits` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteColimits` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG`	—	`instHasColimitsOfShapeOfFinCategory`
`instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteColimits` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `CategoryTheory.forget₂` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.carrier` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `CategoryTheory.FullSubcategory.concreteCategory` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.FullSubcategory.hasForget₂`	—	`CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape` `ModuleCat.hasColimitsOfShape` `AddCommGrpCat.hasColimitsOfShape` `UnivLE.small` `univLE_of_max` `UnivLE.self`

---

← Back to Index