isLimitLimitCone — Mathlib

English

The limit cone for a presheaf of modules F is a limit in the category of presheaves; in particular, the cone constructed is universal.

Русский

У предельный конус для F является пределом в категории прешефов; в частности, конус универсален.

LaTeX

$$$\\text{isLimitLimitCone } F$$$

Lean4

/-- The cone `limitCone F` is limit for any `F : J ⥤ PresheafOfModules.{v} R`. -/
noncomputable def isLimitLimitCone : IsLimit (limitCone F) :=
  evaluationJointlyReflectsLimits _ _ (fun _ => limit.isLimit _)

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