colimitUncurryIsoColimitCompColim_ι_ι_inv

English

The cone built from a diagram of limit cones is a limit cone.

Русский

Конус, построенный из диаграммы предельных конусов, является пределом.

LaTeX

$$$\text{coneOfConeUncurryIsLimit } Q c$$$

Lean4

@[simp, reassoc]
theorem colimitUncurryIsoColimitCompColim_ι_ι_inv {j} {k} :
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j ≫ (colimitUncurryIsoColimitCompColim F).inv =
      colimit.ι (uncurry.obj F) (j, k) :=
  by
  dsimp [colimitUncurryIsoColimitCompColim, IsColimit.coconePointUniqueUpToIso, IsColimit.uniqueUpToIso]
  simp

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