lift_comp_conePointsIsoOfNatIso_hom

English

For limit cones s and t and a natural iso w, the lifted morphism respects the iso: Q.lift r ≫ (conePointsIsoOfNatIso P Q w).hom = Q.map r w.hom.

Русский

Для предельных конусов s и t и натурального изоморфизма w, подъём соблюдает изоморфизм: Q.lift r ≫ (conePointsIsoOfNatIso P Q w).hom = Q.map r w.hom.

LaTeX

$$$ Q.lift(r) \\circ (conePointsIsoOfNatIso\\, P\\, Q\\, w).hom = Q.map(r, w.hom) $$$

Lean4

@[reassoc]
theorem lift_comp_conePointsIsoOfNatIso_hom {F G : J ⥤ C} {r s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t)
    (w : F ≅ G) : P.lift r ≫ (conePointsIsoOfNatIso P Q w).hom = Q.map r w.hom :=
  Q.hom_ext (by simp)

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