rank_top_le_rank_of_isScalarTower

English

Let f: M →_R M' be injective. Then the lifted rank of the range is equal to the lifted rank of M.

Русский

Пусть f: M →_R M' инъективно; тогда поднимаемый ранг образа равен поднимаемому рангу M.

LaTeX

$$$\operatorname{lift} (\operatorname{Module.rank} R (\operatorname{LinearMap.range} f)) = \operatorname{lift} (\operatorname{Module.rank} R M)$$$

Lean4

theorem rank_top_le_rank_of_isScalarTower [Module R' M] [SMulWithZero R R'] [IsScalarTower R R' M] [FaithfulSMul R R']
    [IsScalarTower R R' R'] : Module.rank R' M ≤ Module.rank R M :=
  by
  rw [Module.rank, Module.rank]
  exact
    ciSup_le' fun ⟨s, hs⟩ ↦
      le_ciSup_of_le (Cardinal.bddAbove_range _)
        ⟨s, hs.restrict_scalars (by simpa [← faithfulSMul_iff_injective_smul_one])⟩ le_rfl

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