English
The limit cone defined for F: J ⥤ PresheafOfModules R is indeed a limit cone, establishing the existence of the limit for F in the presheaf category.
Русский
Определённый предел-конус для F: J ⥤ PresheafOfModules R действительно является пределом, обеспечивая существование предела для F в пресешафной категории.
LaTeX
$$IsLimit (limitCone F)$$
Lean4
/-- The (limit) cone for `F : J ⥤ PresheafOfModules.{v} R` that is constructed from the limit
of `F ⋙ evaluation R X` for all `X`. -/
@[simps]
noncomputable def limitCone : Cone F where
pt := limitPresheafOfModules F
π :=
{ app := fun j ↦
{ app := fun X ↦ limit.π (F ⋙ evaluation R X) j
naturality := fun {X Y} f ↦ by
dsimp
simp only [assoc, preservesLimitIso_inv_π]
apply limMap_π }
naturality := fun {j j'} f ↦ by
ext1 X
simpa using (limit.w (F ⋙ evaluation R X) f).symm }
