Theorems · Theorem · category theory

CategoryTheory.GrothendieckTopology.preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {ι : Type u_1} [CategoryTheory.Limits.CoproductsOfShapeDisjoint C ι]
  [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasStrictInitialObjects C],
  (∀ {X : ι → C} {c : CategoryTheory.Limits.Cofan X} (x : CategoryTheory.Limits.IsColimit c),
      CategoryTheory.Sieve.ofArrows X c.inj ∈ J c.pt) →
    (∀ (Y : C) (a : CategoryTheory.Limits.IsInitial Y), ⊥ ∈ J Y) →
      CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) J.yoneda

If the coproduct inclusions form a covering of J and coproducts are disjoint, the yoneda embedding to J-sheaves preserves coproducts.

Defined in

Mathlib.CategoryTheory.Sites.Subcanonical

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GrothendieckTopology.SubcanonicalCategoryTheory.Limits.CoproductsOfShapeDisjointCategoryTheory.Limits.HasPullbacksCategoryTheory.Limits.HasStrictInitialObjects