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.
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
@[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)
@[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
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 : 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]
:
(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
@[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)
@[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)
@[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 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 η))
@[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 (J.Cover X)ᵒᵖ D]
[∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
{F 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]
{Z : CategoryTheory.Functor Cᵒᵖ E}
(h : J.plusObj (P.comp G) ⟶ Z)
:
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)
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
@[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
@[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
@[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 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))
@[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 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)
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 : 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]
:
(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
@[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
@[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
@[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)
@[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
@[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 : 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 (J.toPlus (P.comp F)) (J.plusCompIso F P).inv = CategoryTheory.whiskerRight (J.toPlus P) F
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 : 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]
(hP : CategoryTheory.Presheaf.IsSheaf J ((J.plusObj P).comp F))
:
(J.plusCompIso F P).inv = J.plusLift (CategoryTheory.whiskerRight (J.toPlus P) F) hP