awayMapₐ — Mathlib

English

For a ring homomorphism f: A → B over R, there is a canonical map between localized algebras Aₐ → B_{f a} over R.

Русский

Для алгебраического гомоморфа f: A → B над R существует каноническое отображение между локализациями Aₐ → B_{f a}.

LaTeX

$$$\mathrm{awayMap\_\!\!A}(f,a) : A\_a \to+* B_{f a}$$$

Lean4

/-- Given a map `f : A →ₐ[R] B` and an element `a : A`, we may construct a map `Aₐ →ₐ[R] Bₐ`. -/
noncomputable abbrev awayMapₐ (f : A →ₐ[R] B) (a : A) : Localization.Away a →ₐ[R] Localization.Away (f a) :=
  IsLocalization.Away.mapₐ _ _ f a

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