localized'_ker_eq_ker_localizedMap

English

For a linear map g: M → P, the localized kernel of g equals the localization of the kernel: (ker g).localized' S p f = ker (LocalizedMap g).

Русский

Для линейного отображения g: M → P локализованное ядро совпадает с локализацией ядра: (ker g).localized' S p f = ker (LocalizedMap g).

LaTeX

$$$\mathrm{ker}\, g \;\text{localized}'\; S\; p\; f = \ker(\mathrm{map\ p\, f\, f'}\; g).\text{extendScalars}$$$

Lean4

theorem localized'_ker_eq_ker_localizedMap (g : M →ₗ[R] P) :
    (ker g).localized' S p f = ker ((map p f f' g).extendScalarsOfIsLocalization p S) :=
  SetLike.ext (by apply SetLike.ext_iff.mp (f.ker_localizedMap_eq_localized₀_ker p f' g).symm)

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