Equivalences of sheaf categories

Given a site (C, J) and a category D which is equivalent to C, with C and D possibly large and possibly in different universes, we transport the Grothendieck topology J on C to D and prove that the sheaf categories are equivalent.

We also prove that sheafification and the property HasSheafCompose transport nicely over this equivalence, and apply it to essentially small sites. We also provide instances for existence of sufficiently small limits in the sheaf category on the essentially small site.

Main definitions

• CategoryTheory.Equivalence.sheafCongr is the equivalence of sheaf categories.

• CategoryTheory.Equivalence.transportAndSheafify is the functor which takes a presheaf on C, transports it over the equivalence to D, sheafifies there and then transports back to C.

• CategoryTheory.Equivalence.transportSheafificationAdjunction: transportAndSheafify is left adjoint to the functor taking a sheaf to its underlying presheaf.

• CategoryTheory.smallSheafify is the functor which takes a presheaf on an essentially small site (C, J), transports to a small model, sheafifies there and then transports back to C.

• CategoryTheory.smallSheafificationAdjunction: smallSheafify is left adjoint to the functor taking a sheaf to its underlying presheaf.

@[instance 900]

instance CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor D C) [G.IsEquivalence] : G.IsCoverDense J

instance CategoryTheory.Equivalence.instIsDenseSubsiteInducedTopologyInverseFunctor {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : Functor.IsDenseSubsite J (e.inverse.inducedTopology J) e.functor

theorem CategoryTheory.Equivalence.eq_inducedTopology_of_isDenseSubsite {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) [Functor.IsDenseSubsite K J e.inverse] : K = e.inverse.inducedTopology J

theorem CategoryTheory.Equivalence.isDenseSubsite_functor_of_isCocontinuous {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) [e.functor.IsCocontinuous J K] [e.inverse.IsCocontinuous K J] : Functor.IsDenseSubsite J K e.functor

theorem CategoryTheory.Equivalence.isDenseSubsite_inverse_of_isCocontinuous {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) [e.functor.IsCocontinuous J K] [e.inverse.IsCocontinuous K J] : Functor.IsDenseSubsite K J e.inverse

instance CategoryTheory.Equivalence.instIsDenseSubsiteFunctor {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) [Functor.IsDenseSubsite K J e.inverse] : Functor.IsDenseSubsite J K e.functor

def CategoryTheory.Equivalence.sheafCongr.functor {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] : Functor (Sheaf J A) (Sheaf K A)

The functor in the equivalence of sheaf categories.

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.functor_map_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] {X✝ Y✝ : Sheaf J A} (f : X✝ ⟶ Y✝) (X : Dᵒᵖ) : ((functor J K e A).map f).hom.app X = f.hom.app (Opposite.op (e.inverse.obj (Opposite.unop X)))

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.functor_obj_obj_map {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] (X : Sheaf J A) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) : ((functor J K e A).obj X).obj.map f = X.obj.map (e.inverse.map f.unop).op

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.functor_obj_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] (X : Sheaf J A) (X✝ : Dᵒᵖ) : ((functor J K e A).obj X).obj.obj X✝ = X.obj.obj (Opposite.op (e.inverse.obj (Opposite.unop X✝)))

def CategoryTheory.Equivalence.sheafCongr.inverse {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] : Functor (Sheaf K A) (Sheaf J A)

The inverse in the equivalence of sheaf categories.

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.inverse_map_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] {X✝ Y✝ : Sheaf K A} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) : ((inverse J K e A).map f).hom.app X = f.hom.app (Opposite.op (e.functor.obj (Opposite.unop X)))

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.inverse_obj_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] (X : Sheaf K A) (X✝ : Cᵒᵖ) : ((inverse J K e A).obj X).obj.obj X✝ = X.obj.obj (Opposite.op (e.functor.obj (Opposite.unop X✝)))

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.inverse_obj_obj_map {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] (X : Sheaf K A) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : ((inverse J K e A).obj X).obj.map f = X.obj.map (e.functor.map f.unop).op

def CategoryTheory.Equivalence.sheafCongr.unitIso {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] : Functor.id (Sheaf J A) ≅ (functor J K e A).comp (inverse J K e A)

