finite_of_isColimit — Mathlib

English

If c is an IsColimit cocone for a functor K: J ⥤ Type*, with finite K(j), then c.pt is finite.

Русский

Если cocone c является IsColimit для K: J ⥤ Type*, и все K(j) конечны, то c.pt конечно.

LaTeX

$$$\\mathrm{Finite}(c.\\mathrm{pt})$$$

Lean4

/-- Any functor from a finite category to Types that only involves finite objects,
has a finite colimit. -/
theorem finite_of_isColimit {J : Type} [SmallCategory J] [FinCategory J] {K : J ⥤ Type*} [∀ j, Finite (K.obj j)]
    {c : Cocone K} (hc : IsColimit c) : Finite c.pt :=
  Finite.of_equiv _ ((Types.isColimit_iff_coconeTypesIsColimit c).1 ⟨hc⟩).equiv

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