Theorems · Theorem · category theory

CategoryTheory.RanIsSheafOfIsCocontinuous.hom_ext

∀ {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) [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A},
  CategoryTheory.Presheaf.IsSheaf J F →
    ∀ {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F}
      (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} {W : A}
      {f g : W ⟶ R.obj (Opposite.op X)},
      (∀ (i : S.Arrow),
          CategoryTheory.CategoryStruct.comp f (R.map i.f.op) = CategoryTheory.CategoryStruct.comp g (R.map i.f.op)) →
        f = g

Defined in

Mathlib.CategoryTheory.Sites.CoverLifting

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsCocontinuous