preservesColimit_of_iso_diagram — Mathlib

English

If two diagrams K1 and K2 are isomorphic and F preserves colimits of K1, then F preserves colimits of K2.

Русский

Если диаграммы K1 и K2 изоморфны и F сохраняет колимиты диаграммы K1, то она сохраняет колимиты диаграммы K2.

LaTeX

$$$ (K_1 \\cong K_2) \\;[PreservesColimit(K_1, F)] \\Rightarrow PreservesColimit(K_2, F). $$$

Lean4

/-- Transfer preservation of colimits along a natural isomorphism in the shape. -/
theorem preservesColimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [PreservesColimit K₁ F] :
    PreservesColimit K₂ F where
  preserves {c}
    t :=
    ⟨by
      apply IsColimit.precomposeHomEquiv (Functor.isoWhiskerRight h F :) _ _
      have := (IsColimit.precomposeHomEquiv h c).symm t
      apply IsColimit.ofIsoColimit (isColimitOfPreserves F this)
      exact Cocones.ext (Iso.refl _)⟩

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