Three-term descent with a fixed terminal module

Let A be a localization of a Noetherian ring R. A zero-composite diagram M₀ → M₁ → A ⊗[R] T, with the first two A-modules finite and T an arbitrary R-module, descends to L₀ → L₁ → T. Both Lᵢ are finitely presented over R; the original arrows agree with their scalar extensions through specified equivalences.

The zero composite cannot be inferred just because its scalar extension is zero: T may have S-torsion. Finite presentation supplies one denominator annihilating the descended composite. Scaling the first arrow and its source equivalence by inverse localization units then makes the composite exactly zero without changing either comparison equation.

This is a module-level diagram witness. It does not package a ShortComplex or prove a derived, geometric, or heart-level extension theorem.

theorem Module.exists_finitely_presented_fixedTerminalThreeTerm_of_isLocalization {R : Type u_1} {A : Type u_2} {M₀ : Type u_3} {M₁ : Type u_4} {T : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (S : Submonoid R) [IsLocalization S A] [IsNoetherianRing R] [AddCommGroup M₀] [Module R M₀] [Module A M₀] [IsScalarTower R A M₀] [AddCommGroup M₁] [Module R M₁] [Module A M₁] [IsScalarTower R A M₁] [Module.Finite A M₀] [Module.Finite A M₁] [AddCommGroup T] [Module R T] (d : M₀ →ₗ[A] M₁) (β : M₁ →ₗ[A] TensorProduct R A T) (hz : β ∘ₗ d = 0) : ∃ (L₀ : Submodule R M₀) (L₁ : Submodule R M₁), FinitePresentation R ↥L₀ ∧ FinitePresentation R ↥L₁ ∧ ∃ (d₀ : ↥L₀ →ₗ[R] ↥L₁) (f : ↥L₁ →ₗ[R] T) (e₀ : M₀ ≃ₗ[A] TensorProduct R A ↥L₀) (e₁ : M₁ ≃ₗ[A] TensorProduct R A ↥L₁), f ∘ₗ d₀ = 0 ∧ ↑e₁ ∘ₗ d = (IsLocalizedModule.mapExtendScalars S ((TensorProduct.mk R A ↥L₀) 1) ((TensorProduct.mk R A ↥L₁) 1) A) d₀ ∘ₗ ↑e₀ ∧ β = (IsLocalizedModule.mapExtendScalars S ((TensorProduct.mk R A ↥L₁) 1) ((TensorProduct.mk R A T) 1) A) f ∘ₗ ↑e₁

Descend a zero-composite three-term module diagram with fixed terminal R-module T. Only M₀ and M₁ must be finite over the localization; T may be arbitrary. The equivalences need not be induced by the submodule inclusions, since clearing the composite rescales the first equivalence.