of_iso_comparison — Mathlib

English

If the initial comparison map is an isomorphism, then G preserves initial objects.

Русский

Если начальное сравнение изоморфно, то G сохраняет начальные объекты.

LaTeX

$$$\\text{IsIso}(\\text{initialComparison } G) \\Rightarrow \\text{PreservesColimit}(\\mathrm{empty}, G).$$$

Lean4

/-- If the initial comparison map for `G` is an isomorphism, then `G` preserves initial objects.
-/
theorem of_iso_comparison [i : IsIso (initialComparison G)] : PreservesColimit (Functor.empty.{0} C) G :=
  by
  apply preservesColimit_of_preserves_colimit_cocone initialIsInitial
  apply (isColimitMapCoconeEmptyCoconeEquiv _ _).symm _
  exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (Functor.empty.{0} D)) i

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