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.

theorem CategoryTheory.Equivalence.locallyCoverDense {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (e : C ≌ D) : CategoryTheory.LocallyCoverDense J e.inverse

theorem CategoryTheory.Equivalence.coverPreserving {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) : CategoryTheory.CoverPreserving J (CategoryTheory.LocallyCoverDense.inducedTopology ⋯) e.functor

instance CategoryTheory.Equivalence.instIsCoverDenseFunctorInducedTopologyInverseFullOfEquivalenceOfEquivalenceInverseFaithfulOfEquivalenceLocallyCoverDense {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) : CategoryTheory.Functor.IsCoverDense e.functor (CategoryTheory.LocallyCoverDense.inducedTopology ⋯)

Equations

• ⋯ = ⋯

instance CategoryTheory.Equivalence.instIsCoverDenseInverse {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) : CategoryTheory.Functor.IsCoverDense e.inverse J

Equations

• ⋯ = ⋯

class CategoryTheory.Equivalence.TransportsGrothendieckTopology {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) : Prop

A class saying that the equivalence e transports the Grothendieck topology J to K.

• eq_inducedTopology : K = CategoryTheory.LocallyCoverDense.inducedTopology ⋯

  K is equal to the induced topology.

instance CategoryTheory.Equivalence.instTransportsGrothendieckTopologyInducedTopologyInverseFullOfEquivalenceOfEquivalenceInverseFaithfulOfEquivalenceLocallyCoverDense {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) : CategoryTheory.Equivalence.TransportsGrothendieckTopology J (CategoryTheory.LocallyCoverDense.inducedTopology ⋯) e

Equations

• ⋯ = ⋯

theorem CategoryTheory.Equivalence.eq_inducedTopology_of_transports {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] : K = CategoryTheory.LocallyCoverDense.inducedTopology ⋯

instance CategoryTheory.Equivalence.instIsContinuousFunctor {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] : CategoryTheory.Functor.IsContinuous e.functor J K

Equations

• ⋯ = ⋯

instance CategoryTheory.Equivalence.instIsContinuousInverse {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] : CategoryTheory.Functor.IsContinuous e.inverse K J

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.functor_obj_val_obj {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] (F : CategoryTheory.Sheaf J A) (X : Dᵒᵖ) : ((CategoryTheory.Equivalence.sheafCongr.functor J K e A).obj F).val.obj X = F.val.obj (Opposite.op (e.inverse.obj X.unop))

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.functor_obj_val_map {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] (F : CategoryTheory.Sheaf J A) : ∀ {X Y : Dᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.Equivalence.sheafCongr.functor J K e A).obj F).val.map f = F.val.map (e.inverse.map f.unop).op

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.functor_map_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] : ∀ {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y) (X_1 : Dᵒᵖ), ((CategoryTheory.Equivalence.sheafCongr.functor J K e A).map f).val.app X_1 = f.val.app (Opposite.op (e.inverse.obj X_1.unop))

def CategoryTheory.Equivalence.sheafCongr.functor {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] : CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf K A)

The functor in the equivalence of sheaf categories.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.inverse_obj_val_obj {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] (F : CategoryTheory.Sheaf K A) (X : Cᵒᵖ) : ((CategoryTheory.Equivalence.sheafCongr.inverse J K e A).obj F).val.obj X = F.val.obj (Opposite.op (e.functor.obj X.unop))

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.inverse_map_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] : ∀ {X Y : CategoryTheory.Sheaf K A} (f : X ⟶ Y) (X_1 : Cᵒᵖ), ((CategoryTheory.Equivalence.sheafCongr.inverse J K e A).map f).val.app X_1 = f.val.app (Opposite.op (e.functor.obj X_1.unop))

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.inverse_obj_val_map {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] (F : CategoryTheory.Sheaf K A) : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.Equivalence.sheafCongr.inverse J K e A).obj F).val.map f = F.val.map (e.functor.map f.unop).op

def CategoryTheory.Equivalence.sheafCongr.inverse {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] : CategoryTheory.Functor (CategoryTheory.Sheaf K A) (CategoryTheory.Sheaf J A)

The inverse in the equivalence of sheaf categories.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.unitIso_hom_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] (X : CategoryTheory.Sheaf J A) (X : Cᵒᵖ) : ((CategoryTheory.Equivalence.sheafCongr.unitIso J K e A).hom.app X✝).val.app X = X✝.val.map (e.unitIso.inv.app X.unop).op

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.unitIso_inv_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] (X : CategoryTheory.Sheaf J A) (X : Cᵒᵖ) : ((CategoryTheory.Equivalence.sheafCongr.unitIso J K e A).inv.app X✝).val.app X = X✝.val.map (e.unitIso.hom.app X.unop).op

def CategoryTheory.Equivalence.sheafCongr.unitIso {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] : CategoryTheory.Functor.id (CategoryTheory.Sheaf J A) ≅ CategoryTheory.Functor.comp (CategoryTheory.Equivalence.sheafCongr.functor J K e A) (CategoryTheory.Equivalence.sheafCongr.inverse J K e A)

