Colimits

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

Statistics

Metric	Count
Definitions colimitCocone, colimitPresheafOfModules, evaluationJointlyReflectsColimits, isColimitColimitCocone	4
Theorems evaluation_preservesFiniteColimits, hasFiniteColimits, toPresheaf_preservesFiniteColimits, colimitCocone_pt, colimitCocone_ι_app_app, colimitPresheafOfModules_map, colimitPresheafOfModules_obj, evaluation_preservesColimit, evaluation_preservesColimitsOfShape, evaluation_preservesColimitsOfSize, hasColimit, hasColimitsOfShape, hasColimitsOfSize, instHasColimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap, toPresheaf_preservesColimit, toPresheaf_preservesColimitsOfShape, toPresheaf_preservesColimitsOfSize	17
Total	21

PresheafOfModules

Definitions

Name	Category	Theorems
colimitCocone 📖	CompOp	2 math math: colimitCocone_pt, colimitCocone_ι_app_app
colimitPresheafOfModules 📖	CompOp	4 math math: colimitCocone_pt, colimitPresheafOfModules_map, colimitCocone_ι_app_app, colimitPresheafOfModules_obj
evaluationJointlyReflectsColimits 📖	CompOp	—
isColimitColimitCocone 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitCocone_pt 📖	mathematical	CategoryTheory.Limits.PreservesColimit ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.comp PresheafOfModules instCategory evaluation ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.Limits.HasColimit	CategoryTheory.Limits.Cocone.pt PresheafOfModules instCategory colimitCocone colimitPresheafOfModules	—	—
colimitCocone_ι_app_app 📖	mathematical	CategoryTheory.Limits.PreservesColimit ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.comp PresheafOfModules instCategory evaluation ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.Limits.HasColimit	Hom.app CategoryTheory.Functor.obj PresheafOfModules instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const colimitPresheafOfModules CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι colimitCocone CategoryTheory.Limits.colimit.ι ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.comp evaluation	—	—
colimitPresheafOfModules_map 📖	mathematical	CategoryTheory.Limits.PreservesColimit ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.comp PresheafOfModules instCategory evaluation ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.Limits.HasColimit	map colimitPresheafOfModules CategoryTheory.CategoryStruct.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.Limits.colimit CategoryTheory.Functor.comp PresheafOfModules instCategory evaluation ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map instHasColimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap CategoryTheory.Limits.colimMap CategoryTheory.Functor.whiskerLeft restriction CategoryTheory.Iso.inv CategoryTheory.preservesColimitIso	—	—
colimitPresheafOfModules_obj 📖	mathematical	CategoryTheory.Limits.PreservesColimit ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.comp PresheafOfModules instCategory evaluation ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.Limits.HasColimit	obj colimitPresheafOfModules CategoryTheory.Limits.colimit ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.comp PresheafOfModules instCategory evaluation	—	—
evaluation_preservesColimit 📖	mathematical	CategoryTheory.Limits.PreservesColimit ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.comp PresheafOfModules instCategory evaluation ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.Limits.HasColimit	CategoryTheory.Limits.PreservesColimit PresheafOfModules instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory evaluation	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
evaluation_preservesColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape PresheafOfModules instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory evaluation	—	evaluation_preservesColimit ModuleCat.preservesColimit_restrictScalars CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape ModuleCat.hasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit ModuleCat.forget₂PreservesColimitsOfShape
evaluation_preservesColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize PresheafOfModules instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory evaluation	—	evaluation_preservesColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
hasColimit 📖	mathematical	CategoryTheory.Limits.PreservesColimit ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.comp PresheafOfModules instCategory evaluation ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.Limits.HasColimit	CategoryTheory.Limits.HasColimit PresheafOfModules instCategory	—	—
hasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape PresheafOfModules instCategory	—	hasColimit ModuleCat.preservesColimit_restrictScalars CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape ModuleCat.hasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit ModuleCat.forget₂PreservesColimitsOfShape
hasColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfSize PresheafOfModules instCategory	—	hasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
instHasColimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap 📖	mathematical	CategoryTheory.Limits.PreservesColimit ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.comp PresheafOfModules instCategory evaluation ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.Limits.HasColimit	CategoryTheory.Limits.HasColimit ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.comp PresheafOfModules instCategory evaluation ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map	—	—
toPresheaf_preservesColimit 📖	mathematical	CategoryTheory.Limits.PreservesColimit ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.Functor.comp PresheafOfModules instCategory evaluation ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map CategoryTheory.Limits.HasColimit 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 PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category toPresheaf	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
toPresheaf_preservesColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category toPresheaf	—	toPresheaf_preservesColimit ModuleCat.preservesColimit_restrictScalars CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape hasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit evaluation_preservesColimitsOfShape ModuleCat.forget₂PreservesColimitsOfShape CategoryTheory.Limits.comp_preservesColimit
toPresheaf_preservesColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category toPresheaf	—	toPresheaf_preservesColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize

PresheafOfModules.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evaluation_preservesFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits PresheafOfModules PresheafOfModules.instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory PresheafOfModules.evaluation	—	PresheafOfModules.evaluation_preservesColimitsOfShape AddCommGrpCat.hasColimitsOfShape UnivLE.small univLE_of_max UnivLE.self
hasFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteColimits PresheafOfModules PresheafOfModules.instCategory	—	PresheafOfModules.hasColimitsOfShape AddCommGrpCat.hasColimitsOfShape UnivLE.small univLE_of_max UnivLE.self
toPresheaf_preservesFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits PresheafOfModules PresheafOfModules.instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category PresheafOfModules.toPresheaf	—	PresheafOfModules.toPresheaf_preservesColimitsOfShape AddCommGrpCat.hasColimitsOfShape UnivLE.small univLE_of_max UnivLE.self

---

← Back to Index