English
Restriction of scalars forms a complete lattice homomorphism between submodule lattices.
Русский
Ограничение скаляров образует отображение гомоморфизма полного решета между решетками подмодулей.
LaTeX
$$$$ \\text{restrictScalarsLatticeHom}(S) : \\text{CompleteLatticeHom}(\\text{Submodule}_R M, \\text{Submodule}_S M). $$$$
Lean4
/-- If ring `S` acts on a ring `R` and `M` is a module over both (compatibly with this action) then
we can turn an `R`-submodule into an `S`-submodule by forgetting the action of `R`. -/
def restrictScalarsLatticeHom : CompleteLatticeHom (Submodule R M) (Submodule S M)
where
toFun := restrictScalars S
map_sInf' s := by ext; simp
map_sSup' s := by rw [← toAddSubmonoid_inj, toAddSubmonoid_sSup, ← Set.image_comp]; simp