Limits

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

Statistics

Metric	Count
Definitions createsLimit	1
Theorems isSheaf_of_isLimit, evaluationPreservesFiniteLimits, forgetPreservesFiniteLimits, hasFiniteLimits, evaluationPreservesLimit, evaluationPreservesLimitsOfShape, evaluationPreservesLimitsOfSize, forgetPreservesLimitsOfShape, forgetPreservesLimitsOfSize, hasLimit, hasLimitsOfShape, hasLimitsOfSize, instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf, instSmallElemForallObjCompModuleCatCarrierOppositeRingCatValPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections	15
Total	16

PresheafOfModules

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf_of_isLimit 📖	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.Presheaf.IsSheaf Ab AddCommGrpCat.instCategory presheaf	CategoryTheory.Limits.Cone.pt	—	CategoryTheory.Functor.map_id CategoryTheory.Functor.map_comp CategoryTheory.Sheaf.isSheaf_of_isLimit toPresheaf_preservesLimit

SheafOfModules

Definitions

Name	Category	Theorems
createsLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evaluationPreservesLimit 📖	mathematical	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory CategoryTheory.types SheafOfModules 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.comp_preservesLimit CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit PresheafOfModules.hasLimit instSmallElemForallObjCompModuleCatCarrierOppositeRingCatValPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections PresheafOfModules.evaluation_preservesLimit
evaluationPreservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape SheafOfModules instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory evaluation	—	evaluationPreservesLimit small_subtype small_Pi UnivLE.small UnivLE.self AddCommGrpCat.hasLimitsOfShape
evaluationPreservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize SheafOfModules instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory evaluation	—	evaluationPreservesLimitsOfShape UnivLE.small UnivLE.self
forgetPreservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape SheafOfModules instCategory PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory forget	—	CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit small_subtype small_Pi UnivLE.small UnivLE.self AddCommGrpCat.hasLimitsOfShape PresheafOfModules.hasLimit instSmallElemForallObjCompModuleCatCarrierOppositeRingCatValPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections
forgetPreservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize SheafOfModules instCategory PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory forget	—	forgetPreservesLimitsOfShape UnivLE.small 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 CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory CategoryTheory.types SheafOfModules 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	—	CategoryTheory.hasLimit_of_created PresheafOfModules.hasLimit instSmallElemForallObjCompModuleCatCarrierOppositeRingCatValPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape SheafOfModules instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self AddCommGrpCat.hasLimitsOfShape
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize SheafOfModules instCategory	—	hasLimitsOfShape UnivLE.small UnivLE.self
instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits SheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf toSheaf CategoryTheory.sheafToPresheaf	—	CategoryTheory.Limits.comp_preservesFiniteLimits Finite.forgetPreservesFiniteLimits PresheafOfModules.toPresheaf_preservesFiniteLimits
instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits SheafOfModules instCategory CategoryTheory.Sheaf AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Sheaf.instCategorySheaf toSheaf	—	CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms CategoryTheory.instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf CategoryTheory.Sheaf.instHasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits AddCommGrpCat.hasLimits CategoryTheory.Sheaf.instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits
instSmallElemForallObjCompModuleCatCarrierOppositeRingCatValPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections 📖	mathematical	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory CategoryTheory.types SheafOfModules instCategory evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier	PresheafOfModules PresheafOfModules.instCategory forget PresheafOfModules.evaluation	—	—

SheafOfModules.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evaluationPreservesFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits SheafOfModules SheafOfModules.instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory SheafOfModules.evaluation	—	SheafOfModules.evaluationPreservesLimitsOfShape UnivLE.small univLE_of_max UnivLE.self
forgetPreservesFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits SheafOfModules SheafOfModules.instCategory PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory SheafOfModules.forget	—	SheafOfModules.forgetPreservesLimitsOfShape UnivLE.small univLE_of_max UnivLE.self
hasFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits SheafOfModules SheafOfModules.instCategory	—	SheafOfModules.hasLimitsOfShape UnivLE.small univLE_of_max UnivLE.self

---

← Back to Index