English
If M is finite over R and there exist compatible scalar towers S over R acting on M, with an IsScalarTower R S S and FaithfulSMul, then finrank S M ≤ finrank R M.
Русский
Пусть M конечномерен над R и существует совместимость скалярных торов S над R, действующих на M, с IsScalarTower R S S и FaithfulSMul. Тогда finrank_S M ≤ finrank_R M.
LaTeX
$$$\\operatorname{finrank} S M \\le \\operatorname{finrank} R M$$$
Lean4
theorem finrank_le_of_isSMulRegular {S : Type*} [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M]
(L L' : Submodule R M) [Module.Finite R L'] {s : S} (hr : IsSMulRegular M s) (h : ∀ x ∈ L, s • x ∈ L') :
Module.finrank R L ≤ Module.finrank R L' :=
by
refine finrank_le_finrank_of_rank_le_rank (lift_le.mpr <| rank_le_of_isSMulRegular L L' hr h) ?_
rw [← Module.finrank_eq_rank R L']
exact nat_lt_aleph0 (finrank R ↥L')
