epi_iff_inl_eq_inr — Mathlib

English

Let c be a PushoutCocone f f which is a colimit. Then f is epi if and only if c.inl = c.inr.

Русский

Пусть c — пушплот-коcone f f, являющийся колимитом. Тогда f эпиморфен тогда и только если c.inl = c.inr.

LaTeX

$$$ IsColimit\, c \rightarrow (Epi\, f \iff c.inl = c.inr) $$$

Lean4

theorem epi_iff_inl_eq_inr (hc : IsColimit c) : Epi f ↔ c.inl = c.inr :=
  by
  constructor
  · intro hf
    simpa only [← cancel_epi f] using c.condition
  · intro hf
    constructor
    intro Z g g' h
    obtain ⟨φ, rfl, rfl⟩ := PushoutCocone.IsColimit.desc' hc g g' h
    rw [hf]

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