In this file, we prove that sheafification is compatible with functors which preserve the correct limits and colimits.

noncomputable def CategoryTheory.GrothendieckTopology.sheafifyCompIso {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w₁} [Category.{max v u, w₁} D] {E : Type w₂} [Category.{max v u, w₂} E] (F : Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) : (J.sheafify P).comp F ≅ J.sheafify (P.comp F)

The isomorphism between the sheafification of P composed with F and the sheafification of P ⋙ F.

Use the lemmas whisker_right_to_sheafify_sheafify_comp_iso_hom, to_sheafify_comp_sheafify_comp_iso_inv and sheafify_comp_iso_inv_eq_sheafify_lift to reduce the components of this isomorphisms to a state that can be handled using the universal property of sheafification.

Equations

• J.sheafifyCompIso F P = J.plusCompIso F (J.plusObj P) ≪≫ (J.plusFunctor E).mapIso (J.plusCompIso F P)

noncomputable def CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w₁} [Category.{max v u, w₁} D] {E : Type w₂} [Category.{max v u, w₂} E] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : Functor Cᵒᵖ D) [∀ (F : Functor D E) (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (F : Functor D E) (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] : (whiskeringLeft Cᵒᵖ D E).obj (J.sheafify P) ≅ ((whiskeringLeft Cᵒᵖ D E).obj P).comp (J.sheafification E)

The isomorphism between the sheafification of P composed with F and the sheafification of P ⋙ F, functorially in F.

Equations

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso_hom_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w₁} [Category.{max v u, w₁} D] {E : Type w₂} [Category.{max v u, w₂} E] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : Functor Cᵒᵖ D) (F : Functor D E) [∀ (F : Functor D E) (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (F : Functor D E) (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] : (J.sheafificationWhiskerLeftIso P).hom.app F = (J.sheafifyCompIso F P).hom

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso_inv_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w₁} [Category.{max v u, w₁} D] {E : Type w₂} [Category.{max v u, w₂} E] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : Functor Cᵒᵖ D) (F : Functor D E) [∀ (F : Functor D E) (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (F : Functor D E) (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] : (J.sheafificationWhiskerLeftIso P).inv.app F = (J.sheafifyCompIso F P).inv

noncomputable def CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w₁} [Category.{max v u, w₁} D] {E : Type w₂} [Category.{max v u, w₂} E] (F : Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] : (J.sheafification D).comp ((whiskeringRight Cᵒᵖ D E).obj F) ≅ ((whiskeringRight Cᵒᵖ D E).obj F).comp (J.sheafification E)

The isomorphism between the sheafification of P composed with F and the sheafification of P ⋙ F, functorially in P.

Equations

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_hom_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w₁} [Category.{max v u, w₁} D] {E : Type w₂} [Category.{max v u, w₂} E] (F : Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) : (J.sheafificationWhiskerRightIso F).hom.app P = (J.sheafifyCompIso F P).hom

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_inv_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w₁} [Category.{max v u, w₁} D] {E : Type w₂} [Category.{max v u, w₂} E] (F : Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) : (J.sheafificationWhiskerRightIso F).inv.app P = (J.sheafifyCompIso F P).inv

@[simp]

theorem CategoryTheory.GrothendieckTopology.whiskerRight_toSheafify_sheafifyCompIso_hom {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w₁} [Category.{max v u, w₁} D] {E : Type w₂} [Category.{max v u, w₂} E] (F : Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) : CategoryStruct.comp (whiskerRight (J.toSheafify P) F) (J.sheafifyCompIso F P).hom = J.toSheafify (P.comp F)

theorem CategoryTheory.GrothendieckTopology.whiskerRight_toSheafify_sheafifyCompIso_hom_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w₁} [Category.{max v u, w₁} D] {E : Type w₂} [Category.{max v u, w₂} E] (F : Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) {Z : Functor Cᵒᵖ E} (h : J.sheafify (P.comp F) ⟶ Z) : CategoryStruct.comp (whiskerRight (J.toSheafify P) F) (CategoryStruct.comp (J.sheafifyCompIso F P).hom h) = CategoryStruct.comp (J.toSheafify (P.comp F)) h

@[simp]

theorem CategoryTheory.GrothendieckTopology.toSheafify_comp_sheafifyCompIso_inv {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w₁} [Category.{max v u, w₁} D] {E : Type w₂} [Category.{max v u, w₂} E] (F : Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) : CategoryStruct.comp (J.toSheafify (P.comp F)) (J.sheafifyCompIso F P).inv = whiskerRight (J.toSheafify P) F

theorem CategoryTheory.GrothendieckTopology.toSheafify_comp_sheafifyCompIso_inv_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w₁} [Category.{max v u, w₁} D] {E : Type w₂} [Category.{max v u, w₂} E] (F : Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) {Z : Functor Cᵒᵖ E} (h : (J.sheafify P).comp F ⟶ Z) : CategoryStruct.comp (J.toSheafify (P.comp F)) (CategoryStruct.comp (J.sheafifyCompIso F P).inv h) = CategoryStruct.comp (whiskerRight (J.toSheafify P) F) h

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafifyCompIso_inv_eq_sheafifyLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w₁} [Category.{max v u, w₁} D] {E : Type w₂} [Category.{max v u, w₂} E] (F : Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) [HasForget D] [Limits.PreservesLimits (forget D)] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [(forget D).ReflectsIsomorphisms] : (J.sheafifyCompIso F P).inv = J.sheafifyLift (whiskerRight (J.toSheafify P) F) ⋯