epi_of_epi_app — Mathlib

English

If every component α.app X is an epimorphism, then α : F ⟶ G is an epimorphism.

Русский

Если каждый компонент α.app X является эпиморфизмом, то α : F ⟶ G эпиморфно.

LaTeX

$$$ (\forall X, \operatorname{Epi}(\alpha.app X)) \Rightarrow \operatorname{Epi}(\alpha). $$$

Lean4

/-- A natural transformation is an epimorphism if each component is. -/
theorem epi_of_epi_app (α : F ⟶ G) [∀ X : C, Epi (α.app X)] : Epi α :=
  ⟨fun g h eq => by
    ext X
    rw [← cancel_epi (α.app X), ← comp_app, eq, comp_app]⟩

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