Theorems · Theorem · category theory

CategoryTheory.Presieve.firstMap_eq_secondMap

∀ {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} [inst_1 : Small.{w, u_1} α] {X : α → C}
      (c : CategoryTheory.Limits.Cofan X) [inst_2 : (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.Equalizer.Presieve.Arrows.firstMap F X c.inj =
          CategoryTheory.Equalizer.Presieve.Arrows.secondMap F X c.inj

The two parallel maps in the equalizer diagram for the sheaf condition corresponding to the inclusion maps in a disjoint coproduct are equal.

Defined in

Mathlib.CategoryTheory.Sites.Preserves

Cited by

0 results in Mathlib

Foundations

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

Assumes

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