rankAtStalk_pos_iff_mem_support — Mathlib

English

Under a base change S over R, rankAtStalk(S ⊗_R M) at p equals rankAtStalk(M) at the corresponding prime in S.

Русский

При базовом изменении S над R ранг на локализации S ⊗_R M равен рангу на соответствующей точке в S.

LaTeX

$$$\\operatorname{rankAtStalk}(S \\otimes_{R} M)(p) = \\operatorname{rankAtStalk}(M)((\\mathrm{algebraMap\\} R \\; S)^{\\mathrm{specComap}}(p))$$$

Lean4

theorem rankAtStalk_pos_iff_mem_support (p : PrimeSpectrum R) : 0 < rankAtStalk M p ↔ p ∈ support R M :=
  Nat.pos_iff_ne_zero.trans (rankAtStalk_eq_zero_iff_notMem_support _).not_left

Похожие утверждения