preservesColimit_of_isIso_post — Mathlib

English

If the post-colimit comparison morphism colimit.post F G is an isomorphism, then G preserves colimits of F; i.e., PreservesColimit F G.

Русский

Если сравнение пост-колимита colimit.post F G является изоморфизмом, то G сохраняет колимиты F; то есть PreservesColimit F G.

LaTeX

$$$[IsIso\\big(\\operatorname{colimit.post} F G\\big)] \\Rightarrow \\operatorname{PreservesColimit} F G$$$

Lean4

/-- If the comparison morphism `colimit (F ⋙ G) ⟶ G.obj (colimit F)` is an isomorphism, then `G`
preserves colimits of `F`. -/
theorem preservesColimit_of_isIso_post [IsIso (colimit.post F G)] : PreservesColimit F G :=
  preservesColimit_of_preserves_colimit_cocone (colimit.isColimit F)
    (by
      convert IsColimit.ofPointIso (colimit.isColimit (F ⋙ G))
      assumption)

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