baseChange — Mathlib

English

Forgetting the B-action, a submodule over A ⊗R B is simply a submodule over A.

Русский

Забывая про действие B, подмодуль над A ⊗R B просто является подмодулем над A.

LaTeX

$$$$ \\text{toSubmodule}(p) = p \\quad\\text{is a Submodule of } A \\text{ on } M. $$$$

Lean4

/-- If `A` and `B` are also `Algebra`s over yet another set of scalars `S` then we may "base change"
from `R` to `S`. -/
@[simps!]
def baseChange (S : Type*) [CommSemiring S] [Module S M] [Algebra S A] [Algebra S B] [IsScalarTower S A M]
    [IsScalarTower S B M] (p : Submodule (A ⊗[R] B) M) : Submodule (A ⊗[S] B) M :=
  mk p.toAddSubmonoid (smul_mem p) (smul_mem' p)

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