ker_localizedMap_eq_localized'_ker

English

The map toKerIsLocalized provides a canonical localized map from ker g to ker (map p f f' g).

Русский

Каноническое отображение toKerIsLocalized задаёт локализованное отображение от ker g к ker (map p f f' g).

LaTeX

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

Lean4

theorem ker_localizedMap_eq_localized'_ker (g : M →ₗ[R] P) :
    ker (map p f f' g) = ((ker g).localized' S p f).restrictScalars _ :=
  by
  ext
  simp [localized'_ker_eq_ker_localizedMap S p f f']

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