evaluation_preservesLimit — Mathlib

English

For a functor F: J ⥤ K ⥤ C, if for each k the functor F.flip.obj k preserves limits, then F preserves limits after composing with evaluation at k.

Русский

Для функторa F: J ⥤ K ⥤ C, если для каждого k функтор F.flip.obj k сохраняет пределы, то F сохраняет пределы после композиции с ev_k.

LaTeX

$$$\forall k,\ PreservesLimit(F, (\mathrm{ev}_k))$$$

Lean4

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

  let X : (k : K) → LimitCone (F.flip.obj k) := fun k => getLimitCone (F.flip.obj k)
  preservesLimit_of_preserves_limit_cone (combinedIsLimit _ X) <|
    IsLimit.ofIsoLimit (limit.isLimit _) (evaluateCombinedCones F X k).symm

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