preservesColimit_of_comp — Mathlib

English

When F is final, if HasColimitsOfShape C E holds, then HasColimitsOfShape D E also holds.

Русский

Если F финален, и HasColimitsOfShape C E выполняется, то HasColimitsOfShape D E также выполняется.

LaTeX

$$$$ [\operatorname{HasColimitsOfShape} C E] \Rightarrow \operatorname{HasColimitsOfShape} D E. $$$$

Lean4

theorem preservesColimit_of_comp {B : Type u₄} [Category.{v₄} B] {H : E ⥤ B} [PreservesColimit (F ⋙ G) H] :
    PreservesColimit G H where
  preserves {c}
    hc := by
    refine ⟨isColimitWhiskerEquiv F _ ?_⟩
    let hc' := isColimitOfPreserves H ((isColimitWhiskerEquiv F _).symm hc)
    exact IsColimit.ofIsoColimit hc' (Cocones.ext (Iso.refl _) (by simp))

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