Uniform vanishing of an ascending family of boundary maps

Pointwise eventual vanishing becomes uniform on a Noetherian source. The localized statement deliberately assumes Noetherianity only after localization.

theorem AlgebraicAnalysis.exists_uniform_zero_of_noetherian {R : Type u_1} {U : Type u_2} [Semiring R] [AddCommMonoid U] [Module R U] {V : ℕ → Type u_3} [(r : ℕ) → AddCommMonoid (V r)] [(r : ℕ) → Module R (V r)] (b : (r : ℕ) → U →ₗ[R] V r) (hmono : ∀ (r s : ℕ), r ≤ s → (b r).ker ≤ (b s).ker) (hpoint : ∀ (u : U), ∃ (r : ℕ), (b r) u = 0) [IsNoetherian R U] : ∃ (r : ℕ), b r = 0

theorem AlgebraicAnalysis.exists_uniform_subsingleton_of_noetherian {R : Type u_1} {U : Type u_2} [Semiring R] [AddCommMonoid U] [Module R U] {V : ℕ → Type u_3} [(r : ℕ) → AddCommMonoid (V r)] [(r : ℕ) → Module R (V r)] (b : (r : ℕ) → U →ₗ[R] V r) (hmono : ∀ (r s : ℕ), r ≤ s → (b r).ker ≤ (b s).ker) (hpoint : ∀ (u : U), ∃ (r : ℕ), (b r) u = 0) (hsurj : ∀ (r : ℕ), Function.Surjective ⇑(b r)) [IsNoetherian R U] : ∃ (r : ℕ), Subsingleton (V r)

theorem AlgebraicAnalysis.exists_uniform_zero_localized {R : Type u_1} [CommRing R] (S : Submonoid R) {U : Type u_2} [AddCommMonoid U] [Module R U] {V : ℕ → Type u_3} [(r : ℕ) → AddCommMonoid (V r)] [(r : ℕ) → Module R (V r)] (b : (r : ℕ) → U →ₗ[R] V r) (hmono : ∀ (r s : ℕ), r ≤ s → (b r).ker ≤ (b s).ker) (hpoint : ∀ (u : U), ∃ (r : ℕ), (b r) u = 0) [IsNoetherian (Localization S) (LocalizedModule S U)] : ∃ (r : ℕ), (LocalizedModule.map S) (b r) = 0

theorem AlgebraicAnalysis.exists_uniform_subsingleton_localized {R : Type u_1} [CommRing R] (S : Submonoid R) {U : Type u_2} [AddCommMonoid U] [Module R U] {V : ℕ → Type u_3} [(r : ℕ) → AddCommMonoid (V r)] [(r : ℕ) → Module R (V r)] (b : (r : ℕ) → U →ₗ[R] V r) (hmono : ∀ (r s : ℕ), r ≤ s → (b r).ker ≤ (b s).ker) (hpoint : ∀ (u : U), ∃ (r : ℕ), (b r) u = 0) (hsurj : ∀ (r : ℕ), Function.Surjective ⇑(b r)) [IsNoetherian (Localization S) (LocalizedModule S U)] : ∃ (r : ℕ), Subsingleton (LocalizedModule S (V r))