comp_reflectsColimit — Mathlib

English

If HasColimit (F ⋙ G), then HasColimit G.

Русский

Если у F ⋙ G имеется колимит, то у G имеется колимит.

LaTeX

$$$$ \text{HasColimit}(F \cdot G) \Rightarrow \text{HasColimit}(G). $$$$

Lean4

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

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