toPiLocalization_injective — Mathlib

English

For a commutative semiring R and any commutative semiring S, the map toPiLocalization R is injective on prime ideals: prime spectra embed under localization at Pi-localization.

Русский

Для коммутативного полускольца R и любого коммутативного полускольца S отображение toPiLocalization R инъективно на(множества?)prime-спектров: вложение спектров п Prime после локализации.

LaTeX

$$$\\text{toPiLocalization}_R: \\operatorname{PrimeSpectrum}(R) \\to \\operatorname{PrimeSpectrum}(R_{\\mathrm{Away}}) \\text{ is injective}.$$

Lean4

theorem toPiLocalization_injective : Function.Injective (toPiLocalization R) := fun _ _ eq ↦
  MaximalSpectrum.toPiLocalization_injective R <| funext fun I ↦ congr_fun eq I.toPrimeSpectrum

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