toKerIsLocalization — Mathlib

English

An algebra map A → B induces a localized algebra map between localizations of A and B, namely (algebraMapSubmonoid A M).map f.toRingHom localized at B_p.

Русский

Алгебраическая карта $A\\to B$ индуцирует локализованную карту между локализациями $A_p$ и $B_p$.

LaTeX

$$$IsLocalization\\ ((algebraMapSubmonoid A M).map f.toRingHom) B_p$$$

Lean4

/-- The canonical linear map from the kernel of an algebra homomorphism to its localization. -/
noncomputable def toKerIsLocalization (f : A →ₐ[R] B) : RingHom.ker f →ₗ[A] RingHom.ker (mapₐ M Rₚ Aₚ Bₚ f) :=
  RingHom.toKerIsLocalization Aₚ Bₚ f.toRingHom (algebraMapSubmonoid_le_comap M f)

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