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, instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections	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.Presheaf.IsSheaf Ab AddCommGrpCat.instCategory presheaf CategoryTheory.Limits.Cone.pt PresheafOfModules instCategory	—	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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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 SheafOfModules instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf RingCat.ring ModuleCat.moduleCategory evaluation	—	CategoryTheory.Limits.comp_preservesLimit CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit PresheafOfModules.hasLimit instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections PresheafOfModules.evaluation_preservesLimit
evaluationPreservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape SheafOfModules instCategory ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf RingCat.ring ModuleCat.moduleCategory evaluation	—	evaluationPreservesLimitsOfShape UnivLE.small UnivLE.self
forgetPreservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape SheafOfModules instCategory PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf PresheafOfModules.instCategory forget	—	CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit small_subtype small_Pi UnivLE.small UnivLE.self AddCommGrpCat.hasLimitsOfShape PresheafOfModules.hasLimit instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections
forgetPreservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize SheafOfModules instCategory PresheafOfModules CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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 SheafOfModules instCategory	—	CategoryTheory.hasLimit_of_created PresheafOfModules.hasLimit instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections
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.ObjectProperty.FullSubcategory.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf toSheaf	—	CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι CategoryTheory.Sheaf.instHasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits AddCommGrpCat.hasLimits CategoryTheory.Sheaf.instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits
instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections 📖	mathematical	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp ModuleCat RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf RingCat.ring ModuleCat.moduleCategory CategoryTheory.types PresheafOfModules PresheafOfModules.instCategory SheafOfModules instCategory forget PresheafOfModules.evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier	—	—

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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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