Colimits

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

Statistics

Metric	Count
Definitions coconePointSMul, colimitCocone, isColimitColimitCocone, finsuppCocone, finsuppCoconeIsColimit	5
Theorems coconePointSMul_apply, colimitCocone_pt_carrier, colimitCocone_pt_isAddCommGroup, colimitCocone_pt_isModule, colimitCocone_ι_app, instHasColimit, instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, reflectsColimit, forget₂PreservesColimitsOfShape, forget₂PreservesColimitsOfSize, hasColimitsOfShape, hasColimitsOfSize, instHasCoequalizers, instHasFiniteColimits, instPreservesColimitsOfSizeAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax, reflectsColimitsOfShape	16
Total	21

ModuleCat

Definitions

Name	Category	Theorems
finsuppCocone 📖	CompOp	—
finsuppCoconeIsColimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget₂PreservesColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape ModuleCat moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	HasColimit.instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
forget₂PreservesColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize ModuleCat moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	forget₂PreservesColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
hasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape ModuleCat moduleCategory	—	HasColimit.instHasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
hasColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfSize ModuleCat moduleCategory	—	hasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
instHasCoequalizers 📖	mathematical	—	CategoryTheory.Limits.HasCoequalizers ModuleCat moduleCategory	—	HasColimit.instHasColimit AddCommGrpCat.hasColimit UnivLE.small univLE_of_max UnivLE.self
instHasFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteColimits ModuleCat moduleCategory	—	CategoryTheory.Limits.hasFiniteColimits_of_hasColimits hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize UnivLE.self
instPreservesColimitsOfSizeAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize ModuleCat moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	forget₂PreservesColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
reflectsColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.ReflectsColimitsOfShape ModuleCat moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	HasColimit.reflectsColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape

ModuleCat.HasColimit

Definitions

Name	Category	Theorems
coconePointSMul 📖	CompOp	5 math math: colimitCocone_pt_isAddCommGroup, colimitCocone_ι_app, colimitCocone_pt_isModule, coconePointSMul_apply, colimitCocone_pt_carrier
colimitCocone 📖	CompOp	4 math math: colimitCocone_pt_isAddCommGroup, colimitCocone_ι_app, colimitCocone_pt_isModule, colimitCocone_pt_carrier
isColimitColimitCocone 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconePointSMul_apply 📖	mathematical	—	DFunLike.coe RingHom CategoryTheory.End AddCommGrpCat CategoryTheory.Category.toCategoryStruct AddCommGrpCat.instCategory CategoryTheory.Limits.colimit CategoryTheory.Functor.comp ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule 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 CategoryTheory.Preadditive.instSemiringEnd AddCommGrpCat.instPreadditive RingHom.instFunLike coconePointSMul CategoryTheory.Limits.colimMap CategoryTheory.Functor.obj ModuleCat.smul	—	—
colimitCocone_pt_carrier 📖	mathematical	—	ModuleCat.carrier CategoryTheory.Limits.Cocone.pt ModuleCat ModuleCat.moduleCategory colimitCocone AddCommGrpCat.carrier ModuleCat.mkOfSMul' CategoryTheory.Limits.colimit AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.comp CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier ModuleCat.hasForgetToAddCommGroup coconePointSMul	—	—
colimitCocone_pt_isAddCommGroup 📖	mathematical	—	ModuleCat.isAddCommGroup CategoryTheory.Limits.Cocone.pt ModuleCat ModuleCat.moduleCategory colimitCocone ModuleCat.instAddCommGroupCarrierMkOfSMul' CategoryTheory.Limits.colimit AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.comp CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isModule 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 coconePointSMul	—	—
colimitCocone_pt_isModule 📖	mathematical	—	ModuleCat.isModule CategoryTheory.Limits.Cocone.pt ModuleCat ModuleCat.moduleCategory colimitCocone ModuleCat.instModuleCarrierMkOfSMul' CategoryTheory.Limits.colimit AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.comp CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup 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 coconePointSMul	—	—
colimitCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const ModuleCat.mkOfSMul CategoryTheory.Limits.colimit AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.comp CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule 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 coconePointSMul CategoryTheory.Limits.Cocone.ι colimitCocone ModuleCat.homMk CategoryTheory.Limits.colimit.ι	—	—
instHasColimit 📖	mathematical	—	CategoryTheory.Limits.HasColimit ModuleCat ModuleCat.moduleCategory	—	—
instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit ModuleCat ModuleCat.moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule 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	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
reflectsColimit 📖	mathematical	—	CategoryTheory.Limits.ReflectsColimit ModuleCat ModuleCat.moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule 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	—	CategoryTheory.Limits.reflectsColimit_of_reflectsIsomorphisms ModuleCat.instReflectsIsomorphismsAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier instHasColimit instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier

---

← Back to Index