Theorems · Theorem · category theory

CategoryTheory.GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3}
  {E : Type u_4} [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  {FD : D → D → Type u_5} {CD : D → Type u_6} {FE : E → E → Type u_7} {CE : E → Type u_8}
  [inst_9 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_10 : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)]
  [instCCD : CategoryTheory.ConcreteCategory D FD] [instCCE : CategoryTheory.ConcreteCategory E FE]
  [inst_11 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_12 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)]
  [inst_13 :
    CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (CategoryTheory.forget D)]
  [inst_14 :
    CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (CategoryTheory.forget E)]
  [inst_15 : (CategoryTheory.forget D).ReflectsIsomorphisms] [inst_16 : (CategoryTheory.forget E).ReflectsIsomorphisms]
  (P : CategoryTheory.Functor Cᵒᵖ D),
  (CategoryTheory.sheafToPresheaf J E).map
      ((CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D)
            (CategoryTheory.plusPlusAdjunction J E)).app
        P) =
    (J.sheafifyCompIso F P).inv

Defined in

Mathlib.CategoryTheory.Sites.PreservesSheafification

Cited by

0 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasLimitsOfShapeCategoryTheory.Limits.HasLimitsOfShapeCategoryTheory.Limits.HasColimitsOfShapeCategoryTheory.Limits.HasColimitsOfShapeCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.Limits.PreservesLimitFunLikeFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.ConcreteCategoryCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.Limits.PreservesLimitsOfSizeCategoryTheory.Limits.PreservesLimitsOfSizeCategoryTheory.Functor.ReflectsIsomorphismsCategoryTheory.Functor.ReflectsIsomorphisms