Pseudocoherent modules

A module M over a ring R is m-pseudocoherent, for m ∈ ℕ ∪ {∞}, when it has a resolution ⋯ → F₁ → F₀ → M → 0 by finite free modules that is exact at M, F₀, …, F_{m-1}: only the terms F₀, …, F_m of the resolution matter. It is pseudocoherent when it is ∞-pseudocoherent. The notion is a property of the module alone. A module is 0-pseudocoherent exactly when it is finitely generated and 1-pseudocoherent exactly when it is finitely presented. Over a coherent ring, for instance a noetherian ring, every finitely presented module is pseudocoherent, but in general m-pseudocoherence becomes strictly stronger as m grows. Pseudocoherent modules replace finitely presented ones in the module theory of sheafy rings that are not noetherian.

The predicate TauCeti.Huber.IsPseudoCoherentOver R M m uses coordinate resolutions: the terms are the modules Fin k → R, and exactness is Function.Exact.

The main results describe pseudocoherence one degree at a time. M is (m + 1)-pseudocoherent exactly when the kernel of a surjection onto M from a finite free module is m-pseudocoherent, and then the kernel of every surjection from a finitely generated projective module is m-pseudocoherent. The second statement rests on Schanuel's lemma (TauCeti.exists_linearEquiv_comp_fst_eq_comp_snd_comp). It allows a resolution to be extended one step at a time, which shows that pseudocoherence is pseudocoherence in every finite degree.

Main definitions

• TauCeti.Huber.IsPseudoCoherentOver R M m: M has a finite free resolution exact at M, F₀, …, F_{m-1}.

Main results

• TauCeti.Huber.IsPseudoCoherentOver.zero_iff, TauCeti.Huber.IsPseudoCoherentOver.one_iff: 0-pseudocoherent means finitely generated, and 1-pseudocoherent means finitely presented.
• TauCeti.Huber.IsPseudoCoherentOver.succ_iff_ker: for a surjection f from a finite free module, M is (m + 1)-pseudocoherent exactly when ker f is m-pseudocoherent.
• TauCeti.Huber.IsPseudoCoherentOver.ker_of_projective: the kernel of a surjection from a finitely generated projective module onto an (m + 1)-pseudocoherent module is m-pseudocoherent.
• TauCeti.Huber.IsPseudoCoherentOver.top_iff: a module is pseudocoherent exactly when it is m-pseudocoherent for every natural number m.
• TauCeti.Huber.IsPseudoCoherentOver.of_projective: finitely generated projective modules are pseudocoherent.
• TauCeti.Huber.IsPseudoCoherentOver.prod: products of m-pseudocoherent modules are m-pseudocoherent.
• TauCeti.Huber.IsPseudoCoherentOver.pi: finite products of m-pseudocoherent modules are m-pseudocoherent.
• TauCeti.Huber.IsPseudoCoherentOver.of_isNoetherianRing: over a noetherian ring, finitely generated modules are pseudocoherent.

References

• K. S. Kedlaya and R. Liu, Relative p-adic Hodge theory, II: Imperfect period rings, §1.1, Definition 1.1.1 and Remark 1.1.6.
• The Stacks Project, Tags 064Q, 064T, 064U and 066E (with the index negated).

def TauCeti.Huber.IsPseudoCoherentOver (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] (m : ℕ∞) : Prop

M is m-pseudocoherent over R: it has a resolution ⋯ → F₁ → F₀ → M → 0 by finite free modules Fᵢ = Fin (n i) → R, with augmentation ε and differentials d i : Fᵢ₊₁ → Fᵢ, which is exact at M, F₀, …, F_{m-1}. Thus 0-pseudocoherent means finitely generated, 1-pseudocoherent means finitely presented, and for m = ⊤ the whole resolution is exact (Kedlaya–Liu II, Definition 1.1.1; Stacks, Tag 064T, with the index negated).

theorem TauCeti.Huber.isPseudoCoherentOver_iff (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] (m : ℕ∞) : IsPseudoCoherentOver R M m ↔ ∃ (n : ℕ → ℕ) (d : (i : ℕ) → (Fin (n (i + 1)) → R) →ₗ[R] Fin (n i) → R) (ε : (Fin (n 0) → R) →ₗ[R] M), Function.Surjective ⇑ε ∧ (1 ≤ m → Function.Exact ⇑(d 0) ⇑ε) ∧ ∀ (i : ℕ), ↑(i + 2) ≤ m → Function.Exact ⇑(d (i + 1)) ⇑(d i)

M is m-pseudocoherent over R if and only if it has a resolution ⋯ → Fin (n 1) → R → Fin (n 0) → R → M → 0, with augmentation ε and differentials d i, that is exact at M, F₀, …, F_{m-1}.

