of_horiz_isIso — Mathlib

English

Let f : Z → X and g : Z → Y be morphisms with inl : X → P and inr : Y → P such that the square commutes and f is an isomorphism and inr is an isomorphism. Then the square is a pushout: IsPushout f g inl inr.

Русский

Пусть f: Z → X и g: Z → Y — морфизмы, а inl: X → P и inr: Y → P — такие, что диаграмма коммутирует и f, а также inr — изоморфизмы. Тогда диаграмма является пуш-аутом: IsPushout f g inl inr.

LaTeX

$$$ (\\text{CommSq}(f,g,inl,inr)) \\land \\operatorname{IsIso}(f) \\land \\operatorname{IsIso}(inr) \\Rightarrow \\operatorname{IsPushout}(f,g,inl,inr) $$$

Lean4

theorem of_horiz_isIso [IsIso f] [IsIso inr] (sq : CommSq f g inl inr) : IsPushout f g inl inr :=
  of_horiz_isIso_epi sq

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