preservesColimit_of_natIso — Mathlib

English

Preservation of colimits is stable under a natural isomorphism between functors: if F preserves colimits, then G does as well when F ≅ G.

Русский

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

LaTeX

$$$ (h : F \\cong G) \\; [PreservesColimit\\,K\\, F] \\Rightarrow PreservesColimit\\,K\\, G. $$$

Lean4

/-- Transfer preservation of a colimit along a natural isomorphism in the functor. -/
theorem preservesColimit_of_natIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [PreservesColimit K F] : PreservesColimit K G
    where preserves t := ⟨IsColimit.mapCoconeEquiv h (isColimitOfPreserves F t)⟩

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