Two-out-of-three for pseudocoherent modules

Let 0 → M₁ → M → M₂ → 0 be a short exact sequence of modules over a ring R, given by an injective f : M₁ →ₗ[R] M and a surjective g : M →ₗ[R] M₂ with Function.Exact f g. This file shows how m-pseudocoherence (TauCeti.Huber.IsPseudoCoherentOver) moves along it:

• an extension of m-pseudocoherent modules is m-pseudocoherent;
• a cokernel loses at most one degree: if M₁ is (m - 1)-pseudocoherent and M is m-pseudocoherent, then M₂ is m-pseudocoherent, and in degree 0 nothing is asked of M₁;
• a kernel loses at most one degree: if M is m-pseudocoherent and M₂ is (m + 1)-pseudocoherent, then M₁ is m-pseudocoherent.

The degree m ranges over ℕ∞. Since ⊤ + 1 = ⊤ - 1 = ⊤, the case m = ⊤ says that if two of M₁, M, M₂ are pseudocoherent then so is the third, so pseudocoherent modules are closed under extensions, kernels of surjections and cokernels of injections. This is the module theory that makes pseudocoherent modules, unlike finitely presented ones, behave well over rings that are not coherent.

Main results

• TauCeti.Huber.IsPseudoCoherentOver.extension: extensions of m-pseudocoherent modules are m-pseudocoherent.
• TauCeti.Huber.IsPseudoCoherentOver.cokernel: the cokernel of an injection from an (m - 1)-pseudocoherent module into an m-pseudocoherent module is m-pseudocoherent.
• TauCeti.Huber.IsPseudoCoherentOver.kernel: the kernel of a surjection from an m-pseudocoherent module onto an (m + 1)-pseudocoherent module is m-pseudocoherent.

References

• K. S. Kedlaya and R. Liu, Relative p-adic Hodge theory, II: Imperfect period rings, §1.1, Lemma 1.1.5.
• The Stacks Project, Lemma 15.66.2, Tag 064R (with the index negated).

theorem TauCeti.Huber.IsPseudoCoherentOver.extension {R : Type u} [Ring R] {M₁ : Type u_1} {M : Type u_2} {M₂ : Type u_3} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {f : M₁ →ₗ[R] M} {g : M →ₗ[R] M₂} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) {m : ℕ∞} (h₁ : IsPseudoCoherentOver R M₁ m) (h₂ : IsPseudoCoherentOver R M₂ m) : IsPseudoCoherentOver R M m

Extensions of m-pseudocoherent modules are m-pseudocoherent. If 0 → M₁ → M → M₂ → 0 is exact and M₁ and M₂ are m-pseudocoherent, so is M (Kedlaya–Liu II, Lemma 1.1.5(a); Stacks, Tag 064R).

theorem TauCeti.Huber.IsPseudoCoherentOver.cokernel {R : Type u} [Ring R] {M₁ : Type u_1} {M : Type u_2} {M₂ : Type u_3} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {f : M₁ →ₗ[R] M} {g : M →ₗ[R] M₂} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) {m : ℕ∞} (h₁ : 0 < m → IsPseudoCoherentOver R M₁ (m - 1)) (hM : IsPseudoCoherentOver R M m) : IsPseudoCoherentOver R M₂ m

A cokernel loses at most one degree of pseudocoherence. If 0 → M₁ → M → M₂ → 0 is exact, M is m-pseudocoherent and, when m > 0, M₁ is (m - 1)-pseudocoherent, then M₂ is m-pseudocoherent; in degree 0 this only says that a quotient of a finitely generated module is finitely generated (Kedlaya–Liu II, Lemma 1.1.5(b); Stacks, Tag 064R).

theorem TauCeti.Huber.IsPseudoCoherentOver.kernel {R : Type u} [Ring R] {M₁ : Type u_1} {M : Type u_2} {M₂ : Type u_3} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {f : M₁ →ₗ[R] M} {g : M →ₗ[R] M₂} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) {m : ℕ∞} (hM : IsPseudoCoherentOver R M m) (h₂ : IsPseudoCoherentOver R M₂ (m + 1)) : IsPseudoCoherentOver R M₁ m

A kernel loses at most one degree of pseudocoherence. If 0 → M₁ → M → M₂ → 0 is exact, M is m-pseudocoherent and M₂ is (m + 1)-pseudocoherent, then M₁ is m-pseudocoherent (Kedlaya–Liu II, Lemma 1.1.5(c); Stacks, Tag 064R).