Chain complexes supported in a single degree

We define single V j c : V ⥤ HomologicalComplex V c, which constructs complexes in V of shape c, supported in degree j.

Similarly single₀ V : V ⥤ ChainComplex V ℕ is the special case for ℕ-indexed chain complexes, with the object supported in degree 0, but with better definitional properties.

In toSingle₀Equiv we characterize chain maps to an ℕ-indexed complex concentrated in degree 0; they are equivalent to { f : C.X 0 ⟶ X // C.d 1 0 ≫ f = 0 }. (This is useful translating between a projective resolution and an augmented exact complex of projectives.)

@[simp]

theorem HomologicalComplex.single_map_f (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) : ∀ {X Y : V} (f : X ⟶ Y) (i : ι), HomologicalComplex.Hom.f ((HomologicalComplex.single V c j).map f) i = if h : i = j then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : HomologicalComplex.X ((fun A => HomologicalComplex.mk (fun i => if i = j then A else 0) fun i j => 0) X) i = X)) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom (_ : Y = HomologicalComplex.X ((fun A => HomologicalComplex.mk (fun i => if i = j then A else 0) fun i j => 0) Y) i))) else 0

@[simp]

theorem HomologicalComplex.single_obj_X (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) (i : ι) : HomologicalComplex.X ((HomologicalComplex.single V c j).obj A) i = if i = j then A else 0

@[simp]

theorem HomologicalComplex.single_obj_d (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) (i : ι) (j : ι) : HomologicalComplex.d ((HomologicalComplex.single V c j).obj A) i j = 0

def HomologicalComplex.single (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) : CategoryTheory.Functor V (HomologicalComplex V c)

The functor V ⥤ HomologicalComplex V c creating a chain complex supported in a single degree.

See also ChainComplex.single₀ : V ⥤ ChainComplex V ℕ, which has better definitional properties, if you are working with ℕ-indexed complexes.

@[simp]

theorem HomologicalComplex.singleObjXSelf_hom (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) : (HomologicalComplex.singleObjXSelf V c j A).hom = CategoryTheory.eqToHom (_ : (if j = j then A else 0) = A)

@[simp]

theorem HomologicalComplex.singleObjXSelf_inv (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) : (HomologicalComplex.singleObjXSelf V c j A).inv = CategoryTheory.eqToHom (_ : A = if j = j then A else 0)

def HomologicalComplex.singleObjXSelf (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) : HomologicalComplex.X ((HomologicalComplex.single V c j).obj A) j ≅ A

The object in degree j of (single V c h).obj A is just A.

@[simp]

theorem HomologicalComplex.single_map_f_self (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A : V} {B : V} (f : A ⟶ B) : HomologicalComplex.Hom.f ((HomologicalComplex.single V c j).map f) j = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf V c j A).hom (CategoryTheory.CategoryStruct.comp f (HomologicalComplex.singleObjXSelf V c j B).inv)

instance HomologicalComplex.instFaithfulHomologicalComplexInstCategoryHomologicalComplexSingle (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) : CategoryTheory.Faithful (HomologicalComplex.single V c j)

instance HomologicalComplex.instFullHomologicalComplexInstCategoryHomologicalComplexSingle (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) : CategoryTheory.Full (HomologicalComplex.single V c j)

def ChainComplex.single₀ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Functor V (ChainComplex V ℕ)

ChainComplex.single₀ V is the embedding of V into ChainComplex V ℕ as chain complexes supported in degree 0.

This is naturally isomorphic to single V _ 0, but has better definitional properties.

@[simp]

theorem ChainComplex.single₀_obj_X_0 (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) : HomologicalComplex.X ((ChainComplex.single₀ V).obj X) 0 = X

@[simp]

theorem ChainComplex.single₀_obj_X_succ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) (n : ℕ) : HomologicalComplex.X ((ChainComplex.single₀ V).obj X) (n + 1) = 0

@[simp]

theorem ChainComplex.single₀_obj_X_d (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) (i : ℕ) (j : ℕ) : HomologicalComplex.d ((ChainComplex.single₀ V).obj X) i j = 0

@[simp]

