Sheaves over Abelian categories

We provide instances for categories of sheaves over Abelian categories.

Main Results

• TopCat.Sheaf.exact_iff_stalkFunctor_map_exact: A complex of sheaves over a concrete abelian category is exact if and only if it is exact on stalks.

@[implicit_reducible]

noncomputable instance TopCat.instAbelianPresheaf {X : TopCat} {C : Type v₁} [CategoryTheory.Category.{v₂, v₁} C] [CategoryTheory.Abelian C] : CategoryTheory.Abelian (Presheaf C X)

Equations

• TopCat.instAbelianPresheaf = inferInstanceAs (CategoryTheory.Abelian (CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C))

@[implicit_reducible]

noncomputable instance TopCat.Sheaf.instAbelian {X : TopCat} {C : Type v₁} [CategoryTheory.Category.{v₂, v₁} C] [CategoryTheory.HasSheafify (Opens.grothendieckTopology ↑X) C] [CategoryTheory.Abelian C] : CategoryTheory.Abelian (Sheaf C X)

Equations

• TopCat.Sheaf.instAbelian = inferInstanceAs (CategoryTheory.Abelian (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) C))

instance TopCat.Sheaf.instAdditivePresheafForget {X : TopCat} {C : Type v₁} [CategoryTheory.Category.{v₂, v₁} C] [CategoryTheory.HasSheafify (Opens.grothendieckTopology ↑X) C] [CategoryTheory.Abelian C] : (forget C X).Additive

instance TopCat.Sheaf.instIsGrothendieckAbelian {X : TopCat} {D : Type u_1} [CategoryTheory.Category.{u, u_1} D] [CategoryTheory.Abelian D] [CategoryTheory.IsGrothendieckAbelian.{u, u, u_1} D] [CategoryTheory.HasSheafify (Opens.grothendieckTopology ↑X) D] : CategoryTheory.IsGrothendieckAbelian.{u, u, max u_1 u} (Sheaf D X)

instance TopCat.instAdditivePresheafStalkFunctor {X : TopCat} (p₀ : ↑X) {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasColimits C] : (Presheaf.stalkFunctor C p₀).Additive

The stalk functor is additive

instance TopCat.Sheaf.instPreservesFiniteLimitsCompPresheafForgetStalkFunctor {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C] {FC : C → C → Type u_1} {CC : C → Type u} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Abelian C] {X : TopCat} (p₀ : ↑X) : CategoryTheory.Limits.PreservesFiniteLimits ((forget C X).comp (Presheaf.stalkFunctor C p₀))

theorem TopCat.Sheaf.isZero_iff_stalkFunctor_obj_isZero {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C] {FC : C → C → Type u_1} {CC : C → Type u} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Abelian C] {X : TopCat} (F : Sheaf C X) : CategoryTheory.Limits.IsZero F ↔ ∀ (x : ↑X), CategoryTheory.Limits.IsZero (((forget C X).comp (Presheaf.stalkFunctor C x)).obj F)

A sheaf is zero if and only if its stalks are all zero.

theorem TopCat.Sheaf.exact_iff_stalkFunctor_map_exact {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C] {FC : C → C → Type u_1} {CC : C → Type u} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Abelian C] {X : TopCat} (S : CategoryTheory.ShortComplex (Sheaf C X)) : S.Exact ↔ ∀ (x : ↑X), (S.map ((forget C X).comp (Presheaf.stalkFunctor C x))).Exact

Exactness can be checked on stalks for complexes of sheaves.