Theorems · Theorem · category theory

CategoryTheory.RanIsSheafOfIsCocontinuous.lift.congr_simp

∀ {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 J_1 : CategoryTheory.GrothendieckTopology C} (e_J : J = J_1)
  {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}
  (hR hR_1 : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension),
  hR = hR_1 →
    ∀ {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)),
      CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s = CategoryTheory.RanIsSheafOfIsCocontinuous.lift ⋯ hR_1 s

Defined in

Mathlib.CategoryTheory.Sites.CoverLifting

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsCocontinuous