lift_isoOfNatIso_hom — Mathlib

English

The lift along a cone t and the nat-iso w satisfy: limit.lift F t ≫ (HasLimit.isoOfNatIso w).hom = limit.lift G ((Cones.postcompose w.hom).obj _) .

Русский

Лифтинг по конусу t и нат-изоморфизм w удовлетворяют: limit.lift F t ≫ (HasLimit.isoOfNatIso w).hom = limit.lift G ((Cones.postcompose w.hom).obj _).

LaTeX

$$$\\operatorname{limit.lift} F t \\gg (\\operatorname{HasLimit.isoOfNatIso} w).hom = \\operatorname{limit.lift} G ((\\operatorname{Cones.postcompose} w.hom).obj _) $$$

Lean4

@[reassoc (attr := simp)]
theorem lift_isoOfNatIso_hom {F G : J ⥤ C} [HasLimit F] [HasLimit G] (t : Cone F) (w : F ≅ G) :
    limit.lift F t ≫ (HasLimit.isoOfNatIso w).hom = limit.lift G ((Cones.postcompose w.hom).obj _) :=
  IsLimit.lift_comp_conePointsIsoOfNatIso_hom _ _ _

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