English
Let f: M → N be a linear map over R, with a localization of R given by p and S, and IsLocalizedModule p f. Then the ranks of N and M over R agree after lifting to a larger universe; i.e., lift(rank_R N) = lift(rank_R M).
Русский
Пусть дано отображение f: M → N линейно над кольцом R, имеется локализация p и соответствующий S, и есть условие IsLocalizedModule p f. Тогда ранги модулей N и M над R совпадают после подъема по кардиналам: lift(rank_R N) = lift(rank_R M).
LaTeX
$$$\operatorname{lift}\big(\operatorname{Module.rank} R N\big) = \operatorname{lift}\big(\operatorname{Module.rank} R M\big)$$$
Lean4
theorem lift_rank_eq : Cardinal.lift.{uM} (Module.rank R N) = Cardinal.lift.{uN} (Module.rank R M) :=
by
cases subsingleton_or_nontrivial R
· simp only [rank_subsingleton, lift_one]
apply le_antisymm <;> rw [Module.rank_def, lift_iSup (bddAbove_range _)] <;> apply ciSup_le' <;> intro ⟨s, hs⟩
exacts [(IsLocalizedModule.linearIndependent_lift p f hs).choose_spec.cardinal_lift_le_rank,
hs.of_isLocalizedModule_of_isRegular p f (le_nonZeroDivisors_iff_isRegular.mp hp) |>.cardinal_lift_le_rank]
