Injective dimension

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

We also define the Injective dimension in WithBot ℕ∞ as injectiveDimension, injectiveDimension X = ⊥ iff X is zero and behaves as expected on non-negative values.

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

An object X in an abelian category has Injective dimension < n if all Ext X Y i vanish when n ≤ i. See also HasInjectiveDimensionLE. (Do not use the subsingleton' field directly. Use the constructor HasInjectiveDimensionLT.mk, and the lemmas hasInjectiveDimensionLT_iff and Ext.eq_zero_of_hasInjectiveDimensionLT.)

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

@[reducible, inline]

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

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

Equations

• CategoryTheory.HasInjectiveDimensionLE X n = CategoryTheory.HasInjectiveDimensionLT X (n + 1)

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

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

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

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

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

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

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

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

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

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

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

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

instance CategoryTheory.instHasInjectiveDimensionLTOfNatNatOfInjective {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) [Injective X] : HasInjectiveDimensionLT X 1

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

theorem CategoryTheory.injective_iff_hasInjectiveDimensionLT_one {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} : Injective X ↔ HasInjectiveDimensionLT X 1

theorem CategoryTheory.injective_iff_hasInjectiveDimensionLE_zero {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) : Injective X ↔ HasInjectiveDimensionLE X 0

@[instance 100]

instance CategoryTheory.instInjectiveOfHasInjectiveDimensionLTOfNatNat {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) [HasInjectiveDimensionLT X 1] : Injective X

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

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

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

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

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

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

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

theorem CategoryTheory.hasInjectiveDimensionLT_of_enoughProjectives {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] [EnoughProjectives C] (X : C) (n : ℕ) (hX : ∀ (Y : C), Subsingleton (Abelian.Ext Y X n)) : HasInjectiveDimensionLT X n

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

The injective dimension of an object in an abelian category.

Equations

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

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

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

theorem CategoryTheory.injectiveDimension_lt_iff {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} {n : ℕ} : injectiveDimension X < ↑n ↔ HasInjectiveDimensionLT X n

theorem CategoryTheory.injectiveDimension_le_iff {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (n : ℕ) : injectiveDimension X ≤ ↑n ↔ HasInjectiveDimensionLE X n

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

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

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

theorem CategoryTheory.Injective.injectiveDimension_le_zero {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) [Injective X] : injectiveDimension X ≤ 0

An injective object has injective dimension at most zero.

theorem CategoryTheory.injectiveDimension_eq_zero_iff {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) : injectiveDimension X = 0 ↔ Injective X ∧ ¬Limits.IsZero X

An object has injective dimension zero iff it is injective and it is not zero object.

theorem CategoryTheory.injectiveDimension_ge_zero_iff {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) : 0 ≤ injectiveDimension X ↔ ¬Limits.IsZero X

theorem CategoryTheory.ShortComplex.ShortExact.injectiveDimension_X₂_le_sup {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) : injectiveDimension S.X₂ ≤ max (injectiveDimension S.X₁) (injectiveDimension S.X₃)

In a short exact complex, the injective dimension of the middle object is bounded by the supremum of the injective dimensions of the outer objects.

theorem CategoryTheory.ShortComplex.ShortExact.injectiveDimension_X₁_le_sup {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) : injectiveDimension S.X₁ ≤ max (injectiveDimension S.X₂) (injectiveDimension S.X₃ + 1)

In a short exact complex, the injective dimension of the left object is bounded by max (injectiveDimension S.X₂) (injectiveDimension S.X₃ + 1).

theorem CategoryTheory.ShortComplex.ShortExact.injectiveDimension_X₃_succ_le_sup {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) : injectiveDimension S.X₃ + 1 ≤ max (injectiveDimension S.X₂ + 1) (injectiveDimension S.X₁)

In a short exact complex, the successor of the injective dimension of the right object is bounded by max (injectiveDimension S.X₂ + 1) (injectiveDimension S.X₁).

theorem CategoryTheory.ShortComplex.ShortExact.injectiveDimension_X₁_eq_succ_of_not_injective {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) (i : Injective S.X₂) (ni : ¬Injective S.X₁) : injectiveDimension S.X₁ = injectiveDimension S.X₃ + 1

If the middle object of a short exact complex is injective and the left object is not, then the injective dimension of the left object is one more than that of the right object.