English
For any pushout R,S,A,B and any b ∈ B, x in the base-changed tensor, the base-change map commutes with B-scalar multiplication: liftBaseChange is B-linear.
Русский
Для пуш-аута R,S,A,B и любого b ∈ B, x в соответствующем базисном тензорном модуле отображение базового изменения совместимо с умножением на скаляры из B; отображение сохраняет скалярное умножение.
LaTeX
$$$((map\\, R\\, S\\, A\\, B).restrictScalars\\ R).liftBaseChange S (b \\cdot x) = b \\cdot ((map\\, R\\, S\\, A\\, B).restrictScalars R).liftBaseChange S x$$$
Lean4
theorem map_liftBaseChange_smul [h : Algebra.IsPushout R S A B] (b : B) (x) :
((map R S A B).restrictScalars R).liftBaseChange S (b • x) =
b • ((map R S A B).restrictScalars R).liftBaseChange S x :=
by
induction b using h.1.inductionOn with
| zero => simp only [zero_smul, map_zero]
| smul s b e => rw [smul_assoc, map_smul, e, smul_assoc]
| add b₁ b₂ e₁ e₂ => simp only [map_add, e₁, e₂, add_smul]
| tmul a =>
induction x
· simp only [smul_zero, map_zero]
· simp [smul_comm]
· simp only [map_add, smul_add, *]
