rank_le_of_injective_injectiveₛ

English

A variant of the rank bound under injective maps producing a monotone inequality.

Русский

Вариант границы ранга под инъективными отображениями, дающий монотонное неравенство.

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ₛ (i : R' → R) (j : M →+ M₁) (hi : Injective i) (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

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