English
If f: M ≃_R M' is a linear equivalence, then the dimensions of M and M' are the same after lifting to the appropriate universes.
Русский
Если существует линейное эквивалентное отображение f: M ≃_R M', то размерности M и M' совпадают (после подъема к необходимым вселенным).
LaTeX
$$$\mathrm{lift} \big( \operatorname{rank}_R M \big) = \mathrm{lift} \big( \operatorname{rank}_R M' \big)$$$
Lean4
/-- Two linearly equivalent vector spaces have the same dimension, a version with different
universes. -/
theorem lift_rank_eq (f : M ≃ₗ[R] M') : Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M') :=
by
apply le_antisymm
· exact f.toLinearMap.lift_rank_le_of_injective f.injective
· exact f.symm.toLinearMap.lift_rank_le_of_injective f.symm.injective
