colimitObjIsoColimitCompEvaluation_ι_inv

English

For F: J ⥤ K ⥤ C and j ∈ J, k ∈ K, the inverse of the colimit object iso composed with the colimit injection satisfies a simple relation.

Русский

Для F: J ⥤ K ⥤ C и j ∈ J, k ∈ K, обратный изоморфизм colimitObjIsoColimitCompEvaluation удовлетворяет простой зависимости.

LaTeX

$$$(\mathrm{colimitObjIsoColimitCompEvaluation}\, F\, k)^{-1} \circ (\mathrm{colimit}.ι(F)\!_j) = (\mathrm{colimit}.ι(F)\!_j).app\,k$$$

Lean4

@[reassoc (attr := simp)]
theorem colimitObjIsoColimitCompEvaluation_ι_inv [HasColimitsOfShape J C] (F : J ⥤ K ⥤ C) (j : J) (k : K) :
    colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation F k).inv = (colimit.ι F j).app k :=
  by
  dsimp [colimitObjIsoColimitCompEvaluation]
  simp

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