TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections
theorem TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} (F : TopCat.Presheaf C X),
F.IsSheaf ↔ F.IsSheafPairwiseIntersections
The theorem `TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections` states that for any category `C`, any topological space `X` in the category of topological spaces (`TopCat`), and any `C`-valued presheaf `F` on `X`, the condition of `F` being a sheaf is equivalent to `F` satisfying the sheaf condition for pairwise intersections. In other words, a presheaf is a sheaf if and only if, whenever we take the limit over an open set `U i` and its intersection with another open set `U j`, the presheaf satisfies the sheaf condition.
More concisely: A presheaf on a topological space is a sheaf if and only if it satisfies the sheaf condition for pairwise intersections.
|
TopCat.Presheaf.isSheaf_iff_isSheafPreservesLimitPairwiseIntersections
theorem TopCat.Presheaf.isSheaf_iff_isSheafPreservesLimitPairwiseIntersections :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} (F : TopCat.Presheaf C X),
F.IsSheaf ↔ F.IsSheafPreservesLimitPairwiseIntersections
The theorem `TopCat.Presheaf.isSheaf_iff_isSheafPreservesLimitPairwiseIntersections` states that for any category `C`, and any presheaf `F` on a topological space `X` in the category of topological spaces (`TopCat`), `F` satisfies the sheaf condition if and only if `F` preserves the limit of the diagram consisting of open subsets `U i` and their pairwise intersections `U i ⊓ U j`. Here, the sheaf condition in terms of an equalizer diagram is equivalent to the reformulation in terms of the presheaf preserving the limit of the diagram.
More concisely: A presheaf on a topological space in `TopCat` satisfies the sheaf condition if and only if it preserves the limit of the diagram consisting of open subsets and their pairwise intersections.
|
TopCat.Presheaf.isSheafOpensLeCover_iff_isSheafPairwiseIntersections
theorem TopCat.Presheaf.isSheafOpensLeCover_iff_isSheafPairwiseIntersections :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} (F : TopCat.Presheaf C X),
F.IsSheafOpensLeCover ↔ F.IsSheafPairwiseIntersections
This theorem, `TopCat.Presheaf.isSheafOpensLeCover_iff_isSheafPairwiseIntersections`, establishes an equivalence between two different conditions that can be used to define a sheaf of presheaves on a topological space.
Specifically, for any category `C`, any topological space `X`, and any `C`-valued presheaf `F` on `X`, the property of `F` being a sheaf with respect to the cover of open sets `U i` (denoted by `F.IsSheafOpensLeCover`) is equivalent to the property of `F` being a sheaf with respect to the pairwise intersections of these open sets (denoted by `F.IsSheafPairwiseIntersections`).
In other words, a presheaf is a sheaf if and only if it satisfies the sheaf condition for both the open cover and their pairwise intersections. This theorem hence provides two equivalent ways to check if a presheaf is indeed a sheaf.
More concisely: For any topological space X and C-valued presheaf F on X, F is a sheaf if and only if it satisfies the sheaf condition for both the open cover and their pairwise intersections.
|