theorem TauCeti.Huber.IsPseudoCoherentOver.mono {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {m m' : ℕ∞} (h : IsPseudoCoherentOver R M m) (hm : m' ≤ m) : IsPseudoCoherentOver R M m'

An m-pseudocoherent module is m'-pseudocoherent for every m' ≤ m.

theorem TauCeti.Huber.IsPseudoCoherentOver.of_equiv {R : Type u} {M : Type v} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {m : ℕ∞} (e : M ≃ₗ[R] N) (h : IsPseudoCoherentOver R M m) : IsPseudoCoherentOver R N m

Pseudocoherence is invariant under linear equivalence.

theorem TauCeti.Huber.IsPseudoCoherentOver.finite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {m : ℕ∞} (h : IsPseudoCoherentOver R M m) : Module.Finite R M

A pseudocoherent module, in any degree, is finitely generated.

@[simp]

theorem TauCeti.Huber.IsPseudoCoherentOver.zero_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] : IsPseudoCoherentOver R M 0 ↔ Module.Finite R M

0-pseudocoherent means finitely generated.

theorem TauCeti.Huber.IsPseudoCoherentOver.succ_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {m : ℕ∞} : IsPseudoCoherentOver R M (m + 1) ↔ ∃ (k : ℕ) (f : (Fin k → R) →ₗ[R] M), Function.Surjective ⇑f ∧ IsPseudoCoherentOver R (↥f.ker) m

Pseudocoherence one degree at a time. M is (m + 1)-pseudocoherent exactly when there is a surjection onto M from a finite free module whose kernel is m-pseudocoherent.

theorem TauCeti.Huber.IsPseudoCoherentOver.of_projective {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : IsPseudoCoherentOver R M ⊤

Finitely generated projective modules are ⊤-pseudocoherent.

@[simp]

theorem TauCeti.Huber.IsPseudoCoherentOver.one_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] : IsPseudoCoherentOver R M 1 ↔ Module.FinitePresentation R M

1-pseudocoherent means finitely presented.

theorem TauCeti.Huber.IsPseudoCoherentOver.finitePresentation {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {m : ℕ∞} (h : IsPseudoCoherentOver R M m) (hm : 1 ≤ m) : Module.FinitePresentation R M

A module that is pseudocoherent in some positive degree is finitely presented.

Products, and cancellation of free summands, in finite degrees

Kernels of maps between finite free modules lie in the universe of the ring, so the inductions on the degree run there. A finitely generated module M is equivalent to a quotient of some Rᵏ, which lies in that universe.

Pseudocoherence in every finite degree

theorem TauCeti.Huber.IsPseudoCoherentOver.top_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] : IsPseudoCoherentOver R M ⊤ ↔ ∀ (m : ℕ), IsPseudoCoherentOver R M ↑m

Pseudocoherence is pseudocoherence in every finite degree. M is ⊤-pseudocoherent exactly when it is m-pseudocoherent for every natural number m (Stacks, Tag 064U).

theorem TauCeti.Huber.IsPseudoCoherentOver.prod {R : Type u} {M : Type v} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {m : ℕ∞} (h₁ : IsPseudoCoherentOver R M m) (h₂ : IsPseudoCoherentOver R N m) : IsPseudoCoherentOver R (M × N) m

Products of m-pseudocoherent modules are m-pseudocoherent.

theorem TauCeti.Huber.IsPseudoCoherentOver.pi {R : Type u} [Ring R] {m : ℕ∞} {ι : Type u_1} [Finite ι] {M : ι → Type u_2} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (h : ∀ (i : ι), IsPseudoCoherentOver R (M i) m) : IsPseudoCoherentOver R ((i : ι) → M i) m

Finite products of m-pseudocoherent modules are m-pseudocoherent.

theorem TauCeti.Huber.IsPseudoCoherentOver.ker_of_projective {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {m : ℕ∞} {P : Type u_1} [AddCommGroup P] [Module R P] [Module.Finite R P] [Module.Projective R P] (h : IsPseudoCoherentOver R M (m + 1)) {f : P →ₗ[R] M} (hf : Function.Surjective ⇑f) : IsPseudoCoherentOver R (↥f.ker) m

Kernels of surjections from projective modules. If M is (m + 1)-pseudocoherent, the kernel of every surjection onto M from a finitely generated projective module is m-pseudocoherent.

theorem TauCeti.Huber.IsPseudoCoherentOver.succ_iff_ker {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {m : ℕ∞} {F : Type u_1} [AddCommGroup F] [Module R F] [Module.Free R F] [Module.Finite R F] {f : F →ₗ[R] M} (hf : Function.Surjective ⇑f) : IsPseudoCoherentOver R M (m + 1) ↔ IsPseudoCoherentOver R (↥f.ker) m

For a surjection f onto M from a finite free module, M is (m + 1)-pseudocoherent exactly when ker f is m-pseudocoherent (Stacks, Tag 064T, with the index negated).

theorem TauCeti.Huber.IsPseudoCoherentOver.of_isNoetherianRing {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : IsPseudoCoherentOver R M ⊤

Over a noetherian ring, finitely generated modules are pseudocoherent (Stacks, Tag 066E).