of_iso_comparison — Mathlib

English

If sigmaComparison G f is an isomorphism, then Discrete.functor f along with G preserves the colimit of the diagram f.

Русский

Если sigmaComparison G f является изоморфизмом, то дискремный функтор по f совместно с G сохраняют колимит диаграммы f.

LaTeX

$$$\\text{IsIso}(\\sigma_{G,f}) \\Rightarrow \\text{PreservesColimit}(\\mathrm{Discrete.functor} f, G)$$$

Lean4

/-- If `sigma_comparison G f` is an isomorphism, then `G` preserves the colimit of `f`. -/
theorem of_iso_comparison [i : IsIso (sigmaComparison G f)] : PreservesColimit (Discrete.functor f) G :=
  by
  apply preservesColimit_of_preserves_colimit_cocone (coproductIsCoproduct f)
  apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _
  exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (Discrete.functor fun j : J => G.obj (f j))) i

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