Sheaves

We define sheaves on a topological space, with values in an arbitrary category.

A presheaf on a topological space X is a sheaf precisely when it is a sheaf under the Grothendieck topology on opens X, which expands out to say: For each open cover { Uᵢ } of U, and a family of compatible functions A ⟶ F(Uᵢ) for an A : X, there exists a unique gluing A ⟶ F(U) compatible with the restriction.

See the docstring of TopCat.Presheaf.IsSheaf for an explanation on the design decisions and a list of equivalent conditions.

We provide the instance CategoryTheory.Category (TopCat.Sheaf C X) as the full subcategory of presheaves, and the fully faithful functor Sheaf.forget : TopCat.Sheaf C X ⥤ TopCat.Presheaf C X.

def TopCat.Presheaf.IsSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (F : Presheaf C X) : Prop

The sheaf condition has several different equivalent formulations. The official definition chosen here is in terms of Grothendieck topologies so that the results on sites could be applied here easily, and this condition does not require additional constraints on the value category. The equivalent formulations of the sheaf condition on presheaf C X are as follows :

1. TopCat.Presheaf.IsSheaf: (the official definition) It is a sheaf with respect to the Grothendieck topology on opens X, which is to say: For each open cover { Uᵢ } of U, and a family of compatible functions A ⟶ F(Uᵢ) for an A : X, there exists a unique gluing A ⟶ F(U) compatible with the restriction.

2. TopCat.Presheaf.IsSheafEqualizerProducts: (requires C to have all products) For each open cover { Uᵢ } of U, F(U) ⟶ ∏ᶜ F(Uᵢ) is the equalizer of the two morphisms ∏ᶜ F(Uᵢ) ⟶ ∏ᶜ F(Uᵢ ∩ Uⱼ). See TopCat.Presheaf.isSheaf_iff_isSheafEqualizerProducts.

3. TopCat.Presheaf.IsSheafOpensLeCover: For each open cover { Uᵢ } of U, F(U) is the limit of the diagram consisting of arrows F(V₁) ⟶ F(V₂) for every pair of open sets V₁ ⊇ V₂ that are contained in some Uᵢ. See TopCat.Presheaf.isSheaf_iff_isSheafOpensLeCover.

4. TopCat.Presheaf.IsSheafPairwiseIntersections: For each open cover { Uᵢ } of U, F(U) is the limit of the diagram consisting of arrows from F(Uᵢ) and F(Uⱼ) to F(Uᵢ ∩ Uⱼ) for each pair (i, j). See TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections.

The following requires C to be concrete and complete, and forget C to reflect isomorphisms and preserve limits. This applies to most "algebraic" categories, e.g. groups, abelian groups and rings.

5. TopCat.Presheaf.IsSheafUniqueGluing: (requires C to be concrete and complete; forget C to reflect isomorphisms and preserve limits) For each open cover { Uᵢ } of U, and a compatible family of elements x : F(Uᵢ), there exists a unique gluing x : F(U) that restricts to the given elements. See TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing.

6. The underlying sheaf of types is a sheaf. See TopCat.Presheaf.isSheaf_iff_isSheaf_comp and CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget.

Equations

• F.IsSheaf = CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑X) F

theorem TopCat.Presheaf.isSheaf_unit {X : TopCat} (F : Presheaf (CategoryTheory.Discrete Unit) X) : F.IsSheaf

The presheaf valued in Unit over any topological space is a sheaf.

theorem TopCat.Presheaf.isSheaf_iso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {F G : Presheaf C X} (α : F ≅ G) : F.IsSheaf ↔ G.IsSheaf

theorem TopCat.Presheaf.isSheaf_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {F G : Presheaf C X} (α : F ≅ G) (h : F.IsSheaf) : G.IsSheaf

Transfer the sheaf condition across an isomorphism of presheaves.

def TopCat.Sheaf (C : Type u) [CategoryTheory.Category.{v, u} C] (X : TopCat) : Type (max u v w)

A TopCat.Sheaf C X is a presheaf of objects from C over a (bundled) topological space X, satisfying the sheaf condition.

Equations

• TopCat.Sheaf C X = CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) C

instance TopCat.instCategorySheaf (C : Type u_3) [CategoryTheory.Category.{u_1, u_3} C] (X : TopCat) : CategoryTheory.Category.{max u_1 u_2, max (max u_3 u_1) u_2} (Sheaf C X)

Equations

• TopCat.instCategorySheaf C X = CategoryTheory.Sheaf.instCategorySheaf

@[reducible, inline]

abbrev TopCat.Sheaf.presheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (F : Sheaf C X) : Presheaf C X

The underlying presheaf of a sheaf

Equations

• F.presheaf = F.val

instance TopCat.sheafInhabited (X : TopCat) : Inhabited (Sheaf (CategoryTheory.Discrete PUnit.{1}) X)

Equations

• X.sheafInhabited = { default := { val := CategoryTheory.Functor.star (TopologicalSpace.Opens ↑X)ᵒᵖ, cond := ⋯ } }

def TopCat.Sheaf.forget (C : Type u) [CategoryTheory.Category.{v, u} C] (X : TopCat) : CategoryTheory.Functor (Sheaf C X) (Presheaf C X)

The forgetful functor from sheaves to presheaves.

Equations

• TopCat.Sheaf.forget C X = CategoryTheory.sheafToPresheaf (Opens.grothendieckTopology ↑X) C

instance TopCat.Sheaf.forget_full (C : Type u) [CategoryTheory.Category.{v, u} C] (X : TopCat) : (forget C X).Full

instance TopCat.Sheaf.forgetFaithful (C : Type u) [CategoryTheory.Category.{v, u} C] (X : TopCat) : (forget C X).Faithful

theorem TopCat.Sheaf.id_app (C : Type u) [CategoryTheory.Category.{v, u} C] (X : TopCat) (F : Sheaf C X) (t : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (CategoryTheory.CategoryStruct.id F).val.app t = CategoryTheory.CategoryStruct.id (F.val.obj t)

theorem TopCat.Sheaf.comp_app (C : Type u) [CategoryTheory.Category.{v, u} C] (X : TopCat) {F G H : Sheaf C X} (f : F ⟶ G) (g : G ⟶ H) (t : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (CategoryTheory.CategoryStruct.comp f g).val.app t = CategoryTheory.CategoryStruct.comp (f.val.app t) (g.val.app t)

theorem TopCat.Presheaf.IsSheaf.section_ext {X : TopCat} {A : Type u_1} [CategoryTheory.Category.{u, u_1} A] {FC : A → A → Type u_2} {CC : A → Type u} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [(CategoryTheory.forget A).ReflectsIsomorphisms] {F : Presheaf A X} (hF : F.IsSheaf) {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} {s t : CategoryTheory.ToType (F.obj U)} (hst : ∀ x ∈ Opposite.unop U, ∃ (V : TopologicalSpace.Opens ↑X) (hV : V ≤ Opposite.unop U), x ∈ V ∧ (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hV).op)) s = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hV).op)) t) : s = t