Documentation

Mathlib.CategoryTheory.Sites.CompatiblePlus

Compatibility of the plus construction with functors #

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

See CategoryTheory/Sites/CompatibleSheafification for the compatibility of sheafification, which follows easily from the content in this file.

source
noncomputable def CategoryTheory.GrothendieckTopology.diagramCompIso {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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) (X : C) :
(J.diagram P X).comp F ≅ J.diagram (P.comp F) X

The diagram used to define P⁺, composed with F, is isomorphic to the diagram used to define P ⋙ F.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.diagramCompIso_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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) (X : C) (W : (J.Cover X)ᵒᵖ) (i : (Opposite.unop W).Arrow) :
    CategoryStruct.comp ((J.diagramCompIso F P X).hom.app W) (Limits.Multiequalizer.ι ((Opposite.unop W).index (P.comp F)) i) = F.map (Limits.Multiequalizer.ι ((Opposite.unop W).index P) i)
    source
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.diagramCompIso_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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) (X : C) (W : (J.Cover X)ᵒᵖ) (i : (Opposite.unop W).Arrow) {Z : E} (h : ((Opposite.unop W).index (P.comp F)).left i ⟶ Z) :
    CategoryStruct.comp ((J.diagramCompIso F P X).hom.app W) (CategoryStruct.comp (Limits.Multiequalizer.ι ((Opposite.unop W).index (P.comp F)) i) h) = CategoryStruct.comp (F.map (Limits.Multiequalizer.ι ((Opposite.unop W).index P) i)) h
    source
    noncomputable def CategoryTheory.GrothendieckTopology.plusCompIso {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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] :
    (J.plusObj P).comp F ≅ J.plusObj (P.comp F)

    The isomorphism between P⁺ ⋙ F and (P ⋙ F)⁺.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.GrothendieckTopology.ι_plusCompIso_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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) [∀ (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 (Opposite.unop X))ᵒᵖ) :
      CategoryStruct.comp (F.map (Limits.colimit.ι (J.diagram P (Opposite.unop X)) W)) ((J.plusCompIso F P).hom.app X) = CategoryStruct.comp ((J.diagramCompIso F P (Opposite.unop X)).hom.app W) (Limits.colimit.ι (J.diagram (P.comp F) (Opposite.unop X)) W)
      source
      @[simp]
      theorem CategoryTheory.GrothendieckTopology.ι_plusCompIso_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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) [∀ (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 (Opposite.unop X))ᵒᵖ) {Z : E} (h : (J.plusObj (P.comp F)).obj X ⟶ Z) :
      CategoryStruct.comp (F.map (Limits.colimit.ι (J.diagram P (Opposite.unop X)) W)) (CategoryStruct.comp ((J.plusCompIso F P).hom.app X) h) = CategoryStruct.comp ((J.diagramCompIso F P (Opposite.unop X)).hom.app W) (CategoryStruct.comp (Limits.colimit.ι (J.diagram (P.comp F) (Opposite.unop X)) W) h)
      source
      @[simp]
      theorem CategoryTheory.GrothendieckTopology.plusCompIso_whiskerLeft {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] {F G : Functor D E} (η : F ⟶ G) (P : Functor Cᵒᵖ D) [∀ (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] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ G] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan G] :
      CategoryStruct.comp ((J.plusObj P).whiskerLeft η) (J.plusCompIso G P).hom = CategoryStruct.comp (J.plusCompIso F P).hom (J.plusMap (P.whiskerLeft η))
      source
      @[simp]
      theorem CategoryTheory.GrothendieckTopology.plusCompIso_whiskerLeft_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] [∀ (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] {F G : Functor D E} (η : F ⟶ G) (P : Functor Cᵒᵖ D) [∀ (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] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ G] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan G] {Z : Functor Cᵒᵖ E} (h : J.plusObj (P.comp G) ⟶ Z) :
      CategoryStruct.comp ((J.plusObj P).whiskerLeft η) (CategoryStruct.comp (J.plusCompIso G P).hom h) = CategoryStruct.comp (J.plusCompIso F P).hom (CategoryStruct.comp (J.plusMap (P.whiskerLeft η)) h)
      source
      noncomputable def CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso {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.plusObj P) ≅ ((Functor.whiskeringLeft Cᵒᵖ D E).obj P).comp (J.plusFunctor E)

      The isomorphism between P⁺ ⋙ F and (P ⋙ F)⁺, functorially in F.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso_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) (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] (X : Functor D E) :
        (J.plusFunctorWhiskerLeftIso P).hom.app X = (J.plusCompIso X P).hom
        source
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso_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) (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] (X : Functor D E) :
        (J.plusFunctorWhiskerLeftIso P).inv.app X = (J.plusCompIso X P).inv
        source
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.plusCompIso_whiskerRight {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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) :
        CategoryStruct.comp (Functor.whiskerRight (J.plusMap η) F) (J.plusCompIso F Q).hom = CategoryStruct.comp (J.plusCompIso F P).hom (J.plusMap (Functor.whiskerRight η F))
        source
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.plusCompIso_whiskerRight_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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] {P Q : Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : Functor Cᵒᵖ E} (h : J.plusObj (Q.comp F) ⟶ Z) :
        CategoryStruct.comp (Functor.whiskerRight (J.plusMap η) F) (CategoryStruct.comp (J.plusCompIso F Q).hom h) = CategoryStruct.comp (J.plusCompIso F P).hom (CategoryStruct.comp (J.plusMap (Functor.whiskerRight η F)) h)
        source
        noncomputable def CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso {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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] :
        (J.plusFunctor D).comp ((Functor.whiskeringRight Cᵒᵖ D E).obj F) ≅ ((Functor.whiskeringRight Cᵒᵖ D E).obj F).comp (J.plusFunctor E)

        The isomorphism between P⁺ ⋙ F and (P ⋙ F)⁺, functorially in P.

        Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso_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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] [∀ (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 : Functor Cᵒᵖ D) :
          (J.plusFunctorWhiskerRightIso F).inv.app X = (J.plusCompIso F X).inv
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso_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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] [∀ (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 : Functor Cᵒᵖ D) :
          (J.plusFunctorWhiskerRightIso F).hom.app X = (J.plusCompIso F X).hom
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.whiskerRight_toPlus_comp_plusCompIso_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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] :
          CategoryStruct.comp (Functor.whiskerRight (J.toPlus P) F) (J.plusCompIso F P).hom = J.toPlus (P.comp F)
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.whiskerRight_toPlus_comp_plusCompIso_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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] {Z : Functor Cᵒᵖ E} (h : J.plusObj (P.comp F) ⟶ Z) :
          CategoryStruct.comp (Functor.whiskerRight (J.toPlus P) F) (CategoryStruct.comp (J.plusCompIso F P).hom h) = CategoryStruct.comp (J.toPlus (P.comp F)) h
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.toPlus_comp_plusCompIso_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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] :
          CategoryStruct.comp (J.toPlus (P.comp F)) (J.plusCompIso F P).inv = Functor.whiskerRight (J.toPlus P) F
          source
          theorem CategoryTheory.GrothendieckTopology.plusCompIso_inv_eq_plusLift {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) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] (hP : Presheaf.IsSheaf J ((J.plusObj P).comp F)) :
          (J.plusCompIso F P).inv = J.plusLift (Functor.whiskerRight (J.toPlus P) F) hP