TopCat.Presheaf.isSheaf_iff_isSheaf_comp'
theorem TopCat.Presheaf.isSheaf_iff_isSheaf_comp' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [inst_2 : G.ReflectsIsomorphisms]
[inst_3 : CategoryTheory.Limits.HasLimitsOfSize.{v, v, v₁, u₁} C]
[inst_4 : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, v₁, v₂, u₁, u₂} G] {X : TopCat}
(F : TopCat.Presheaf C X), F.IsSheaf ↔ TopCat.Presheaf.IsSheaf (CategoryTheory.Functor.comp F G)
This theorem states that if we have a functor `G : C ⥤ D` which both reflects isomorphisms and preserves limits (given that all limits exist in `C`), then the condition for a presheaf `F : presheaf C X` to be a sheaf is equivalent to checking the sheaf condition for the composition `F ⋙ G`. This can be particularly useful when `C` is a concrete category with a forgetful functor that preserves limits and reflects isomorphisms, as it implies we only need to check the sheaf condition on the underlying sheaf of types. Another example where this is valuable is the forgetful functor `TopCommRing ⥤ Top`. This theorem is actually proven in a stronger form that allows for an arbitrary target category.
More concisely: If functor `G : C -> D` reflects isomorphisms and preserves limits, then the condition for a presheaf `F : C -> Set` to be a sheaf is equivalent to `F ⋙ G` being a sheaf in category `D`.
|
TopCat.Presheaf.isSheaf_iff_isSheaf_comp
theorem TopCat.Presheaf.isSheaf_iff_isSheaf_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v, u₂} D] (G : CategoryTheory.Functor C D) [inst_2 : G.ReflectsIsomorphisms]
[inst_3 : CategoryTheory.Limits.HasLimits C] [inst_4 : CategoryTheory.Limits.PreservesLimits G] {X : TopCat}
(F : TopCat.Presheaf C X), F.IsSheaf ↔ TopCat.Presheaf.IsSheaf (CategoryTheory.Functor.comp F G)
This theorem states that for any two categories `C` and `D`, given a functor `G` from `C` to `D` that reflects isomorphisms and preserves limits, and assuming `C` has all (small) limits, a `C`-valued presheaf `F` on a topological space `X` is a sheaf if and only if the composed functor `F` followed by `G` is a sheaf. Here, a sheaf is a presheaf that satisfies certain gluing conditions for sections over open sets.
More concisely: Given a functor `G` from category `C` to `D` that reflects isomorphisms and preserves limits over a category `C` with all limits, a `C`-valued presheaf `F` is a sheaf if and only if the composed functor `F ∘ G` is a sheaf.
|