Theorems · Definition · category theory

CategoryTheory.Limits.Cocone.extInv

{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), c.ι.app j = CategoryTheory.CategoryStruct.comp (c'.ι.app j) φ.inv)
                  CategoryTheory.Limits.Cocone.extInv._auto_1 →
                (c ≅ c')

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

Defined in

Mathlib.CategoryTheory.Limits.Cones

Cited by

11 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category