English
The lift of ranks across a base change bc: M → P matches: lift(rank_T P) = lift(rank_R M).
Русский
Подъем рангов по базовому изменению даёт равенство: lift(rank_T P) = lift(rank_R M).
LaTeX
$$$\operatorname{lift}\big(\operatorname{Module.rank} T P\big) = \operatorname{lift}\big(\operatorname{Module.rank} R M\big)$$$
Lean4
theorem lift_rank_eq : Cardinal.lift.{uM} (Module.rank T P) = Cardinal.lift.{uP} (Module.rank R M) :=
by
have inj := FaithfulSMul.algebraMap_injective R T
have := inj.noZeroDivisors _ (map_zero _) (map_mul _)
cases subsingleton_or_nontrivial R
· have := (algebraMap R T).codomain_trivial; simp only [rank_subsingleton, lift_one]
have := (isDomain_iff_noZeroDivisors_and_nontrivial T).mpr ⟨‹_›, (FaithfulSMul.algebraMap_injective R T).nontrivial⟩
let FR := FractionRing R
let FT := FractionRing T
replace inj : Function.Injective (algebraMap R FT) := (IsFractionRing.injective T _).comp inj
let g := TensorProduct.mk T FT P 1
have : IsLocalizedModule R⁰ (TensorProduct.mk R FR FT 1) := inferInstance
let _ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
let _ :=
isLocalizedModule_iff_isLocalization.mp this |>.atUnits _ _ ?_ |>.symm.isField (Field.toIsField FT) |>.toField
on_goal 2 => rintro _ ⟨_, mem, rfl⟩; exact (map_ne_zero_of_mem_nonZeroDivisors _ inj mem).isUnit
have := bc.comp_iff.2 ((isLocalizedModule_iff_isBaseChange T⁰ FT g).1 inferInstance)
rw [← lift_inj.{_, max uT uP}, lift_lift, lift_lift, ← lift_lift.{max uT uP, uM}, ←
IsLocalizedModule.lift_rank_eq T⁰ g le_rfl, lift_lift, ← lift_lift.{uM}, ← IsLocalization.rank_eq FT T⁰ le_rfl,
lift_rank_eq_of_le_nonZeroDivisors FR (LocalizedModule.mkLinearMap R⁰ M) le_rfl
(map_le_nonZeroDivisors_of_injective _ inj le_rfl) this,
lift_lift]
