localizationMapOfSpecializes — Mathlib

English

If x specializes to y, there is a natural RingHom from Localization.AtPrime(y.asIdeal) to Localization.AtPrime(x.asIdeal).

Русский

Если x специализируется на y, существует естественный кольцевой гомоморфизм из Localization.AtPrime(y.asIdeal) в Localization.AtPrime(x.asIdeal).

LaTeX

$$$$ \text{localizationMapOfSpecializes}(x,y, h) : \operatorname{Localization.AtPrime}(y.asIdeal) \to+* \operatorname{Localization.AtPrime}(x.asIdeal). $$$$

Lean4

/-- If `x` specializes to `y`, then there is a natural map from the localization of `y` to the
localization of `x`. -/
def localizationMapOfSpecializes {x y : PrimeSpectrum R} (h : x ⤳ y) :
    Localization.AtPrime y.asIdeal →+* Localization.AtPrime x.asIdeal :=
  @IsLocalization.lift _ _ _ _ _ _ _ _ Localization.isLocalization (algebraMap R (Localization.AtPrime x.asIdeal))
    (by
      rintro ⟨a, ha⟩
      rw [← PrimeSpectrum.le_iff_specializes, ← asIdeal_le_asIdeal, ← SetLike.coe_subset_coe, ←
        Set.compl_subset_compl] at h
      exact (IsLocalization.map_units (Localization.AtPrime x.asIdeal) ⟨a, show a ∈ x.asIdeal.primeCompl from h ha⟩ :))

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