lift_rank_of_isLocalizedModule_of_free

English

Rank of a localized free module does not change under base change to the localized ring.

Русский

Ранг локализованного свободного модуля не меняется при переходе к локализации кольца.

LaTeX

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

Lean4

/-- Also see `IsLocalizedModule.lift_rank_eq` for a version for non-free modules,
but requires `S` to not contain any zero-divisors.
-/
theorem lift_rank_of_isLocalizedModule_of_free (Rₛ : Type uR') {Mₛ : Type uM'} [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ₛ] :
    Cardinal.lift.{uM} (Module.rank Rₛ Mₛ) = Cardinal.lift.{uM'} (Module.rank R M) :=
  by
  apply Cardinal.lift_injective.{max uM' uR'}
  have := (algebraMap R Rₛ).domain_nontrivial
  have := (IsLocalizedModule.isBaseChange S Rₛ f).equiv.lift_rank_eq.symm
  simp only [rank_tensorProduct, rank_self, Cardinal.lift_one, one_mul, Cardinal.lift_lift] at this ⊢
  convert this
  exact Cardinal.lift_umax

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