toKerIsLocalization_apply — Mathlib

English

The canonical linear map from ker g to ker (IsLocalization.map) is localizing.

Русский

Каноническое линейное отображение от ядра $g$ к ядру локализации является локализующим.

LaTeX

$$$IsLocalizedModule\\ M\\big(\\mathrm{RingHom.toKerIsLocalization} S Q g \\cdots\\big)$$$

Lean4

@[simp]
theorem toKerIsLocalization_apply (f : A →ₐ[R] B) (x : RingHom.ker f) :
    AlgHom.toKerIsLocalization M Rₚ Aₚ Bₚ f x =
      RingHom.toKerIsLocalization Aₚ Bₚ f.toRingHom (algebraMapSubmonoid_le_comap M f) x :=
  rfl

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