English
Under compatible injections i, j between modules, the rank of M does not exceed the rank of M'.
Русский
При совместимых вкачиваниях i, j между модулями ранг M не превосходит ранг M'.
LaTeX
$$$\operatorname{rank}_R(M) \le \operatorname{rank}_{R'}(M')$$$
Lean4
/-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a bijective map which maps zero to zero,
`j : M ≃+ M'` is a group isomorphism, such that the scalar multiplications on `M` and `M'` are
compatible, then the rank of `M / R` is equal to the rank of `M' / R'`.
As a special case, taking `R = R'` it is `LinearEquiv.lift_rank_eq`. -/
theorem lift_rank_eq_of_equiv_equiv (i : R → R') (j : M ≃+ M') (hi : Bijective i)
(hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : lift.{v'} (Module.rank R M) = lift.{v} (Module.rank R' M') :=
(lift_rank_le_of_surjective_injective i j hi.2 j.injective hc).antisymm <|
lift_rank_le_of_injective_injectiveₛ i j.symm hi.1 j.symm.injective fun _ _ ↦ j.symm_apply_eq.2 <| by simp_all
