Sheaves of abelian groups.

Results for sheaves of abelian groups on topological spaces.

theorem TopCat.Presheaf.sections_exact_of_exact {X : TopCat} {U : TopologicalSpace.Opens ↑X} {S : CategoryTheory.ShortComplex (Presheaf AddCommGrpCat X)} (hS : S.Exact) {s : ↑(S.X₂.obj (Opposite.op U))} (h : (CategoryTheory.ConcreteCategory.hom (S.g.app (Opposite.op U))) s = 0) : ∃ (t : ↑(S.X₁.obj (Opposite.op U))), (CategoryTheory.ConcreteCategory.hom (S.f.app (Opposite.op U))) t = s

theorem TopCat.Sheaf.sections_exact_of_left_exact {X : TopCat} {U : TopologicalSpace.Opens ↑X} {S : CategoryTheory.ShortComplex (Sheaf AddCommGrpCat X)} (hS : S.Exact) (hf : CategoryTheory.Mono S.f) (s : ↑(S.X₂.obj.obj (Opposite.op U))) (h : (CategoryTheory.ConcreteCategory.hom (S.g.hom.app (Opposite.op U))) s = 0) : ∃ (t : ↑(S.X₁.obj.obj (Opposite.op U))), (CategoryTheory.ConcreteCategory.hom (S.f.hom.app (Opposite.op U))) t = s

theorem TopCat.Presheaf.restrict_sum {X : TopCat} {U V : TopologicalSpace.Opens ↑X} {F : Presheaf AddCommGrpCat X} (h : V ≤ U) (s t : ↑(F.obj (Opposite.op U))) : restrictOpen (s + t) V h = restrictOpen s V h + restrictOpen t V h