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} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] (F : CategoryTheory.Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] : (CategoryTheory.whiskeringLeft Cᵒᵖ D E).obj (J.sheafify P) ≅ ((CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D) (F : CategoryTheory.Functor D E) [∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D) (F : CategoryTheory.Functor D E) [∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] (F : CategoryTheory.Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] : (J.sheafification D).comp ((CategoryTheory.whiskeringRight Cᵒᵖ D E).obj F) ≅ ((CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] (F : CategoryTheory.Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) : (J.sheafificationWhiskerRightIso F).hom.app P = (J.sheafifyCompIso F P).hom

@[simp]

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

@[simp]

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

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

@[simp]

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