toPiLocalization_injective — Mathlib

English

The canonical PiLocalization map for a bijective base ring homomorphism is injective.

Русский

Каноническое отображение PiLocalization сохраняет инъективность при биективном базовом гомоморфизме.

LaTeX

$$$\operatorname{toPiLocalization}(R) \, \text{injective}$ for bijective base maps$$

Lean4

theorem toPiLocalization_injective : Function.Injective (toPiLocalization R) := fun r r' eq ↦
  by
  rw [← one_mul r, ← one_mul r']
  by_contra ne
  have ⟨I, mI, hI⟩ := (Module.eqIdeal R r r').exists_le_maximal ((Ideal.ne_top_iff_one _).mpr ne)
  have ⟨s, hs⟩ := (IsLocalization.eq_iff_exists I.primeCompl _).mp (congr_fun eq ⟨I, mI⟩)
  exact s.2 (hI hs)

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