isIndObject_limit_of_discrete_of_hasLimitsOfShape

English

If F is a functor from a discrete α to Cᵒᵖ ⥤ Type v and each F.obj a is an Ind-object, then the limit of F is an Ind-object (in the HasLimitsOfShape (Discrete α) setting).

Русский

Если F: Discrete α ⥤ Cᵒᵖ ⥤ Type v и для каждого a ∈ α F.obj a — Ind-объект, то предел F является Ind-объектом (при наличии пределов формы).

LaTeX

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

Lean4

theorem isIndObject_limit_of_discrete_of_hasLimitsOfShape [HasLimitsOfShape (Discrete α) C]
    (F : Discrete α ⥤ Cᵒᵖ ⥤ Type v) (hF : ∀ a, IsIndObject (F.obj a)) : IsIndObject (limit F) :=
  isIndObject_limit_of_discrete
    (fun g =>
      (isIndObject_limit_comp_yoneda (Discrete.functor g)).map
        (HasLimit.isoOfNatIso (Discrete.compNatIsoDiscrete g yoneda)).hom)
    F hF

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