Restriction maps of presheaves

Composing restriction maps along inclusions of opens in both directions gives the identity after any morphism into the starting section object, since the inclusions force the opens to be equal; in particular restriction from an open to itself is the identity on sections. A family of sections over opens is compatible as soon as any two of its sections are restrictions of a common section in the family, and two sections of a sheaf of types that agree on the intersection of their domains glue to a section over the union.

Main results

• TopCat.Presheaf.comp_map_comp_map_eq_self: composing restriction maps along inclusions in both directions gives the identity after any morphism into the starting section object.
• TopCat.Presheaf.map_apply_eq_self: restriction from an open to itself is the identity on sections.
• TopCat.Presheaf.isCompatible_of_directed: a family of sections, any two of which are restrictions of a common member, is compatible.
• TopCat.Presheaf.IsSheaf.exists_gluing_sup: two sections of a sheaf of types that agree on the intersection of their domains glue to a section over the union.

theorem TopCat.Presheaf.comp_map_comp_map_eq_self {C : Type u} [CategoryTheory.Category.{v, u} C] {T : TopCat} {F : Presheaf C T} {A : C} {V V' : TopologicalSpace.Opens ↑T} (a : A ⟶ F.obj (Opposite.op V)) (i : Opposite.op V ⟶ Opposite.op V') (j : Opposite.op V' ⟶ Opposite.op V) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp a (F.map i)) (F.map j) = a

Composing restriction maps along inclusions of opens in both directions gives the identity after any morphism into the starting section object, since those inclusions force the opens to be equal. The sections are given by a morphism a into F.obj (op V), so that the lemma applies by exact even when the intermediate open is only definitionally equal to the one in the composite.

@[simp]

theorem TopCat.Presheaf.map_apply_eq_self {C : Type u} [CategoryTheory.Category.{v, u} C] {T : TopCat} {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] (F : Presheaf C T) {V : TopologicalSpace.Opens ↑T} (i : Opposite.op V ⟶ Opposite.op V) (s : CategoryTheory.ToType (F.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (F.map i)) s = s

Restriction from an open to itself is the identity on sections: there is only one morphism from an open to itself, the identity.

theorem TopCat.Presheaf.isCompatible_of_directed {C : Type u} [CategoryTheory.Category.{v, u} C] {T : TopCat} {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {F : Presheaf C T} {ι : Type u_3} {U : ι → TopologicalSpace.Opens ↑T} {sf : (i : ι) → CategoryTheory.ToType (F.obj (Opposite.op (U i)))} (h : ∀ (i j : ι), ∃ (k : ι) (hik : U i ≤ U k) (hjk : U j ≤ U k), (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hik).op)) (sf k) = sf i ∧ (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hjk).op)) (sf k) = sf j) : F.IsCompatible U sf

A family of sections over a directed family of opens is compatible as soon as any two of its sections are restrictions of a common section in the family.

theorem TopCat.Presheaf.IsSheaf.exists_gluing_sup {T : TopCat} {F : Presheaf (Type u) T} (hF : F.IsSheaf) {U V : TopologicalSpace.Opens ↑T} (a : F.obj (Opposite.op U)) (b : F.obj (Opposite.op V)) (h : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) a = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) b) : ∃ (s : F.obj (Opposite.op (U ⊔ V))), (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) s = a ∧ (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) s = b

Two sections of a sheaf of types over U and V that agree on U ⊓ V glue to a section over U ⊔ V.