CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts
theorem CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C] {X : C}
(S : CategoryTheory.Presieve X) [inst_2 : S.Extensive] (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v)))
[inst_3 : CategoryTheory.Limits.PreservesFiniteProducts F], CategoryTheory.Presieve.IsSheafFor F S
The theorem `CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts` states that for any category `C` which is `FinitaryPreExtensive`, for any presieve `S` on an object `X` in `C` that is extensive, and for any contravariant functor `F` from `C` to the category of Types (that preserves finite products), `F` is a sheaf for the presieve `S`. In simpler terms, if a functor preserves finite products and the topology is extensive, then the functor satisfies the sheaf condition, which is a certain property in category theory related to the gluing of sections.
More concisely: For any FinitaryPreExtensive category `C`, a contravariant functor `F` preserving finite products from `C` to Types makes `F` a sheaf for any extensive presieve on an object in `C`.
|
CategoryTheory.isSheaf_iff_preservesFiniteProducts
theorem CategoryTheory.isSheaf_iff_preservesFiniteProducts :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C]
[inst_2 : CategoryTheory.FinitaryExtensive C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))),
CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.extensiveCoverage C))
F ↔
Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F)
The theorem `CategoryTheory.isSheaf_iff_preservesFiniteProducts` states that for any category `C` which is `FinitaryExtensive`, a presheaf on `C` is a sheaf if and only if it preserves finite products. This means that a functor `F` from the opposite category of `C` to the category of Types is a sheaf with respect to the Grothendieck topology associated with the extensive coverage of `C` if and only if there exists a structure that shows `F` preserves finite products, i.e., the functor `F` maintains the property of product formation under the operation of taking the finite product of objects.
More concisely: A presheaf on a finitary extensive category is a sheaf if and only if it preserves finite products.
|