Theorems · Definition · category theory

CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit

{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} →
            {F : CategoryTheory.PreOneHypercover S} →
              E.Hom F →
                (P : CategoryTheory.Functor Cᵒᵖ A) →
                  {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} →
                    CategoryTheory.Limits.IsLimit c →
                      (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)) → d.pt ⟶ c.pt

A refinement morphism E ⟶ F induces a morphism on associated multiequalizers.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.One

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category