English
For a localization p S, the rank of a module N over S equals its rank over R: Module.rank S N = Module.rank R N.
Русский
При локализации p S ранг модуля N над S равен рангу над R: Module.rank S N = Module.rank R N.
LaTeX
$$$\operatorname{Module.rank} S N = \operatorname{Module.rank} R N$$$
Lean4
theorem lift_rank_eq_of_le_nonZeroDivisors :
Cardinal.lift.{uM} (Module.rank T P) = Cardinal.lift.{uP} (Module.rank R M) :=
by
rw [← lift_inj.{_, max uS uT uN}, lift_lift, lift_lift]
let ST := S ⊗[R] T
conv_rhs =>
rw [← lift_lift.{uN, max uS uT uP}, ← IsLocalizedModule.lift_rank_eq p f hp, ← IsLocalization.rank_eq S p hp,
lift_lift, ← lift_lift.{max uS uT, max uM uP}, ← rank_baseChange (R := ST), ←
lift_id'.{max uS uT, max uS uT uN} (Module.rank ..), lift_lift, ← lift_lift.{max uS uT uP, uM}]
let _ : Algebra T ST := Algebra.TensorProduct.rightAlgebra
set pT := Algebra.algebraMapSubmonoid T p
rw [← lift_lift.{max uS uT, max uM uN}, ← lift_umax.{uP}, ← IsLocalizedModule.lift_rank_eq pT (mk T ST P 1) hpT, ←
IsLocalization.rank_eq ST pT hpT, lift_id'.{uP, max uS uT}, ← lift_id'.{max uS uT, max uS uT uP} (Module.rank ..),
lift_lift, ← lift_lift.{max uS uT uN, uM}, lift_inj]
exact
LinearEquiv.lift_rank_eq <|
AlgebraTensorModule.congr (.refl ST ST) bc.equiv.symm ≪≫ₗ AlgebraTensorModule.cancelBaseChange .. ≪≫ₗ
(AlgebraTensorModule.cancelBaseChange ..).symm ≪≫ₗ
AlgebraTensorModule.congr (.refl ..) ((isLocalizedModule_iff_isBaseChange p S f).mp ‹_›).equiv
