forget_commGrp_preserves_mono — Mathlib

English

In CommGrpCat, the forgetful functor to Sets preserves monomorphisms; equivalently, a morphism is mono iff its underlying function is injective.

Русский

В CommGrpCat забывающий функтор сохраняет мономорфизмы; эквивалентно тому, что морфизм является mono тогда и только тогда, когда соответствующая функция инъективна.

LaTeX

$$$\forall f: A \to B,\ f\ \text{mono} \iff f:|A|\to|B|\ \text{injective}$$$

Lean4

@[to_additive AddCommGrpCat.forget_commGrp_preserves_mono]
instance forget_commGrp_preserves_mono : (forget CommGrpCat).PreservesMonomorphisms where
  preserves f e := by rwa [mono_iff_injective, ← CategoryTheory.mono_iff_injective] at e

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