English
Under a scalar tower R → S → T with appropriate finiteness/flatness hypotheses, the stalk rank respects the tower: rankAtStalk(T ⊗_R M) = rankAtStalk(T) · rankAtStalk(M) evaluated at the composed maps.
Русский
В рамках башни скаляров R → S → T при подходящих условиях ранги на локализации сохраняют пропорцию: rankAtStalk(T ⊗_R M) = rankAtStalk(T) · rankAtStalk(M) по композиции отображений.
LaTeX
$$$\\operatorname{rankAtStalk}(T \\otimes_{R} M) = \\operatorname{rankAtStalk}(T) \\cdot \\operatorname{rankAtStalk}(M) \\text{ (with appropriate composed prime)}$$$
Lean4
theorem rankAtStalk_tensorProduct_of_isScalarTower {S : Type*} [CommRing S] [Algebra R S] (N : Type*) [AddCommGroup N]
[Module R N] [Module S N] [IsScalarTower R S N] [Module.Finite S N] [Module.Flat S N] (p : PrimeSpectrum S) :
rankAtStalk (N ⊗[R] M) p = rankAtStalk N p * rankAtStalk M ((algebraMap R S).specComap p) := by
simp [rankAtStalk_eq_of_equiv (AlgebraTensorModule.cancelBaseChange R S S N M).symm, rankAtStalk_tensorProduct,
rankAtStalk_baseChange]