theorem ChainComplex.single₀_obj_X_dTo (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) (j : ℕ) : HomologicalComplex.dTo ((ChainComplex.single₀ V).obj X) j = 0

@[simp]

theorem ChainComplex.single₀_obj_x_dFrom (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) (i : ℕ) : HomologicalComplex.dFrom ((ChainComplex.single₀ V).obj X) i = 0

@[simp]

theorem ChainComplex.single₀_map_f_0 (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {X : V} {Y : V} (f : X ⟶ Y) : HomologicalComplex.Hom.f ((ChainComplex.single₀ V).map f) 0 = f

@[simp]

theorem ChainComplex.single₀_map_f_succ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {X : V} {Y : V} (f : X ⟶ Y) (n : ℕ) : HomologicalComplex.Hom.f ((ChainComplex.single₀ V).map f) (n + 1) = 0

noncomputable def ChainComplex.homologyFunctor0Single₀ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasCokernels V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] : CategoryTheory.Functor.comp (ChainComplex.single₀ V) (homologyFunctor V (ComplexShape.down ℕ) 0) ≅ CategoryTheory.Functor.id V

Sending objects to chain complexes supported at 0 then taking 0-th homology is the same as doing nothing.

noncomputable def ChainComplex.homologyFunctorSuccSingle₀ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasCokernels V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] (n : ℕ) : CategoryTheory.Functor.comp (ChainComplex.single₀ V) (homologyFunctor V (ComplexShape.down ℕ) (n + 1)) ≅ 0

Sending objects to chain complexes supported at 0 then taking (n+1)-st homology is the same as the zero functor.

@[simp]

