toKerIsLocalization_isLocalizedModule

English

If an algebra homomorphism f is injective, then its induced localization map on algebras is also injective (repeat statement).

Русский

Если отображение $f$ инъективно, то локализованное отображение по $f$ инъективно (повтор).

LaTeX

$$$\\text{Injective}(f) \\Rightarrow \\text{Injective}(\\mathrm{mapₐ} M R_p A_p B_p f)$$$

Lean4

/-- The canonical linear map from the kernel of an algebra homomorphism to its localization
is localizing. -/
theorem toKerIsLocalization_isLocalizedModule (f : A →ₐ[R] B) :
    IsLocalizedModule (Algebra.algebraMapSubmonoid A M) (AlgHom.toKerIsLocalization M Rₚ Aₚ Bₚ f) :=
  RingHom.toKerIsLocalization_isLocalizedModule Bₚ f.toRingHom (algebraMapSubmonoid_map_eq M f)

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