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 behaves as expected on non-negative values.
class
CategoryTheory.HasProjectiveDimensionLT
{C : Type u}
[Category.{v, u} C]
[Abelian C]
(X : C)
(n : ℕ)
:
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' :: (
- )
Instances
@[reducible, inline]
abbrev
CategoryTheory.HasProjectiveDimensionLE
{C : Type u}
[Category.{v, u} C]
[Abelian C]
(X : C)
(n : ℕ)
:
An object X in an abelian category has projective dimension ≤ n if
all Ext X Y i vanish when n + 1 ≤ i
Instances For
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)
:
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)
:
instance
CategoryTheory.instHasProjectiveDimensionLTOfNatNat
{C : Type u}
[Category.{v, u} C]
[Abelian C]
:
theorem
CategoryTheory.isZero_of_hasProjectiveDimensionLT_zero
{C : Type u}
[Category.{v, u} C]
[Abelian C]
(X : C)
[HasProjectiveDimensionLT X 0]
:
theorem
CategoryTheory.hasProjectiveDimensionLT_zero_iff_isZero
{C : Type u}
[Category.{v, u} C]
[Abelian C]
(X : C)
:
theorem
CategoryTheory.hasProjectiveDimensionLT_of_ge
{C : Type u}
[Category.{v, u} C]
[Abelian C]
(X : C)
(n m : ℕ)
(h : n ≤ m)
[HasProjectiveDimensionLT X n]
:
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]
:
theorem
CategoryTheory.projective_iff_subsingleton_ext_one
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X : C}
[HasExt 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
@[instance 100]
instance
CategoryTheory.instProjectiveOfHasProjectiveDimensionLTOfNatNat
{C : Type u}
[Category.{v, u} C]
[Abelian C]
(X : C)
[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]
:
theorem
CategoryTheory.hasProjectiveDimensionLT_of_iso
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X X' : C}
(e : X ≅ 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)
:
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))
:
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
theorem
CategoryTheory.hasProjectiveDimensionLT_of_enoughInjectives
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
[EnoughInjectives C]
(X : C)
(n : ℕ)
(hX : ∀ (Y : C), Subsingleton (Abelian.Ext X Y n))
:
noncomputable def
CategoryTheory.projectiveDimension
{C : Type u}
[Category.{v, u} C]
[Abelian C]
(X : C)
:
The projective dimension of an object in an abelian category.
Instances For
theorem
CategoryTheory.projectiveDimension_eq_of_iso
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X Y : C}
(e : X ≅ Y)
:
theorem
CategoryTheory.Retract.projectiveDimension_le
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{X Y : C}
(h : Retract X 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