English
If M is finitely presented and the localized module is free, then there exists a r ∈ S giving a free localized module.
Русский
Если M конечно презентационный и локализованный модуль свободен, существует r ∈ S так, что локализованный модуль свободен.
LaTeX
$$Module.FinitePresentation.exists_free_localizedModule_powers$$
Lean4
/-- If `M` is a finitely presented `R`-module
such that `Mₛ` is free over `Rₛ` for some `S : Submonoid R`,
then `Mᵣ` is already free over `Rᵣ` for some `r ∈ S`.
-/
theorem exists_free_localizedModule_powers (Rₛ) [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [IsScalarTower R Rₛ M']
[Nontrivial Rₛ] [IsLocalization S Rₛ] [Module.FinitePresentation R M] [Module.Free Rₛ M'] :
∃ r,
r ∈ S ∧
Module.Free (Localization (.powers r)) (LocalizedModule (.powers r) M) ∧
Module.finrank (Localization (.powers r)) (LocalizedModule (.powers r) M) = Module.finrank Rₛ M' :=
by
let I := Module.Free.ChooseBasisIndex Rₛ M'
let b : Basis I Rₛ M' := Module.Free.chooseBasis Rₛ M'
have : Module.Finite Rₛ M' := Module.Finite.of_isLocalizedModule S (Rₚ := Rₛ) f
obtain ⟨r, hr, b', _⟩ := Module.FinitePresentation.exists_basis_localizedModule_powers S f Rₛ b
have :=
(show Localization (.powers r) →+* Rₛ from
IsLocalization.map (M := .powers r) (T := S) _ (RingHom.id _) (Submonoid.powers_le.mpr hr)).domain_nontrivial
refine ⟨r, hr, .of_basis b', ?_⟩
rw [Module.finrank_eq_nat_card_basis b, Module.finrank_eq_nat_card_basis b']
