English
Finite generation is preserved when restricting scalars along a surjective algebra map, provided the ambient modules satisfy the scalar tower hypothesis.
Русский
Конечная порождаемость сохраняется при ограничении скалярами по сюръективному гомоморфизму алгебр, при условии тождества скаляров.
LaTeX
$$N.FG → Surjective(algebraMap R S) → (Submodule.restrictScalars R N).FG$$
Lean4
theorem fg_restrictScalars {R S M : Type*} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module S M]
[Module R M] [IsScalarTower R S M] (N : Submodule S M) (hfin : N.FG) (h : Function.Surjective (algebraMap R S)) :
(Submodule.restrictScalars R N).FG := by
obtain ⟨X, rfl⟩ := hfin
use X
exact (Submodule.restrictScalars_span R S h (X : Set M)).symm
