English
If N is an R-S-algebra object with appropriate towers of scalars, then rankAtStalk(N ⊗_R M) = rankAtStalk(N) · rankAtStalk(M) at the corresponding prime, reflecting base-change behavior.
Русский
Если имеется подходящая башня скаляров R → S ⊕ N, то ранг на локализации для N ⊗_R M равен произведению рангов: rankAtStalk(N ⊗_R M) = rankAtStalk(N) · rankAtStalk(M) при соответствующем приматe.
LaTeX
$$$\\operatorname{rankAtStalk}(N \\otimes_{R} M) = \\operatorname{rankAtStalk}(N) \\cdot \\operatorname{rankAtStalk}(M) \\;\\text{(at appropriate prime)}$$$
Lean4
theorem rankAtStalk_eq_zero_iff_notMem_support (p : PrimeSpectrum R) : rankAtStalk M p = 0 ↔ p ∉ support R M :=
by
rw [notMem_support_iff]
refine ⟨fun h ↦ ?_, fun h ↦ Module.finrank_zero_of_subsingleton⟩
apply subsingleton_of_rank_zero (R := Localization.AtPrime p.asIdeal)
dsimp [rankAtStalk] at h
simp [← finrank_eq_rank, h]
