rankAtStalk_eq_finrank_of_free — Mathlib

English

If M is free as an R-module, then the stalk rank of M equals the R-rank of M (finrank).

Русский

Если M свободен как R-модуль, то ранг на локализации равен рангу модуля (finrank).

LaTeX

$$$[\,Module.Free\\ R\\ M\] \\Rightarrow \\operatorname{rankAtStalk}(R, M) = \\operatorname{finrank} R M$$

Lean4

/-- If `M` is `R`-free, its rank at stalks is constant and agrees with the `R`-rank of `M`. -/
@[simp]
theorem rankAtStalk_eq_finrank_of_free [Module.Free R M] : rankAtStalk (R := R) M = Module.finrank R M :=
  by
  ext p
  simp [rankAtStalk,
    finrank_of_isLocalizedModule_of_free _ p.asIdeal.primeCompl (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)]

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