Finite-window complex models over a localization

A strictly bounded cochain complex of finite modules over a localization has a strictly bounded model with finite terms over the base ring. The model is isomorphic after termwise scalar extension as an ordinary cochain complex. There is no Noetherian hypothesis and no claim about descending arrows, derived localization, or a bounded semiorthogonal component.

The construction chooses a finite submodule B i of each restricted-scalar term and sets L i = B i ⊔ d(B (i - 1)). The next differential kills the second summand by d² = 0. Its restricted square is literally zero because each L i is a subtype of the original term; no localization faithfulness is used.

theorem CochainComplex.exists_finite_model_of_isLocalization {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (S : Submonoid R) [IsLocalization S A] (K : CochainComplex (ModuleCat A) ℤ) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] (hfinite : ∀ (i : ℤ), Module.Finite A ↑(K.X i)) : ∃ (L : CochainComplex (ModuleCat R) ℤ), (∀ (i : ℤ), Module.Finite R ↑(L.X i)) ∧ L.IsStrictlyGE a ∧ L.IsStrictlyLE b ∧ Nonempty (K ≅ ((ModuleCat.extendScalars (algebraMap R A)).mapHomologicalComplex (ComplexShape.up ℤ)).obj L)

A finite strict window of finite modules over a localization has a termwise finite model over the base ring, isomorphic after ordinary scalar extension. This is complex-object descent, not descent of a map or a derived or component-level statement.