map_id_lsmul_eq_lsmul_algebraMap — Mathlib

English

For every x in R, the base-changed scaling map corresponds to scaling by the image of x in S after base change.

Русский

Пусть x ∈ R. Тогда переход к основанию S перевешивает умножение на x в M на умножение на algebraMap_R^S(x) в N.

LaTeX

$$hf.map hf LinearMap.id (LinearMap.lsmul R M x) = LinearMap.lsmul S N (algebraMap R S x)$$

Lean4

theorem map_id_lsmul_eq_lsmul_algebraMap {f : M →ₗ[R] N} (hf : IsBaseChange S f) (x : R) :
    hf.map hf LinearMap.id (LinearMap.lsmul R M x) = LinearMap.lsmul S N (algebraMap R S x) :=
  by
  ext y
  refine IsTensorProduct.inductionOn hf y (by simp) ?_ (fun _ _ ha hb ↦ by simp [ha, hb])
  intro s m
  rw [hf.map_eq hf]
  simpa using smul_comm x s (f m)

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