finiteColimitOfFiniteDiagram — Mathlib

English

Any diagram K:J ⥤ Type* with finite objects has a finite colimit.

Русский

Любой диаграммы K:J ⥤ Type* с конечными объектами имеет конечный колимит.

LaTeX

$$$\\mathrm{Finite}(\\mathrm{colimit}\\ K)$$$

Lean4

/-- Any functor from a finite category to Types that only involves finite objects,
has a finite colimit. -/
noncomputable instance finiteColimitOfFiniteDiagram {J : Type} [SmallCategory J] [FinCategory J] (K : J ⥤ Type*)
    [∀ j, Finite (K.obj j)] : Fintype (colimit K) :=
  by
  have : Finite (colimit K) := finite_of_isColimit (colimit.isColimit K)
  apply Fintype.ofFinite

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