epi_of_epi — Mathlib

English

The forgetful functor forget F reflects isomorphisms.

Русский

Забывающий функтор forget F отражает изоморфизмы.

LaTeX

$$$\\operatorname{forget} F \\;:\\; \\mathbf{Endofunctor.Algebra} F \\to \\mathbf{C}$ ReflectsIsomorphisms$$

Lean4

/-- An algebra morphism with an underlying epimorphism hom in `C` is an algebra epimorphism. -/
theorem epi_of_epi {X Y : Algebra F} (f : X ⟶ Y) [h : Epi f.1] : Epi f :=
  (forget F).epi_of_epi_map h

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