TopCat.Presheaf.stalk_hom_ext
theorem TopCat.Presheaf.stalk_hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
(F : TopCat.Presheaf C X) {x : ↑X} {Y : C} {f₁ f₂ : F.stalk x ⟶ Y},
(∀ (U : TopologicalSpace.Opens ↑X) (hxU : x ∈ U),
CategoryTheory.CategoryStruct.comp (F.germ ⟨x, hxU⟩) f₁ =
CategoryTheory.CategoryStruct.comp (F.germ ⟨x, hxU⟩) f₂) →
f₁ = f₂
This theorem states that for any category `C` that has all colimits, any topological space `X`, any `C`-valued presheaf `F` on `X`, any point `x` in `X`, and any two morphisms `f₁` and `f₂` from the stalk of `F` at `x` to some object `Y` in `C`, if for every open set `U` containing `x`, the composition of the germ morphism at `x` of `F` and `f₁` is equal to the composition of the germ morphism at `x` of `F` and `f₂`, then `f₁` is equal to `f₂`. In simpler terms, this theorem asserts that a morphism from the stalk of a presheaf at a point to another object is uniquely determined by its compositions with the germ morphisms.
More concisely: In any category with all colimits, if for any topological space `X`, presheaf `F` on `X`, point `x` in `X`, and morphisms `f₁` and `f₂` from the stalk of `F` at `x` to some object `Y`, the germ morphisms of `F` at `x` and `f₁` are equal to the germ morphisms of `F` at `x` and `f₂`, then `f₁` is equal to `f₂`.
|
TopCat.Presheaf.germ_exist
theorem TopCat.Presheaf.germ_exist :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
[inst_2 : CategoryTheory.ConcreteCategory C]
[inst_3 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (F : TopCat.Presheaf C X)
(x : ↑X) (t : (CategoryTheory.forget C).obj (F.stalk x)), ∃ U, ∃ (m : x ∈ U), ∃ s, (F.germ ⟨x, m⟩) s = t
The theorem `TopCat.Presheaf.germ_exist` states that for any presheaf valued in a concrete category `C`, where `C` has all (small) colimits and the forgetful functor from `C` preserves filtered colimits, every element of the stalk at a point `x` in a topological space `X` is the germ of a section. In other words, given an element `t` of the stalk of presheaf `F` at `x`, there exists an open set `U` containing `x` and a section `s` of `F` over `U` such that the germ of `s` at `x` is `t`. This essentially means we can "localize" elements of the stalk to sections over some open neighborhood of each point.
More concisely: For any presheaf over a topological space with values in a category having all small colimits and preserving filtered colimits by the forgetful functor, every stalk element has a local section.
|
TopCat.Presheaf.isIso_of_stalkFunctor_map_iso
theorem TopCat.Presheaf.isIso_of_stalkFunctor_map_iso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
[inst_2 : CategoryTheory.ConcreteCategory C]
[inst_3 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[inst_4 : CategoryTheory.Limits.HasLimits C]
[inst_5 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[inst_6 : (CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G)
[inst_7 : ∀ (x : ↑X), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C x).map f.val)],
CategoryTheory.IsIso f
This theorem states that if `F` and `G` are sheaves with values in a concrete category `C`, and the forgetful functor from `C` reflects isomorphisms and preserves both limits and filtered colimits, then if the stalk maps of a morphism `f : F ⟶ G` are all isomorphisms, `f` must also be an isomorphism. Essentially, it's saying that if all the stalk maps are isomorphisms (invertible maps), this property can be "lifted" to the whole morphism `f`, making `f` an isomorphism as well. This theorem is important in topology and algebraic geometry, where the study of sheaves and their stalks is a central topic.
More concisely: If `F` and `G` are sheaves on a site with values in a concrete category `C` and the forgetful functor reflects isomorphisms, preserves limits, and filtered colimits, then `f : F ⟶ G` is an isomorphism if and only if all its stalk maps are isomorphisms.
|
TopCat.Presheaf.section_ext
theorem TopCat.Presheaf.section_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
[inst_2 : CategoryTheory.ConcreteCategory C]
[inst_3 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[inst_4 : CategoryTheory.Limits.HasLimits C]
[inst_5 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[inst_6 : (CategoryTheory.forget C).ReflectsIsomorphisms] (F : TopCat.Sheaf C X) (U : TopologicalSpace.Opens ↑X)
(s t : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op U))),
(∀ (x : ↥U), (F.presheaf.germ x) s = (F.presheaf.germ x) t) → s = t
The theorem `TopCat.Presheaf.section_ext` states that for any sheaf `F` valued in a concrete category `C` (a category where every object is associated with a set and every morphism is a function between these sets), if the forgetful functor from `C` to the category of sets reflects isomorphisms, preserves limits and filtered colimits, then two sections `s` and `t` of the sheaf `F` over an open set `U` of a topological space `X` that agree on every stalk must be the same. A stalk of a sheaf `F` at a point `x` in the topological space is, roughly speaking, the direct limit of the sections of `F` over all open sets containing `x`, and the 'forgetful functor' from a category to the category of sets is the functor that 'forgets' the extra structure beyond the underlying set.
More concisely: If a sheaf over a topological space valued in a concrete category with reflecting isomorphisms, preserving limits and filtered colimits has agreeing sections on an open set, then these sections are equal.
|
TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective
theorem TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
[inst_2 : CategoryTheory.ConcreteCategory C]
[inst_3 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[inst_4 : CategoryTheory.Limits.HasLimits C]
[inst_5 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[inst_6 : (CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G)
(U : TopologicalSpace.Opens ↑X),
(∀ (x : ↥U), Function.Injective ⇑((TopCat.Presheaf.stalkFunctor C ↑x).map f.val)) →
(∀ (t : (CategoryTheory.forget C).obj (G.val.obj (Opposite.op U))) (x : ↥U),
∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (Opposite.op V)) s = (G.val.map iVU.op) t) →
Function.Surjective ⇑(f.val.app (Opposite.op U))
This theorem states that, for a morphism `f` between two sheaves `F` and `G` over a topological space `X`, in a category `C` that has colimits and limits and in which isomorphisms are reflected in the underlying type, if the induced morphisms on the stalks at each point in `X` are injective, and every global section of `G` has a local section of `F` mapping to it under `f`, then `f` is surjective on global sections. In simpler terms, if we can relate sections of `F` and `G` on a local level and the relations are one-to-one at each point, then we can extend this to a global one-to-one relationship.
More concisely: If `f: F --> G` is a morphism between sheaves on a topological space `X` in a category with colimits and limits and reflecting isomorphisms, with injective stalk morphisms and every global section of `G` having a local section of `F` mapping to it, then `f` is surjective on global sections.
|
TopCat.Presheaf.germ_stalkSpecializes
theorem TopCat.Presheaf.germ_stalkSpecializes :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
(F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {y : ↥U} {x : ↑X} (h : x ⤳ ↑y),
CategoryTheory.CategoryStruct.comp (F.germ y) (F.stalkSpecializes h) = F.germ ⟨x, ⋯⟩
The theorem `TopCat.Presheaf.germ_stalkSpecializes` states that for any category `C` that has all small colimits, given a topological space `X` and a `C`-valued presheaf `F` on `X`, for any open set `U` in `X` and points `x` and `y` in `U` such that `x` specializes to `y`, the composition of the germ of `F` at `y` and the specialization of the stalk of `F` at `x` to `y` is equal to the germ of `F` at `x`. This essentially captures a certain commutativity property in the category of topological spaces related to presheaves and the specialization of points.
More concisely: For any topological space `X`, presheaf `F` on `X` in a category with small colimits, and open sets `U`, points `x, y` in `U` with `x` specializing to `y`, the germ of `F` at `x` equals the composition of the germ of `F` at `y` and the specialization of the stalk of `F` at `x` to `y`.
|
TopCat.Presheaf.germ.proof_2
theorem TopCat.Presheaf.germ.proof_2 : ∀ {X : TopCat} {U : TopologicalSpace.Opens ↑X} (x : ↥U), ↑x ∈ U
This theorem states that for any topological space `X` and any open subset `U` of `X`, any point `x` in `U` (considered as a type of elements of `U`) is indeed an element of `U`. In mathematical terms, if `X` is a topological space and `U` is an open subset of `X`, then every point in `U` actually belongs to `U`. This might seem tautological, but it's an important base case in certain types of reasoning about topological spaces and presheaves.
More concisely: For any topological space X and open subset U, every element of U is an element of U.
|
TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso
theorem TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
[inst_2 : CategoryTheory.ConcreteCategory C]
[inst_3 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[inst_4 : CategoryTheory.Limits.HasLimits C]
[inst_5 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[inst_6 : (CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G),
CategoryTheory.IsIso f ↔ ∀ (x : ↑X), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C x).map f.val)
The theorem `TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso` states that for any two sheaves `F` and `G` in a concrete category `C` (a category that has a function to the category of sets that preserves the structure of the category), if the corresponding forgetful functor reflects isomorphisms, preserves limits and filtered colimits, then a morphism `f` from `F` to `G` is an isomorphism if and only if all of its stalk maps are isomorphisms. A stalk map in this context is the map induced on the stalks (an object at a point `x` in the space) of the sheaves by a morphism of sheaves. This essentially means that the local behavior of a sheaf morphism, as captured by its action on stalks, determines its global behavior.
More concisely: For sheaves in a concrete category with a reflecting, limit-preserving, and filtered colimit-preserving forgetful functor, a morphism is an isomorphism if and only if its stalk maps are isomorphisms.
|