Theorems · Definition · category theory

CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence

{J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {s : CategoryTheory.Limits.Cone F} →
                {G : CategoryTheory.Functor K C} →
                  {t : CategoryTheory.Limits.Cone G} →
                    CategoryTheory.Limits.IsLimit s →
                      CategoryTheory.Limits.IsLimit t → (e : J ≌ K) → (e.functor.comp G ≅ F) → (s.pt ≅ t.pt)

We can prove two cone points (s : Cone F).pt and (t : Cone G).pt are isomorphic if * both cones are limit cones * their indexing categories are equivalent via some e : J ≌ K, * the triangle of functors commutes up to a natural isomorphism: e.functor ⋙ G ≅ F. This is the most general form of uniqueness of cone points, allowing relabelling of both the indexing category (up to equivalence) and the functor (up to natural isomorphism).

Defined in

Mathlib.CategoryTheory.Limits.IsLimit

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category