rankAtStalk — Mathlib

English

The function rankAtStalk(M) is locally constant on freeLocus, i.e., rank is locally constant on primes where M is locally free.

Русский

Функция rankAtStalk(M) локально константна на freeLocus, то есть ранг стабилен в окрестностях точек, где M локально свободен.

LaTeX

$$$IsLocallyConstant(\mathrm{rankAtStalk}(M))\ on\ freeLocus(R,M)$$$

Lean4

/-- The rank of `M` at the stalk of `p` is the rank of `Mₚ` as a `Rₚ`-module. -/
noncomputable def rankAtStalk (p : PrimeSpectrum R) : ℕ :=
  Module.finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M)

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