mono_iff_injective — Mathlib

English

For any X,Y and f: X → Y, Mono f is equivalent to Injective ((forget₂ C Ab).map f).

Русский

Моно morphism f эквивалентен инъективности отображения forget₂ C Ab от f.

LaTeX

$$$$ \\operatorname{Mono}(f) \\iff \\operatorname{Injective}\\left( (\\mathrm{forget}_{2} C Ab).map f \\right). $$$$

Lean4

theorem mono_iff_injective {X Y : C} (f : X ⟶ Y) : Mono f ↔ Function.Injective ((forget₂ C Ab).map f) :=
  by
  rw [← AddCommGrpCat.mono_iff_injective]
  constructor
  · intro
    infer_instance
  · apply Functor.mono_of_mono_map

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