CategoryTheory.LocallyCoverDense.inducedTopology_isCocontinuous
theorem CategoryTheory.LocallyCoverDense.inducedTopology_isCocontinuous :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D}
{K : CategoryTheory.GrothendieckTopology D} [inst_2 : G.Full] [inst_3 : G.Faithful]
(Hld : CategoryTheory.LocallyCoverDense K G), G.IsCocontinuous Hld.inducedTopology K
This theorem states that, given a category `C` with objects of type `u_1` and morphisms of type `u_3`, and another category `D` with objects of type `u_2` and morphisms of type `u_4`, if we have a functor `G` from `C` to `D` which is both full (meaning every morphism in `D` is the image of some morphism in `C` under `G`) and faithful (meaning distinct morphisms in `C` remain distinct in `D`), and we have a Grothendieck topology `K` on `D`, and if `G` is locally cover-dense with respect to `K` (meaning roughly that 'small' covers in `D` can be lifted to 'small' covers in `C`), then `G` is cocontinuous with respect to the induced topology from `K` on `C` and `K` itself. In simpler terms, this theorem is about preserving the structure of 'smallness' when mapping from one category to another.
More concisely: Given a full, faithful functor between categories with a locally cover-dense morphism and a Grothendieck topology on the target category, the functor is cocontinuous and preserves the given topology.
|
CategoryTheory.Functor.locallyCoverDense_of_isCoverDense
theorem CategoryTheory.Functor.locallyCoverDense_of_isCoverDense :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D)
(K : CategoryTheory.GrothendieckTopology D) [inst_2 : G.Full] [inst_3 : G.IsCoverDense K],
CategoryTheory.LocallyCoverDense K G
The theorem `CategoryTheory.Functor.locallyCoverDense_of_isCoverDense` states that for any categories `C` and `D`, a functor `G` from `C` to `D`, and a Grothendieck topology `K` on `D`, if `G` is fully faithful and is cover dense with respect to `K`, then `G` is locally cover dense with respect to `K`. In category theory, a functor being "cover dense" or "locally cover dense" roughly means that it interacts with the Grothendieck topology in a way that the topology can be transferred across the functor in some sense, making it useful for studying sheaves and toposes.
More concisely: If `G: C -> D` is a fully faithful functor between categories and is cover dense with respect to a Grothendieck topology `K` on `D`, then `G` is locally cover dense with respect to `K`.
|
CategoryTheory.LocallyCoverDense.inducedTopology_coverPreserving
theorem CategoryTheory.LocallyCoverDense.inducedTopology_coverPreserving :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D}
{K : CategoryTheory.GrothendieckTopology D} [inst_2 : G.Full] [inst_3 : G.Faithful]
(Hld : CategoryTheory.LocallyCoverDense K G), CategoryTheory.CoverPreserving Hld.inducedTopology K G
This theorem states that given a Category `C` and a Category `D`, along with a functor `G` from `C` to `D` and a Grothendieck topology `K` on `D`, if `G` is locally cover-dense with respect to `K`, then `G` preserves the cover in the topology induced by `G` on `C` and the Grothendieck topology `K` on `D`. This is true under the assumption that `G` is a fully faithful functor, i.e., it reflects and preserves all morphisms in the categories.
More concisely: Given a fully faithful functor `G` from category `C` to category `D`, if `G` is locally cover-dense with respect to a Grothendieck topology `K` on `D`, then `G` preserves covers in both `C` and the topology `G^(-1)(K)` on `C`.
|