Flat base change of pseudocoherent modules

Extension of scalars along a flat algebra preserves pseudocoherence, in every finite degree and in degree infinity. In particular localizations of pseudocoherent modules are pseudocoherent. This supplies the module-theoretic stability needed for flat pullback of locally pseudocoherent sheaves. No Noetherian or finite-presentation hypothesis is imposed on the algebra.

The proof tensors the finite free resolution defining TauCeti.Huber.IsPseudoCoherentOver. It uses Mathlib's Module.Flat.lTensor_exact for exactness and TensorProduct.piScalarRight to put the resulting free modules in coordinate form.

References

• The Stacks Project, Lemma 15.66.13, Tag 066C (flat base change).

theorem TauCeti.Huber.IsPseudoCoherentOver.baseChange {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {m : ℕ∞} (h : IsPseudoCoherentOver R M m) (S : Type u_3) [CommRing S] [Algebra R S] [Module.Flat R S] : IsPseudoCoherentOver S (TensorProduct R S M) m

Flat extension of scalars preserves m-pseudocoherence, including m = ⊤.

theorem TauCeti.Huber.IsPseudoCoherentOver.of_isLocalizedModule {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {m : ℕ∞} (h : IsPseudoCoherentOver R M m) (p : Submonoid R) {Rₚ : Type u_3} [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization p Rₚ] {Mₚ : Type u_4} [AddCommGroup Mₚ] [Module R Mₚ] [Module Rₚ Mₚ] [IsScalarTower R Rₚ Mₚ] (f : M →ₗ[R] Mₚ) [IsLocalizedModule p f] : IsPseudoCoherentOver Rₚ Mₚ m

Localizations of pseudocoherent modules are pseudocoherent. If M is m-pseudocoherent over R and f : M → Mₚ is a localization of M at a submonoid p, then Mₚ is m-pseudocoherent over the corresponding localization Rₚ of R.