hasColimit_of_closedUnderColimits

English

If a property P is closed under isomorphisms and F : J ⥤ P.FullSubcategory has a colimit in P, then F has a colimit in P

Русский

Если свойство P замкнуто по изоморфизмам, и F : J ⥤ P.FullSubcategory имеет колимит в P, то F имеет колимит в P

LaTeX

$$$\\text{HasColimit } F\\text{ for } F : J \\to P^{\\text{FullSubcategory}}$ given [HasColimit (F \\circ P.ι)]$$

Lean4

theorem hasColimit_of_closedUnderColimits (h : ClosedUnderColimitsOfShape J P) (F : J ⥤ P.FullSubcategory)
    [HasColimit (F ⋙ P.ι)] : HasColimit F :=
  have : CreatesColimit F P.ι := createsColimitFullSubcategoryInclusionOfClosed h F
  hasColimit_of_created F P.ι

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