injective_of_map_zero — Mathlib

English

From the previous injectivity criterion, one deduces that if ∀ m, g(f m) = 0 implies f m = 0, then g is injective.

Русский

Из предыдущего критерия инъективности следует, что если ∀ m, g(f m) = 0 ⇒ f m = 0, то g инъективно.

LaTeX

$$$$ \\forall m,\\; g(f m) = 0 \\Rightarrow f m = 0 \\quad\\Rightarrow\\quad \\text{Injective } g $$$$

Lean4

theorem injective_of_map_zero {M M' N : Type*} [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M']
    (f : M →ₗ[R] M') [IsLocalizedModule S f] [AddCommGroup N] [Module R N] {g : M' →ₗ[R] N}
    (H : ∀ m, g (f m) = 0 → f m = 0) : Function.Injective g :=
  by
  refine IsLocalizedModule.injective_of_map_eq S f (fun hxy ↦ ?_)
  rw [← sub_eq_zero, ← map_sub]
  apply H
  simpa [sub_eq_zero]

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