restrictScalarsLatticeHom — Mathlib

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

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