Theorems · Theorem · category theory

CategoryTheory.isSheaf_pointwiseColimit

∀ {A : Type u_1} {C : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} J]
  [inst_3 : CategoryTheory.FinitaryExtensive C] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J A]
  [CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim]
  (G : CategoryTheory.Functor J (CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A)),
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C)
    (CategoryTheory.Limits.pointwiseCocone
        (G.comp (CategoryTheory.sheafToPresheaf (CategoryTheory.extensiveTopology C) A))).pt

Defined in

Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.FinitaryExtensiveCategoryTheory.Limits.HasColimitsOfShapeCategoryTheory.Limits.PreservesFiniteProducts