English
If there exists a finite set t ⊆ R, and 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
$$$\\forall t,\\|t\\|<\\infty, \\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 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.
-/
theorem of_localizationSpan' (t : Set R) (ht : Ideal.span t = ⊤) {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)] [h₁ : ∀ (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)
[h₂ : ∀ (g : t), IsLocalizedModule (Submonoid.powers g.val) (f g)] (H : ∀ (g : t), Module.Finite (Rₚ g) (Mₚ g)) :
Module.Finite R M := by
rw [Ideal.span_eq_top_iff_finite] at ht
obtain ⟨t', hc, ht'⟩ := ht
have (g : t') : IsLocalization.Away g.val (Rₚ ⟨g.val, hc g.property⟩) := h₁ ⟨g.val, hc g.property⟩
have (g : t') : IsLocalizedModule (Submonoid.powers g.val) ((fun g ↦ f ⟨g.val, hc g.property⟩) g) :=
h₂ ⟨g.val, hc g.property⟩
apply of_localizationSpan_finite' t' ht' (fun g ↦ f ⟨g.val, hc g.property⟩) (fun g ↦ H ⟨g.val, hc g.property⟩)
