equivOfNatIsoOfIso — Mathlib

English

The coconePointsIsoOfNatIso relation gives a natural isomorphism, relating maps between cocones via their legs.

Русский

Связь coconePointsIsoOfNatIso задаёт натуральный изоморфизм, связывающий отображения между коконами через их каркасы.

LaTeX

$$$ (P \!\!\; Q \!\!\; w).hom \; ≫ Q. desc r = P.map r w.hom $$$

Lean4

/-- Constructing an equivalence `is_colimit c ≃ is_colimit d` from a natural isomorphism
between the underlying functors, and then an isomorphism between `c` transported along this and `d`.
-/
def equivOfNatIsoOfIso {F G : J ⥤ C} (α : F ≅ G) (c : Cocone F) (d : Cocone G)
    (w : (Cocones.precompose α.inv).obj c ≅ d) : IsColimit c ≃ IsColimit d :=
  (precomposeInvEquiv α _).symm.trans (equivIsoColimit w)

Похожие утверждения