mono_of_mono — Mathlib

English

An algebra morphism with underlying mono morphism in C is a mono in Coalgebra F.

Русский

Гомоморфизм алгебры с монообразной морфизмом в C является моно в категории Coalgebra F.

LaTeX

$$$\forall X,Y \in \mathrm{CoAlg}(F),\ f: X \to Y,\ [\text{mono}(f_1)] \Rightarrow \text{mono}(f)$$$

Lean4

/-- An algebra morphism with an underlying monomorphism hom in `C` is an algebra monomorphism. -/
theorem mono_of_mono {X Y : Coalgebra F} (f : X ⟶ Y) [h : Mono f.1] : Mono f :=
  (forget F).mono_of_mono_map h

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