isoOfNatIso_inv_desc — Mathlib

English

Dually, the inverse component of the natural iso combined with a colimit descent equals the colimit descent along the precomposition by w.inv.

Русский

Аналогично, косвенная компонента обратного изоморфизма вместе с декомпозицией колимита равна колимитной декомуляции через precompose w.inv.

LaTeX

$$$ (\\operatorname{HasColimit.isoOfNatIso} w)^{\\mathrm{inv}} \\; \\circ \\operatorname{colimit.desc} F t = \\operatorname{colimit.desc} G \\Big( (\\operatorname{Cocones.precompose} w.\\mathrm{inv}).obj _ \\Big) $$$

Lean4

@[reassoc (attr := simp)]
theorem isoOfNatIso_inv_desc {F G : J ⥤ C} [HasColimit F] [HasColimit G] (t : Cocone F) (w : F ≅ G) :
    (HasColimit.isoOfNatIso w).inv ≫ colimit.desc F t = colimit.desc G ((Cocones.precompose w.inv).obj _) :=
  IsColimit.coconePointsIsoOfNatIso_inv_desc _ _ _

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