colimitObjIsoColimitCompEvaluation_ι_app_hom

English

The app component of the colimit-OBJ iso composed with the colimit injection equals the app of the evaluated colimit.

Русский

Компонента app изоморфизма colimitObjIsoColimitCompEvaluation для колимит-объекта совпадает с приложением к оценённому колимиту.

LaTeX

$$$(\mathrm{colimitObjIsoColimitCompEvaluation}\, F\, k).\mathrm{app}\,j \circ (\mathrm{colimit}.ι F j) = (\mathrm{colimit}.ι(F \circ (\mathrm evaluation \! k))\, j)$$$

Lean4

@[reassoc (attr := simp)]
theorem colimitObjIsoColimitCompEvaluation_ι_app_hom [HasColimitsOfShape J C] (F : J ⥤ K ⥤ C) (j : J) (k : K) :
    (colimit.ι F j).app k ≫ (colimitObjIsoColimitCompEvaluation F k).hom = colimit.ι (F ⋙ (evaluation K C).obj k) j :=
  by
  dsimp [colimitObjIsoColimitCompEvaluation]
  rw [← Iso.eq_comp_inv]
  simp

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