TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing
theorem TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C]
[inst_2 : CategoryTheory.Limits.HasLimits C] [inst_3 : (CategoryTheory.forget C).ReflectsIsomorphisms]
[inst_4 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] {X : TopCat} (F : TopCat.Presheaf C X),
F.IsSheaf ↔ F.IsSheafUniqueGluing
The theorem `TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing` states that for any presheaf `F`, valued in a concrete category `C`, the condition for `F` to be a sheaf is equivalent to the condition for `F` to have unique gluings. This is under the assumptions that the category `C` has limits, the forgetful functor from `C` to its underlying type structure reflects isomorphisms and preserves limits. In other words, a presheaf over a topological space is a sheaf if and only if it satisfies the unique gluing property, given the certain conditions on the underlying category and its forgetful functor.
More concisely: A presheaf over a topological space is a sheaf if and only if it satisfies the unique gluing property, given that the underlying category has limits and the forgetful functor reflects isomorphisms and preserves limits.
|
TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types
theorem TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types :
∀ {X : TopCat} (F : TopCat.Presheaf (Type u) X), F.IsSheaf ↔ F.IsSheafUniqueGluing
This theorem states that for a presheaf `F` of types on a topological space `X`, the condition of being a sheaf (in the categorical sense) is equivalent to the condition of having unique "gluings". In other words, a presheaf is a sheaf if and only if, whenever we have a collection of sections (elements of the presheaf) defined on open sets that cover a given open set and that agree on intersections, there exists a unique section on the whole given open set that restricts to the given sections on each of the covering sets.
More concisely: A presheaf on a topological space is a sheaf if and only if it satisfies the unique gluing property: given any open cover and compatible sections, there exists a unique global section that restricts to them.
|
TopCat.Sheaf.existsUnique_gluing
theorem TopCat.Sheaf.existsUnique_gluing :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C]
[inst_2 : CategoryTheory.Limits.HasLimits C]
[inst_3 : CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms]
[inst_4 : CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat}
(F : TopCat.Sheaf C X) {ι : Type v} (U : ι → TopologicalSpace.Opens ↑X)
(sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (Opposite.op (U i)))),
TopCat.Presheaf.IsCompatible F.val U sf → ∃! s, TopCat.Presheaf.IsGluing F.val U sf s
The theorem `TopCat.Sheaf.existsUnique_gluing` states that, given a sheaf `F` on a topological space `X` in a category `C` with certain properties (such as having all (small) limits, and the forgetful functor from `C` to `Type` reflecting isomorphisms and preserving limits), for any family `U` of open subsets of `X` and any family `sf` of sections of the sheaf `F` over these open subsets that is compatible (in the sense of the sheaf condition), there exists a unique global section `s` that is a gluing of the given sections. This theorem provides a more convenient way to achieve a unique gluing of sections for a sheaf. The existence and uniqueness of such a gluing is one of the key properties of sheaves in category theory and topology.
More concisely: Given a sheaf on a topological space in a category with all small limits and reflecting isomorphisms, there exists a unique global section as the gluing of any compatible family of local sections.
|
TopCat.Sheaf.existsUnique_gluing'
theorem TopCat.Sheaf.existsUnique_gluing' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C]
[inst_2 : CategoryTheory.Limits.HasLimits C]
[inst_3 : CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms]
[inst_4 : CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat}
(F : TopCat.Sheaf C X) {ι : Type v} (U : ι → TopologicalSpace.Opens ↑X) (V : TopologicalSpace.Opens ↑X)
(iUV : (i : ι) → U i ⟶ V),
V ≤ iSup U →
∀ (sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (Opposite.op (U i)))),
TopCat.Presheaf.IsCompatible F.val U sf → ∃! s, ∀ (i : ι), (F.val.map (iUV i).op) s = sf i
This theorem states that, within the category of topological spaces `TopCat` and for a sheaf `F` representing objects from a concrete category `C` over a topological space `X`, given a family `U` of open subsets of `X` and a subset `V`, we can identify some inclusion homomorphisms `iUV` between the open subsets and `V` under the condition that `V` is a subset of the supremum of `U`. For a family `sf` of objects in `C` that are compatible with the presheaf `F`, there exists a unique `s` such that the mapping of `s` via the `F` functor equals the original `sf` for each open subset in `U`. This is a form of the gluing axiom in sheaf theory, which guarantees the existence and uniqueness of a global section `s` under certain conditions. This version of the lemma allows the user to specify the inclusion homomorphisms `iUV` directly, which can be more convenient in practice.
More concisely: Given a sheaf `F` over a topological space `X`, a family `U` of open subsets, a subset `V` contained in the supremum of `U`, and a compatible family `sf` of objects in the base category, there exists a unique global section `s` in `F(X)` such that `F(iUV)(s) = sf` for all `iUV` in `U`.
|
TopCat.Sheaf.eq_of_locally_eq'
theorem TopCat.Sheaf.eq_of_locally_eq' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C]
[inst_2 : CategoryTheory.Limits.HasLimits C]
[inst_3 : CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms]
[inst_4 : CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat}
(F : TopCat.Sheaf C X) {ι : Type v} (U : ι → TopologicalSpace.Opens ↑X) (V : TopologicalSpace.Opens ↑X)
(iUV : (i : ι) → U i ⟶ V),
V ≤ iSup U →
∀ (s t : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op V))),
(∀ (i : ι), (F.val.map (iUV i).op) s = (F.val.map (iUV i).op) t) → s = t
This theorem, `TopCat.Sheaf.eq_of_locally_eq'`, states that within a topological space `X` for a given sheaf `F` of a category `C` that has all small limits, reflects isomorphisms and preserves limits, if we have a family `U` of open subsets of `X` and another open subset `V` of `X` such that `V` is a subset of the indexed supremum of `U`, then for any two elements `s` and `t` of the object of the forgetful functor applied to the value of `F` at the opposite of `V`, if `s` and `t` are mapped to the same element under the map `F.val.map (iUV i).op` for every `i` in `ι`, then `s` and `t` must be equal. This theorem essentially says that if two elements of a sheaf have the same images under all inclusion maps from a covering family of open sets, then those two elements must be the same.
More concisely: If `F` is a sheaf on a topological space `X` with all small limits, and `U` is a family of open subsets of `X` such that `V` is the indexed supremum of `U`, then for any two elements `s` and `t` of `F(V)`, if `s` and `t` have the same image under `F.val.map (i ∈ ι) (iUV i).op`, then `s = t`.
|
TopCat.Presheaf.isSheaf_of_isSheafUniqueGluing_types
theorem TopCat.Presheaf.isSheaf_of_isSheafUniqueGluing_types :
∀ {X : TopCat} (F : TopCat.Presheaf (Type u) X), F.IsSheafUniqueGluing → F.IsSheaf
The theorem `TopCat.Presheaf.isSheaf_of_isSheafUniqueGluing_types` states that for any topological space `X` and any presheaf `F` of types on `X`, if `F` satisfies the sheaf condition in terms of unique gluings, then `F` is a sheaf. In other words, if a presheaf `F` on a topological space `X` has the property that sections over open covers can be uniquely glued together, then `F` is a sheaf, which means locally defined sections over an open cover can be glued together to form a global section.
More concisely: If a presheaf on a topological space satisfies the unique gluing condition, then it is a sheaf.
|