lift_comp_conePointsIsoOfNatIso_inv

English

If F ≅ G and P, Q are IsLimit structures on t and s respectively, then Q.lift r ≫ (conePointsIsoOfNatIso P Q w).inv = P.map r w.inv.

Русский

Если F ≅ G и P, Q — IsLimit на t и s, то Q.lift r ≫ (conePointsIsoOfNatIso P Q w).inv = P.map r w.inv.

LaTeX

$$$ Q.lift(r) \\circ (conePointsIsoOfNatIso\\, P\\, Q\\, w)^{-1} = P.map(r, w.inv) $$$

Lean4

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

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