CategoryTheory.Functor.IsCoverDense.ext
theorem CategoryTheory.Functor.IsCoverDense.ext :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_7, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
(G : CategoryTheory.Functor C D) [inst_2 : G.IsCoverDense K] (ℱ : CategoryTheory.SheafOfTypes K) (X : D)
{s t : ℱ.val.obj (Opposite.op X)}, (∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t) → s = t
The theorem `CategoryTheory.Functor.IsCoverDense.ext` states that for any categories `C` and `D`, Grothendieck topology `K` on `D`, a functor `G` from `C` to `D` which is cover dense, a sheaf of types `ℱ` on `K`, and two sections `s` and `t` of the sheaf `ℱ` over some object `X` in `D`, if for all objects `Y` in `C` and for all morphisms `f` from `G(Y)` to `X`, the image of `s` under the mapping `ℱ.val.map f.op` equals the image of `t` under the same mapping, then `s` and `t` must be equal.
In simpler terms, it indicates that if two sections of a sheaf coincide when mapped under any morphism from the image of `G`, then the two sections are identical. This theorem is a generalization of the uniqueness property of sections in the category of sheaves.
More concisely: If `G` is a cover dense functor from category `C` to category `D` with Grothendieck topology `K`, and `s` and `t` are sections of sheaf `ℱ` on `K` over object `X` in `D` such that for all morphisms `f : G(Y) → X` from `C`, `ℱ.val.map f.op s = ℱ.val.map f.op t`, then `s = t`.
|
CategoryTheory.Functor.IsCoverDense.sheafHom_restrict_eq
theorem CategoryTheory.Functor.IsCoverDense.sheafHom_restrict_eq :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_6, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_7, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
[inst_2 : CategoryTheory.Category.{u_5, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
[inst_4 : G.Full] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
(α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val),
CategoryTheory.whiskerLeft G.op (CategoryTheory.Functor.IsCoverDense.sheafHom α) = α
The theorem `CategoryTheory.Functor.IsCoverDense.sheafHom_restrict_eq` states that for any categories `C`, `D`, and `A`, a Grothendieck topology `K` on `D`, a functor `G` from `C` to `D` that is dense with respect to `K`, a functor `ℱ` from the opposite category of `D` to `A`, a sheaf `ℱ'` of `A` with respect to `K`, and a natural transformation `α` from the composition of `G.op` and `ℱ` to the composition of `G.op` and `ℱ'.val`, the restriction of the sheaf-homomorphism associated with `α` to the category `C` (obtained by left whiskering with `G.op`) is equal to `α` itself.
More concisely: For a functor G from category C to D, dense with respect to a Grothendieck topology K on D, a functor ℱ from the opposite category of D to A, a sheaf ℱ' of A with respect to K, and a natural transformation α from G.op ∘ ℱ to G.op ∘ ℱ', the restriction of the sheaf-homomorphism associated with α to C is equal to α.
|
CategoryTheory.Functor.IsCoverDense.compatiblePreserving
theorem CategoryTheory.Functor.IsCoverDense.compatiblePreserving :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_6, u_2} D] (K : CategoryTheory.GrothendieckTopology D)
(G : CategoryTheory.Functor C D) [inst_2 : G.IsCoverDense K] [inst_3 : G.Full] [inst_4 : G.Faithful],
CategoryTheory.CompatiblePreserving K G
The theorem states that for any category `C` and category `D`, given a Grothendieck topology `K` on `D`, if a functor `G` from `C` to `D` is cover-dense, full and faithful, then `G` preserves compatible families with respect to the topology `K`. In the context of Category Theory, a functor is said to be full and faithful if it reflects and preserves the structure of the categories it maps between, and cover-dense if its image under the functor covers the category `D`. A functor is said to preserve compatible families if, loosely speaking, it "respects" the limits imposed by the Grothendieck topology.
More concisely: Given a Grothendieck topology on a category `D`, if a functor from a category `C` to `D` is cover-dense, full, and faithful, then it preserves limits imposed by the topology.
|
CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible
theorem CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_6, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_5, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
{G : CategoryTheory.Functor C D} [inst_2 : G.IsCoverDense K] [inst_3 : G.Full]
{ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K}
(α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) {X : D} (x : ℱ.obj (Opposite.op X)),
(CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x).Compatible
This theorem states that for any categories `C` and `D`, Grothendieck topology `K` on `D`, and a functor `G` from `C` to `D` that is cover dense with respect to `K`, given two functors `ℱ` and `ℱ'` from the opposite of `D` to the type `v`, such that `ℱ'` is a sheaf of types with respect to `K`, and a natural transformation `α` from the composition of `G` and `ℱ` to the composition of `G` and the value of `ℱ'`, for any object `X` in `D` and any element `x` of the object `ℱ` maps to the opposite of `X`, the `pushforwardFamily` of `α` and `x` is compatible. In other words, the `pushforwardFamily` is a system of elements in the sections of `ℱ'` that is compatible in the sense of the definition in category theory.
More concisely: Given categories `C`, `D`, a Grothendieck topology `K` on `D`, a functor `G:` `C` -> `D` that is cover dense with respect to `K`, and functors `ℱ:` `D` -> Type and `ℱ':` `D`^op -> Type with `ℱ'` a sheaf and a natural transformation `α:` `G ∘ ℱ` ≈ `G ∘ ℱ'`, for any `x` in the sections of `ℱ` over an object `X` in `D`, the pushforward families `(α x)_X` and `ℱ' x` are compatible.
|
CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso
theorem CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_7, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_5, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
[inst_2 : CategoryTheory.Category.{u_6, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
[inst_4 : G.Full] {ℱ ℱ' : CategoryTheory.Sheaf K A} (α : ℱ ⟶ ℱ'),
CategoryTheory.IsIso (CategoryTheory.whiskerLeft G.op α.val) → CategoryTheory.IsIso α
This theorem states that, given a full and cover-dense functor `G` and a natural transformation of sheaves `α` from `ℱ` to `ℱ'`, if the pullback of `α` along `G` is an isomorphism, then `α` itself is also an isomorphism. In category theory, this theorem helps us to understand the relationship between the properties of a natural transformation and its pullbacks.
More concisely: Given a full and cover-dense functor `G` and a natural transformation `α:` `F ⟶ F'` between sheaves such that the pullback of `α` along `G` is an isomorphism, then `α` is an isomorphism.
|
CategoryTheory.Functor.IsCoverDense.Types.appHom_restrict
theorem CategoryTheory.Functor.IsCoverDense.Types.appHom_restrict :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_6, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_5, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
{G : CategoryTheory.Functor C D} [inst_2 : G.IsCoverDense K] [inst_3 : G.Full]
{ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.SheafOfTypes K}
(α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) {X : D} {Y : C} (f : Opposite.op X ⟶ Opposite.op (G.obj Y))
(x : ℱ.obj (Opposite.op X)),
ℱ'.val.map f (CategoryTheory.Functor.IsCoverDense.Types.appHom α X x) = α.app (Opposite.op Y) (ℱ.map f x)
This theorem states that given a category `C` and another category `D`, with a functor `G` from `C` to `D`, a Grothendieck topology `K` on `D`, and the functor `G` is cover-dense with respect to `K`. Further, if `G` is full and we have two functors `ℱ` and `ℱ'` from `Dᵒᵖ` to `Type v` and `ℱ'` is a sheaf of types with respect to `K`, respectively. Then, for a natural transformation `α` from the composite functor `G.op` and `ℱ` to the composite functor `G.op` and `ℱ'.val`, an object `X` in `D`, an object `Y` in `C`, a morphism `f` from the opposite of `X` to the opposite of `G.obj Y` in `C`, and an object `x` in `ℱ.obj` of the opposite of `X`, the assertion is that mapping `f` under `ℱ'.val` on the result of applying `α` with `X` and `x` using `appHom` of `CategoryTheory.Functor.IsCoverDense.Types` equals applying `α.app` with the opposite of `Y` on the result of mapping `f` under `ℱ` on `x`.
More concisely: Given a cover-dense functor `G` from category `C` to `D` with respect to a Grothendieck topology `K` on `D`, if `ℱ'` is a sheaf of types over `D` with respect to `K` and `α` is a natural transformation from `G.op ∘ ℱ` to `G.op ∘ ℱ'`, then for any object `X` in `D`, any object `Y` in `C`, any morphism `f` from `X` to `G.obj Y` in `D`, and any `x` in `ℱ.obj` over `X`, `α.val.app (f, x) = ℱ'.val.app (G.map f, ℱ.val.app f x)`.
|
CategoryTheory.Functor.IsCoverDense.isContinuous
theorem CategoryTheory.Functor.IsCoverDense.isContinuous :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_5, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_6, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) [inst_2 : G.IsCoverDense K]
[inst_3 : G.Full] [inst_4 : G.Faithful], CategoryTheory.CoverPreserving J K G → G.IsContinuous J K
This theorem states that for any two types `C` and `D` that have category structures and any Grothendieck topologies `J` and `K` on `C` and `D` respectively, if a functor `G` from `C` to `D` is cover-dense with respect to topology `K`, full, and faithful, then if `G` is also cover-preserving with respect to topologies `J` and `K`, it is continuous with respect to `J` and `K`. In other words, if a functor preserves coverings and is cover-dense, full, and faithful, it ensures the continuity of the functor under the given Grothendieck topologies.
More concisely: Given functors G from type C to D with category structures, if G is cover-preserving, cover-dense, full, and faithful between the Grothendieck topologies J on C and K on D, then G is continuous with respect to J and K.
|
CategoryTheory.Functor.IsCoverDense.sheafHom_eq
theorem CategoryTheory.Functor.IsCoverDense.sheafHom_eq :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_7, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_6, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
[inst_2 : CategoryTheory.Category.{u_5, u_4} A] (G : CategoryTheory.Functor C D) [inst_3 : G.IsCoverDense K]
[inst_4 : G.Full] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : ℱ ⟶ ℱ'.val),
CategoryTheory.Functor.IsCoverDense.sheafHom (CategoryTheory.whiskerLeft G.op α) = α
The theorem states that in the context of category theory, given the categories C, D, and A, a Grothendieck topology K on D, functors G and ℱ from C to D and Dᵒᵖ to A respectively, a sheaf ℱ' of K on A, and a natural transformation α from ℱ to the value of ℱ', if the pullback map is obtained via the process of 'whiskering' to the left with the functor G, then the sheaf homomorphism obtained when applying the whisker left operation to the natural transformation α is equal to α itself. This theorem is under the condition that G is full and G densely covers the Grothendieck topology K.
More concisely: Given functors G from C to D, ℱ from Dᵒᵖ to A, a Grothendieck topology K on D, a sheaf ℱ' of K on A, and a natural transformation α from ℱ to ℱ', if G is full and densely covering, then the sheaf homomorphism obtained by whiskering α with G is equal to α itself.
|