isoOfNatIso_ι_inv — Mathlib

English

Under the same hypotheses as above, for each j ∈ J the inverse of the nat-iso transports the injection from G: colimit.ι G j ≫ (HasColimit.isoOfNatIso w).inv equals w.inv.app j ≫ colimit.ι F j.

Русский

При тех же предположениях для каждого j ∈ J выполняется: colimit.ι G j затем (HasColimit.isoOfNatIso w).inv равно w.inv.app j затем colimit.ι F j.

LaTeX

$$$ \\operatorname{colimit.ι} G j \\circ (\\operatorname{HasColimit.isoOfNatIso} w)^{\\mathrm{inv}} = w^{\\mathrm{inv}}_{j} \\circ \\operatorname{colimit.ι} F j $$$

Lean4

@[reassoc (attr := simp)]
theorem isoOfNatIso_ι_inv {F G : J ⥤ C} [HasColimit F] [HasColimit G] (w : F ≅ G) (j : J) :
    colimit.ι G j ≫ (HasColimit.isoOfNatIso w).inv = w.inv.app j ≫ colimit.ι F j :=
  IsColimit.comp_coconePointsIsoOfNatIso_inv _ _ _ _

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