English
If S is a localization of R and N is an S-module, then the R-rank of N equals the S-rank (i.e., the rank over R does not change under localization): Module.rank S N = Module.rank R N.
Русский
Пусть S локализация R, и N — модуль над S. Тогда ранг как модуль над S равен рангу над R: Module.rank S N = Module.rank R N.
LaTeX
$$$\operatorname{Module.rank} S N = \operatorname{Module.rank} R N$$$
Lean4
theorem rank_eq : Module.rank S N = Module.rank R N :=
by
cases subsingleton_or_nontrivial R
· have := (algebraMap R S).codomain_trivial; simp only [rank_subsingleton]
have inj := IsLocalization.injective S hp
apply le_antisymm <;> (rw [Module.rank]; apply ciSup_le'; intro ⟨s, hs⟩)
· have := (faithfulSMul_iff_algebraMap_injective R S).mpr inj
exact (hs.restrict_scalars' R).cardinal_le_rank
· have := inj.nontrivial
exact (hs.localization S p).cardinal_le_rank
