pushout_inr_iso_of_left_iso — Mathlib

English

Let f: X → Y and g: X → Z be morphisms in a category, and assume f is an isomorphism. Then the pushout of (f, g) exists.

Русский

Пусть f: X → Y и g: X → Z — морфизмы в категории, и предположим, что f является изоморфизмом. Тогда существует пушаут пары (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

instance pushout_inr_iso_of_left_iso : IsIso (pushout.inr f g) :=
  by
  refine ⟨⟨pushout.desc (inv f ≫ g) (𝟙 _) (by simp), by simp, ?_⟩⟩
  ext
  · simp [← pushout.condition]
  · simp

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