finiteLimitOfFiniteDiagram — Mathlib

English

Any functor K : J ⥤ Type* with finite objects and J finite has a finite limit; equivalently, the limit is a finite type.

Русский

Любой функтор K : J ⥤ Type* с конечными объектами и J конечным имеет конечный предел; предел эквивалентно конечному типу.

LaTeX

$$$\\text{K : J ⥤ Type}^* ,\\ \\forall j,\\ Finite(K.obj j) \\Rightarrow\\ Finite(\\mathrm{limit}\\;K)$$$

Lean4

/-- Any functor from a finite category to Types that only involves finite objects,
has a finite limit. -/
noncomputable instance finiteLimitOfFiniteDiagram {J : Type} [SmallCategory J] [FinCategory J] (K : J ⥤ Type*)
    [∀ j, Finite (K.obj j)] : Fintype (limit K) :=
  by
  have : Fintype (sections K) := Fintype.ofFinite (sections K)
  exact Fintype.ofEquiv (sections K) (Types.limitEquivSections K).symm

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