inj — Mathlib

English

The canonical localization map is injective.

Русский

Каноническое отображение локализации инъективно.

LaTeX

$$$$ \mathrm{fromLocalizedModule} \text{ is injective}. $$$$

Lean4

theorem inj : Function.Injective <| fromLocalizedModule S f := fun x y eq1 =>
  by
  induction x with
  | _ a b
  induction y with
  | _ a' b'
  simp only [fromLocalizedModule_mk] at eq1
  rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← LinearMap.map_smul,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff'] at eq1
  rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def, Submonoid.smul_def, f.map_smul,
    f.map_smul, eq1]

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