Theorems · Definition · category theory

CategoryTheory.PreOneHypercover.isLimitSigmaOfIsColimitEquiv

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
        {S : C} →
          (E : CategoryTheory.PreOneHypercover S) →
            {c : CategoryTheory.Limits.Cofan E.X} →
              (hc : CategoryTheory.Limits.IsColimit c) →
                {d : CategoryTheory.Limits.Cofan E.Y'} →
                  (hd : CategoryTheory.Limits.IsColimit d) →
                    (F : CategoryTheory.Functor Cᵒᵖ A) →
                      [CategoryTheory.Limits.PreservesLimit
                            (CategoryTheory.Discrete.functor fun i => Opposite.op (E.X i)) F] →
                        [CategoryTheory.Limits.PreservesLimit
                              (CategoryTheory.Discrete.functor fun i => Opposite.op (E.Y' i)) F] →
                          CategoryTheory.Limits.IsLimit ((E.sigmaOfIsColimit hc hd).multifork F) ≃
                            CategoryTheory.Limits.IsLimit (E.multifork F)

If E is a pre-1-hypercover and F a presheaf, the induced equalizer of the single object covering obtained from E by taking coproducts is limiting if and only if the induced multiequalizer of E is limiting.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.One

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.PreservesLimitCategoryTheory.Limits.PreservesLimit