hasPushout_of_right_iso — Mathlib

English

Let f: X → Y and g: X → Z with g an isomorphism. Then a pushout of (f,g) exists.

Русский

Пусть f: X → Y и g: X → Z, причём g является изоморфизмом. Тогда существует пушаут пары (f,g).

LaTeX

$$$\exists P, i_Y: Y \to P, i_Z: Z \to P,\; i_Y \circ f = i_Z \circ g \;\land\; \forall Q, a_Y: Y \to Q, a_Z: Z \to Q\; (a_Y \circ f = a_Z \circ g) \Rightarrow \exists! u: P \to Q,\; u \circ i_Y = a_Y \land u \circ i_Z = a_Z.$$$

Lean4

theorem hasPushout_of_right_iso : HasPushout f g :=
  ⟨⟨⟨_, pushoutCoconeOfRightIsoIsLimit f g⟩⟩⟩

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