Theorems · Definition · category theory

CategoryTheory.Limits.BinaryBicone.IsBilimit.ofIso

{C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q P' Q' : C} →
        {b : CategoryTheory.Limits.BinaryBicone P Q} →
          b.IsBilimit → (eP : P ≅ P') → (eQ : Q ≅ Q') → (b.ofIso eP eQ).IsBilimit

If a binary bicone for P and Q is bilimit, then the binary bicone for P' and Q' obtained using isomorphisms P ≅ P' and Q ≅ Q' is also bilimit.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms