Comparing projective dimensions, and subobjects of projectives

If every bound HasProjectiveDimensionLT X n on one object implies the same bound on another object Y, possibly in a different abelian category, then the projective dimension of Y is at most that of X. This compares projective dimensions degree by degree without unfolding their definition as an infimum.

In an abelian category with enough projectives, every object has projective dimension at most one if and only if every subobject of a projective object is projective. This is the hereditary condition, expressed using Mathlib's existing projective-dimension predicate.

A morphism f of projective objects shifts dimension by two between its kernel and its cokernel (CategoryTheory.hasProjectiveDimensionLT_cokernel_iff_kernel).

When every object has projective dimension at most one, the criterion shows that the cycles and boundaries of a complex of projective objects are projective. Surjections onto these boundaries then split, so the cycles split off the terms.

The chosen projective presentation 0 ⟶ ker π ⟶ P ⟶ X ⟶ 0 of an object is short exact (CategoryTheory.Projective.kernelShortComplex_shortExact).

When coproducts indexed by ι are exact, for instance for direct sums of modules, a coproduct of objects of projective dimension at most n has projective dimension at most n (CategoryTheory.hasProjectiveDimensionLT_of_isColimit_cofan). The index type is arbitrary, so this also covers countable direct sums in a category of modules in any universe.

References

• C. Weibel, An Introduction to Homological Algebra, Section 4.2 (hereditary rings).

theorem CategoryTheory.projectiveDimension_le_of_hasProjectiveDimensionLT {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {D : Type u_2} [Category.{v_2, u_2} D] [Abelian D] {X : C} {Y : D} (h : ∀ (n : ℕ), HasProjectiveDimensionLT X n → HasProjectiveDimensionLT Y n) : projectiveDimension Y ≤ projectiveDimension X

If every bound on the projective dimension of X is also a bound for Y, then the projective dimension of Y is at most that of X. The objects may lie in different abelian categories.

theorem CategoryTheory.projective_of_mono_of_hasProjectiveDimensionLE_one {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X Y : C} (f : X ⟶ Y) [Mono f] [Projective Y] [HasProjectiveDimensionLE (Limits.cokernel f) 1] : Projective X

A subobject of a projective object is projective if its quotient has projective dimension at most one.

theorem CategoryTheory.hasProjectiveDimensionLT_cokernel_iff_kernel {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {P Q : C} (f : P ⟶ Q) [Projective P] [Projective Q] (n : ℕ) : HasProjectiveDimensionLT (Limits.cokernel f) (n + 3) ↔ HasProjectiveDimensionLT (Limits.kernel f) (n + 1)

Dimension shifting along a morphism of projectives. For a morphism f : P ⟶ Q of projective objects, the exact sequence 0 ⟶ ker f ⟶ P ⟶ Q ⟶ coker f ⟶ 0 lowers the projective dimension of coker f by two: it is less than n + 3 exactly when that of ker f is less than n + 1.

theorem CategoryTheory.forall_hasProjectiveDimensionLE_one_iff_projective_of_mono (C : Type u_1) [Category.{v_1, u_1} C] [Abelian C] [EnoughProjectives C] : (∀ (X : C), HasProjectiveDimensionLE X 1) ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [Mono f] [Projective Y], Projective X

Every object has projective dimension at most one precisely when every monomorphism into a projective object has projective source.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Projective.kernelShortComplex {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] [EnoughProjectives C] (X : C) : ShortComplex C

The short complex ker π ⟶ P ⟶ X of the chosen projective presentation π : P ⟶ X.

theorem CategoryTheory.Projective.kernelShortComplex_shortExact {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] [EnoughProjectives C] (X : C) : (kernelShortComplex X).ShortExact

The chosen projective presentation 0 ⟶ ker π ⟶ P ⟶ X ⟶ 0 is short exact.

instance CategoryTheory.instProjectiveX₂KernelShortComplex (C : Type u_1) [Category.{v_1, u_1} C] [Abelian C] [EnoughProjectives C] (X : C) : Projective (Projective.kernelShortComplex X).X₂

theorem CategoryTheory.hasProjectiveDimensionLT_of_isColimit_cofan {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] [EnoughProjectives C] {ι : Type u_2} [Limits.HasColimitsOfShape (Discrete ι) C] [HasExactColimitsOfShape (Discrete ι) C] {X : ι → C} {c : Limits.Cofan X} (hc : Limits.IsColimit c) (n : ℕ) (h : ∀ (i : ι), HasProjectiveDimensionLT (X i) n) : HasProjectiveDimensionLT c.pt n

When coproducts indexed by ι are exact, the point of a colimit cofan of objects of projective dimension < n has projective dimension < n.

instance CategoryTheory.instHasProjectiveDimensionLTSigmaObj_tauCeti {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] [EnoughProjectives C] {ι : Type u_2} [Limits.HasColimitsOfShape (Discrete ι) C] [HasExactColimitsOfShape (Discrete ι) C] (X : ι → C) (n : ℕ) [∀ (i : ι), HasProjectiveDimensionLT (X i) n] : HasProjectiveDimensionLT (∐ X) n

When coproducts indexed by ι are exact, a coproduct of objects of projective dimension < n has projective dimension < n.