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 (_ : CategoryTheory.LocallyCoverDense J e.inverse)) 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 (_ : CategoryTheory.LocallyCoverDense J e.inverse))

Equations

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

instance CategoryTheory.Equivalence.instIsContinuousFunctorInducedTopologyInverseFullOfEquivalenceOfEquivalenceInverseFaithfulOfEquivalenceLocallyCoverDense {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.IsContinuous e.functor J (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse))

Equations

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

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

• (_ : CategoryTheory.Functor.IsCoverDense e.inverse J) = (_ : CategoryTheory.Functor.IsCoverDense e.inverse J)

instance CategoryTheory.Equivalence.instIsContinuousInverseInducedTopologyFullOfEquivalenceOfEquivalenceInverseFaithfulOfEquivalenceLocallyCoverDense {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.IsContinuous e.inverse (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) J

Equations

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

@[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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (F : CategoryTheory.Sheaf J A) (X : Dᵒᵖ) : ((CategoryTheory.Equivalence.sheafCongr.functor J e A).toPrefunctor.obj F).val.toPrefunctor.obj X = F.val.toPrefunctor.obj (Opposite.op (e.inverse.toPrefunctor.obj X.unop))

@[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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] : ∀ {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y) (X_1 : Dᵒᵖ), ((CategoryTheory.Equivalence.sheafCongr.functor J e A).toPrefunctor.map f).val.app X_1 = f.val.app (Opposite.op (e.inverse.toPrefunctor.obj X_1.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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (F : CategoryTheory.Sheaf J A) : ∀ {X Y : Dᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.Equivalence.sheafCongr.functor J e A).toPrefunctor.obj F).val.toPrefunctor.map f = F.val.toPrefunctor.map (e.inverse.toPrefunctor.map f.unop).op

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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] : CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) 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_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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] : ∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) A} (f : X ⟶ Y) (X_1 : Cᵒᵖ), ((CategoryTheory.Equivalence.sheafCongr.inverse J e A).toPrefunctor.map f).val.app X_1 = f.val.app (Opposite.op (e.functor.toPrefunctor.obj X_1.unop))

@[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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (F : CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) A) (X : Cᵒᵖ) : ((CategoryTheory.Equivalence.sheafCongr.inverse J e A).toPrefunctor.obj F).val.toPrefunctor.obj X = F.val.toPrefunctor.obj (Opposite.op (e.functor.toPrefunctor.obj X.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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (F : CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) A) : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.Equivalence.sheafCongr.inverse J e A).toPrefunctor.obj F).val.toPrefunctor.map f = F.val.toPrefunctor.map (e.functor.toPrefunctor.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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] : CategoryTheory.Functor (CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) 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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (X : CategoryTheory.Sheaf J A) (X : Cᵒᵖ) : ((CategoryTheory.Equivalence.sheafCongr.unitIso J e A).hom.app X✝).val.app X = X✝.val.toPrefunctor.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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (X : CategoryTheory.Sheaf J A) (X : Cᵒᵖ) : ((CategoryTheory.Equivalence.sheafCongr.unitIso J e A).inv.app X✝).val.app X = X✝.val.toPrefunctor.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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] : CategoryTheory.Functor.id (CategoryTheory.Sheaf J A) ≅ CategoryTheory.Functor.comp (CategoryTheory.Equivalence.sheafCongr.functor J e A) (CategoryTheory.Equivalence.sheafCongr.inverse J 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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (X : CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) A) (X : Dᵒᵖ) : ((CategoryTheory.Equivalence.sheafCongr.counitIso J e A).hom.app X✝).val.app X = X✝.val.toPrefunctor.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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (X : CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) A) (X : Dᵒᵖ) : ((CategoryTheory.Equivalence.sheafCongr.counitIso J e A).inv.app X✝).val.app X = X✝.val.toPrefunctor.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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] : CategoryTheory.Functor.comp (CategoryTheory.Equivalence.sheafCongr.inverse J e A) (CategoryTheory.Equivalence.sheafCongr.functor J e A) ≅ CategoryTheory.Functor.id (CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) 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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] : CategoryTheory.Sheaf J A ≌ CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) 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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.HasSheafify (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) 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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] : CategoryTheory.Functor.comp (CategoryTheory.Equivalence.sheafCongr J e A).functor (CategoryTheory.Functor.comp (CategoryTheory.sheafToPresheaf (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) 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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.HasSheafify (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) A] : CategoryTheory.Equivalence.transportAndSheafify J 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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.HasSheafify (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) A] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Equivalence.transportAndSheafify J e A)

Equations

• CategoryTheory.Equivalence.instPreservesFiniteLimitsFunctorOppositeOppositeCategorySheafInstCategorySheafTransportAndSheafify J e A = CategoryTheory.Limits.PreservesFiniteLimits.mk

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] (e : C ≌ D) (A : Type u_3) [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.HasSheafify (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) 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] (e : C ≌ D) {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 (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J e.inverse)) F] : CategoryTheory.GrothendieckTopology.HasSheafCompose J F

noncomputable def CategoryTheory.smallSheafify {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.EssentiallySmall.{u_5, u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_2) [CategoryTheory.Category.{u_6, u_2} A] [CategoryTheory.HasSheafify (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J (CategoryTheory.equivSmallModel C).inverse)) 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.equivSmallModel C) A

noncomputable def CategoryTheory.smallSheafificationAdjunction {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.EssentiallySmall.{u_5, u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_2) [CategoryTheory.Category.{u_6, u_2} A] [CategoryTheory.HasSheafify (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J (CategoryTheory.equivSmallModel C).inverse)) 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

• CategoryTheory.smallSheafificationAdjunction J A = CategoryTheory.Equivalence.transportSheafificationAdjunction J (CategoryTheory.equivSmallModel C) A

noncomputable instance CategoryTheory.hasSheafifyEssentiallySmallSite {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.EssentiallySmall.{u_5, u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_2) [CategoryTheory.Category.{u_6, u_2} A] [CategoryTheory.HasSheafify (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J (CategoryTheory.equivSmallModel C).inverse)) A] : CategoryTheory.HasSheafify J A

Equations

• (_ : CategoryTheory.HasSheafify J A) = (_ : CategoryTheory.HasSheafify J A)

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

Equations

• (_ : CategoryTheory.GrothendieckTopology.HasSheafCompose J F) = (_ : CategoryTheory.GrothendieckTopology.HasSheafCompose J F)

instance CategoryTheory.hasLimitsEssentiallySmallSite {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.EssentiallySmall.{u_5, u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_2) [CategoryTheory.Category.{u_6, u_2} A] [CategoryTheory.Limits.HasLimits (CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J (CategoryTheory.equivSmallModel C).inverse)) A)] : CategoryTheory.Limits.HasLimitsOfSize.{max u_5 u_6, max u_5 u_6, max u_1 u_6, max (max (max u_2 u_1) u_6) u_4} (CategoryTheory.Sheaf J A)

Equations

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

instance CategoryTheory.hasColimitsEssentiallySmallSite {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.EssentiallySmall.{u_5, u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_2) [CategoryTheory.Category.{u_6, u_2} A] [CategoryTheory.Limits.HasColimits (CategoryTheory.Sheaf (CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense J (CategoryTheory.equivSmallModel C).inverse)) A)] : CategoryTheory.Limits.HasColimitsOfSize.{max u_5 u_6, max u_5 u_6, max u_1 u_6, max (max (max u_2 u_1) u_6) u_4} (CategoryTheory.Sheaf J A)

Equations

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