Cocontinuous functors between sites.

We define cocontinuous functors between sites as functors that pull covering sieves back to covering sieves. This concept is also known as cover-lifting or cover-reflecting functors. We use the original terminology and definition of SGA 4 III 2.1. However, the notion of cocontinuous functor should not be confused with the general definition of cocontinuous functors between categories as functors preserving small colimits.

Main definitions

• CategoryTheory.Functor.IsCocontinuous: a functor between sites is cocontinuous if it pulls back covering sieves to covering sieves
• CategoryTheory.Functor.sheafPushforwardCocontinuous: A cocontinuous functor G : (C, J) ⥤ (D, K) induces a functor Sheaf J A ⥤ Sheaf K A.

Main results

• CategoryTheory.ran_isSheaf_of_isCocontinuous: If G : C ⥤ D is cocontinuous, then G.op.ran (ₚu) as a functor (Cᵒᵖ ⥤ A) ⥤ (Dᵒᵖ ⥤ A) of presheaves maps sheaves to sheaves.
• CategoryTheory.Functor.sheafAdjunctionCocontinuous: If G : (C, J) ⥤ (D, K) is cocontinuous and continuous, then G.sheafPushforwardContinuous A J K and G.sheafPushforwardCocontinuous A J K are adjoint.

References

• [Elephant]: Sketches of an Elephant, P. T. Johnstone: C2.3.
• [S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic][MM92]
• https://stacks.math.columbia.edu/tag/00XI

class CategoryTheory.Functor.IsCocontinuous {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) : Prop

A functor G : (C, J) ⥤ (D, K) between sites is called cocontinuous (SGA 4 III 2.1) if for all covering sieves R in D, R.pullback G is a covering sieve in C.

• cover_lift : ∀ {U : C} {S : CategoryTheory.Sieve (G.obj U)}, S ∈ K (G.obj U) → CategoryTheory.Sieve.functorPullback G S ∈ J U

theorem CategoryTheory.Functor.IsCocontinuous.cover_lift {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_4, u_1} C} {D : Type u_2} {inst_1 : CategoryTheory.Category.{u_5, u_2} D} {G : CategoryTheory.Functor C D} {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [self : G.IsCocontinuous J K] {U : C} {S : CategoryTheory.Sieve (G.obj U)}, S ∈ K (G.obj U) → CategoryTheory.Sieve.functorPullback G S ∈ J U

theorem CategoryTheory.Functor.cover_lift {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] {U : C} {S : CategoryTheory.Sieve (G.obj U)} (hS : S ∈ K (G.obj U)) : CategoryTheory.Sieve.functorPullback G S ∈ J U

instance CategoryTheory.isCocontinuous_id {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) : (CategoryTheory.Functor.id C).IsCocontinuous J J

The identity functor on a site is cocontinuous.

Equations

• ⋯ = ⋯

theorem CategoryTheory.isCocontinuous_comp {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] (G : CategoryTheory.Functor C D) (G' : CategoryTheory.Functor D E) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {L : CategoryTheory.GrothendieckTopology E} [G.IsCocontinuous J K] [G'.IsCocontinuous K L] : (G.comp G').IsCocontinuous J L

The composition of two cocontinuous functors is cocontinuous.

We will now prove that G.op.ran : (Cᵒᵖ ⥤ A) ⥤ (Dᵒᵖ ⥤ A) maps sheaves to sheaves when G : C ⥤ D is a cocontinuous functor.

We do not follow the proofs in SGA 4 III 2.2 or https://stacks.math.columbia.edu/tag/00XK. Instead, we verify as directly as possible that if F : Cᵒᵖ ⥤ A is a sheaf, then G.op.ran.obj F is a sheaf. in order to do this, we use the "multifork" characterization of sheaves which involves limits in the category A. As G.op.ran.obj F is the chosen right Kan extension of F along G.op : Cᵒᵖ ⥤ Dᵒᵖ, we actually verify that any pointwise right Kan extension of F along G.op is a sheaf.

def CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux {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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y : C} (f : G.obj Y ⟶ X) : s.pt ⟶ F.obj (Opposite.op Y)

Auxiliary definition for lift.

Equations

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

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map {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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y : C} (f : G.obj Y ⟶ X) {W : C} (g : W ⟶ Y) (i : S.Arrow) (h : G.obj W ⟶ i.Y) (w : CategoryTheory.CategoryStruct.comp h i.f = CategoryTheory.CategoryStruct.comp (G.map g) f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map g.op) = CategoryTheory.CategoryStruct.comp (s.ι i) (CategoryTheory.CategoryStruct.comp (R.map h.op) (α.app (Opposite.op W)))

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map' {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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y : C} {Y' : C} (f : G.obj Y ⟶ X) (f' : G.obj Y' ⟶ X) {W : C} (a : W ⟶ Y) (b : W ⟶ Y') (w : CategoryTheory.CategoryStruct.comp (G.map a) f = CategoryTheory.CategoryStruct.comp (G.map b) f') : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map a.op) = CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f') (F.map b.op)

