Finite module descent through localization

A finite module over a localized ring is obtained by extending scalars from the finite base-ring submodule generated by a chosen finite set of localized generators. Over a Noetherian base that submodule is finitely presented.

These are module-level object lifts and closure steps for one or two arrows. They do not descend a complex, a map of complexes, or a bounded-coherent semiorthogonal component.

theorem Module.exists_finite_submodule_of_isLocalization {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (S : Submonoid R) [IsLocalization S A] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] [Module.Finite A N] : ∃ (L : Submodule R N), Module.Finite R ↥L ∧ IsLocalizedModule S L.subtype ∧ Nonempty (TensorProduct R A ↥L ≃ₗ[A] N)

A finite module over a localization has a finite base-ring submodule whose scalar extension is the original module.

theorem Module.exists_finitely_presented_submodule_of_isLocalization {R : Type u_1} {A : Type u_2} {N : Type u_3} [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] : ∃ (L : Submodule R N), FinitePresentation R ↥L ∧ IsLocalizedModule S L.subtype ∧ Nonempty (TensorProduct R A ↥L ≃ₗ[A] N)

Over a Noetherian base ring the descended finite submodule is finitely presented.

theorem Module.exists_finite_submodule_of_isLocalization_containing {R : Type u_1} {A : Type u_2} {N : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (S : Submonoid R) [IsLocalization S A] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] [Module.Finite A N] (F : Submodule R N) [Module.Finite R ↥F] : ∃ (L : Submodule R N), F ≤ L ∧ Module.Finite R ↥L ∧ IsLocalizedModule S L.subtype

The finite descent witness can be chosen to contain any prescribed finite base-ring submodule. This permits adjoining images of a differential before descending the next term of a bounded complex.

theorem Module.exists_finitely_presented_submodule_of_isLocalization_containing {R : Type u_1} {A : Type u_2} {N : Type u_3} [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] (F : Submodule R N) [Module.Finite R ↥F] : ∃ (L : Submodule R N), F ≤ L ∧ FinitePresentation R ↥L ∧ IsLocalizedModule S L.subtype

Over a Noetherian base, the prescribed-set descent witness is finitely presented as well as finite.

theorem Module.exists_finite_submodules_of_isLocalization_map {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing A] [Algebra R A] (S : Submonoid R) [IsLocalization S A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] [Module.Finite A M] [Module.Finite A N] (f : M →ₗ[A] N) : ∃ (L : Submodule R M) (K : Submodule R N), Module.Finite R ↥L ∧ Module.Finite R ↥K ∧ IsLocalizedModule S L.subtype ∧ IsLocalizedModule S K.subtype ∧ Submodule.map (↑R f) L ≤ K

A map between finite modules over a localization has finite base-ring submodules on both sides that localize back to the given modules and are closed under that map. This is the one-arrow step toward descending a bounded complex; no complex or component descent is asserted here.

theorem Module.exists_finite_submodules_of_isLocalization_two_maps {R : Type u_1} {A : Type u_2} {M₀ : Type u_3} {M₁ : Type u_4} {M₂ : Type u_5} [CommRing R] [CommRing A] [Algebra R A] (S : Submonoid R) [IsLocalization S A] [AddCommGroup M₀] [Module R M₀] [Module A M₀] [IsScalarTower R A M₀] [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₁] [Module.Finite A M₂] (f₀ : M₀ →ₗ[A] M₁) (f₁ : M₁ →ₗ[A] M₂) : ∃ (L₀ : Submodule R M₀) (L₁ : Submodule R M₁) (L₂ : Submodule R M₂), Module.Finite R ↥L₀ ∧ Module.Finite R ↥L₁ ∧ Module.Finite R ↥L₂ ∧ IsLocalizedModule S L₀.subtype ∧ IsLocalizedModule S L₁.subtype ∧ IsLocalizedModule S L₂.subtype ∧ Submodule.map (↑R f₀) L₀ ≤ L₁ ∧ Submodule.map (↑R f₁) L₁ ≤ L₂

Three finite modules over a localization admit finite base-ring submodules that localize back to them and are simultaneously closed under two consecutive arrows. The theorem supplies submodules and closure only. A zero-composite hypothesis on the original arrows must be supplied and checked on the restricted arrows before these data form a complex.