filtered_colim_preservesFiniteLimits

English

The colimit functor preserves finite limits when K is filtered and J is finite, under appropriate forgetful and forgetful-preserves conditions.

Русский

Функтор колимита сохраняет конечные пределы, когда K фильтрован и J конечно, при надлежащих условиях забывания.

LaTeX

$$PreservesFiniteLimits colim$$

Lean4

noncomputable instance filtered_colim_preservesFiniteLimits : PreservesLimitsOfShape J (colim : (K ⥤ C) ⥤ _) :=
  haveI : PreservesLimitsOfShape J ((colim : (K ⥤ C) ⥤ _) ⋙ forget C) :=
    preservesLimitsOfShape_of_natIso (preservesColimitNatIso _).symm
  preservesLimitsOfShape_of_reflects_of_preserves _ (forget C)

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