rankAtStalk_eq_of_equiv — Mathlib

English

If two R-modules M and N are linearly isomorphic, their stalk ranks agree: rankAtStalk M = rankAtStalk N.

Русский

Если модули M и N над R линейно эквивалентны, их ранги на локализации совпадают: rankAtStalk M = rankAtStalk N.

LaTeX

$$$\\exists e : M \\simeq_{R} N \\;\\Rightarrow\\; \\operatorname{rankAtStalk}(R, M) = \\operatorname{rankAtStalk}(R, N)$$$

Lean4

theorem rankAtStalk_eq_of_equiv {N : Type*} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) :
    rankAtStalk (R := R) M = rankAtStalk N := by
  ext p
  exact
    IsLocalizedModule.mapEquiv p.asIdeal.primeCompl (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)
        (LocalizedModule.mkLinearMap p.asIdeal.primeCompl N) _ e |>.finrank_eq

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