restrictScalarsEmbedding — Mathlib

English

Restriction of scalars defines an order-embedding from Submodule_R M to Submodule_S M.

Русский

Ограничение скаляров задаёт вложение по порядку из Submodule_R M в Submodule_S M.

LaTeX

$$$$ \\operatorname{restrictScalarsEmbedding}(S) : \\text{Submodule}_R M \\hookrightarrow \\text{Submodule}_S M \\text{ is an order-embedding, i.e. } V_1 \\le V_2 \\iff V_1.\\restrictionScalars S \\le V_2.\\restrictionScalars S. $$$$

Lean4

/-- `restrictScalars S` is an embedding of the lattice of `R`-submodules into
the lattice of `S`-submodules. -/
@[simps]
def restrictScalarsEmbedding : Submodule R M ↪o Submodule S M
    where
  toFun := restrictScalars S
  inj' := restrictScalars_injective S R M
  map_rel_iff' := by simp [SetLike.le_def]

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