isoOfNatIso_inv_π — Mathlib

English

The inverse component of the nat-iso between F and G interacts with projections by: (HasLimit.isoOfNatIso w).inv ≫ limit.π F j = limit.π G j ≫ w.inv.app j.

Русский

Обратная компонента нат-изоморфизма между F и G взаимодействует с проекциями так: (HasLimit.isoOfNatIso w).inv ≫ limit.π F j = limit.π G j ≫ w.inv.app j.

LaTeX

$$$(HasLimit.isoOfNatIso w).inv \\gg \\operatorname{limit.}\\pi F j = \\operatorname{limit.}\\pi G j \\gg w.inv.app j$$$

Lean4

@[reassoc (attr := simp)]
theorem isoOfNatIso_inv_π {F G : J ⥤ C} [HasLimit F] [HasLimit G] (w : F ≅ G) (j : J) :
    (HasLimit.isoOfNatIso w).inv ≫ limit.π F j = limit.π G j ≫ w.inv.app j :=
  IsLimit.conePointsIsoOfNatIso_inv_comp _ _ _ _

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