isIndObject_limit_of_discrete — Mathlib

English

If h : ∀ g, IsIndObject (∏ᶜ yoneda.obj ∘ g) and F is a discrete α-indexed diagram in Cᵒᵖ ⥤ Type v with each F.obj a Ind-object, then the limit of F is an Ind-object.

Русский

Пусть F : Discrete α ⥤ Cᵒᵖ ⥤ Type v имеет для каждого a Ind-объект F.obj a; тогда предел F является Ind-объектом.

LaTeX

$$$\IsIndObject (\lim F)$$$

Lean4

theorem isIndObject_limit_of_discrete (h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g))
    (F : Discrete α ⥤ Cᵒᵖ ⥤ Type v) (hF : ∀ a, IsIndObject (F.obj a)) : IsIndObject (limit F) :=
  IsIndObject.map (Pi.isoLimit _).hom (isIndObject_pi h _ (fun a => hF ⟨a⟩))

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