The equivalence of categories of sheaves of a dense subsite #
If G : C ⥤ D exhibits (C, J) as a dense subsite of (D, K), and A is
a category with suitable limits, then the functor
G.sheafPushforwardContinuous A J K : Sheaf K A ⥤ Sheaf J A is an equivalence
of categories. The equivalence of categories can be obtained as sheafEquiv J K G A
which is defined in the file Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean.
References #
- [Joh02]: Sketches of an Elephant, P. T. Johnstone: C2.2.
- https://ncatlab.org/nlab/show/dense+sub-site
- https://ncatlab.org/nlab/show/comparison+lemma
theorem CategoryTheory.Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (G : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) {A : Type w} [Category.{w', w} A] [∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A] [IsDenseSubsite J K G] (Y : Sheaf J A) (U : C) (X : A) :
instance CategoryTheory.Functor.IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (G : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) {A : Type w} [Category.{w', w} A] [∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A] [IsDenseSubsite J K G] (Y : Sheaf J A) :
IsIso ((G.sheafAdjunctionCocontinuous A J K).counit.app Y)
instance CategoryTheory.Functor.IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (G : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) {A : Type w} [Category.{w', w} A] [∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A] [IsDenseSubsite J K G] :
(G.sheafPushforwardContinuous A J K).IsEquivalence