mono_iff_injective' — Mathlib

English

Mono f is equivalent to Injective f in the forgetful setting.

Русский

Моно f эквивалентен инъективности f в forgetful настройке.

LaTeX

$$$$ \\operatorname{Mono}(f) \\iff \\operatorname{Injective}(f). $$$$

Lean4

theorem mono_iff_injective' {X Y : C} (f : X ⟶ Y) : Mono f ↔ Function.Injective f :=
  by
  simp only [mono_iff_injective, ← CategoryTheory.mono_iff_injective]
  apply (MorphismProperty.monomorphisms (Type w)).arrow_mk_iso_iff
  have e : forget₂ C Ab ⋙ forget Ab ≅ forget C := eqToIso (HasForget₂.forget_comp)
  exact Arrow.isoOfNatIso e (Arrow.mk f)

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