The disk complex of an object

For an object Q of a category with zero morphisms and a zero object, the disk of Q is the cochain complex Q --𝟙--> Q concentrated in degrees -1 and 0. It is acyclic, its terms are projective when Q is, and its cycles in degree 0 are Q; so it is a complete resolution of a projective object.

Main definitions

• CochainComplex.disk Q: the complex Q --𝟙--> Q in degrees -1 and 0, with its terms CochainComplex.diskXIso₀ and CochainComplex.diskXIso₁ and differential CochainComplex.disk_d.
• CochainComplex.diskCyclesIso Q: the cycles of the disk in degree 0 are Q.

Main results

• CochainComplex.projective_disk_X: the terms of the disk of a projective object are projective.
• CochainComplex.acyclic_double_id: the complex X --𝟙--> X in any two consecutive degrees is acyclic; in particular the disk is acyclic (CochainComplex.acyclic_disk).

noncomputable def CochainComplex.disk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (Q : C) : CochainComplex C ℤ

The disk of Q: the complex Q --𝟙--> Q concentrated in degrees -1 and 0.

noncomputable def CochainComplex.diskXIso₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (Q : C) : (disk Q).X (-1) ≅ Q

The term of the disk in degree -1 is Q.

noncomputable def CochainComplex.diskXIso₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (Q : C) : (disk Q).X 0 ≅ Q

The term of the disk in degree 0 is Q.

theorem CochainComplex.disk_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (Q : C) : (disk Q).d (-1) 0 = CategoryTheory.CategoryStruct.comp (diskXIso₀ Q).hom (diskXIso₁ Q).inv

The differential of the disk from degree -1 to degree 0 is the identity of Q.

instance CochainComplex.isIso_disk_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (Q : C) : CategoryTheory.IsIso ((disk Q).d (-1) 0)

The differential of the disk from degree -1 to degree 0 is an isomorphism.

theorem CochainComplex.disk_d_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (Q : C) (j k : ℤ) (hj : j ≠ -1) : (disk Q).d j k = 0

The differentials of the disk out of degrees other than -1 vanish.

theorem CochainComplex.isZero_disk_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (Q : C) (n : ℤ) (h₀ : n ≠ -1) (h₁ : n ≠ 0) : CategoryTheory.Limits.IsZero ((disk Q).X n)

The terms of the disk outside degrees -1 and 0 are zero.

theorem CochainComplex.projective_disk_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (Q : C) [CategoryTheory.Projective Q] (n : ℤ) : CategoryTheory.Projective ((disk Q).X n)

The terms of the disk of a projective object are projective.

noncomputable def CochainComplex.diskCyclesIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (Q : C) [HomologicalComplex.HasHomology (disk Q) 0] : HomologicalComplex.cycles (disk Q) 0 ≅ Q

The cycles of the disk in degree 0 are Q.

theorem CochainComplex.acyclic_double_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) {i₀ i₁ : ℤ} (h : (ComplexShape.up ℤ).Rel i₀ i₁) : (HomologicalComplex.double (CategoryTheory.CategoryStruct.id X) h).Acyclic

The complex X --𝟙--> X concentrated in two consecutive degrees is acyclic.

theorem CochainComplex.acyclic_disk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (Q : C) : HomologicalComplex.Acyclic (disk Q)

The disk is acyclic.