hasLimit_of_closedUnderLimitsOfShape

English

If D : J ⥤ P.Comma L R is closed under limits of shape J, and the forgetful functor creates the limit for D, then D has a limit.

Русский

Если D: J → P.Comma L R замкнут по пределам формы J, и функция забывания создаёт предел для D, то D имеет предел.

LaTeX

$$$$ \\operatorname{ClosedUnderLimitsOfShape}\\bigl(J,\\, P.\\mathrm{commaObj}(L,R)\\bigr) \\Rightarrow \\bigl[\\operatorname{HasLimit}(D \\circ \\mathrm{forget}_{L,R,\\top,\\top})\\bigr] \\Rightarrow \\operatorname{HasLimit} D $$$$

Lean4

theorem hasLimit_of_closedUnderLimitsOfShape (h : ClosedUnderLimitsOfShape J (P.commaObj L R))
    [HasLimit (D ⋙ forget L R P ⊤ ⊤)] : HasLimit D :=
  haveI : CreatesLimit D (forget L R P ⊤ ⊤) := forgetCreatesLimitOfClosed _ D h
  hasLimit_of_created D (forget L R P ⊤ ⊤)

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