CategoryTheory.Equivalence.hasSheafify
theorem CategoryTheory.Equivalence.hasSheafify :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
{D : Type u_2} [inst_1 : CategoryTheory.Category.{u_6, u_2} D] (K : CategoryTheory.GrothendieckTopology D)
(e : C ≌ D) (A : Type u_3) [inst_2 : CategoryTheory.Category.{u_5, u_3} A]
[inst_3 : CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e]
[inst_4 : CategoryTheory.HasSheafify K A], CategoryTheory.HasSheafify J A
This theorem states that, given two categories `C` and `D` with their respective Grothendieck topologies `J` and `K`, and an equivalence `e` between `C` and `D`, if the category `D` has a property called `HasSheafify` with respect to the category `A`, then the Category `C` also has the `HasSheafify` property with respect to `A`. This is under the condition that the equivalence `e` also transports the Grothendieck topology from `J` to `K`. Therefore, this theorem demonstrates the transportation of the `HasSheafify` property along an equivalence of sites.
More concisely: If $e: C \to D$ is an equivalence of categories between $C$ and $D$ with Grothendieck topologies $J$ and $K$, respectively, and $D$ has the property of having sheafify with respect to a category $A$ with $e$ transporting $J$ to $K$, then $C$ also has the property of having sheafify with respect to $A$.
|
CategoryTheory.Equivalence.locallyCoverDense
theorem CategoryTheory.Equivalence.locallyCoverDense :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_5, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
{D : Type u_2} [inst_1 : CategoryTheory.Category.{u_4, u_2} D] (e : C ≌ D),
CategoryTheory.LocallyCoverDense J e.inverse
This theorem states that for any category `C` with a Grothendieck topology `J` and any category `D`, if `C` and `D` are equivalent as categories with the equivalence `e`, then the inverse of `e` is locally cover dense for the topology `J`. Locally cover dense is a property of a functor for spanning a cover in a Grothendieck topology.
More concisely: If categories `C` and `D` are equivalent with an equivalence `e` in a category with a Grothendieck topology `J`, then the inverse of `e` is locally cover-preserving for `J`. (This means that for every cover `C'` in `C` by `J`, the image `e(C')` is a cover in `D`.)
|