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)))
: