Fixed-target arrows over a localized ring

Let A be a localization of a Noetherian ring R. An arrow from a finite A-module N into the base change of an arbitrary R-module T comes from an arrow into that same target T, after replacing the domain by a finitely presented R-module whose base change is isomorphic to N.

The domain is obtained by finite module descent. Finite presentation then localizes its Hom module, and a denominator is absorbed into the domain isomorphism. This is a module-level statement: it does not descend complexes or establish fixed-target extension in a derived category or a t-heart.

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

Over a localization of a Noetherian ring, every arrow from a finite localized module into the base change of a fixed R-module descends after changing its domain by an isomorphism. The target T need not be finite.