reflectsColimit_of_comp — Mathlib

English

If F is final and PreservesColimit G H, then PreservesColimit (F ⋙ G) H.

Русский

Если F финален и PreservesColimit G H, тогда PreservesColimit (F ⋙ G) H.

LaTeX

$$$$ \text{PreservesColimit}(F \circ G, H). $$$$

Lean4

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

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