mapPiEvalRingHom — Mathlib

English

There is a canonical map between localizations induced by projecting a product ring to its i-th component.

Русский

Существует каноническое отображение между локализациями, индуцируемое проекцией из произведения кольца в i-й компонент.

LaTeX

$$$\\operatorname{map}\\_\\mathrm{PiEval}(\\,\\mathrm{Pi.evalRingHom}\\,)$$$

Lean4

/-- `IsLocalization.map` applied to a projection homomorphism from a product ring. -/
noncomputable abbrev mapPiEvalRingHom : Localization (S.comap <| Pi.evalRingHom R i) →+* Localization S :=
  map (T := S) _ (Pi.evalRingHom R i) le_rfl

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