English
The stalk rank of a tensor product M ⊗_R N equals the product of stalk ranks: rankAtStalk(M ⊗_R N) = rankAtStalk(M) · rankAtStalk(N).
Русский
Ранг на локализации тензорного произведения равен произведению рангов: rankAtStalk(M ⊗_R N) = rankAtStalk(M) · rankAtStalk(N).
LaTeX
$$$\\operatorname{rankAtStalk}(M \\otimes_{R} N) = \\operatorname{rankAtStalk}(M) \\cdot \\operatorname{rankAtStalk}(N)$$$
Lean4
/-- See `rankAtStalk_tensorProduct_of_isScalarTower` for a hetero-basic version. -/
theorem rankAtStalk_tensorProduct (N : Type*) [AddCommGroup N] [Module R N] [Module.Finite R N] [Module.Flat R N] :
rankAtStalk (M ⊗[R] N) = rankAtStalk M * rankAtStalk (R := R) N :=
by
ext p
let e :
Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
(Localization.AtPrime p.asIdeal ⊗[R] M) ⊗[Localization.AtPrime p.asIdeal]
(Localization.AtPrime p.asIdeal ⊗[R] N) :=
(AlgebraTensorModule.assoc _ _ _ _ _ _).symm ≪≫ₗ (AlgebraTensorModule.cancelBaseChange _ _ _ _ _).symm
rw [rankAtStalk_eq_finrank_tensorProduct, e.finrank_eq, finrank_tensorProduct, ← rankAtStalk_eq_finrank_tensorProduct,
← rankAtStalk_eq_finrank_tensorProduct, Pi.mul_apply]
