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.)
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
Equations
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)
:
theorem
CategoryTheory.hasProjectiveDimensionLT_iff
{C : Type u}
[Category.{v, u} C]
[Abelian C]
(X : C)
(n : ℕ)
[HasExt C]
:
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_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]
:
instance
CategoryTheory.instHasProjectiveDimensionLTOfNatNatOfProjective
{C : Type u}
[Category.{v, u} C]
[Abelian C]
(X : C)
[Projective X]
:
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₂)
:
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