algebra_epi_of_epi — Mathlib

English

If a coalgebra morphism f has an epi underlying map f.f, then f is an epi in Coalgebra(G).

Русский

Если морфизм коалгебр f имеет эпиморфную carrier-часть f.f, то f является эпиморфизмом в категории коалгебр.

LaTeX

$$$\\\\forall X,Y \\\\in G. Coalgebra, \\\\forall f: X \\\\to Y, [Epi f.f] \\\\Rightarrow Epi f.$$$

Lean4

/-- Given a coalgebra morphism whose carrier part is an epimorphism, we get an algebra epimorphism.
-/
theorem algebra_epi_of_epi {X Y : Coalgebra G} (f : X ⟶ Y) [h : Epi f.f] : Epi f :=
  (forget G).epi_of_epi_map h

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