hasColimit_of_closedUnderColimitsOfShape

English

If D : J ⥤ P.Comma L R ⊤ ⊤ is closed under shape J colimits, and HasColimit of D followed by forget, then HasColimit D.

Русский

Если D: J ⥤ P.Comma L R ⊤ ⊤ замкнута по колимитам формы J, и у D существует колимит после забывающей функции, то у D существует колимит.

LaTeX

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

Lean4

theorem hasColimit_of_closedUnderColimitsOfShape (h : ClosedUnderColimitsOfShape J (P.commaObj L R))
    [HasColimit (D ⋙ forget L R P ⊤ ⊤)] : HasColimit D :=
  haveI : CreatesColimit D (forget L R P ⊤ ⊤) := forgetCreatesColimitOfClosed _ D h
  hasColimit_of_created D (forget L R P ⊤ ⊤)

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