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 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 CategoryTheory.Functor.category CategoryTheory.Functor.const colimitPresheafOfModules CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι colimitCocone CategoryTheory.Limits.colimit.ι	—	—
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 CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.colimit 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	—	—
evaluation_preservesColimit 📖	—	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_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 📖	—	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	—	—	—
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 📖	—	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	—	—	—
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.Functor Ab 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