English
If there exists a finite set t ⊆ R such that each localized module M_p is finite over R_p for p ∈ t, then M is finite over R.
Русский
Если существует конечный набор t ⊆ R, такой что каждый локализованный модуль M_p конечен над R_p для p ∈ t, то M конечен над R.
LaTeX
$$$\\exists t,\\text{ finite}, \\ \\, (\\forall g \\in t),\\ Module.Finite (Localization.Away g.val) (LocalizedModule (Submonoid.powers g.val) M) \\Rightarrow \\text{Module.Finite}(R,M)$$$
Lean4
/-- If there exists a finite set `{ r }` of `R` such that `Mᵣ` is `Rᵣ`-finite for each `r`,
then `M` is a finite `R`-module.
General version for any modules `Mᵣ` and rings `Rᵣ` satisfying the correct universal properties.
See `Module.Finite.of_localizationSpan_finite` for the specialized version.
See `of_localizationSpan'` for a version without the finite set assumption.
-/
theorem of_localizationSpan_finite' (t : Finset R) (ht : Ideal.span (t : Set R) = ⊤) {Mₚ : ∀ (_ : t), Type*}
[∀ (g : t), AddCommMonoid (Mₚ g)] [∀ (g : t), Module R (Mₚ g)] {Rₚ : ∀ (_ : t), Type u} [∀ (g : t), CommRing (Rₚ g)]
[∀ (g : t), Algebra R (Rₚ g)] [∀ (g : t), IsLocalization.Away g.val (Rₚ g)] [∀ (g : t), Module (Rₚ g) (Mₚ g)]
[∀ (g : t), IsScalarTower R (Rₚ g) (Mₚ g)] (f : ∀ (g : t), M →ₗ[R] Mₚ g)
[∀ (g : t), IsLocalizedModule (Submonoid.powers g.val) (f g)] (H : ∀ (g : t), Module.Finite (Rₚ g) (Mₚ g)) :
Module.Finite R M := by
classical
constructor
choose s₁ s₂ using (fun g ↦ (H g).1)
let sf := fun x : t ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers x.val) (f x) (s₁ x)
use t.attach.biUnion sf
rw [Submodule.span_attach_biUnion, eq_top_iff]
rintro x -
refine Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (t : Set R) ht _ (fun r ↦ ?_)
set S : Submonoid R := Submonoid.powers r.val
obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
multiple_mem_span_of_mem_localization_span S (Rₚ r) (s₁ r : Set (Mₚ r)) (IsLocalizedModule.mk' (f r) x (1 : S))
(by rw [s₂ r]; trivial)
rw [Submonoid.smul_def, ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_one] at hn₁
obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalizedModule.smul_mem_finsetIntegerMultiple_span S (f r) _ (s₁ r) hn₁
rw [Submonoid.smul_def] at hn₂
use n₂ + n₁
apply le_iSup (fun x : t ↦ Submodule.span R (sf x : Set M)) r
rw [pow_add, mul_smul]
exact hn₂
