TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.proof_1
theorem TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.proof_1 :
∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] [inst_1 : CategoryTheory.Limits.HasProducts C]
{X : TopCat} (F : TopCat.Presheaf C X) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X),
CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i)))
This theorem states that for any category `C` with products, any `C`-valued presheaf `F` on a topological space `X`, and any family `U` of open subsets of `X` indexed by a type `ι`, there exists a limit of the functor from the discrete category on `ι` to `C` that sends each index `i` to the value of the presheaf `F` on the open subset `U i`. In other words, given a collection of open subsets of a topological space and a presheaf that assigns to each open set an object of a category, we can find a product in the category that represents all the objects assigned to the open sets by the presheaf.
More concisely: Given a topological space X, any C-valued presheaf F, and a family U of open subsets of X indexed by a type ι, there exists an object in C that is the limit of F over U.
|
TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.proof_1
theorem TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.proof_1 :
∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] [inst_1 : CategoryTheory.Limits.HasProducts C]
{X : TopCat} (F : TopCat.Presheaf C X) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X),
CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2)))
This theorem states that for any category `C` with products, any topological space `X`, any presheaf `F` of `C` on `X`, and any function `U` from an index set `ι` to the open sets of `X`, there is a limit in `C` for the functor from the discrete category on ι² to `C` that sends a pair `p` to the object of `F` corresponding to the intersection of `U p.1` and `U p.2`. In simpler terms, this is a condition for a presheaf `F` to be a sheaf in terms of equalizer products, stating that certain limits exist in the category.
More concisely: For any category with products, given a topological space, a presheaf, and a function to its open sets, the presheaf is a sheaf if and only if it satisfies the condition that for any index set and any pair of elements, the limit of the functor sending a pair to the intersection of their images exists in the category.
|
TopCat.Presheaf.isSheaf_iff_isSheafEqualizerProducts
theorem TopCat.Presheaf.isSheaf_iff_isSheafEqualizerProducts :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
(F : TopCat.Presheaf C X), F.IsSheaf ↔ F.IsSheafEqualizerProducts
This theorem states that for any category `C` with products, and for any presheaf `F` over a topological space `X`, the condition for `F` to be a sheaf is equivalent to the condition for `F` to be a sheaf in terms of an equalizer diagram. In other words, a presheaf `F` satisfies the sheaf condition if and only if it satisfies the equalizer products sheaf condition. In the context of category theory, this relates two different ways of defining what it means for a presheaf on a topological space to be a sheaf.
More concisely: A presheaf over a topological space is a sheaf if and only if it satisfies the equalizer products sheaf condition in its category.
|