CategoryTheory.Functor.op_comp_isSheaf
theorem CategoryTheory.Functor.op_comp_isSheaf :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {A : Type u₃}
[inst_2 : CategoryTheory.Category.{v₃, u₃} A] (J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K] (G : CategoryTheory.Sheaf K A),
CategoryTheory.Presheaf.IsSheaf J (F.op.comp G.val)
This theorem states that for any categories `C`, `D`, and `A`, with respective Grothendieck topologies `J` and `K`, if a functor `F` from `C` to `D` is continuous with respect to these topologies, and if `G` is a sheaf on `D` with values in `A` with respect to `K`, then the composition of the opposite of `F` with the presheaf associated with `G` is a sheaf on `C` with respect to `J`. This is a statement about how sheaves and continuous functors interact within the context of category theory and Grothendieck topologies.
More concisely: If functor F from category C to D is continuous with respect to Grothendieck topologies J and K, and G is a sheaf on D with values in A with respect to K, then the composition of the opposite of F and the presheaf associated with G is a sheaf on C with respect to J.
|
CategoryTheory.Functor.isContinuous_of_coverPreserving
theorem CategoryTheory.Functor.isContinuous_of_coverPreserving :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D}
{J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D},
CategoryTheory.CompatiblePreserving K F → CategoryTheory.CoverPreserving J K F → F.IsContinuous J K
This theorem states that, given two categories `C` and `D` along with a functor `F` from `C` to `D`, and two Grothendieck topologies `J` on `C` and `K` on `D`, if `F` is compatible-preserving with respect to the topology `K` and cover-preserving with respect to the topologies `J` and `K`, then `F` is a continuous functor between `C` and `D` with respect to the topologies `J` and `K`. This is essentially a Lean formulation of the mathematical result found at https://stacks.math.columbia.edu/tag/00WW.
More concisely: Given functors F : C -> D between categories C and D, and Grothendieck topologies J on C and K on D, if F preserves covers with respect to J and K, and is compatible-preserving with respect to K, then F is a continuous functor between (C, J) and (D, K).
|
CategoryTheory.CoverPreserving.comp
theorem CategoryTheory.CoverPreserving.comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A]
(J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
{L : CategoryTheory.GrothendieckTopology A} {F : CategoryTheory.Functor C D},
CategoryTheory.CoverPreserving J K F →
∀ {G : CategoryTheory.Functor D A},
CategoryTheory.CoverPreserving K L G → CategoryTheory.CoverPreserving J L (F.comp G)
This theorem states that if there are two functors (F from category C to D and G from category D to A) that preserve covers with respect to the Grothendieck topologies J, K and L respectively, then the composition of these two functors (F followed by G) also preserves covers with respect to the Grothendieck topologies J and L. Grothendieck topologies are a mathematical concept used in category theory to generalize the notion of an open cover from topology.
More concisely: If functors F : C -> D and G : D -> A preserve covers with respect to Grothendieck topologies J, K respectively, then the composition F \circ G preserves covers with respect to J and L.
|
CategoryTheory.idCoverPreserving
theorem CategoryTheory.idCoverPreserving :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C),
CategoryTheory.CoverPreserving J J (CategoryTheory.Functor.id C)
This theorem states that for any category `C` with a given Grothendieck topology `J`, the identity functor on `C` is cover-preserving in the context of `J`. In other words, if we map the objects and morphisms of the category `C` to itself through the identity functor, the covering sieves of `J` will be preserved.
More concisely: For any category `C` and Grothendieck topology `J` on it, the identity functor preserves covering sieves in `C` with respect to `J`.
|
CategoryTheory.Functor.op_comp_isSheafOfTypes
theorem CategoryTheory.Functor.op_comp_isSheafOfTypes :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D)
(J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
[inst_2 : F.IsContinuous J K] (G : CategoryTheory.SheafOfTypes K),
CategoryTheory.Presieve.IsSheaf J (F.op.comp G.val)
The theorem `CategoryTheory.Functor.op_comp_isSheafOfTypes` states that for any two categories `C` and `D` with respective Grothendieck topologies `J` and `K`, a functor `F` from `C` to `D` that is continuous with respect to these topologies, and a sheaf of types `G` on `D` (with respect to `K`), the composition of the functor's opposite `F.op` with `G.val` is a sheaf on `C` with respect to the topology `J`. This essentially means that applying a continuous functor to a sheaf of types and then taking the opposite results in a sheaf on the original category.
More concisely: For any continuous functors F from category C with Grothendieck topology J to category D with topology K, the composition of F.op and a sheaf G on D is a sheaf on C with respect to J.
|
CategoryTheory.Presieve.FamilyOfElements.Compatible.functorPushforward
theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.functorPushforward :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D}
{G : CategoryTheory.Functor C D},
CategoryTheory.CompatiblePreserving K G →
∀ (ℱ : CategoryTheory.SheafOfTypes K) {Z : C} {T : CategoryTheory.Presieve Z}
{x : CategoryTheory.Presieve.FamilyOfElements (G.op.comp ℱ.val) T},
x.Compatible → (CategoryTheory.Presieve.FamilyOfElements.functorPushforward G x).Compatible
This theorem states that for any category `C` and any category `D` associated with a Grothendieck topology `K`, if a functor `G` from `C` to `D` is "compatible preserving" with respect to `K`, then for any sheaf of types `ℱ` over `D`, any object `Z` in `C`, and any presieve `T` on `Z`, if a family of elements `x` indexed by `T` and with values in the opposite functor of `G` composed with `ℱ` is compatible, then the family obtained by pushing forward `x` under the functor `G` is also compatible.
In other words, the theorem asserts that the process of "pushing forward" a compatible family of elements under a "compatible preserving" functor preserves the property of being compatible. The compatibility of a family of elements corresponds to a certain coherence condition in the context of sheaf theory, a central concept in algebraic geometry.
More concisely: Given a category `C`, a category `D` with a Grothendieck topology `K`, a functor `G: C -> D` preserving limits and colimits, and a sheaf of types `ℱ` over `D`, if for any object `Z` in `C`, any presieve `T` on `Z`, and any family `x: T -> ⊢` of elements of `G(ℱ(Z))` indexed by `T`, the family `x` is compatible, then the family `G(x)` obtained by pushing forward `x` under `G` is also compatible.
|