preservesColimitsOfShape_of_natIso

English

Preserving colimits of shape J is preserved under a natural isomorphism F ≅ G: if F preserves colimits of shape J, so does G.

Русский

Сохранение колимитов по форме J сохраняется при натуральном изоморфизме F ≅ G: если F сохраняет колимиты по форме J, то и G сохраняет их.

LaTeX

$$$ (h : F \\cong G) \\ [PreservesColimitsOfShape J\\, F] \\Rightarrow PreservesColimitsOfShape J\\, G. $$$

Lean4

/-- Transfer preservation of colimits of shape along a natural isomorphism in the functor. -/
theorem preservesColimitsOfShape_of_natIso {F G : C ⥤ D} (h : F ≅ G) [PreservesColimitsOfShape J F] :
    PreservesColimitsOfShape J G where preservesColimit {K} := preservesColimit_of_natIso K h

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