Projective dimension

In an abelian category C, we shall say that X : C has projective dimension < n if all Ext X Y i vanish when n ≤ i. This defines a type class HasProjectiveDimensionLT X n. We also define a type class HasProjectiveDimensionLE X n as an abbreviation for HasProjectiveDimensionLT X (n + 1). (Note that the fact that X is a zero object is equivalent to the condition HasProjectiveDimensionLT X 0, but this cannot be expressed in terms of HasProjectiveDimensionLE.)

We also define the projective dimension in WithBot ℕ∞ as projectiveDimension, projectiveDimension X = ⊥ iff X is zero and acts in common sense in the non-negative values.

class CategoryTheory.HasProjectiveDimensionLT {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (n : ℕ) : Prop

An object X in an abelian category has projective dimension < n if all Ext X Y i vanish when n ≤ i. See also HasProjectiveDimensionLE. (Do not use the subsingleton' field directly. Use the constructor HasProjectiveDimensionLT.mk, and the lemmas hasProjectiveDimensionLT_iff and Ext.eq_zero_of_hasProjectiveDimensionLT.)

• mk' :: (
• subsingleton' (i : ℕ) (hi : n ≤ i) ⦃Y : C⦄ : Subsingleton (Abelian.Ext X Y i)
• )

@[reducible, inline]

abbrev CategoryTheory.HasProjectiveDimensionLE {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (n : ℕ) : Prop

An object X in an abelian category has projective dimension ≤ n if all Ext X Y i vanish when n + 1 ≤ i

Equations

• CategoryTheory.HasProjectiveDimensionLE X n = CategoryTheory.HasProjectiveDimensionLT X (n + 1)

theorem CategoryTheory.HasProjectiveDimensionLT.subsingleton {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X : C) (n : ℕ) [hX : HasProjectiveDimensionLT X n] (i : ℕ) (hi : n ≤ i) (Y : C) : Subsingleton (Abelian.Ext X Y i)

theorem CategoryTheory.HasProjectiveDimensionLT.mk {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X : C} {n : ℕ} (hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Abelian.Ext X Y i), e = 0) : HasProjectiveDimensionLT X n

theorem CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} {i : ℕ} (e : Ext X Y i) (n : ℕ) [HasProjectiveDimensionLT X n] (hi : n ≤ i) : e = 0

theorem CategoryTheory.hasProjectiveDimensionLT_iff {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (n : ℕ) [HasExt C] : HasProjectiveDimensionLT X n ↔ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Abelian.Ext X Y i), e = 0

theorem CategoryTheory.Limits.IsZero.hasProjectiveDimensionLT_zero {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (hX : IsZero X) : HasProjectiveDimensionLT X 0

instance CategoryTheory.instHasProjectiveDimensionLTOfNatNat {C : Type u} [Category.{v, u} C] [Abelian C] : HasProjectiveDimensionLT 0 0

theorem CategoryTheory.isZero_of_hasProjectiveDimensionLT_zero {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) [HasProjectiveDimensionLT X 0] : Limits.IsZero X

theorem CategoryTheory.hasProjectiveDimensionLT_zero_iff_isZero {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) : HasProjectiveDimensionLT X 0 ↔ Limits.IsZero X

theorem CategoryTheory.hasProjectiveDimensionLT_of_ge {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (n m : ℕ) (h : n ≤ m) [HasProjectiveDimensionLT X n] : HasProjectiveDimensionLT X m

instance CategoryTheory.instHasProjectiveDimensionLTHAddNat {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (n : ℕ) [HasProjectiveDimensionLT X n] (k : ℕ) : HasProjectiveDimensionLT X (n + k)

instance CategoryTheory.instHasProjectiveDimensionLTHAddNat_1 {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (n : ℕ) [HasProjectiveDimensionLT X n] (k : ℕ) : HasProjectiveDimensionLT X (k + n)

instance CategoryTheory.instHasProjectiveDimensionLTSucc {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (n : ℕ) [HasProjectiveDimensionLT X n] : HasProjectiveDimensionLT X n.succ

instance CategoryTheory.instHasProjectiveDimensionLTOfNatNatOfProjective {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) [Projective X] : HasProjectiveDimensionLT X 1

theorem CategoryTheory.projective_iff_subsingleton_ext_one {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X : C} : Projective X ↔ ∀ ⦃Y : C⦄, Subsingleton (Abelian.Ext X Y 1)

theorem CategoryTheory.projective_iff_hasProjectiveDimensionLT_one {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) : Projective X ↔ HasProjectiveDimensionLT X 1

theorem CategoryTheory.Retract.hasProjectiveDimensionLT {C : Type u} [Category.{v, u} C] [Abelian C] {X Y : C} (h : Retract X Y) (n : ℕ) [HasProjectiveDimensionLT Y n] : HasProjectiveDimensionLT X n

theorem CategoryTheory.hasProjectiveDimensionLT_of_iso {C : Type u} [Category.{v, u} C] [Abelian C] {X X' : C} (e : X ≅ X') (n : ℕ) [HasProjectiveDimensionLT X n] : HasProjectiveDimensionLT X' n

theorem CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₂ {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) (n : ℕ) (h₁ : HasProjectiveDimensionLT S.X₁ n) (h₃ : HasProjectiveDimensionLT S.X₃ n) : HasProjectiveDimensionLT S.X₂ n

theorem CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃ {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) (n : ℕ) (h₁ : HasProjectiveDimensionLT S.X₁ n) (h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)) : HasProjectiveDimensionLT S.X₃ (n + 1)

theorem CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₁ {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) (n : ℕ) (h₂ : HasProjectiveDimensionLT S.X₂ n) (h₃ : HasProjectiveDimensionLT S.X₃ (n + 1)) : HasProjectiveDimensionLT S.X₁ n

theorem CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) (n : ℕ) (h₂ : Projective S.X₂) : HasProjectiveDimensionLT S.X₃ (n + 2) ↔ HasProjectiveDimensionLT S.X₁ (n + 1)

instance CategoryTheory.instHasProjectiveDimensionLTBiprod {C : Type u} [Category.{v, u} C] [Abelian C] (X Y : C) (n : ℕ) [HasProjectiveDimensionLT X n] [HasProjectiveDimensionLT Y n] : HasProjectiveDimensionLT (X ⊞ Y) n

noncomputable def CategoryTheory.projectiveDimension {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) : WithBot ℕ∞

The projective dimension of an object in an abelian category.

Equations

• CategoryTheory.projectiveDimension X = sInf {n : WithBot ℕ∞ | ∀ (i : ℕ), n < ↑i → CategoryTheory.HasProjectiveDimensionLT X i}

theorem CategoryTheory.projectiveDimension_eq_of_iso {C : Type u} [Category.{v, u} C] [Abelian C] {X Y : C} (e : X ≅ Y) : projectiveDimension X = projectiveDimension Y

theorem CategoryTheory.Retract.projectiveDimension_le {C : Type u} [Category.{v, u} C] [Abelian C] {X Y : C} (h : Retract X Y) : projectiveDimension X ≤ projectiveDimension Y

theorem CategoryTheory.projectiveDimension_lt_iff {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} {n : ℕ} : projectiveDimension X < ↑n ↔ HasProjectiveDimensionLT X n

theorem CategoryTheory.projectiveDimension_le_iff {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (n : ℕ) : projectiveDimension X ≤ ↑n ↔ HasProjectiveDimensionLE X n

theorem CategoryTheory.projectiveDimension_ge_iff {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (n : ℕ) : ↑n ≤ projectiveDimension X ↔ ¬HasProjectiveDimensionLT X n

theorem CategoryTheory.projectiveDimension_eq_bot_iff {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) : projectiveDimension X = ⊥ ↔ Limits.IsZero X

theorem CategoryTheory.projectiveDimension_ne_top_iff {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) : projectiveDimension X ≠ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE X n