mapPiLocalization — Mathlib

English

Naturality with respect to composition: (mapPiLocalization f) ∘ (toPiLocalization R) = (toPiLocalization S) ∘ f.

Русский

Натуральность относительно композиции: (mapPiLocalization f) ∘ (toPiLocalization R) = (toPiLocalization S) ∘ f.

LaTeX

$$$ (\mathrm{mapPiLocalization}\ f \circ \mathrm{toPiLocalization}\ R) = (\mathrm{toPiLocalization}\ S \circ f) $$$

Lean4

/-- Functoriality of `PiLocalization` but restricted to bijective ring homs.
If R and S are commutative rings, surjectivity would be enough. -/
noncomputable def mapPiLocalization : PiLocalization R →+* PiLocalization S :=
  Pi.ringHom fun I ↦
    (Localization.localRingHom _ _ f rfl).comp <| Pi.evalRingHom _ (⟨_, I.2.comap_bijective f hf⟩ : MaximalSpectrum R)

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