Documentation

Mathlib.CategoryTheory.Sites.Equivalence

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₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [G.IsEquivalence] :

G.IsCoverDense J

Equations

⋯ = ⋯

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

CategoryTheory.Functor.IsDenseSubsite J (e.inverse.inducedTopology J) e.functor

Equations

⋯ = ⋯

theorem CategoryTheory.Equivalence.coverPreserving {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

CategoryTheory.CoverPreserving J (e.inverse.inducedTopology J) e.functor

class CategoryTheory.Equivalence.TransportsGrothendieckTopology {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) :

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

eq_inducedTopology : K = e.inverse.inducedTopology J
K is equal to the induced topology.

Instances

theorem CategoryTheory.Equivalence.TransportsGrothendieckTopology.eq_inducedTopology {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {e : C ≌ D} [self : CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] :

K = e.inverse.inducedTopology J

K is equal to the induced topology.

instance CategoryTheory.Equivalence.instTransportsGrothendieckTopologyInducedTopologyInverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

CategoryTheory.Equivalence.TransportsGrothendieckTopology J (e.inverse.inducedTopology J) e

Equations

⋯ = ⋯

theorem CategoryTheory.Equivalence.eq_inducedTopology_of_transports {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] :

K = e.inverse.inducedTopology J

instance CategoryTheory.Equivalence.instIsContinuousFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] :

e.functor.IsContinuous J K

Equations

⋯ = ⋯

instance CategoryTheory.Equivalence.instIsContinuousInverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] :

e.inverse.IsContinuous K J

Equations

⋯ = ⋯

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.functor_obj_val_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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 (Opposite.unop X)))

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.functor_map_val_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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 (Opposite.unop X_1)))

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.functor_obj_val_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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

def CategoryTheory.Equivalence.sheafCongr.functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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.

Instances For

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.inverse_map_val_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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 (Opposite.unop X_1)))

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.inverse_obj_val_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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 (Opposite.unop X)))

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.inverse_obj_val_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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.

Instances For

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.unitIso_inv_app_val_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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 (Opposite.unop X)).op

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.unitIso_hom_app_val_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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 (Opposite.unop X)).op

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

CategoryTheory.Functor.id (CategoryTheory.Sheaf J A) ≅ (CategoryTheory.Equivalence.sheafCongr.functor J K e A).comp (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.

Instances For

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.counitIso_hom_app_val_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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 (Opposite.unop X)).op

@[simp]

theorem CategoryTheory.Equivalence.sheafCongr.counitIso_inv_app_val_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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 (Opposite.unop X)).op

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

(CategoryTheory.Equivalence.sheafCongr.inverse J K e A).comp (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.

Instances For

def CategoryTheory.Equivalence.sheafCongr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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.

Instances For

noncomputable def CategoryTheory.Equivalence.transportAndSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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

CategoryTheory.Equivalence.transportAndSheafify J K e A = e.op.congrLeft.functor.comp ((CategoryTheory.presheafToSheaf K A).comp (CategoryTheory.Equivalence.sheafCongr J K e A).inverse)

Instances For

noncomputable def CategoryTheory.Equivalence.transportIsoSheafToPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] :

(CategoryTheory.Equivalence.sheafCongr J K e A).functor.comp ((CategoryTheory.sheafToPresheaf K A).comp e.op.congrLeft.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.

Instances For

noncomputable def CategoryTheory.Equivalence.transportSheafificationAdjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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.

Instances For

noncomputable instance CategoryTheory.Equivalence.instPreservesFiniteLimitsFunctorOppositeSheafTransportAndSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} 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₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e] {A : Type u_1} [CategoryTheory.Category.{u_3, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) [K.HasSheafCompose F] :

J.HasSheafCompose F

noncomputable def CategoryTheory.smallSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.EssentiallySmall.{w, v₁, u₁} C] [CategoryTheory.HasSheafify ((CategoryTheory.equivSmallModel C).inverse.inducedTopology J) 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).inverse.inducedTopology J) (CategoryTheory.equivSmallModel C) A

Instances For

noncomputable def CategoryTheory.smallSheafificationAdjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.EssentiallySmall.{w, v₁, u₁} C] [CategoryTheory.HasSheafify ((CategoryTheory.equivSmallModel C).inverse.inducedTopology J) 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.

Instances For

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

CategoryTheory.HasSheafify J A

Equations

⋯ = ⋯

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

J.HasSheafCompose F

Equations

⋯ = ⋯

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

CategoryTheory.Limits.HasLimitsOfSize.{max v₃ w, max v₃ w, max u₁ v₃, max (max (max u₃ u₁) v₃) v₁} (CategoryTheory.Sheaf J A)

Equations

⋯ = ⋯

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

CategoryTheory.Limits.HasColimitsOfSize.{max v₃ w, max v₃ w, max u₁ v₃, max (max (max u₃ u₁) v₃) v₁} (CategoryTheory.Sheaf J A)

Equations

⋯ = ⋯

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

K.W.inverseImage ((CategoryTheory.whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) = J.W

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

K.W (CategoryTheory.whiskerLeft G.op f) ↔ J.W f

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

J.WEqualsLocallyBijective A