toKerIsLocalized — Mathlib

English

There is a localized map from the kernel to the kernel of the localized map: toKerLocalized.

Русский

Существует локализованное отображение от ядра к ядру локализованного отображения: toKerLocalized.

LaTeX

$$$\mathrm{toKerLocalized}: \ker g \to\ker(\mathrm{map\ p\, f\, f'}\, g)$$$

Lean4

/-- The canonical map from the kernel of `g` to the kernel of `g` localized at a submonoid.

This is a localization map by `LinearMap.toKerLocalized_isLocalizedModule`.
-/
@[simps!]
noncomputable def toKerIsLocalized (g : M →ₗ[R] P) : ker g →ₗ[R] ker (map p f f' g) :=
  f.restrict (fun x hx ↦ by simp [mem_ker, mem_ker.mp hx])

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