English
If g : M' → N satisfies the condition that g(f x) = g(f y) implies f x = f y for all x,y, then g is injective.
Русский
Если g : M' → N удовлетворяет условию: g(f x) = g(f y) ⇒ f x = f y для всех x,y, то g инъективно.
LaTeX
$$$$ \\forall x,y,\\; g(f x) = g(f y) \\Rightarrow f x = f y \\quad\\Rightarrow\\quad \\text{Injective } g $$$$
Lean4
theorem injective_of_map_eq {N : Type*} [AddCommMonoid N] [Module R N] {g : M' →ₗ[R] N}
(H : ∀ {x y}, g (f x) = g (f y) → f x = f y) : Function.Injective g :=
by
intro a b hab
obtain ⟨⟨x, m⟩, (hxm : m • a = f x)⟩ := IsLocalizedModule.surj S f a
obtain ⟨⟨y, n⟩, (hym : n • b = f y)⟩ := IsLocalizedModule.surj S f b
suffices h : g (f (n.val • x)) = g (f (m.val • y)) by
apply H at h
rw [map_smul, map_smul] at h
rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]
simp [← hxm, ← hym, hab, ← S.smul_def, ← mul_smul, mul_comm, ← mul_smul]
