Theorems · Theorem · category theory

CategoryTheory.Presieve.isSheafFor_sigmaDesc_iff

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} {ι : Type u_3} {X : ι → C}
  (f : (i : ι) → X i ⟶ S) [inst_1 : (CategoryTheory.Presieve.ofArrows X f).HasPairwisePullbacks]
  {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.IsUniversalColimit c →
    ∀
      [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)
          (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)]
      [∀ (i : ι), CategoryTheory.Limits.HasPullback (f i) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)]
      (F : CategoryTheory.Functor Cᵒᵖ (Type u_4))
      [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (X i)) F]
      [CategoryTheory.Limits.PreservesLimit
          (CategoryTheory.Discrete.functor fun ij => Opposite.op (CategoryTheory.Limits.pullback (f ij.1) (f ij.2))) F],
      CategoryTheory.Presieve.IsSheafFor F
          (CategoryTheory.Presieve.singleton (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)) ↔
        CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X f)

Let { fᵢ : Xᵢ ⟶ S } be a family of morphisms. If ∐ᵢ Xᵢ is a universal coproduct and the presheaf F preserves products, then F is a sheaf for the single object covering { ∐ᵢ Xᵢ ⟶ S } if and only if it is a sheaf for { fᵢ : Xᵢ ⟶ S }ᵢ.

Defined in

Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Presieve.HasPairwisePullbacksCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.PreservesLimitCategoryTheory.Limits.PreservesLimit