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 : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.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_ι_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 : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.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) :

CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P X).hom.app W) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (P.comp F)) i) h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index 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 : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (W : (J.Cover X)ᵒᵖ) (i : (Opposite.unop W).Arrow) :

CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P X).hom.app W) (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (P.comp F)) i) = F.map (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index P) i)

source

(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_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 : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (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 (Opposite.unop X))ᵒᵖ) {Z : E} (h : (J.plusObj (P.comp F)).obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.colimit.ι (J.diagram P (Opposite.unop X)) W)) (CategoryTheory.CategoryStruct.comp ((J.plusCompIso F P).hom.app X) h) = CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P (Opposite.unop X)).hom.app W) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (J.diagram (P.comp F) (Opposite.unop X)) 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 : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (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 (Opposite.unop X))ᵒᵖ) :

CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.colimit.ι (J.diagram P (Opposite.unop X)) W)) ((J.plusCompIso F P).hom.app X) = CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P (Opposite.unop X)).hom.app W) (CategoryTheory.Limits.colimit.ι (J.diagram (P.comp F) (Opposite.unop X)) W)

source

@[simp]

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (J.plusObj P) η) (CategoryTheory.CategoryStruct.comp (J.plusCompIso G P).hom h) = CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom (CategoryTheory.CategoryStruct.comp (J.plusMap (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 (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor D E} (η : F ⟶ G) (P : CategoryTheory.Functor Cᵒᵖ D) [(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] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ G] [(X : C) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan G] :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (J.plusObj P) η) (J.plusCompIso G P).hom = CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom (J.plusMap (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 (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] (X : CategoryTheory.Functor D E) :

(J.plusFunctorWhiskerLeftIso P).inv.app X = (J.plusCompIso 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 (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] (X : CategoryTheory.Functor D E) :

(J.plusFunctorWhiskerLeftIso P).hom.app X = (J.plusCompIso 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 (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.plusObj P) ≅ ((CategoryTheory.whiskeringLeft Cᵒᵖ D E).obj P).comp (J.plusFunctor E)

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

Equations

J.plusFunctorWhiskerLeftIso P = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.Functor D E) => J.plusCompIso x P) ⋯

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 : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (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] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : CategoryTheory.Functor Cᵒᵖ E} (h : J.plusObj (Q.comp F) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (J.plusMap η) F) (CategoryTheory.CategoryStruct.comp (J.plusCompIso F Q).hom h) = CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom (CategoryTheory.CategoryStruct.comp (J.plusMap (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 : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (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] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (J.plusMap η) F) (J.plusCompIso F Q).hom = CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom (J.plusMap (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 : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (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 : CategoryTheory.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} [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 : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [∀ (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 : CategoryTheory.Functor Cᵒᵖ D) :

(J.plusFunctorWhiskerRightIso F).hom.app X = (J.plusCompIso F X).hom

source

(J.plusFunctor D).comp ((CategoryTheory.whiskeringRight Cᵒᵖ D E).obj F) ≅ ((CategoryTheory.whiskeringRight Cᵒᵖ D E).obj F).comp (J.plusFunctor E)

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

Equations

J.plusFunctorWhiskerRightIso F = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.Functor Cᵒᵖ D) => J.plusCompIso F x) ⋯

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 : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (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] {Z : CategoryTheory.Functor Cᵒᵖ E} (h : J.plusObj (P.comp F) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (J.toPlus P) F) (CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom h) = CategoryTheory.CategoryStruct.comp (J.toPlus (P.comp 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 : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (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] :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (J.toPlus P) F) (J.plusCompIso F P).hom = J.toPlus (P.comp F)

source

@[simp]

CategoryTheory.CategoryStruct.comp (J.toPlus (P.comp F)) (J.plusCompIso F P).inv = CategoryTheory.whiskerRight (J.toPlus P) F

source

(J.plusCompIso F P).inv = J.plusLift (CategoryTheory.whiskerRight (J.toPlus P) F) hP