map_mk — Mathlib

English

Locally mapping identity corresponds to the identity map on the localized module.

Русский

Локализованное отображение единицы идентично единичному отображению на локализованном модуле.

LaTeX

$$$\\text{map}_S((\\mathrm{id})) = \\mathrm{Id}$$$

Lean4

@[simp]
theorem map_mk (f : M →ₗ[R] N) (x y) : map S f (.mk x y) = LocalizedModule.mk (f x) y :=
  by
  rw [IsLocalizedModule.mk_eq_mk', IsLocalizedModule.mk_eq_mk']
  exact IsLocalizedModule.map_mk' _ _ _ _ _ _

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