def CategoryTheory.RanIsSheafOfIsCocontinuous.lift {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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) : s.pt ⟶ R.obj (Opposite.op X)

Auxiliary definition for isLimitMultifork

Equations

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

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.fac' {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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) (j : CategoryTheory.StructuredArrow (Opposite.op X) G.op) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (CategoryTheory.CategoryStruct.comp (R.map j.hom) (α.app j.right)) = CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s j.hom.unop

@[simp]

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.fac {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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) (i : S.Arrow) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (R.map i.f.op) = s.ι i

@[simp]

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.fac_assoc {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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) (i : S.Arrow) {Z : A} (h : R.obj (Opposite.op i.Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (CategoryTheory.CategoryStruct.comp (R.map i.f.op) h) = CategoryTheory.CategoryStruct.comp (s.ι i) h

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.hom_ext {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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} {W : A} {f : W ⟶ R.obj (Opposite.op X)} {g : W ⟶ R.obj (Opposite.op X)} (h : ∀ (i : S.Arrow), CategoryTheory.CategoryStruct.comp f (R.map i.f.op) = CategoryTheory.CategoryStruct.comp g (R.map i.f.op)) : f = g

def CategoryTheory.RanIsSheafOfIsCocontinuous.isLimitMultifork {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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} (S : K.Cover X) : CategoryTheory.Limits.IsLimit (S.multifork R)

Auxiliary definition for ran_isSheaf_of_isCocontinuous: if G : C ⥤ D is a cocontinuous functor,

Equations

• CategoryTheory.RanIsSheafOfIsCocontinuous.isLimitMultifork hF hR S = CategoryTheory.Limits.Multifork.IsLimit.mk (S.multifork R) (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR) ⋯ ⋯

theorem CategoryTheory.ran_isSheaf_of_isCocontinuous {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) {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] (ℱ : CategoryTheory.Sheaf J A) : CategoryTheory.Presheaf.IsSheaf K (G.op.ran.obj ℱ.val)

If G is cocontinuous, then G.op.ran pushes sheaves to sheaves.

This is SGA 4 III 2.2. An alternative reference is https://stacks.math.columbia.edu/tag/00XK (where results are obtained under the additional assumption that C and D have pullbacks).

def CategoryTheory.Functor.sheafPushforwardCocontinuous {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) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] : CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf K A)

A cocontinuous functor induces a pushforward functor on categories of sheaves.

Equations

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

def CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso {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) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] : (G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A) ≅ (CategoryTheory.sheafToPresheaf J A).comp G.op.ran

G.sheafPushforwardCocontinuous A J K : Sheaf J A ⥤ Sheaf K A is induced by the right Kan extension functor G.op.ran on presheaves.

Equations

• G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K = CategoryTheory.Iso.refl ((G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A))

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_hom {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) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] : (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).hom = CategoryTheory.CategoryStruct.id ((G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A))

@[simp]

theorem CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_inv {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) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] : (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).inv = CategoryTheory.CategoryStruct.id ((G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A))

noncomputable def CategoryTheory.Functor.sheafAdjunctionCocontinuous {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) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K

Given a functor between sites that is continuous and cocontinuous, the pushforward for the continuous functor G is left adjoint to the pushforward for the cocontinuous functor G.

Equations

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

theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val {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) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] (F : CategoryTheory.Sheaf K A) : ((G.sheafAdjunctionCocontinuous A J K).unit.app F).val = (G.op.ranAdjunction A).unit.app F.val

theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val {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) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] (F : CategoryTheory.Sheaf J A) : ((G.sheafAdjunctionCocontinuous A J K).counit.app F).val = (G.op.ranAdjunction A).counit.app F.val

theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val {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) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] {F : CategoryTheory.Sheaf K A} {H : CategoryTheory.Sheaf J A} (f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H) : (((G.sheafAdjunctionCocontinuous A J K).homEquiv F H) f).val = ((G.op.ranAdjunction A).homEquiv F.val H.val) f.val

def CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility {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) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] [G.IsContinuous J K] : ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp (CategoryTheory.presheafToSheaf J A) ≅ (CategoryTheory.presheafToSheaf K A).comp (G.sheafPushforwardContinuous A J K)

The natural isomorphism exhibiting compatibility between pushforward and sheafification.

Equations

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

theorem CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility {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) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] (F : CategoryTheory.Functor Dᵒᵖ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (G.op.comp F)) ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val = CategoryTheory.whiskerLeft G.op (CategoryTheory.toSheafify K F)

@[simp]

theorem CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val {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) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] (F : CategoryTheory.Functor Dᵒᵖ A) : ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val = CategoryTheory.sheafifyLift J (CategoryTheory.whiskerLeft G.op (CategoryTheory.toSheafify K F)) ⋯