mapPiLocalization_naturality — Mathlib

English

Naturality of mapPiLocalization with respect to composition: as in composition of ring homs.

Русский

Натуральность mapPiLocalization относительно композиции гомоморфизмов колец.

LaTeX

$$$ (mapPiLocalization f) \circ (toPiLocalization R) = (toPiLocalization S) \circ f$$$

Lean4

theorem mapPiLocalization_naturality : (mapPiLocalization f).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

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