localization_specComap_injective — Mathlib

English

Let M be a submonoid and S a localization of R at M. The map algebraMap R S .specComap is injective.

Русский

Пусть M — подмоноид и S — локализация кольца R в M. Отображение algebraMap R S .specComap инъективно.

LaTeX

$$Function.Injective ((algebraMap R S).specComap).$$

Lean4

theorem localization_specComap_injective [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
    Function.Injective (algebraMap R S).specComap := by
  intro p q h
  replace h := _root_.congr_arg (fun x : PrimeSpectrum R => Ideal.map (algebraMap R S) x.asIdeal) h
  dsimp only [RingHom.specComap] at h
  rw [IsLocalization.map_comap M S, IsLocalization.map_comap M S] at h
  ext1
  exact h

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