Documentation

Mathlib.CategoryTheory.Sites.CompatiblePlus

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
def CategoryTheory.GrothendieckTopology.diagramCompIso {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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) :
CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.diagram J P X) F ≅ CategoryTheory.GrothendieckTopology.diagram J (CategoryTheory.Functor.comp P 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_ι_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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (W : (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ) (i : CategoryTheory.GrothendieckTopology.Cover.Arrow W.unop) {Z : E} (h : (CategoryTheory.GrothendieckTopology.Cover.index W.unop (CategoryTheory.Functor.comp P F)).left i ⟶ Z) :
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.diagramCompIso J F P X).hom.app W) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index W.unop (CategoryTheory.Functor.comp P F)) i) h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index W.unop P) i)) h
    source
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.diagramCompIso_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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (W : (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ) (i : CategoryTheory.GrothendieckTopology.Cover.Arrow W.unop) :
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.diagramCompIso J F P X).hom.app W) (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index W.unop (CategoryTheory.Functor.comp P F)) i) = F.map (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index W.unop P) i)
    source
    def CategoryTheory.GrothendieckTopology.plusCompIso {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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] :
    CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.plusObj J P) F ≅ CategoryTheory.GrothendieckTopology.plusObj J (CategoryTheory.Functor.comp P 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_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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] (X : Cᵒᵖ) (W : (CategoryTheory.GrothendieckTopology.Cover J X.unop)ᵒᵖ) {Z : E} (h : (CategoryTheory.GrothendieckTopology.plusObj J (CategoryTheory.Functor.comp P F)).obj X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.colimit.ι (CategoryTheory.GrothendieckTopology.diagram J P X.unop) W)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.plusCompIso J F P).hom.app X) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.diagramCompIso J F P X.unop).hom.app W) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.GrothendieckTopology.diagram J (CategoryTheory.Functor.comp P F) X.unop) W) h)
      source
      @[simp]
      theorem CategoryTheory.GrothendieckTopology.ι_plusCompIso_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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] (X : Cᵒᵖ) (W : (CategoryTheory.GrothendieckTopology.Cover J X.unop)ᵒᵖ) :
      CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.colimit.ι (CategoryTheory.GrothendieckTopology.diagram J P X.unop) W)) ((CategoryTheory.GrothendieckTopology.plusCompIso J F P).hom.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.diagramCompIso J F P X.unop).hom.app W) (CategoryTheory.Limits.colimit.ι (CategoryTheory.GrothendieckTopology.diagram J (CategoryTheory.Functor.comp P F) X.unop) W)
      source
      @[simp]
      theorem CategoryTheory.GrothendieckTopology.plusCompIso_whiskerLeft_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] [∀ (α β : 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor D E} (η : F ⟶ G) (P : CategoryTheory.Functor Cᵒᵖ D) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ G] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) G] {Z : CategoryTheory.Functor Cᵒᵖ E} (h : CategoryTheory.GrothendieckTopology.plusObj J (CategoryTheory.Functor.comp P G) ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.GrothendieckTopology.plusObj J P) η) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.plusCompIso J G P).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.plusCompIso J F P).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.plusMap J (CategoryTheory.whiskerLeft P η)) h)
      source
      @[simp]
      theorem CategoryTheory.GrothendieckTopology.plusCompIso_whiskerLeft {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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor D E} (η : F ⟶ G) (P : CategoryTheory.Functor Cᵒᵖ D) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ G] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) G] :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.GrothendieckTopology.plusObj J P) η) (CategoryTheory.GrothendieckTopology.plusCompIso J G P).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.plusCompIso J F P).hom (CategoryTheory.GrothendieckTopology.plusMap J (CategoryTheory.whiskerLeft P η))
      source
      @[simp]
      theorem CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso_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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D) [(F : CategoryTheory.Functor D E) → (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(F : CategoryTheory.Functor D E) → (X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (X : CategoryTheory.Functor D E) :
      (CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso J P).inv.app X = (CategoryTheory.GrothendieckTopology.plusCompIso J X P).inv
      source
      @[simp]
      theorem CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso_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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D) [(F : CategoryTheory.Functor D E) → (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(F : CategoryTheory.Functor D E) → (X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (X : CategoryTheory.Functor D E) :
      (CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso J P).hom.app X = (CategoryTheory.GrothendieckTopology.plusCompIso J X P).hom
      source
      def CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso {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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D) [(F : CategoryTheory.Functor D E) → (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(F : CategoryTheory.Functor D E) → (X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] :
      (CategoryTheory.whiskeringLeft Cᵒᵖ D E).obj (CategoryTheory.GrothendieckTopology.plusObj J P) ≅ CategoryTheory.Functor.comp ((CategoryTheory.whiskeringLeft Cᵒᵖ D E).obj P) (CategoryTheory.GrothendieckTopology.plusFunctor J E)

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.plusCompIso_whiskerRight_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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : CategoryTheory.Functor Cᵒᵖ E} (h : CategoryTheory.GrothendieckTopology.plusObj J (CategoryTheory.Functor.comp Q F) ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.GrothendieckTopology.plusMap J η) F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.plusCompIso J F Q).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.plusCompIso J F P).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.plusMap J (CategoryTheory.whiskerRight η F)) h)
        source
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.plusCompIso_whiskerRight {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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.GrothendieckTopology.plusMap J η) F) (CategoryTheory.GrothendieckTopology.plusCompIso J F Q).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.plusCompIso J F P).hom (CategoryTheory.GrothendieckTopology.plusMap J (CategoryTheory.whiskerRight η F))
        source
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso_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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] (X : CategoryTheory.Functor Cᵒᵖ D) :
        (CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso J F).inv.app X = (CategoryTheory.GrothendieckTopology.plusCompIso J F X).inv
        source
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso_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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] (X : CategoryTheory.Functor Cᵒᵖ D) :
        (CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso J F).hom.app X = (CategoryTheory.GrothendieckTopology.plusCompIso J F X).hom
        source
        def CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso {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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] :
        CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.plusFunctor J D) ((CategoryTheory.whiskeringRight Cᵒᵖ D E).obj F) ≅ CategoryTheory.Functor.comp ((CategoryTheory.whiskeringRight Cᵒᵖ D E).obj F) (CategoryTheory.GrothendieckTopology.plusFunctor J E)

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.whiskerRight_toPlus_comp_plusCompIso_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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] {Z : CategoryTheory.Functor Cᵒᵖ E} (h : CategoryTheory.GrothendieckTopology.plusObj J (CategoryTheory.Functor.comp P F) ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.GrothendieckTopology.toPlus J P) F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.plusCompIso J F P).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toPlus J (CategoryTheory.Functor.comp P F)) h
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.whiskerRight_toPlus_comp_plusCompIso_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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.GrothendieckTopology.toPlus J P) F) (CategoryTheory.GrothendieckTopology.plusCompIso J F P).hom = CategoryTheory.GrothendieckTopology.toPlus J (CategoryTheory.Functor.comp P F)
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.toPlus_comp_plusCompIso_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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toPlus J (CategoryTheory.Functor.comp P F)) (CategoryTheory.GrothendieckTopology.plusCompIso J F P).inv = CategoryTheory.whiskerRight (CategoryTheory.GrothendieckTopology.toPlus J P) F
          source
          theorem CategoryTheory.GrothendieckTopology.plusCompIso_inv_eq_plusLift {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) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] (hP : CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.plusObj J P) F)) :
          (CategoryTheory.GrothendieckTopology.plusCompIso J F P).inv = CategoryTheory.GrothendieckTopology.plusLift J (CategoryTheory.whiskerRight (CategoryTheory.GrothendieckTopology.toPlus J P) F) hP