English
An extension lemma ensuring equality of two S-linear maps N → Q given agreement on M after base-change and restriction to R.
Русский
Лемма продолжения гомоморфизмов: если два S-линейных отображения N → Q совпадают на M после базового изменения и ограничения, то они совпадают на всей N.
LaTeX
$$$ \text{algHom_ext }(g_1,g_2,e) \Rightarrow g_1 = g_2 $$$
Lean4
/-- The base change of `M` along `R → S` is linearly equivalent to `S ⊗[R] M`. -/
noncomputable nonrec def equiv : S ⊗[R] M ≃ₗ[S] N :=
{ h.equiv with
map_smul' := fun r x => by
change h.equiv (r • x) = r • h.equiv x
refine TensorProduct.induction_on x ?_ ?_ ?_
· rw [smul_zero, map_zero, smul_zero]
· intro x y
simp [smul_tmul', Algebra.linearMap_apply, smul_comm r x]
· intro x y hx hy
rw [map_add, smul_add, map_add, smul_add, hx, hy] }
