Theorems · Theorem · category theory

CategoryTheory.Presieve.preservesProduct_of_isSheafFor

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a) →
    ∀ (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C}
      (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c)
      [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [inst_3 : CategoryTheory.Limits.HasInitial C]
      [∀ (i : α), CategoryTheory.Mono (c.inj i)],
      (Pairwise fun i j =>
          CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j))
            (c.inj i) (c.inj j)) →
        CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj) →
          CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F

If F is a presheaf which IsSheafFor a presieve of arrows and the empty presieve, then it preserves the product corresponding to the presieve of arrows.

Defined in

Mathlib.CategoryTheory.Sites.Preserves

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategorySmallCategoryTheory.Presieve.HasPairwisePullbacksCategoryTheory.Limits.HasInitialCategoryTheory.Mono