rank_le_of_injective_injective — Mathlib

English

The same-universe version of rank inequalities under injective maps gives an inequality between ranks with matchable universes.

Русский

Та же самая единая вселенная версия неравенств ранга при инъективах между модулями дает неравенство между рангами.

LaTeX

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

Lean4

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

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