mapPiLocalization_naturality — Mathlib

English

If f is bijective, then mapPiLocalization f is bijective.

Русский

Если отображение f биективно, то mapPiLocalization f биективно.

LaTeX

$$$\text{If } f:\, R \to S \text{ is bijective, then } \mathrm{mapPiLocalization}(f) \text{ is bijective}$$$

Lean4

theorem mapPiLocalization_naturality :
    (mapPiLocalization f hf).comp (toPiLocalization R) = (toPiLocalization S).comp f :=
  by
  ext r I
  change Localization.localRingHom _ _ _ rfl (algebraMap _ _ r) = algebraMap _ _ (f r)
  simp_rw [← IsLocalization.mk'_one (M := (I.1.comap f).primeCompl), Localization.localRingHom_mk', ←
    IsLocalization.mk'_one (M := I.1.primeCompl), Submonoid.coe_one, map_one f]
  rfl

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