The unit iso in the equivalence of sheaf categories.

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.unitIso_inv_app_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] (X : Sheaf J A) (X✝ : Cᵒᵖ) : ((unitIso J K e A).inv.app X).hom.app X✝ = X.obj.map (e.unitIso.hom.app (Opposite.unop X✝)).op

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.unitIso_hom_app_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] (X : Sheaf J A) (X✝ : Cᵒᵖ) : ((unitIso J K e A).hom.app X).hom.app X✝ = X.obj.map (e.unitIso.inv.app (Opposite.unop X✝)).op

def CategoryTheory.Equivalence.sheafCongr.counitIso {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] : (inverse J K e A).comp (functor J K e A) ≅ Functor.id (Sheaf K A)

The counit iso in the equivalence of sheaf categories.

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.counitIso_inv_app_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] (X : Sheaf K A) (X✝ : Dᵒᵖ) : ((counitIso J K e A).inv.app X).hom.app X✝ = X.obj.map (e.counitIso.hom.app (Opposite.unop X✝)).op

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.counitIso_hom_app_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] (X : Sheaf K A) (X✝ : Dᵒᵖ) : ((counitIso J K e A).hom.app X).hom.app X✝ = X.obj.map (e.counitIso.inv.app (Opposite.unop X✝)).op

def CategoryTheory.Equivalence.sheafCongr {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] : Sheaf J A ≌ Sheaf K A

The equivalence of sheaf categories.

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr_counitIso {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] : (sheafCongr J K e A).counitIso = sheafCongr.counitIso J K e A

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr_functor {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] : (sheafCongr J K e A).functor = sheafCongr.functor J K e A

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr_inverse {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] : (sheafCongr J K e A).inverse = sheafCongr.inverse J K e A

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr_unitIso {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] : (sheafCongr J K e A).unitIso = sheafCongr.unitIso J K e A

noncomputable def CategoryTheory.Equivalence.transportAndSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] [HasSheafify K A] : Functor (Functor Cᵒᵖ A) (Sheaf J A)

Transport a presheaf to the equivalent category and sheafify there.

noncomputable def CategoryTheory.Equivalence.transportIsoSheafToPresheaf {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] : (sheafCongr J K e A).functor.comp ((sheafToPresheaf K A).comp e.op.congrLeft.inverse) ≅ sheafToPresheaf J A

An auxiliary definition for the sheafification adjunction.

noncomputable def CategoryTheory.Equivalence.transportSheafificationAdjunction {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] [HasSheafify K A] : transportAndSheafify J K e A ⊣ sheafToPresheaf J A

Transporting and sheafifying is left adjoint to taking the underlying presheaf.

instance CategoryTheory.Equivalence.instPreservesFiniteLimitsFunctorOppositeSheafTransportAndSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] [HasSheafify K A] : Limits.PreservesFiniteLimits (transportAndSheafify J K e A)

theorem CategoryTheory.Equivalence.hasSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [Category.{v₃, u₃} A] [Functor.IsDenseSubsite K J e.inverse] [HasSheafify K A] : HasSheafify J A

Transport HasSheafify along an equivalence of sites.

theorem CategoryTheory.Equivalence.hasSheafCompose {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (e : C ≌ D) [Functor.IsDenseSubsite K J e.inverse] {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] (F : Functor A B) [K.HasSheafCompose F] : J.HasSheafCompose F

noncomputable def CategoryTheory.smallSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₃) [Category.{v₃, u₃} A] [EssentiallySmall.{w, v₁, u₁} C] [HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A] : Functor (Functor Cᵒᵖ A) (Sheaf J A)

Transport to a small model and sheafify there.

noncomputable def CategoryTheory.smallSheafificationAdjunction {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₃) [Category.{v₃, u₃} A] [EssentiallySmall.{w, v₁, u₁} C] [HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A] : smallSheafify J A ⊣ sheafToPresheaf J A

Transporting to a small model and sheafifying there is left adjoint to the underlying presheaf functor

theorem CategoryTheory.hasSheafifyEssentiallySmallSite {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₃) [Category.{v₃, u₃} A] [EssentiallySmall.{w, v₁, u₁} C] [HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A] : HasSheafify J A

