English
The scalar multiplication inside the restricted module commutes with map of I by algebra map, giving the expected restricted action.
Русский
Умножение скаляра внутри ограниченного модуля коммутирует с отображением умножения через алгебраическое отображение, давая ожидаемое ограниченное действие.
LaTeX
$$$\\bigl(I.\\text{map}(\\mathrm{algebraMap}_{R S}) \\cdot N\\bigr)^{\\text{restrictScalars }R} = I \\cdot N^{\\text{restrictScalars }R}$$$
Lean4
theorem smul_restrictScalars {R S M} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M]
[Module S M] [IsScalarTower R S M] (I : Ideal R) (N : Submodule S M) :
(I.map (algebraMap R S) • N).restrictScalars R = I • N.restrictScalars R :=
by
simp_rw [map, Submodule.span_smul_eq, ← Submodule.coe_set_smul, Submodule.set_smul_eq_iSup, ←
element_smul_restrictScalars, iSup_image]
exact map_iSup₂ (Submodule.restrictScalarsLatticeHom R S M) _
