Injective resolutions

An injective resolution I : InjectiveResolution Z of an object Z : C consists of an ℕ-indexed cochain complex I.cocomplex of injective objects, along with a quasi-isomorphism I.ι from the cochain complex consisting just of Z in degree zero to I.cocomplex.

Z ----> 0 ----> ... ----> 0 ----> ...
|       |                 |
|       |                 |
v       v                 v
I⁰ ---> I¹ ---> ... ----> Iⁿ ---> ...

structure CategoryTheory.InjectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) : Type (max u v)

An InjectiveResolution Z consists of a bundled ℕ-indexed cochain complex of injective objects, along with a quasi-isomorphism from the complex consisting of just Z supported in degree 0.

• cocomplex : CochainComplex C ℕ

  the cochain complex involved in the resolution

• injective : ∀ (n : ℕ), CategoryTheory.Injective (self.cocomplex.X n)

  the cochain complex must be degreewise injective

• hasHomology : ∀ (i : ℕ), HomologicalComplex.HasHomology self.cocomplex i

  the cochain complex must have homology

• ι : (CochainComplex.single₀ C).obj Z ⟶ self.cocomplex

  the morphism from the single cochain complex with Z in degree 0

• quasiIso : QuasiIso self.ι

  the morphism from the single cochain complex with Z in degree 0 is a quasi-isomorphism

theorem CategoryTheory.InjectiveResolution.injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.InjectiveResolution Z) (n : ℕ) : CategoryTheory.Injective (self.cocomplex.X n)

the cochain complex must be degreewise injective

theorem CategoryTheory.InjectiveResolution.hasHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.InjectiveResolution Z) (i : ℕ) : HomologicalComplex.HasHomology self.cocomplex i

the cochain complex must have homology

theorem CategoryTheory.InjectiveResolution.quasiIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.InjectiveResolution Z) : QuasiIso self.ι

the morphism from the single cochain complex with Z in degree 0 is a quasi-isomorphism

class CategoryTheory.HasInjectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) : Prop

An object admits an injective resolution.

• out : Nonempty (CategoryTheory.InjectiveResolution Z)

  An object admits an injective resolution.

theorem CategoryTheory.HasInjectiveResolution.out {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {Z : C} [self : CategoryTheory.HasInjectiveResolution Z], Nonempty (CategoryTheory.InjectiveResolution Z)

An object admits an injective resolution.

class CategoryTheory.HasInjectiveResolutions (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] : Prop

You will rarely use this typeclass directly: it is implied by the combination [EnoughInjectives C] and [Abelian C].

• out : ∀ (Z : C), CategoryTheory.HasInjectiveResolution Z

theorem CategoryTheory.HasInjectiveResolutions.out {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} [self : CategoryTheory.HasInjectiveResolutions C] (Z : C), CategoryTheory.HasInjectiveResolution Z

theorem CategoryTheory.InjectiveResolution.cocomplex_exactAt_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) (n : ℕ) : HomologicalComplex.ExactAt I.cocomplex (n + 1)

theorem CategoryTheory.InjectiveResolution.exact_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) (n : ℕ) : (CategoryTheory.ShortComplex.mk (I.cocomplex.d n (n + 1)) (I.cocomplex.d (n + 1) (n + 2)) ⋯).Exact

@[simp]

theorem CategoryTheory.InjectiveResolution.ι_f_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) (n : ℕ) : I.ι.f (n + 1) = 0

theorem CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (I.cocomplex.d 0 1) = 0

theorem CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z✝) {Z : C} (h : I.cocomplex.X 1 ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (CategoryTheory.CategoryStruct.comp (I.cocomplex.d 0 1) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.InjectiveResolution.complex_d_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) (n : ℕ) : CategoryTheory.CategoryStruct.comp (I.cocomplex.d n (n + 1)) (I.cocomplex.d (n + 1) (n + 2)) = 0

def CategoryTheory.InjectiveResolution.kernelFork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) : CategoryTheory.Limits.KernelFork (I.cocomplex.d 0 1)

The (limit) kernel fork given by the composition Z ⟶ I.cocomplex.X 0 ⟶ I.cocomplex.X 1 when I : InjectiveResolution Z.

Equations

• I.kernelFork = CategoryTheory.Limits.KernelFork.ofι (I.ι.f 0) ⋯

def CategoryTheory.InjectiveResolution.isLimitKernelFork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) : CategoryTheory.Limits.IsLimit I.kernelFork

Z is the kernel of I.cocomplex.X 0 ⟶ I.cocomplex.X 1 when I : InjectiveResolution Z.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.InjectiveResolution.instMonoFNatι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) (n : ℕ) : CategoryTheory.Mono (I.ι.f n)

Equations

• ⋯ = ⋯

def CategoryTheory.InjectiveResolution.self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [CategoryTheory.Injective Z] : CategoryTheory.InjectiveResolution Z

An injective object admits a trivial injective resolution: itself in degree 0.

Equations

• CategoryTheory.InjectiveResolution.self Z = CategoryTheory.InjectiveResolution.mk ((CochainComplex.single₀ C).obj Z) ⋯ (CategoryTheory.CategoryStruct.id ((CochainComplex.single₀ C).obj Z)) ⋯

@[simp]

theorem CategoryTheory.InjectiveResolution.self_cocomplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [CategoryTheory.Injective Z] : (CategoryTheory.InjectiveResolution.self Z).cocomplex = (CochainComplex.single₀ C).obj Z

@[simp]

theorem CategoryTheory.InjectiveResolution.self_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [CategoryTheory.Injective Z] : (CategoryTheory.InjectiveResolution.self Z).ι = CategoryTheory.CategoryStruct.id ((CochainComplex.single₀ C).obj Z)