comp_preservesColimit — Mathlib

English

IsColimitExtendCoconeEquiv t is an equivalence between colimits for whiskers.

Русский

IsColimitExtendCoconeEquiv t задаёт эквивалентность для колимитов при закачках.

LaTeX

$$$$ \text{IsColimitExtendCoconeEquiv}(t) : \text{IsColimit}(\operatorname{extendCocone.obj} t) \simeq \text{IsColimit}(t). $$$$

Lean4

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

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