lift_isoOfNatIso_inv — Mathlib

English

Similarly, the inverse component yields: limit.lift G t ≫ (HasLimit.isoOfNatIso w).inv = limit.lift F ((Cones.postcompose w.inv).obj _).

Русский

Аналогично, обратная компонента даёт: limit.lift G t ≫ (HasLimit.isoOfNatIso w).inv = limit.lift F ((Cones.postcompose w.inv).obj _).

LaTeX

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

Lean4

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

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