createsLimit — Mathlib

English

The functor forget R creates limits of shape D; i.e., the limit in the base category lifts to the sheaf level.

Русский

Функтор забывания R создает пределы формы D; то есть предел в базовой категории поднимается до слоя шейфа.

LaTeX

$$$\text{CreatesLimit } F (\mathrm{forget}\, R)$$$

Lean4

noncomputable instance createsLimit : CreatesLimit F (forget _) :=
  createsLimitOfFullyFaithfulOfIso' (limit.isLimit (F ⋙ forget _))
    (mk (limit (F ⋙ forget _))
      (PresheafOfModules.isSheaf_of_isLimit (limit.isLimit (F ⋙ forget _)) (fun j => (F.obj j).isSheaf)))
    (Iso.refl _)

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