rank_le_of_surjective_injective — Mathlib

English

In a surjective/injective setting with compatible scalar action, the rank inequality holds in the same-universe form.

Русский

В условиях сюръекции/инъекции с совместимым действием скаляров сохраняется неравенство ранга в однотипном виде.

LaTeX

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

Lean4

/-- The same-universe version of `lift_rank_le_of_surjective_injective`. -/
theorem rank_le_of_surjective_injective (i : R → R') (j : M →+ M₁) (hi : Surjective i) (hj : Injective j)
    (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : Module.rank R M ≤ Module.rank R' M₁ := by
  simpa only [lift_id] using lift_rank_le_of_surjective_injective i j hi hj hc

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