map_mk' — Mathlib

English

If h is injective, then the composed map (map S f g h) is injective; this follows from the injectivity of h and the localization properties.

Русский

Если h инъективно, то и композиция map S f g h инъективна; следует из инъективности h и свойств локализации.

LaTeX

$$$$ \\text{Injective } h \\Rightarrow \\text{Injective } (\\text{map } S f g h) $$$$

Lean4

@[simp]
theorem map_mk' (h : M →ₗ[R] N) (x) (s : S) :
    map S f g h (IsLocalizedModule.mk' f x s) = (IsLocalizedModule.mk' g (h x) s) :=
  by
  simp only [map, lift, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply]
  rw [iso_symm_apply' S f (mk' f x s) x s (mk'_cancel' f x s), LocalizedModule.lift_mk]
  rfl

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