English
The canonical linear map from the kernel of an algebra homomorphism to the kernel of its algebra-localization is localizing.
Русский
Каноническое линейное отображение от ядра алгебраического гомоморфа к ядру его локализации по алгебре является локализующим.
LaTeX
$$$IsLocalizedModule (\\mathrm{Algebra.algebraMapSubmonoid } A M) (\\mathrm{AlgHom.toKerIsLocalization} M R_p A_p B_p f)$$$
Lean4
/-- An algebra map `A →ₐ[R] B` induces an algebra map on localizations `Aₚ →ₐ[Rₚ] Bₚ`. -/
noncomputable def mapₐ (f : A →ₐ[R] B) : Aₚ →ₐ[Rₚ] Bₚ :=
⟨IsLocalization.map Bₚ f.toRingHom (Algebra.algebraMapSubmonoid_le_comap M f), fun r ↦
by
obtain ⟨a, m, rfl⟩ := IsLocalization.mk'_surjective M r
simp [algebraMap_mk' (S := A), algebraMap_mk' (S := B), map_mk']⟩
