instRespectsIsoPushouts — Mathlib

English

Pushouts preserve isomorphisms: the pushouts construction is compatible with isomorphisms of the involved arrows.

Русский

Пушоуты сохраняют изоморфизмы: конструкция пушоута совместима с изоморфизмами участвующих стрелок.

LaTeX

$$P.pushouts.RespectsIso$$

Lean4

instance : P.pushouts.RespectsIso :=
  RespectsIso.of_respects_arrow_iso _
    (by
      rintro q q' e ⟨A, B, p, f, g, hp, h⟩
      exact
        ⟨A, B, p, f ≫ e.hom.left, g ≫ e.hom.right, hp, IsPushout.paste_horiz h (IsPushout.of_horiz_isIso ⟨e.hom.w⟩)⟩)

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