English
Under a base change bc: M → P along T, the lift of ranks matches: lift(rank_T P) = lift(rank_R M).
Русский
При базовом изменении bc: M → P ранги поднимаются одинаково: 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
/-- The **rank-nullity theorem** for commutative domains. Also see `rank_quotient_add_rank`. -/
theorem rank_quotient_add_rank_of_isDomain [IsDomain R] (M' : Submodule R M) :
Module.rank R (M ⧸ M') + Module.rank R M' = Module.rank R M :=
by
apply lift_injective.{max uR uM}
simp_rw [lift_add, ← IsLocalizedModule.lift_rank_eq R⁰ (M'.toLocalized R⁰) le_rfl, ←
IsLocalizedModule.lift_rank_eq R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl, ←
IsLocalizedModule.lift_rank_eq R⁰ (M'.toLocalizedQuotient R⁰) le_rfl, ←
IsLocalization.rank_eq (FractionRing R) R⁰ le_rfl, ← lift_add, rank_quotient_add_rank_of_divisionRing]
