CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify_isSheaf
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify_isSheaf :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
{F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F),
CategoryTheory.Presieve.IsSheaf J F →
CategoryTheory.Presieve.IsSheaf J (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G).toPresheaf
This theorem states that for any category `C`, Grothendieck topology `J` on `C`, functor `F` from `Cᵒᵖ` to a type `w`, and a sub-presheaf `G` of the functor `F`, if `F` is a sheaf for the topology `J`, then the presheaf obtained by applying the `sheafify` operation to `G` and then converting the resulting sub-presheaf back into a presheaf is also a sheaf for the topology `J`. In other words, sheafifying a sub-presheaf and then converting it to a presheaf preserves the sheaf property when the original functor is a sheaf.
More concisely: If a functor sheafifies a sub-presheaf in a Grothendieck topology and is itself a sheaf, then the resulting presheaf is also a sheaf.
|
CategoryTheory.GrothendieckTopology.Subpresheaf.map
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
(self : CategoryTheory.GrothendieckTopology.Subpresheaf F) {U V : Cᵒᵖ} (i : U ⟶ V),
self.obj U ⊆ F.map i ⁻¹' self.obj V
This theorem states that if `G` is a sub-presheaf of `F` in a category `C`, and `i` is a morphism from `U` to `V` in the opposite category `Cᵒᵖ`, then for every section `x` of `G` on `U`, the image of `x` under the functor `F` mapped by `i` lies in `F(V)`. This is equivalent to saying that the preimage under `F` of the function `i` mapped on `x` belongs to `F(V)`. This theorem is a crucial part of describing how sections of a sub-presheaf transform under morphisms in the category.
More concisely: If `G` is a sub-presheaf of `F` in a category `C`, and `i` is a morphism in `Cᵒᵖ`, then for every section `x` of `G` on the domain of `i`, the image of `x` under the functor `F` lies in the image of `i`.
|
CategoryTheory.GrothendieckTopology.Subpresheaf.le_sheafify
theorem CategoryTheory.GrothendieckTopology.Subpresheaf.le_sheafify :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
{F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.GrothendieckTopology.Subpresheaf F),
G ≤ CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G
This theorem states that for any category `C`, Grothendieck topology `J` on `C`, and subpresheaf `G` on `C`, `G` is less than or equal to the sheafification of `G` with respect to `J`. In other words, in the context of category theory and Grothendieck topologies, any subpresheaf is always dominated by its sheafification.
More concisely: For any category `C`, Grothendieck topology `J`, and subpresheaf `G` on `C`, `G` is pointwise included in the sheafification of `G` with respect to `J`.
|