English
The rank at stalk equals the dimension after choosing a residue field and tensoring; equivalently, rank equals finrank over the residue field after base-change.
Русский
Ранг на локализации равен размерности после выбора остаточного поля и тензорного произведения; то есть ранг равен finrank после редуцирования по остаточному полю.
LaTeX
$$$\\operatorname{rankAtStalk}(M)(p) = \\operatorname{finrank}_{\\kappa(p)} (\\kappa(p) \\otimes_{R} M)$$$
Lean4
/-- The rank of a module `M` at a prime `p` is equal to the dimension
of `κ(p) ⊗[R] M` as a `κ(p)`-module. -/
theorem rankAtStalk_eq (p : PrimeSpectrum R) :
rankAtStalk M p = finrank p.asIdeal.ResidueField (p.asIdeal.ResidueField ⊗[R] M) :=
by
let k := p.asIdeal.ResidueField
let e : k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) ≃ₗ[k] k ⊗[R] M :=
AlgebraTensorModule.cancelBaseChange _ _ _ _ _
rw [← e.finrank_eq, finrank_baseChange, rankAtStalk_eq_finrank_tensorProduct]
