CategoryTheory.Functor.cover_lift
theorem CategoryTheory.Functor.cover_lift :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_5, u_2} D] (G : CategoryTheory.Functor C D)
(J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
[inst_2 : G.IsCocontinuous J K] {U : C} {S : CategoryTheory.Sieve (G.obj U)},
S ∈ K.sieves (G.obj U) → CategoryTheory.Sieve.functorPullback G S ∈ J.sieves U
This theorem, `CategoryTheory.Functor.cover_lift`, asserts that for any categories `C` and `D` with a functor `G` between them, if `G` is cocontinuous with respect to Grothendieck topologies `J` on `C` and `K` on `D`, then for any object `U` in `C` and any sieve `S` on `G(U)` in `D` that belongs to the topology `K`, the pullback of `S` along `G` to `U` in `C` belongs to the topology `J`. This essentially states a condition for lifting covers from the codomain to the domain of a functor in the context of Grothendieck topologies.
More concisely: Given functors between categories `G: C -> D`, cocontinuous with respect to Grothendieck topologies `J` on `C` and `K` on `D`, for any object `U` in `C` and sieve `S` on `G(U)` in `D` belonging to `K`, the pullback of `S` along `G` is a subobject of `Ob(C/U)` belonging to `J`.
|
CategoryTheory.isCocontinuous_comp
theorem CategoryTheory.isCocontinuous_comp :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_5, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{u_6, u_3} E]
(G : CategoryTheory.Functor C D) (G' : CategoryTheory.Functor D E) (J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D) {L : CategoryTheory.GrothendieckTopology E}
[inst_3 : G.IsCocontinuous J K] [inst_4 : G'.IsCocontinuous K L], (G.comp G').IsCocontinuous J L
The theorem `CategoryTheory.isCocontinuous_comp` states that if we have two functors `G: C -> D` and `G': D -> E` between three categories `C, D, E`, and if each of these functors is cocontinuous with respect to given Grothendieck topologies `J, K, L` on `C, D, E` respectively, then the composition of these functors `(G.comp G')` is also cocontinuous with respect to the Grothendieck topologies `J` and `L`. In other words, the property of being cocontinuous is preserved under the composition of functors.
More concisely: If functors $G: C \to D$ and $G': D \to E$ between categories $C, D, E$ are cocontinuous with respect to Grothendieck topologies $J$ on $C$, $K$ on $D$, and $L$ on $E$ respectively, then their composition $G \circ G'$ is cocontinuous with respect to $J$ and $L$.
|
CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection_is_unique
theorem CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection_is_unique :
∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
{G : CategoryTheory.Functor C D} {A : Type w} [inst_2 : CategoryTheory.Category.{max u v, w} A]
[inst_3 : CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D} [inst_4 : G.IsCocontinuous J K] (ℱ : CategoryTheory.Sheaf J A) {X : A}
{U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U)
{x :
CategoryTheory.Presieve.FamilyOfElements
(((CategoryTheory.ran G.op).obj ℱ.val).comp (CategoryTheory.coyoneda.obj (Opposite.op X))) S.arrows}
(hx : x.Compatible)
(y :
(((CategoryTheory.ran G.op).obj ℱ.val).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).obj (Opposite.op U)),
x.IsAmalgamation y → y = CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection ℱ hS hx
This theorem states that the amalgamation in the glued section of a sheaf is unique. More specifically, given categories `C` and `D`, a functor `G` from `C` to `D`, a Grothendieck topology `J` on `C` and `K` on `D`, and the functor `G` is cocontinuous from `J` to `K`. Let `A` be another category that has all limits, `ℱ` a sheaf on `J` with values in `A`, and `X` an object in `A`. Further, let `U` be an object in `D` and `S` be a sieve on `U` that is in the Grothendieck topology `K`. Suppose `x` is a family of elements that is compatible with the arrows of the sieve `S` and the functor obtained by composing `ℱ.val` with `ran G.op` and `coyoneda.obj (Opposite.op X)`. If `y` is an amalgamation of `x`, then `y` is equal to the glued section of `ℱ` with respect to the sieve `S` and the compatibility condition `hx`. The glued section here refers to a construct in sheaf theory, denoting a section that has been constructed by "gluing" together local sections over the sieves in a Grothendieck topology.
More concisely: Given a cocontinuous functor between categories with Grothendieck topologies and a sheaf, any two amalgamations of compatible local sections over a sieve are equal to each other and the glued section of the sheaf with respect to that sieve.
|
CategoryTheory.RanIsSheafOfIsCocontinuous.helper
theorem CategoryTheory.RanIsSheafOfIsCocontinuous.helper :
∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
{G : CategoryTheory.Functor C D} {A : Type w} [inst_2 : CategoryTheory.Category.{max u v, w} A]
[inst_3 : CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D} [inst_4 : G.IsCocontinuous J K] (ℱ : CategoryTheory.Sheaf J A) {X : A}
{U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U)
{x :
CategoryTheory.Presieve.FamilyOfElements
(((CategoryTheory.ran G.op).obj ℱ.val).comp (CategoryTheory.coyoneda.obj (Opposite.op X))) S.arrows}
(hx : x.Compatible) {V : D} (f : V ⟶ U) (y : X ⟶ ((CategoryTheory.ran G.op).obj ℱ.val).obj (Opposite.op V))
(W : CategoryTheory.StructuredArrow (Opposite.op V) G.op),
(∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (CategoryTheory.CategoryStruct.comp fV f)),
CategoryTheory.CategoryStruct.comp y (((CategoryTheory.ran G.op).obj ℱ.val).map fV.op) =
x (CategoryTheory.CategoryStruct.comp fV f) hV) →
CategoryTheory.CategoryStruct.comp y
(CategoryTheory.Limits.limit.π (CategoryTheory.Ran.diagram G.op ℱ.val (Opposite.op V)) W) =
(CategoryTheory.RanIsSheafOfIsCocontinuous.gluedLimitCone ℱ hS hx).π.app
((CategoryTheory.StructuredArrow.map f.op).obj W)
The theorem `CategoryTheory.RanIsSheafOfIsCocontinuous.helper` is essentially a technical helper lemma for constructing certain sheaves in the context of category theory. In more detail, it asserts that if a section `y : X ⟶ 𝒢(V)` coincides with some `x` on the functor `G(V')` for all `G(V') ⊆ V ∈ S`, then the composed map `X ⟶ 𝒢(V) ⟶ ℱ(W)` is precisely the section obtained in a process called `get_sections`. The statement is formulated in a somewhat dense categorical language in order to be conveniently applied in subsequent lemmas. This involves a multitude of concepts from category theory including presieves, Grothendieck topologies, limits and structured arrows, among others.
More concisely: If a section of a sheaf over a site agrees with its restriction to every open subset in a cover, then the section is the result of applying the `get_sections` function.
|
CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection_isAmalgamation
theorem CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection_isAmalgamation :
∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
{G : CategoryTheory.Functor C D} {A : Type w} [inst_2 : CategoryTheory.Category.{max u v, w} A]
[inst_3 : CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C}
{K : CategoryTheory.GrothendieckTopology D} [inst_4 : G.IsCocontinuous J K] (ℱ : CategoryTheory.Sheaf J A) {X : A}
{U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U)
{x :
CategoryTheory.Presieve.FamilyOfElements
(((CategoryTheory.ran G.op).obj ℱ.val).comp (CategoryTheory.coyoneda.obj (Opposite.op X))) S.arrows}
(hx : x.Compatible), x.IsAmalgamation (CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection ℱ hS hx)
This theorem states that the `gluedSection` function indeed provides an amalgamation for a given object `x`. More specifically, given categories `C` and `D`, a functor `G` from `C` to `D`, a category `A` with limits, Grothendieck topologies `J` on `C` and `K` on `D`, and assuming that `G` is cocontinuous from `J` to `K`, then for any sheaf `ℱ` on `J`, any object `X` in `A`, any `U` in `D`, and any sieve `S` on `U` that is in the Grothendieck topology `K`, we have that if `x` is a compatible family of elements for the functor composition of the object `ℱ.val` under the 'ran' of the opposite functor of `G` and the co-Yoneda embedding at the opposite of `X` over the arrows of `S`, then `x` is an amalgamation under the `gluedSection` for `ℱ`, `S`, and `x`. This essentially checks an important aspect of the behavior of the `gluedSection` function with respect to the provided data.
More concisely: Given categories `C`, `D`, a functor `G` from `C` to `D`, a limit category `A`, Grothendieck topologies `J` on `C` and `K` on `D`, and cocontinuous `G` from `J` to `K`, for any sheaf `ℱ` on `J`, object `X` in `A`, and sieve `S` in `K`, if `x` is a compatible family of elements of `ℱ.val` under `G` and the co-Yoneda embedding for the arrows in `S`, then `x` is an amalgamation under the `gluedSection` for `ℱ`, `S`, and `X`.
|
CategoryTheory.ran_isSheaf_of_isCocontinuous
theorem CategoryTheory.ran_isSheaf_of_isCocontinuous :
∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
(G : CategoryTheory.Functor C D) {A : Type w} [inst_2 : CategoryTheory.Category.{max u v, w} A]
[inst_3 : CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C}
(K : CategoryTheory.GrothendieckTopology D) [inst_4 : G.IsCocontinuous J K] (ℱ : CategoryTheory.Sheaf J A),
CategoryTheory.Presheaf.IsSheaf K ((CategoryTheory.ran G.op).obj ℱ.val)
This theorem states that if `G` is a cocontinuous functor from category `C` to `D`, then the right Kan extension of `G.op`, denoted as `Ran G.op`, is a process that transforms sheaves into sheaves. This theorem can be applied to any sheaf `ℱ` on a Grothendieck topology `J` in the category `A` that has all limits. The Grothendieck topology `K` on `D` is also considered. The cocontinuity of `G` with respect to `J` and `K` is a prerequisite. The resulting transformed object in the category of presheaves on `D` is a sheaf with respect to `K`. This theorem is an adaptation of the result presented in the Stacks Project (tag 00XK), albeit without the condition that `C` or `D` has pullbacks.
More concisely: If `G` is a cocontinuous functor between categories with all-limit having Grothendieck topologies `J` on `C` and `K` on `D`, then the right Kan extension of `G.op` transforms sheaves on `(C, J)` into sheaves on `(D, K)`.
|