finrank_of_isLocalizedModule_of_free

English

If M is a finitely generated module over R and M_S is its localization, then the localized rank equals the original rank (in suitable sense).

Русский

Если M конечно порожден как модуль над R и локализация дает эквивалентный ранг, то ранги согласуются.

LaTeX

$$$\\operatorname{finrank}_{R_S}(M_S) = \\operatorname{finrank}_{R}(M).$$$

Lean4

theorem finrank_of_isLocalizedModule_of_free (Rₛ : Type*) {Mₛ : Type*} [AddCommGroup Mₛ] [Module R Mₛ] [CommRing Rₛ]
    [Algebra R Rₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (S : Submonoid R) (f : M →ₗ[R] Mₛ) [IsLocalization S Rₛ]
    [IsLocalizedModule S f] [Module.Free R M] [Nontrivial Rₛ] : Module.finrank Rₛ Mₛ = Module.finrank R M := by
  simpa using congr(Cardinal.toNat $(Module.lift_rank_of_isLocalizedModule_of_free Rₛ S f))

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