of_iso_comparison — Mathlib

English

Isomorphisms for pushout projections show that the mapping preserves the pushout structure.

Русский

Изоморфизмы проекции пуш-аута показывают сохранение структуры пуш-аута под отображением.

LaTeX

$$$PreservesPushout.iso\\ G f g$$$

Lean4

/-- If the pushout comparison map for `G` at `(f,g)` is an isomorphism, then `G` preserves the
pushout of `(f,g)`. -/
theorem of_iso_comparison [i : IsIso (pushoutComparison G f g)] : PreservesColimit (span f g) G :=
  by
  apply preservesColimit_of_preserves_colimit_cocone (pushoutIsPushout f g)
  apply (isColimitMapCoconePushoutCoconeEquiv _ _).symm _
  exact IsColimit.ofPointIso _ (i := i)

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