algebra_mono_of_mono — Mathlib

English

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

Русский

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

LaTeX

$$$\\\\forall X,Y \\\\in G. Coalgebra, \\\\forall f: X \\\\to Y, \\\\operatorname{Mono}(f.f) \\\\Rightarrow \\\\operatorname{Mono}(f).$$$

Lean4

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

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