rank_le_of_injective_injective — Mathlib

English

A direct consequence of the surjective/injective rank bound with compatible scalars yields a rank inequality.

Русский

Следствие из неравенствия рангов при сюръективном и инъективном отображении вместе с совместимыми скалярами даёт неравенство рангов.

LaTeX

$$$\operatorname{rank}_R(M) \le \operatorname{rank}_{R'}(M')$$$

Lean4

/-- The same-universe version of `Algebra.lift_rank_le_of_injective_injective`. -/
theorem rank_le_of_injective_injective (i : R' →+* R) (j : S →+* S') (hi : Injective i) (hj : Injective j)
    (hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S') : Module.rank R S ≤ Module.rank R' S' := by
  simpa only [lift_id] using lift_rank_le_of_injective_injective i j hi hj hc

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