evaluation_preservesColimit — Mathlib

English

The inverse limit-Obj iso interacts with limit maps to yield a compatible equality for f: i ⟶ j.

Русский

Обратный предел-объект изоморфизма взаимодействует с пределами, давая совместимое равенство для f: i ⟶ j.

LaTeX

$$$(\mathrm{limitObjIsoLimitCompEvaluation}\, F\, i)^{-1} \circ (\mathrm{limit}.map f) = \mathrm{limMap}(\mathrm{whiskerLeft} (\mathrm ev)) \circ (\mathrm{limitObjIsoLimitCompEvaluation}\, F\, j)^{-1}$$$

Lean4

instance evaluation_preservesColimit (F : J ⥤ K ⥤ C) [∀ k, HasColimit (F.flip.obj k)] (k : K) :
    PreservesColimit F ((evaluation K C).obj k) :=
  -- Porting note: added a let because X was not inferred

  let X : (k : K) → ColimitCocone (F.flip.obj k) := fun k => getColimitCocone (F.flip.obj k)
  preservesColimit_of_preserves_colimit_cocone (combinedIsColimit _ X) <|
    IsColimit.ofIsoColimit (colimit.isColimit _) (evaluateCombinedCocones F X k).symm

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