theorem ChainComplex.toSingle₀Equiv_symm_apply_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V) (f : { f // CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C 1 0) f = 0 }) (i : ℕ) : HomologicalComplex.Hom.f (↑(ChainComplex.toSingle₀Equiv C X).symm f) i = match i with | 0 => ↑f | Nat.succ n => 0

@[simp]

theorem ChainComplex.toSingle₀Equiv_apply_coe {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V) (f : C ⟶ (ChainComplex.single₀ V).obj X) : ↑(↑(ChainComplex.toSingle₀Equiv C X) f) = HomologicalComplex.Hom.f f 0

def ChainComplex.toSingle₀Equiv {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V) : (C ⟶ (ChainComplex.single₀ V).obj X) ≃ { f // CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C 1 0) f = 0 }

Morphisms from an ℕ-indexed chain complex C to a single object chain complex with X concentrated in degree 0 are the same as morphisms f : C.X 0 ⟶ X such that C.d 1 0 ≫ f = 0.

theorem ChainComplex.to_single₀_ext {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {C : ChainComplex V ℕ} {X : V} (f : C ⟶ (ChainComplex.single₀ V).obj X) (g : C ⟶ (ChainComplex.single₀ V).obj X) (h : HomologicalComplex.Hom.f f 0 = HomologicalComplex.Hom.f g 0) : f = g

@[simp]

theorem ChainComplex.fromSingle₀Equiv_apply {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V) (f : (ChainComplex.single₀ V).obj X ⟶ C) : ↑(ChainComplex.fromSingle₀Equiv C X) f = HomologicalComplex.Hom.f f 0

@[simp]

theorem ChainComplex.fromSingle₀Equiv_symm_apply_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V) (f : X ⟶ HomologicalComplex.X C 0) (i : ℕ) : HomologicalComplex.Hom.f (↑(ChainComplex.fromSingle₀Equiv C X).symm f) i = match i with | 0 => f | Nat.succ n => 0

def ChainComplex.fromSingle₀Equiv {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V) : ((ChainComplex.single₀ V).obj X ⟶ C) ≃ (X ⟶ HomologicalComplex.X C 0)

Morphisms from a single object chain complex with X concentrated in degree 0 to an ℕ-indexed chain complex C are the same as morphisms f : X → C.X.

def ChainComplex.single₀IsoSingle (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] : ChainComplex.single₀ V ≅ HomologicalComplex.single V (ComplexShape.down ℕ) 0

single₀ is the same as single V _ 0.

instance ChainComplex.instFaithfulChainComplexNatToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringInstCategoryHomologicalComplexDownSingle₀ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Faithful (ChainComplex.single₀ V)

instance ChainComplex.instFullChainComplexNatToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringInstCategoryHomologicalComplexDownSingle₀ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Full (ChainComplex.single₀ V)

def CochainComplex.single₀ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Functor V (CochainComplex V ℕ)

CochainComplex.single₀ V is the embedding of V into CochainComplex V ℕ as cochain complexes supported in degree 0.

This is naturally isomorphic to single V _ 0, but has better definitional properties.

@[simp]

theorem CochainComplex.single₀_obj_X_0 (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) : HomologicalComplex.X ((CochainComplex.single₀ V).obj X) 0 = X

@[simp]

theorem CochainComplex.single₀_obj_X_succ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) (n : ℕ) : HomologicalComplex.X ((CochainComplex.single₀ V).obj X) (n + 1) = 0

@[simp]

theorem CochainComplex.single₀_obj_X_d (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) (i : ℕ) (j : ℕ) : HomologicalComplex.d ((CochainComplex.single₀ V).obj X) i j = 0

@[simp]

theorem CochainComplex.single₀_obj_x_dFrom (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) (j : ℕ) : HomologicalComplex.dFrom ((CochainComplex.single₀ V).obj X) j = 0

@[simp]

theorem CochainComplex.single₀_obj_x_dTo (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) (i : ℕ) : HomologicalComplex.dTo ((CochainComplex.single₀ V).obj X) i = 0

@[simp]

theorem CochainComplex.single₀_map_f_0 (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {X : V} {Y : V} (f : X ⟶ Y) : HomologicalComplex.Hom.f ((CochainComplex.single₀ V).map f) 0 = f

@[simp]

theorem CochainComplex.single₀_map_f_succ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {X : V} {Y : V} (f : X ⟶ Y) (n : ℕ) : HomologicalComplex.Hom.f ((CochainComplex.single₀ V).map f) (n + 1) = 0

noncomputable def CochainComplex.homologyFunctor0Single₀ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasCokernels V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] : CategoryTheory.Functor.comp (CochainComplex.single₀ V) (homologyFunctor V (ComplexShape.up ℕ) 0) ≅ CategoryTheory.Functor.id V

Sending objects to cochain complexes supported at 0 then taking 0-th homology is the same as doing nothing.

noncomputable def CochainComplex.homologyFunctorSuccSingle₀ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasCokernels V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] (n : ℕ) : CategoryTheory.Functor.comp (CochainComplex.single₀ V) (homologyFunctor V (ComplexShape.up ℕ) (n + 1)) ≅ 0

Sending objects to cochain complexes supported at 0 then taking (n+1)-st homology is the same as the zero functor.

def CochainComplex.fromSingle₀Equiv {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : CochainComplex V ℕ) (X : V) : ((CochainComplex.single₀ V).obj X ⟶ C) ≃ { f // CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d C 0 1) = 0 }

Morphisms from a single object cochain complex with X concentrated in degree 0 to an ℕ-indexed cochain complex C are the same as morphisms f : X ⟶ C.X 0 such that f ≫ C.d 0 1 = 0.

theorem CochainComplex.from_single₀_ext {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {C : CochainComplex V ℕ} {X : V} (f : (CochainComplex.single₀ V).obj X ⟶ C) (g : (CochainComplex.single₀ V).obj X ⟶ C) (h : HomologicalComplex.Hom.f f 0 = HomologicalComplex.Hom.f g 0) : f = g

def CochainComplex.single₀IsoSingle (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] : CochainComplex.single₀ V ≅ HomologicalComplex.single V (ComplexShape.up ℕ) 0

single₀ is the same as single V _ 0.

instance CochainComplex.instFaithfulCochainComplexNatToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringInstCategoryHomologicalComplexUpSingle₀ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Faithful (CochainComplex.single₀ V)

instance CochainComplex.instFullCochainComplexNatToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringInstCategoryHomologicalComplexUpSingle₀ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Full (CochainComplex.single₀ V)