English
For a base change S over R, the stalk rank of S ⊗_R M at p equals rankAtStalk(M) at the corresponding prime.
Русский
Для базового изменения S над R ранг на локализации S ⊗_R M при p равен рангу M при соответствующем примате.
LaTeX
$$$\\operatorname{rankAtStalk}(S \\otimes_{R} M)(p) = \\operatorname{rankAtStalk}(M)((\\mathrm{algebraMap} R S)^{\\mathrm{specComap}}(p))$$$
Lean4
theorem rankAtStalk_baseChange {S : Type*} [CommRing S] [Algebra R S] (p : PrimeSpectrum S) :
rankAtStalk (S ⊗[R] M) p = rankAtStalk M ((algebraMap R S).specComap p) :=
by
let q : PrimeSpectrum R := (algebraMap R S).specComap p
let e :
LocalizedModule p.asIdeal.primeCompl (S ⊗[R] M) ≃ₗ[Localization.AtPrime p.asIdeal]
Localization.AtPrime p.asIdeal ⊗[Localization.AtPrime q.asIdeal] LocalizedModule q.asIdeal.primeCompl M :=
LocalizedModule.equivTensorProduct _ _ ≪≫ₗ (AlgebraTensorModule.cancelBaseChange R S _ _ M) ≪≫ₗ
(AlgebraTensorModule.cancelBaseChange R _ _ _ M).symm ≪≫ₗ
(AlgebraTensorModule.congr (LinearEquiv.refl _ _) (LocalizedModule.equivTensorProduct _ M).symm)
rw [rankAtStalk, e.finrank_eq]
apply Module.finrank_baseChange
