English
Let hc be IsColimit c. Then Epi f holds if and only if c.inl is an isomorphism.
Русский
Пусть hc — IsColimit c. Тогда выполняется эквивалентность: f — эпиморфизм тогда и только если c.inl — изоморфизм.
LaTeX
$$$ IsColimit\, c \rightarrow (Epi\, f \iff IsIso\, c.inl) $$$
Lean4
theorem epi_iff_isIso_inl (hc : IsColimit c) : Epi f ↔ IsIso c.inl :=
by
rw [epi_iff_inl_eq_inr hc]
constructor
· intro h
obtain ⟨φ, hφ₁, hφ₂⟩ := PushoutCocone.IsColimit.desc' hc (𝟙 Y) (𝟙 Y) (by simp)
refine ⟨φ, hφ₁, PushoutCocone.IsColimit.hom_ext hc ?_ ?_⟩
· simp only [comp_id, reassoc_of% hφ₁]
· simp only [comp_id, h, reassoc_of% hφ₂]
· intro
obtain ⟨φ, hφ₁, hφ₂⟩ := PushoutCocone.IsColimit.desc' hc (𝟙 Y) (𝟙 Y) (by simp)
have : IsSplitMono φ := IsSplitMono.mk ⟨SplitMono.mk c.inl (by rw [← cancel_epi c.inl, reassoc_of% hφ₁, comp_id])⟩
rw [← cancel_mono φ, hφ₁, hφ₂]
