mathlib3 documentation

topology.sheaves.abelian

Category of sheaves is abelian #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. Let C, D be categories and J be a grothendieck topology on C, when D is abelian and sheafification is possible in C, Sheaf J D is abelian as well (Sheaf_is_abelian).

Hence, presheaf_to_Sheaf is an additive functor (presheaf_to_Sheaf_additive).

@[protected, instance]

noncomputable def category_theory.functor.abelian {C : Type (max v u)} [category_theory.category C] {D : Type w} [category_theory.category D] [category_theory.abelian D] :

category_theory.abelian (Cᵒᵖ ⥤ D)

Equations

category_theory.functor.abelian = category_theory.abelian.functor_category_abelian

@[protected, instance]

def category_theory.Sheaf.limits.has_finite_products {C : Type (max v u)} [category_theory.category C] {D : Type w} [category_theory.category D] [category_theory.abelian D] {J : category_theory.grothendieck_topology C} :

category_theory.limits.has_finite_products (category_theory.Sheaf J D)

@[protected, instance]

noncomputable def category_theory.Sheaf_is_abelian {C : Type (max v u)} [category_theory.category C] {D : Type w} [category_theory.category D] [category_theory.abelian D] {J : category_theory.grothendieck_topology C} [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] [category_theory.concrete_category D] [category_theory.limits.preserves_limits (category_theory.forget D)] [Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)] [category_theory.reflects_isomorphisms (category_theory.forget D)] [category_theory.limits.has_finite_limits D] :

category_theory.abelian (category_theory.Sheaf J D)

Equations

category_theory.Sheaf_is_abelian = let adj : category_theory.presheaf_to_Sheaf J D ⊣ category_theory.Sheaf_to_presheaf J D := category_theory.sheafification_adjunction J D in category_theory.abelian_of_adjunction (category_theory.Sheaf_to_presheaf J D) (category_theory.presheaf_to_Sheaf J D) (category_theory.as_iso adj.counit) adj

@[protected, instance]

def category_theory.presheaf_to_Sheaf_additive {C : Type (max v u)} [category_theory.category C] {D : Type w} [category_theory.category D] [category_theory.abelian D] {J : category_theory.grothendieck_topology C} [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] [category_theory.concrete_category D] [category_theory.limits.preserves_limits (category_theory.forget D)] [Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)] [category_theory.reflects_isomorphisms (category_theory.forget D)] :

(category_theory.presheaf_to_Sheaf J D).additive