The equivalence of categories of sheaves of a dense subsite

• CategoryTheory.Functor.IsDenseSubsite.sheafEquiv: If G : C ⥤ D exhibits (C, J) as a dense subsite of (D, K), it induces an equivalence of category of sheaves valued in a category with suitable limits.

References

• [Elephant]: 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.{u_3, u_1} C] [Category.{u_4, 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.val).app (Opposite.op U))).app (Opposite.op X))

instance CategoryTheory.Functor.IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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)

noncomputable def CategoryTheory.Functor.IsDenseSubsite.sheafEquiv {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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] : Sheaf J A ≌ Sheaf K A

If G : C ⥤ D exhibits (C, J) as a dense subsite of (D, K), it induces an equivalence of category of sheaves valued in a category with suitable limits.

@[simp]

theorem CategoryTheory.Functor.IsDenseSubsite.sheafEquiv_functor {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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] : (sheafEquiv G J K A).functor = G.sheafPushforwardCocontinuous A J K

@[simp]

theorem CategoryTheory.Functor.IsDenseSubsite.sheafEquiv_inverse {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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] : (sheafEquiv G J K A).inverse = G.sheafPushforwardContinuous A J K

instance CategoryTheory.Functor.IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, 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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Functor.IsDenseSubsite.sheafEquivSheafificationCompatibility {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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] [HasWeakSheafify J A] [HasWeakSheafify K A] : ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp (presheafToSheaf J A) ≅ (presheafToSheaf K A).comp (sheafEquiv G J K A).inverse

The natural isomorphism exhibiting the compatibility of IsDenseSubsite.sheafEquiv with sheafification.