colimitFlipCompColimIsoColimitCompColim_ι_ι_hom

English

There is a colimit isomorphism for the flipped vs original colimit diagram.

Русский

Существует изоморфизм колимита для перевернутой и исходной диаграммы колимита.

LaTeX

$$$\text{colimitFlipColimIsoColimitCompColim } F$$$

Lean4

@[simp, reassoc]
theorem colimitFlipCompColimIsoColimitCompColim_ι_ι_hom (j) (k) :
    colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k ≫ (colimitFlipCompColimIsoColimitCompColim F).hom =
      (colimit.ι _ k ≫ colimit.ι (F ⋙ colim) j : _ ⟶ colimit (F ⋙ colim)) :=
  by
  dsimp [colimitFlipCompColimIsoColimitCompColim]
  slice_lhs 1 3 => simp only []
  simp [Equivalence.unit]

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