The unit iso in the equivalence of sheaf categories.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.counitIso_hom_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] (X : CategoryTheory.Sheaf K A) (X : Dᵒᵖ) : ((CategoryTheory.Equivalence.sheafCongr.counitIso J K e A).hom.app X✝).val.app X = X✝.val.map (e.counitIso.inv.app X.unop).op

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.counitIso_inv_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] (X : CategoryTheory.Sheaf K A) (X : Dᵒᵖ) : ((CategoryTheory.Equivalence.sheafCongr.counitIso J K e A).inv.app X✝).val.app X = X✝.val.map (e.counitIso.hom.app X.unop).op

def CategoryTheory.Equivalence.sheafCongr.counitIso {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] : CategoryTheory.Functor.comp (CategoryTheory.Equivalence.sheafCongr.inverse J K e A) (CategoryTheory.Equivalence.sheafCongr.functor J K e A) ≅ CategoryTheory.Functor.id (CategoryTheory.Sheaf K A)

The counit iso in the equivalence of sheaf categories.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Equivalence.sheafCongr {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] : CategoryTheory.Sheaf J A ≌ CategoryTheory.Sheaf K A

The equivalence of sheaf categories.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Equivalence.transportAndSheafify {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] [CategoryTheory.HasSheafify K A] : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)

Transport a presheaf to the equivalent category and sheafify there.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Equivalence.transportIsoSheafToPresheaf {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] : CategoryTheory.Functor.comp (CategoryTheory.Equivalence.sheafCongr J K e A).functor (CategoryTheory.Functor.comp (CategoryTheory.sheafToPresheaf K A) (CategoryTheory.Equivalence.congrLeft (CategoryTheory.Equivalence.op e)).inverse) ≅ CategoryTheory.sheafToPresheaf J A

An auxiliary definition for the sheafification adjunction.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Equivalence.transportSheafificationAdjunction {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] [CategoryTheory.HasSheafify K A] : CategoryTheory.Equivalence.transportAndSheafify J K e A ⊣ CategoryTheory.sheafToPresheaf J A

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.Equivalence.instPreservesFiniteLimitsFunctorOppositeOppositeCategorySheafInstCategorySheafTransportAndSheafify {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] [CategoryTheory.HasSheafify K A] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Equivalence.transportAndSheafify J K e A)

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Equivalence.hasSheafify {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] [CategoryTheory.HasSheafify K A] : CategoryTheory.HasSheafify J A

Transport HasSheafify along an equivalence of sites.

theorem CategoryTheory.Equivalence.hasSheafCompose {C : Type u_1} [CategoryTheory.Category.{u_6, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{u_9, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] {A : Type u_4} [CategoryTheory.Category.{u_7, u_4} A] {B : Type u_5} [CategoryTheory.Category.{u_8, u_5} B] (F : CategoryTheory.Functor A B) [CategoryTheory.GrothendieckTopology.HasSheafCompose K F] : CategoryTheory.GrothendieckTopology.HasSheafCompose J F

noncomputable def CategoryTheory.smallSheafify {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.EssentiallySmall.{u_7, u_5, u_1} C] [CategoryTheory.HasSheafify (CategoryTheory.LocallyCoverDense.inducedTopology ⋯) A] : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)

Transport to a small model and sheafify there.

Equations

• CategoryTheory.smallSheafify J A = CategoryTheory.Equivalence.transportAndSheafify J (CategoryTheory.LocallyCoverDense.inducedTopology ⋯) (CategoryTheory.equivSmallModel C) A

noncomputable def CategoryTheory.smallSheafificationAdjunction {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.EssentiallySmall.{u_7, u_5, u_1} C] [CategoryTheory.HasSheafify (CategoryTheory.LocallyCoverDense.inducedTopology ⋯) A] : CategoryTheory.smallSheafify J A ⊣ CategoryTheory.sheafToPresheaf J A

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.hasSheafifyEssentiallySmallSite {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.EssentiallySmall.{u_7, u_5, u_1} C] [CategoryTheory.HasSheafify (CategoryTheory.LocallyCoverDense.inducedTopology ⋯) A] : CategoryTheory.HasSheafify J A

Equations

• ⋯ = ⋯

instance CategoryTheory.hasSheafComposeEssentiallySmallSite {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.EssentiallySmall.{u_7, u_5, u_1} C] (B : Type u_4) [CategoryTheory.Category.{u_8, u_4} B] (F : CategoryTheory.Functor A B) [CategoryTheory.GrothendieckTopology.HasSheafCompose (CategoryTheory.LocallyCoverDense.inducedTopology ⋯) F] : CategoryTheory.GrothendieckTopology.HasSheafCompose J F

Equations

• ⋯ = ⋯

instance CategoryTheory.hasLimitsEssentiallySmallSite {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.EssentiallySmall.{u_7, u_5, u_1} C] [CategoryTheory.Limits.HasLimits (CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology ⋯) A)] : CategoryTheory.Limits.HasLimitsOfSize.{max u_6 u_7, max u_6 u_7, max u_1 u_6, max (max (max u_3 u_1) u_6) u_5} (CategoryTheory.Sheaf J A)

Equations

• ⋯ = ⋯

instance CategoryTheory.hasColimitsEssentiallySmallSite {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.EssentiallySmall.{u_7, u_5, u_1} C] [CategoryTheory.Limits.HasColimits (CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology ⋯) A)] : CategoryTheory.Limits.HasColimitsOfSize.{max u_6 u_7, max u_6 u_7, max u_1 u_6, max (max (max u_3 u_1) u_6) u_5} (CategoryTheory.Sheaf J A)

Equations

• ⋯ = ⋯