Theorems · Theorem · category theory

CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map

∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} [inst_3 : G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A}
  (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D}
  {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y : C} (f : G.obj Y ⟶ X) {W : C} (g : W ⟶ Y)
  (i : S.Arrow) (h : G.obj W ⟶ i.Y),
  CategoryTheory.CategoryStruct.comp h i.f = CategoryTheory.CategoryStruct.comp (G.map g) f →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map g.op) =
      CategoryTheory.CategoryStruct.comp (s.ι i)
        (CategoryTheory.CategoryStruct.comp (R.map h.op) (α.app (Opposite.op W)))

Defined in

Mathlib.CategoryTheory.Sites.CoverLifting

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsCocontinuous