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

• [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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {A : Type w} [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] (Y : CategoryTheory.Sheaf J A) (U : C) (X : A) : CategoryTheory.IsIso ((CategoryTheory.yoneda.map ((G.op.ranCounit.app Y.val).app (Opposite.op U))).app (Opposite.op X))

theorem CategoryTheory.Functor.IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {A : Type w} [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] (Y : CategoryTheory.Sheaf J A) : CategoryTheory.IsIso ((G.sheafAdjunctionCocontinuous A J K).counit.app Y)

noncomputable def CategoryTheory.Functor.IsDenseSubsite.sheafEquiv {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (A : Type w) [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] : CategoryTheory.Sheaf J A ≌ CategoryTheory.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.

Equations

• CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G J K A = (G.sheafAdjunctionCocontinuous A J K).toEquivalence.symm

@[simp]

theorem CategoryTheory.Functor.IsDenseSubsite.sheafEquiv_functor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (A : Type w) [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] : (CategoryTheory.Functor.IsDenseSubsite.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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (A : Type w) [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] : (CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G J K A).inverse = G.sheafPushforwardContinuous A J K

theorem CategoryTheory.Functor.IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (A : Type w) [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (A : Type w) [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] : ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp (CategoryTheory.presheafToSheaf J A) ≅ (CategoryTheory.presheafToSheaf K A).comp (CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G J K A).inverse

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

Equations

• CategoryTheory.Functor.IsDenseSubsite.sheafEquivSheafificationCompatibility G J K A = G.pushforwardContinuousSheafificationCompatibility A J K

@[deprecated CategoryTheory.Functor.IsDenseSubsite.sheafEquiv]

def CategoryTheory.Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (A : Type w) [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] : CategoryTheory.Sheaf J A ≌ CategoryTheory.Sheaf K A

Alias of 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.

Equations

• @CategoryTheory.Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting = @CategoryTheory.Functor.IsDenseSubsite.sheafEquiv

@[deprecated CategoryTheory.Functor.IsDenseSubsite.sheafEquivSheafificationCompatibility]

def CategoryTheory.Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLiftingSheafificationCompatibility {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (A : Type w) [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] : ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp (CategoryTheory.presheafToSheaf J A) ≅ (CategoryTheory.presheafToSheaf K A).comp (CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G J K A).inverse

Alias of CategoryTheory.Functor.IsDenseSubsite.sheafEquivSheafificationCompatibility.

---

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

Equations

• @CategoryTheory.Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLiftingSheafificationCompatibility = @CategoryTheory.Functor.IsDenseSubsite.sheafEquivSheafificationCompatibility