Compatibility of sheafification with functors #
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 u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) 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) :
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 isomorphism 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)
Instances For
noncomputable def CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) 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] :
(Functor.whiskeringLeft Cᵒᵖ D E).obj (J.sheafify P) ≅ ((Functor.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.
Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso_hom_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) 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] :
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso_inv_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) 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] :
noncomputable def CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) 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 ((Functor.whiskeringRight Cᵒᵖ D E).obj F) ≅ ((Functor.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.
Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_hom_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) 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) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_inv_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) 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) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.whiskerRight_toSheafify_sheafifyCompIso_hom {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) 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 (Functor.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 u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) 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 (Functor.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 u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) 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 = Functor.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 u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) 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 (Functor.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 u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) 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) {FD : D → D → Type u_3} {CD : D → Type u_4} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [Limits.PreservesLimitsOfSize.{max v u, max v u, v_1, u_4, u_1, u_4 + 1} (forget D)] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [(forget D).ReflectsIsomorphisms] :