English
The stalk rank of M equals the finrank over the localization of the tensor product: rankAtStalk(M) = finrank (Localization.AtPrime p) (Localization.AtPrime p ⊗_R M).
Русский
Ранг на локализации mодуля M равен размерности тензорного произведения над локализацией: rankAtStalk(M) = finrank(Localization.AtPrime p) (Localization.AtPrime p ⊗_R M).
LaTeX
$$$\\operatorname{rankAtStalk}(M, p) = \\operatorname{finrank} \\, (\\operatorname{Localization.AtPrime}(p))\\; (\\operatorname{Localization.AtPrime}(p) \\otimes_{R} M)$$$
Lean4
theorem rankAtStalk_eq_finrank_tensorProduct (p : PrimeSpectrum R) :
rankAtStalk M p = finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M) :=
by
let e :
LocalizedModule p.asIdeal.primeCompl M ≃ₗ[Localization.AtPrime p.asIdeal] Localization.AtPrime p.asIdeal ⊗[R] M :=
LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M
rw [rankAtStalk, e.finrank_eq]
