CategoryTheory.GrothendieckTopology.sheafifyLift_unique
theorem CategoryTheory.GrothendieckTopology.sheafifyLift_unique :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
[inst_1 : CategoryTheory.Category.{max v u, w} D]
[inst_2 :
∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
CategoryTheory.Limits.HasMultiequalizer (S.index P)]
[inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q)
(γ : J.sheafify P ⟶ Q), CategoryTheory.CategoryStruct.comp (J.toSheafify P) γ = η → γ = J.sheafifyLift η hQ
The theorem `CategoryTheory.GrothendieckTopology.sheafifyLift_unique` states that in a category `C` with a Grothendieck topology `J`, for given functors `P` and `Q` from the opposite category `Cᵒᵖ` to another category `D`, if `P` has a multiequalizer for every cover in `J` and `D` has all colimits of shapes given by covers in `J`, then given a morphism `η` from `P` to `Q` and another morphism `γ` from the sheafification of `P` with respect to `J` to `Q`, if the composition of the morphism from `P` to its sheafification and `γ` equals `η`, then `γ` is unique and equals to the lift of `η` with respect to the sheafification process.
In other words, this theorem is about the uniqueness of morphisms in a certain context related to sheafification in the category theory, specifically in the context of Grothendieck topologies.
More concisely: Given functors `P` and `Q` from the opposite category of a Grothendieck topos `(C, J)` to category `D` with colimits of shapes given by covers in `J`, if `P` has a multiequalizer for every cover and `η: P ⥤ Q` has a unique lift `γ: ʃP ⥤ Q` to the sheafification `ʃP` of `P`, then `γ = η⊤`.
|
CategoryTheory.GrothendieckTopology.sheafify_isSheaf
theorem CategoryTheory.GrothendieckTopology.sheafify_isSheaf :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
[inst_1 : CategoryTheory.Category.{max v u, w} D] [inst_2 : CategoryTheory.ConcreteCategory D]
[inst_3 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)]
[inst_4 :
∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
CategoryTheory.Limits.HasMultiequalizer (S.index P)]
[inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[inst_6 : (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
[inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D),
CategoryTheory.Presheaf.IsSheaf J (J.sheafify P)
The theorem `CategoryTheory.GrothendieckTopology.sheafify_isSheaf` states that for any category `C` with a Grothendieck topology `J`, and any category `D` that is a concrete category and whose forgetful functor preserves limits, if for any functor `P` from the opposite category of `C` to `D`, any object `X` in `C`, and any cover `S` of `X` with respect to `J`, the multicospan associated with the indexing of the cover by `P` has a limit (multiequalizer), and if for any object `X` in `C`, `D` has colimits of the shape of the opposite category of the poset of covers of `X` with respect to `J`, and the forgetful functor of `D` preserves these colimits, and if the forgetful functor of `D` reflects isomorphisms, then the sheafification of `P` with respect to `J` is a sheaf.
More concisely: If a functor from the opposite category of a category with a Grothendieck topology to a concrete category preserves limits and colimits of certain shapes, and the forgetful functor reflects isomorphisms, then the sheafification of the functor with respect to the topology is a sheaf.
|
CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep
theorem CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
[inst_1 : CategoryTheory.Category.{max v u, w} D] [inst_2 : CategoryTheory.ConcreteCategory D]
[inst_3 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)]
[inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[inst_5 :
∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
CategoryTheory.Limits.HasMultiequalizer (S.index P)]
[inst_6 : (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
[inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D),
(∀ (X : C) (S : J.Cover X) (x y : (CategoryTheory.forget D).obj (P.obj (Opposite.op X))),
(∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y) →
CategoryTheory.Presheaf.IsSheaf J (J.plusObj P)
This theorem states that if `P` is a separated presheaf on a category `C` with respect to a Grothendieck topology `J`, and `D` is a category that has some additional properties, such as being a concrete category and preserving limits under a forgetful functor, then the functor `P⁺` associated with `P` is a sheaf. More specifically, given a functor `P : Cᵒᵖ → D` and assuming for all `X` in `C`, `S` in `J.Cover X`, and any two objects `x` and `y` in the image under the functor `P` of `X`, if for all arrows `I` in `S`, the images under `P` of `x` and `y` via `I.f` are equal, then `x` and `y` must be equal. Under these conditions, `P⁺` is a sheaf with respect to `J`.
More concisely: Given a separated presheaf `P : C^{(op)} → D` on a category `C` with respect to a Grothendieck topology `J`, if for all `X` in `C`, `S` in `J.Cover X`, and any two objects `x` and `y` in the image under `P` of `X` with equal images under `P` of all arrows `I` in `S`, then `x` and `y` are equal, and `D` has the property of preserving limits under a forgetful functor, then `P⁺` is a sheaf on `(C, J)`.
|
CategoryTheory.GrothendieckTopology.Plus.sep
theorem CategoryTheory.GrothendieckTopology.Plus.sep :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
[inst_1 : CategoryTheory.Category.{max v u, w} D] [inst_2 : CategoryTheory.ConcreteCategory D]
[inst_3 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)]
[inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[inst_5 :
∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
CategoryTheory.Limits.HasMultiequalizer (S.index P)]
[inst_6 : (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
{X : C} (P : CategoryTheory.Functor Cᵒᵖ D) (S : J.Cover X)
(x y : (CategoryTheory.forget D).obj ((J.plusObj P).obj (Opposite.op X))),
(∀ (I : S.Arrow), ((J.plusObj P).map I.f.op) x = ((J.plusObj P).map I.f.op) y) → x = y
This theorem states that for any category 'C' with a Grothendieck topology 'J', and any category 'D' which is a concrete category and has certain limits preserved by the forgetful functor, given any functor 'P' from the opposite of category 'C' to 'D' and a cover 'S' of an object 'X' in 'C', then for every two objects 'x' and 'y' in the image of the object 'X' under the plus construction of 'P' in the category 'D', if for all arrows 'I' in the cover 'S', their action on 'x' and 'y' after applying the plus construction of 'P' is the same, then 'x' and 'y' are equal. This essentially says that the plus construction ('P⁺') is always separated.
More concisely: Given a Grothendieck topology 'J' on a category 'C', a concrete category 'D' with preserved limits, a functor 'P' from 'C'⃚ to 'D', and a cover 'S' of an object 'X' in 'C', if for all 'I' in 'S' and objects 'x' and 'y' in the image of 'X' under 'P⁺', 'P(I)(x) = P(I)(y)', then 'x = y' in 'D'.
|
CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift
theorem CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
[inst_1 : CategoryTheory.Category.{max v u, w} D]
[inst_2 :
∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
CategoryTheory.Limits.HasMultiequalizer (S.index P)]
[inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q),
CategoryTheory.CategoryStruct.comp (J.toSheafify P) (J.sheafifyLift η hQ) = η
This theorem states that, given a Grothendieck topology `J` on a category `C`, two functors `P` and `Q` from the opposite of `C` to another category `D`, a natural transformation `η` from `P` to `Q`, and assuming that `Q` is a sheaf with respect to `J`, the composition of the morphism from `P` to the sheafification of `P` with respect to `J` and the lift of `η` to the sheafification of `P` is equal to `η`. This holds under the conditions that for every object `X` in `C` and every cover `S` of `X` with respect to `J`, the multicospan associated with the indexing of `S` by `P` has a limit, and `D` has colimits of shapes indexed by the opposite of the set of covers of each object in `C`.
More concisely: Given a Grothendieck topology on a category, if two oppositely-valued functors with a natural transformation between them, and one is a sheaf, then the composition of their morphisms to their respective sheafifications equals the natural transformation, provided the limits of multicospans associated with covers exist and the opposing category has colimits of cover shapes.
|
CategoryTheory.GrothendieckTopology.Plus.isSheaf_plus_plus
theorem CategoryTheory.GrothendieckTopology.Plus.isSheaf_plus_plus :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
[inst_1 : CategoryTheory.Category.{max v u, w} D] [inst_2 : CategoryTheory.ConcreteCategory D]
[inst_3 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)]
[inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[inst_5 :
∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
CategoryTheory.Limits.HasMultiequalizer (S.index P)]
[inst_6 : (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
[inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D),
CategoryTheory.Presheaf.IsSheaf J (J.plusObj (J.plusObj P))
The theorem `CategoryTheory.GrothendieckTopology.Plus.isSheaf_plus_plus` states that for any category `C` with a Grothendieck topology `J`, and any category `D` that is a concrete category and where the forgetful functor from `D` to the type preserves limits, if for all objects `X` in `C`, there exists colimits of shape `(J.Cover X)ᵒᵖ` in `D`, and for any functor `P` from the opposite category of `C` to `D`, for any object `X` in `C` and a cover `S` over `X`, if the index of `S` over `P` has a multiequalizer, and the forgetful functor from `D` preserves colimits of shape `(J.Cover X)ᵒᵖ`, and reflects isomorphisms, then the functor `P` composed twice with the plus construction (denoted by `P⁺⁺`) is a sheaf with respect to the topology `J`. In essence, this theorem is about the sheaf property of the double plus construction in the context of Grothendieck topologies.
More concisely: Given a Grothendieck topology J on a category C and a concrete category D with preservation of limits and reflection of isomorphisms, if for each X in C there exists a colimit of shape (J.Cover X)ᵒᵖ in D, and for any functor P from the opposite of C to D, if the index of a cover S over X has a multiequalizer and forgetful functor from D preserves and reflects colimits of shape (J.Cover X)ᵒᵖ, then P composed with the plus construction is a sheaf on C with respect to J.
|