map_injective — Mathlib

English

If h is injective and the localization maps are compatible, then the induced map ĥ is injective.

Русский

Если h инъективно и локализационные отображения совместимы, тогда индукцированное отображение ĥ инъективно.

LaTeX

$$$$ \\text{Injective } h \\Rightarrow \\text{Injective } (\\text{map } S f g h) $$$$

Lean4

@[simp]
theorem map_injective (h : M →ₗ[R] N) (h_inj : Function.Injective h) : Function.Injective (map S f g h) :=
  by
  intro x y
  obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f x
  obtain ⟨⟨y, t⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f y
  simp only [Function.uncurry_apply_pair, map_mk', mk'_eq_mk'_iff, Subtype.exists, Submonoid.mk_smul, exists_prop,
    forall_exists_index, and_imp]
  intro c hc e
  exact ⟨c, hc, h_inj (by simpa)⟩

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