instSmallStrictColimitsOfShapeOfSmallOfLocallySmall

English

If P is small and C and J are locally small and J is small, then P.strictColimitsOfShape J is small.

Русский

Если P-малое, а C и J локально малые, и J мал, тогда P.strictColimitsOfShape J мал.

LaTeX

$$$$ [P.Small] \land [LocallySmall(C)] \land [Small(J)] \land [LocallySmall(J)] \Rightarrow (P.strictColimitsOfShape(J)).Small. $$$$

Lean4

instance [ObjectProperty.Small.{w} P] [LocallySmall.{w} C] [Small.{w} J] [LocallySmall.{w} J] :
    ObjectProperty.Small.{w} (P.strictColimitsOfShape J) :=
  by
  refine
    small_of_surjective (f := fun (F : { F : J ⥤ P.FullSubcategory // HasColimit (F ⋙ P.ι) }) ↦
      (⟨_,
        letI := F.2;
        ⟨F.1 ⋙ P.ι, fun j ↦ (F.1.obj j).2⟩⟩))
      ?_
  rintro ⟨_, ⟨F, hF⟩⟩
  exact ⟨⟨P.lift F hF, by assumption⟩, rfl⟩

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