mono_map_iff_mono — Mathlib

English

If F preserves and reflects monomorphisms, then Mono (F.map f) iff Mono f.

Русский

Если F сохраняет и отражает мономорфизм, то Mono(F.map f) эквивалентно Mono f.

LaTeX

$$$$ \\operatorname{Mono}(F.map f) \\iff \\operatorname{Mono}(f). $$$$

Lean4

@[simp]
theorem mono_map_iff_mono [hF₁ : PreservesMonomorphisms F] [hF₂ : ReflectsMonomorphisms F] : Mono (F.map f) ↔ Mono f :=
  by
  constructor
  · exact F.mono_of_mono_map
  · intro h
    exact F.map_mono f

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