lift_rank_bot_le_lift_rank_of_isScalarTower

English

If T is a module with R → R' acting compatibly with a scalar tower, then the rank of R' as an R-module does not exceed the rank of T.

Русский

Пусть T — модуль с совместной дистрибутивной скалярной структурой и IsScalarTower; тогда ранг R' как R-модуля не превосходит ранг T.

LaTeX

$$$\operatorname{Module.rank} R R' \le \operatorname{Module.rank} R T$$$

Lean4

theorem lift_rank_bot_le_lift_rank_of_isScalarTower (T : Type w) [Module R R'] [NonAssocSemiring T] [Module R T]
    [Module R' T] [IsScalarTower R' T T] [FaithfulSMul R' T] [IsScalarTower R R' T] :
    Cardinal.lift.{w} (Module.rank R R') ≤ Cardinal.lift (Module.rank R T) :=
  LinearMap.lift_rank_le_of_injective ((LinearMap.toSpanSingleton R' T 1).restrictScalars R) <|
    (faithfulSMul_iff_injective_smul_one R' T).mp ‹_›

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