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, ℱ. 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) : IsIso ((yoneda.map ((G.op.ranCounit.app Y.obj).app (Opposite.op U))).app (Opposite.op X))

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