toPresheaf_preservesLimit — Mathlib

English

There is a canonical instance showing that the functor toPresheaf R preserves limits of F.

Русский

Существует канонический инстанс, показывающий, что toPresheaf R сохраняет пределы F.

LaTeX

$$$\\text{toPresheaf_preservesLimit }$$$

Lean4

noncomputable instance toPresheaf_preservesLimit : PreservesLimit F (toPresheaf R) :=
  preservesLimit_of_preserves_limit_cone (isLimitLimitCone F)
    (Limits.evaluationJointlyReflectsLimits _
      (fun X => isLimitOfPreserves (evaluation R X ⋙ forget₂ _ AddCommGrpCat) (isLimitLimitCone F)))

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