Modules of finite projective dimension

A module M over a ring R is m-fpd when it has a resolution 0 → P_m → ⋯ → P₁ → P₀ → M → 0 of length at most m by finitely generated projective modules. Following Kedlaya–Liu, TauCeti.Module.IsFPD R M m states this with a finite free resolution ⋯ → F₁ → F₀ → M → 0, exact everywhere, whose m-th syzygy is projective: the syzygy is M itself when m = 0 and the image of F_m → F_{m-1} otherwise. Cutting the resolution at that syzygy gives a finite projective resolution of length m. In particular every m-fpd module is pseudocoherent.

The main result identifies the definition with Mathlib's projective dimension: M is m-fpd exactly when it is pseudocoherent and HasProjectiveDimensionLE (ModuleCat.of R M) m. The proof is dimension shifting along 0 → ker ε → F₀ → M → 0, and it shows that the projectivity of the m-th syzygy does not depend on the chosen resolution. From it, M is (m + 1)-fpd exactly when the kernel of some, equivalently every, surjection onto M from a finitely generated projective module is m-fpd.

Main definitions

• TauCeti.Module.IsFPD R M m: M has a finite free resolution, exact everywhere, whose m-th syzygy is projective.

Main results

• TauCeti.Module.IsFPD.isPseudoCoherentOver: an m-fpd module is pseudocoherent.
• TauCeti.Module.IsFPD.zero_iff: 0-fpd means finitely generated and projective.
• TauCeti.Module.IsFPD.mono: an m-fpd module is m'-fpd for every m' ≥ m.
• TauCeti.Module.isFPD_iff_hasProjectiveDimensionLE: M is m-fpd exactly when it is pseudocoherent of projective dimension at most m.
• TauCeti.Module.IsFPD.succ_iff_ker: for a surjection f onto M from a finitely generated projective module, M is (m + 1)-fpd exactly when ker f is m-fpd.
• TauCeti.Module.IsFPD.cokernel: in a short exact sequence 0 → M₁ → M → M₂ → 0 with M₁ m-fpd and M (m + 1)-fpd, M₂ is (m + 1)-fpd.

References

• K. S. Kedlaya and R. Liu, Relative p-adic Hodge theory, II: Imperfect period rings, §1.1, Definition 1.1.1.

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

M is m-fpd over R: it has a resolution 0 → P_m → ⋯ → P₀ → M → 0 of length at most m by finitely generated projective modules (Kedlaya–Liu II, Definition 1.1.1). It is stated with a resolution ⋯ → F₁ → F₀ → M → 0 by finite free modules Fᵢ = Fin (n i) → R, exact everywhere, whose m-th syzygy is projective: M itself when m = 0, and the image of d (m - 1) : F_m → F_{m-1} otherwise.

theorem TauCeti.Module.isFPD_iff (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] (m : ℕ) : IsFPD R M m ↔ ∃ (n : ℕ → ℕ) (d : (i : ℕ) → (Fin (n (i + 1)) → R) →ₗ[R] Fin (n i) → R) (ε : (Fin (n 0) → R) →ₗ[R] M), Function.Surjective ⇑ε ∧ Function.Exact ⇑(d 0) ⇑ε ∧ (∀ (i : ℕ), Function.Exact ⇑(d (i + 1)) ⇑(d i)) ∧ (m = 0 → Module.Projective R M) ∧ ∀ (k : ℕ), m = k + 1 → Module.Projective R ↥(d k).range

M is m-fpd over R if and only if it has a finite free resolution ⋯ → Fin (n 1) → R → Fin (n 0) → R → M → 0, exact everywhere, whose m-th syzygy is projective.

theorem TauCeti.Module.IsFPD.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 : IsFPD R M m) : IsFPD R N m

Finite projective dimension is invariant under linear equivalence.

theorem TauCeti.Module.IsFPD.isPseudoCoherentOver {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {m : ℕ} (h : IsFPD R M m) : Huber.IsPseudoCoherentOver R M ⊤

A module of finite projective dimension is pseudocoherent.

@[simp]

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

0-fpd means finitely generated and projective.

theorem TauCeti.Module.IsFPD.of_projective {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : IsFPD R M 0

Finitely generated projective modules are 0-fpd.

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

An m-fpd module is m'-fpd for every m' ≥ m.

Comparison with projective dimension

theorem TauCeti.Module.isFPD_iff_hasProjectiveDimensionLE {R : Type u} [Ring R] {M : Type u} [AddCommGroup M] [Module R M] {m : ℕ} : IsFPD R M m ↔ Huber.IsPseudoCoherentOver R M ⊤ ∧ CategoryTheory.HasProjectiveDimensionLE (↧M) m

Finite projective dimension is pseudocoherence with bounded projective dimension. A module M is m-fpd exactly when it is pseudocoherent and HasProjectiveDimensionLE (ModuleCat.of R M) m, that is, Ext^i(M, -) vanishes for i > m.

theorem TauCeti.Module.IsFPD.succ_iff_ker {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {m : ℕ} {P : Type w} [AddCommGroup P] [Module R P] [Module.Finite R P] [Module.Projective R P] {f : P →ₗ[R] M} (hf : Function.Surjective ⇑f) : IsFPD R M (m + 1) ↔ IsFPD R (↥f.ker) m

Finite projective dimension one degree at a time. For a surjection f onto M from a finitely generated projective module, M is (m + 1)-fpd exactly when ker f is m-fpd. In particular the condition on ker f does not depend on f.

theorem TauCeti.Module.IsFPD.cokernel {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {m : ℕ} {M₁ : Type u_1} {M₂ : Type u_2} [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) (h₁ : IsFPD R M₁ m) (h : IsFPD R M (m + 1)) : IsFPD R M₂ (m + 1)

A cokernel of m-fpd modules is (m + 1)-fpd. If 0 → M₁ → M → M₂ → 0 is exact, M₁ is m-fpd and M is (m + 1)-fpd, then M₂ is (m + 1)-fpd (Kedlaya–Liu II, Lemma 1.1.5).