English
If i: R → R' is surjective and j: M →+ M' is injective, with compatible scalar action, then lift(rank_R M) ≤ lift(rank_R' M').
Русский
Если i: R → R' сюръективно, а j: M →+ M' инъективно, и скалярные действия совместимы, то подъем ранга модуля не больше подъема ранга модуля-образа.
LaTeX
$$$\operatorname{lift}(\operatorname{rank}_R M) \le \operatorname{lift}(\operatorname{rank}_{R'} M')$$$
Lean4
/-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a surjective map, and
`j : M →+ M'` is an injective monoid homomorphism, such that the scalar multiplications on `M` and
`M'` are compatible, then the rank of `M / R` is smaller than or equal to the rank of `M' / R'`.
As a special case, taking `R = R'` it is `LinearMap.lift_rank_le_of_injective`. -/
theorem lift_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) : lift.{v'} (Module.rank R M) ≤ lift.{v} (Module.rank R' M') :=
by
obtain ⟨i', hi'⟩ := hi.hasRightInverse
refine lift_rank_le_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_
· apply_fun i at h
rwa [hi', hi'] at h
rw [hc (i' r) m, hi']
