Theorems · Definition · category theory

CategoryTheory.Limits.Cotrident.IsColimit.homIso

{J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            {t : CategoryTheory.Limits.Cotrident f} →
              CategoryTheory.Limits.IsColimit t →
                (Z : C) →
                  (t.pt ⟶ Z) ≃
                    { h //
                      ∀ (j₁ j₂ : J),
                        CategoryTheory.CategoryStruct.comp (f j₁) h = CategoryTheory.CategoryStruct.comp (f j₂) h }

Given a colimit cocone for the family f : J → (X ⟶ Y), for any Z, morphisms from the cocone point to Z are in bijection with morphisms h : Z ⟶ X such that ∀ j₁ j₂, f j₁ ≫ h = f j₂ ≫ h. Further, this bijection is natural in Z: see Cotrident.IsColimit.homIso_natural.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryNonempty