rank_le_of_surjective_injective — Mathlib

English

If i and j are ring homomorphisms making the algebra scalars compatible, then the rank of the domain is at most the rank of the codomain.

Русский

Если i и j — гомоморфизмы колец, обеспечивающие совместимость алгебраических скаляров, тогда ранг источника не превосходит ранг цели.

LaTeX

$$$\operatorname{rank}_R S \le \operatorname{rank}_{R'} S'$$$

Lean4

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

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