of_restrictScalars — Mathlib

English

If S is a submodule of M over A and its restriction to R is FG, then S is FG over A.

Русский

Если S — подпредмет M над A и S, viewed as R-submodule, FG, то S FG над A.

LaTeX

$$S.FG → (Submodule.restrictScalars R S).FG → S.FG$$

Lean4

theorem of_restrictScalars (R) {A M} [Semiring R] [Semiring A] [AddCommMonoid M] [SMul R A] [Module R M] [Module A M]
    [IsScalarTower R A M] (S : Submodule A M) (hS : (S.restrictScalars R).FG) : S.FG :=
  by
  obtain ⟨s, e⟩ := hS
  refine ⟨s, Submodule.restrictScalars_injective R _ _ (le_antisymm ?_ ?_)⟩
  · change Submodule.span A s ≤ S
    have := Submodule.span_le.mp e.le
    rwa [Submodule.span_le]
  · rw [← e]
    exact Submodule.span_le_restrictScalars _ _ _

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