English
Suppose c is a pushout cocone of f: S → X1 and g: S → X2, hc is IsColimit for c, and f is injective. Then for any x1 ∈ X1 and x2 ∈ X2, c.inl x1 = c.inr x2 precisely when there exists s ∈ S with f s = x1 and g s = x2.
Русский
Пусть c — пушаут-кокон для f: S → X1 и g: S → X2, hc — IsColimit c, и f инъективна. Тогда для любых x1 ∈ X1 и x2 ∈ X2 равенство c.inl x1 = c.inr x2 эквивалентно существованию s ∈ S такого, что f s = x1 и g s = x2.
LaTeX
$$$hc: IsColimit\\ c\\;\\wedge\\; h_1:\\ Function.Injective f\\;\\Rightarrow\\;\\forall x_1:X_1\\, x_2:X_2,\\; c.inl x_1 = c.inr x_2\\iff \\exists s:S, f s = x_1 \\wedge g s = x_2$$$
Lean4
theorem pushoutCocone_inl_eq_inr_iff_of_isColimit {c : PushoutCocone f g} (hc : IsColimit c) (h₁ : Function.Injective f)
(x₁ : X₁) (x₂ : X₂) : c.inl x₁ = c.inr x₂ ↔ ∃ (s : S), f s = x₁ ∧ g s = x₂ :=
by
rw [pushoutCocone_inl_eq_inr_iff_of_iso
(Cocones.ext (IsColimit.coconePointUniqueUpToIso hc (Pushout.isColimitCocone f g)) (by simp))]
have := (mono_iff_injective f).2 h₁
apply Pushout.inl_eq_inr_iff
