Limits

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

Statistics

Metric	Count
Definitions evaluationJointlyReflectsLimits, isLimitLimitCone, limitCone, limitPresheafOfModules	4
Theorems evaluation_preservesFiniteLimits, evaluation_preservesLimit, hasFiniteLimits, hasLimit, hasLimitsOfShape, hasLimitsOfSize, instHasLimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap, instPreservesLimitsOfShapeFunctorOppositeAbToPresheaf, instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation, instPreservesLimitsOfSizeFunctorOppositeAbToPresheaf, instPreservesLimitsOfSizeModuleCatCarrierObjOppositeRingCatEvaluation, limitCone_pt, limitCone_π_app_app, limitPresheafOfModules_map, limitPresheafOfModules_obj, toPresheaf_preservesFiniteLimits, toPresheaf_preservesLimit	17
Total	21

PresheafOfModules

Definitions

Name	Category	Theorems
evaluationJointlyReflectsLimits 📖	CompOp	—
isLimitLimitCone 📖	CompOp	—
limitCone 📖	CompOp	2 math math: limitCone_π_app_app, limitCone_pt
limitPresheafOfModules 📖	CompOp	4 math math: limitPresheafOfModules_map, limitCone_π_app_app, limitPresheafOfModules_obj, limitCone_pt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evaluation_preservesFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits PresheafOfModules instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory evaluation	—	instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation UnivLE.small univLE_of_max UnivLE.self
evaluation_preservesLimit 📖	mathematical	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.types PresheafOfModules instCategory evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier	CategoryTheory.Limits.PreservesLimit	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
hasFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits PresheafOfModules instCategory	—	hasLimitsOfShape UnivLE.small univLE_of_max UnivLE.self
hasLimit 📖	mathematical	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.types PresheafOfModules instCategory evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier	CategoryTheory.Limits.HasLimit	—	—
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape PresheafOfModules instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize PresheafOfModules instCategory	—	hasLimitsOfShape UnivLE.small UnivLE.self
instHasLimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap 📖	mathematical	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.types PresheafOfModules instCategory evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier	CategoryTheory.Limits.HasLimit ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map	—	CategoryTheory.Limits.instHasLimitCompOfPreservesLimit ModuleCat.hasLimit ModuleCat.preservesLimit_restrictScalars
instPreservesLimitsOfShapeFunctorOppositeAbToPresheaf 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category toPresheaf	—	toPresheaf_preservesLimit small_subtype small_Pi UnivLE.small UnivLE.self
instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape PresheafOfModules instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory evaluation	—	evaluation_preservesLimit small_subtype small_Pi UnivLE.small UnivLE.self
instPreservesLimitsOfSizeFunctorOppositeAbToPresheaf 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category toPresheaf	—	instPreservesLimitsOfShapeFunctorOppositeAbToPresheaf UnivLE.small UnivLE.self
instPreservesLimitsOfSizeModuleCatCarrierObjOppositeRingCatEvaluation 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize PresheafOfModules instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory evaluation	—	instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation UnivLE.small UnivLE.self
limitCone_pt 📖	mathematical	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.types PresheafOfModules instCategory evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier	CategoryTheory.Limits.Cone.pt limitCone limitPresheafOfModules	—	—
limitCone_π_app_app 📖	mathematical	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.types PresheafOfModules instCategory evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier	Hom.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const limitPresheafOfModules CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π limitCone CategoryTheory.Limits.limit.π	—	—
limitPresheafOfModules_map 📖	mathematical	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.types PresheafOfModules instCategory evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier	map limitPresheafOfModules CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map instHasLimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap CategoryTheory.Limits.limMap CategoryTheory.Functor.whiskerLeft restriction CategoryTheory.Iso.inv CategoryTheory.preservesLimitIso	—	—
limitPresheafOfModules_obj 📖	mathematical	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.types PresheafOfModules instCategory evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier	obj limitPresheafOfModules CategoryTheory.Limits.limit	—	—
toPresheaf_preservesFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category toPresheaf	—	instPreservesLimitsOfShapeFunctorOppositeAbToPresheaf UnivLE.small univLE_of_max UnivLE.self
toPresheaf_preservesLimit 📖	mathematical	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory CategoryTheory.types PresheafOfModules instCategory evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier	CategoryTheory.Limits.PreservesLimit CategoryTheory.Functor Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category toPresheaf	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone CategoryTheory.Limits.comp_preservesLimit evaluation_preservesLimit ModuleCat.forget₂AddCommGroup_preservesLimit

---

← Back to Index