instance CategoryTheory.hasSheafComposeEssentiallySmallSite {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₃) [Category.{v₃, u₃} A] (B : Type u₄) [Category.{v₄, u₄} B] (F : Functor A B) [EssentiallySmall.{w, v₁, u₁} C] [((equivSmallModel C).inverse.inducedTopology J).HasSheafCompose F] : J.HasSheafCompose F

theorem CategoryTheory.hasLimitsEssentiallySmallSite {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₃) [Category.{v₃, u₃} A] [EssentiallySmall.{w, v₁, u₁} C] [Limits.HasLimits (Sheaf ((equivSmallModel C).inverse.inducedTopology J) A)] : Limits.HasLimitsOfSize.{max v₃ w, max v₃ w, max u₁ v₃, max (max (max u₃ u₁) v₃) v₁} (Sheaf J A)

instance CategoryTheory.hasColimitsEssentiallySmallSite {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₃) [Category.{v₃, u₃} A] [EssentiallySmall.{w, v₁, u₁} C] [Limits.HasColimits (Sheaf ((equivSmallModel C).inverse.inducedTopology J) A)] : Limits.HasColimitsOfSize.{max v₃ w, max v₃ w, max u₁ v₃, max (max (max u₃ u₁) v₃) v₁} (Sheaf J A)

theorem CategoryTheory.GrothendieckTopology.W_inverseImage_whiskeringLeft {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (G : Functor D C) {A : Type u₃} [Category.{v₃, u₃} A] [G.IsCoverDense J] [G.Full] [G.IsContinuous K J] [(G.sheafPushforwardContinuous A K J).EssSurj] : K.W.inverseImage ((Functor.whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) = J.W

theorem CategoryTheory.GrothendieckTopology.W_whiskerLeft_iff {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (G : Functor D C) {A : Type u₃} [Category.{v₃, u₃} A] [G.IsCoverDense J] [G.Full] [G.IsContinuous K J] [(G.sheafPushforwardContinuous A K J).EssSurj] {P Q : Functor Cᵒᵖ A} (f : P ⟶ Q) : K.W (G.op.whiskerLeft f) ↔ J.W f

theorem CategoryTheory.GrothendieckTopology.PreservesSheafification.transport {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (G : Functor D C) {A : Type u₃} [Category.{v₃, u₃} A] (B : Type u₄) [Category.{v₄, u₄} B] (F : Functor A B) [G.IsCoverDense J] [G.Full] [G.IsContinuous K J] [(G.sheafPushforwardContinuous B K J).EssSurj] [(G.sheafPushforwardContinuous A K J).EssSurj] [K.PreservesSheafification F] : J.PreservesSheafification F

theorem CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.transport {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (G : Functor D C) {A : Type u₃} [Category.{v₃, u₃} A] [G.IsCoverDense J] [G.Full] [G.IsContinuous K J] [(G.sheafPushforwardContinuous A K J).EssSurj] [G.IsCocontinuous K J] {FA : A → A → Type u_1} {CA : A → Type u_2} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [K.WEqualsLocallyBijective A] (hG : CoverPreserving K J G) : J.WEqualsLocallyBijective A

theorem CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.ofEssentiallySmall {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {A : Type u₃} [Category.{v₃, u₃} A] {FA : A → A → Type u_1} {CA : A → Type u_2} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [EssentiallySmall.{w, v₁, u₁} C] [∀ (X : Cᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X (equivSmallModel C).inverse.op) A] [((equivSmallModel C).inverse.inducedTopology J).WEqualsLocallyBijective A] : J.WEqualsLocallyBijective A

instance CategoryTheory.GrothendieckTopology.instPreservesSheafification_1 {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {A : Type u₃} [Category.{v₃, u₃} A] (B : Type u₄) [Category.{v₄, u₄} B] (F : Functor A B) [EssentiallySmall.{w, v₁, u₁} C] [∀ (X : Cᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X (equivSmallModel C).inverse.op) A] [∀ (X : Cᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X (equivSmallModel C).inverse.op) B] [((equivSmallModel C).inverse.inducedTopology J).PreservesSheafification F] : J.PreservesSheafification F