Documentation

Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits

Limits in categories of sheaves of modules #

In this file, it is shown that under suitable assumptions, limits exist in the category SheafOfModules R.

TODO #

source
๐Ÿ“ coverage
theorem PresheafOfModules.isSheaf_of_isLimit {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type uโ‚‚} [CategoryTheory.Category.{vโ‚‚, uโ‚‚} D] {R : CategoryTheory.Functor Cแต’แต– RingCat} {F : CategoryTheory.Functor D (PresheafOfModules R)} [โˆ€ (X : Cแต’แต–), Small.{v, max uโ‚‚ v} โ†‘((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat โ†‘(R.obj X)))).sections] {c : CategoryTheory.Limits.Cone F} [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrpCat] (hc : CategoryTheory.Limits.IsLimit c) (hF : โˆ€ (j : D), CategoryTheory.Presheaf.IsSheaf J (F.obj j).presheaf) :
CategoryTheory.Presheaf.IsSheaf J c.pt.presheaf
source
๐Ÿ“ coverage
instance SheafOfModules.instSmallElemForallObjCompModuleCatCarrierOppositeRingCatValPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type uโ‚‚} [CategoryTheory.Category.{vโ‚‚, uโ‚‚} D] {R : CategoryTheory.Sheaf J RingCat} (F : CategoryTheory.Functor D (SheafOfModules R)) [โˆ€ (X : Cแต’แต–), Small.{v, max uโ‚‚ v} โ†‘((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat โ†‘(R.val.obj X)))).sections] (X : Cแต’แต–) :
Small.{v, max uโ‚‚ v} โ†‘(((F.comp (forget R)).comp (PresheafOfModules.evaluation R.val X)).comp (CategoryTheory.forget (ModuleCat โ†‘(R.val.obj X)))).sections
source
๐Ÿ”ธ coverage
noncomputable instance SheafOfModules.createsLimit {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type uโ‚‚} [CategoryTheory.Category.{vโ‚‚, uโ‚‚} D] {R : CategoryTheory.Sheaf J RingCat} (F : CategoryTheory.Functor D (SheafOfModules R)) [โˆ€ (X : Cแต’แต–), Small.{v, max uโ‚‚ v} โ†‘((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat โ†‘(R.val.obj X)))).sections] [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrpCat] :
CategoryTheory.CreatesLimit F (forget R)
Equations
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.hasLimit {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type uโ‚‚} [CategoryTheory.Category.{vโ‚‚, uโ‚‚} D] {R : CategoryTheory.Sheaf J RingCat} (F : CategoryTheory.Functor D (SheafOfModules R)) [โˆ€ (X : Cแต’แต–), Small.{v, max uโ‚‚ v} โ†‘((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat โ†‘(R.val.obj X)))).sections] [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrpCat] :
    CategoryTheory.Limits.HasLimit F
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.evaluationPreservesLimit {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type uโ‚‚} [CategoryTheory.Category.{vโ‚‚, uโ‚‚} D] {R : CategoryTheory.Sheaf J RingCat} (F : CategoryTheory.Functor D (SheafOfModules R)) [โˆ€ (X : Cแต’แต–), Small.{v, max uโ‚‚ v} โ†‘((F.comp (evaluation R X)).comp (CategoryTheory.forget (ModuleCat โ†‘(R.val.obj X)))).sections] [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrpCat] (X : Cแต’แต–) :
    CategoryTheory.Limits.PreservesLimit F (evaluation R X)
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.hasLimitsOfShape {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} (D : Type uโ‚‚) [CategoryTheory.Category.{vโ‚‚, uโ‚‚} D] (R : CategoryTheory.Sheaf J RingCat) [Small.{v, uโ‚‚} D] :
    CategoryTheory.Limits.HasLimitsOfShape D (SheafOfModules R)
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.evaluationPreservesLimitsOfShape {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} (D : Type uโ‚‚) [CategoryTheory.Category.{vโ‚‚, uโ‚‚} D] (R : CategoryTheory.Sheaf J RingCat) [Small.{v, uโ‚‚} D] (X : Cแต’แต–) :
    CategoryTheory.Limits.PreservesLimitsOfShape D (evaluation R X)
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.forgetPreservesLimitsOfShape {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} (D : Type uโ‚‚) [CategoryTheory.Category.{vโ‚‚, uโ‚‚} D] (R : CategoryTheory.Sheaf J RingCat) [Small.{v, uโ‚‚} D] :
    CategoryTheory.Limits.PreservesLimitsOfShape D (forget R)
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.Finite.hasFiniteLimits {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) :
    CategoryTheory.Limits.HasFiniteLimits (SheafOfModules R)
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.Finite.evaluationPreservesFiniteLimits {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X : Cแต’แต–) :
    CategoryTheory.Limits.PreservesFiniteLimits (evaluation R X)
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.Finite.forgetPreservesFiniteLimits {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) :
    CategoryTheory.Limits.PreservesFiniteLimits (forget R)
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.hasLimitsOfSize {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) :
    CategoryTheory.Limits.HasLimitsOfSize.{vโ‚‚, v, max uโ‚ v, max (max (max (v + 1) u) uโ‚) vโ‚} (SheafOfModules R)
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.evaluationPreservesLimitsOfSize {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X : Cแต’แต–) :
    CategoryTheory.Limits.PreservesLimitsOfSize.{vโ‚‚, v, max uโ‚ v, v, max (max (max u uโ‚) (v + 1)) vโ‚, max u (v + 1)} (evaluation R X)
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.forgetPreservesLimitsOfSize {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) :
    CategoryTheory.Limits.PreservesLimitsOfSize.{vโ‚‚, v, max uโ‚ v, max uโ‚ v, max (max (max u uโ‚) (v + 1)) vโ‚, max (max (max u uโ‚) (v + 1)) vโ‚} (forget R)
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) :
    CategoryTheory.Limits.PreservesFiniteLimits ((toSheaf R).comp (CategoryTheory.sheafToPresheaf J AddCommGrpCat))
    source
    ๐Ÿ“ coverage
    instance SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf {C : Type uโ‚} [CategoryTheory.Category.{vโ‚, uโ‚} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) :
    CategoryTheory.Limits.PreservesFiniteLimits (toSheaf R)