hasLimitCompEvaluation — Mathlib

English

For a functor F: J ⥤ K ⥤ C and an object k ∈ K, if HasLimit (F.flip.obj k), then HasLimit (F ⋙ evaluation at k).

Русский

Для функторa F: J ⥤ K ⥤ C и элемента k ∈ K, если существует предел у F.flip.obj k, то существует предел у F ⋙ ev_k.

LaTeX

$$$\forall k,\ HasLimit(F^{\mathrm{flip}}(k)) \Rightarrow HasLimit\big(F \circ (\mathrm{ev}_k)\big)$$$

Lean4

instance hasLimitCompEvaluation (F : J ⥤ K ⥤ C) (k : K) [HasLimit (F.flip.obj k)] :
    HasLimit (F ⋙ (evaluation _ _).obj k) :=
  hasLimit_of_iso (F := F.flip.obj k) (Iso.refl _)

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