Theorems · Definition · category theory

CategoryTheory.Limits.Cocone.ext

{J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {c c' : CategoryTheory.Limits.Cocone F} →
            (φ : c.pt ≅ c'.pt) →
              autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j)
                  CategoryTheory.Limits.Cocone.ext._auto_1 →
                (c ≅ c')

To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.

Defined in

Mathlib.CategoryTheory.Limits.Cones

Cited by

41 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category