Gluing sections of sheaves on disjoint opens

Sections of a sheaf with values in a concrete category on two disjoint open sets glue to a section on their union, provided the forgetful functor preserves binary products. There is no compatibility condition on the intersection: the sections over the empty open form a terminal object, so the sections over the union form the binary product of those over the two opens, and the forgetful functor sends this product to the product of the underlying types. The hypothesis holds in particular for sheaves of commutative rings.

theorem TopCat.Sheaf.exists_section_sup_of_disjoint {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.forget C)] (F : Sheaf C X) {A B : TopologicalSpace.Opens ↑X} (hAB : Disjoint A B) (σ : CategoryTheory.ToType (F.obj.obj (Opposite.op A))) (ρ : CategoryTheory.ToType (F.obj.obj (Opposite.op B))) : ∃ (τ : CategoryTheory.ToType (F.obj.obj (Opposite.op (A ⊔ B)))), (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) τ = σ ∧ (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) τ = ρ

Sections of a sheaf with values in a concrete category on two disjoint opens glue to a section on their union, assuming that the forgetful functor preserves binary products.