# Documentation

Mathlib.Algebra.Homology.Single

# 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) {ι : Type u_1} [] (c : ) (j : ι) :
∀ {X Y : V} (f : X Y) (i : ι), HomologicalComplex.Hom.f (().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) {ι : Type u_1} [] (c : ) (j : ι) (A : V) (i : ι) :
HomologicalComplex.X (().obj A) i = if i = j then A else 0
@[simp]
theorem HomologicalComplex.single_obj_d (V : Type u) {ι : Type u_1} [] (c : ) (j : ι) (A : V) (i : ι) (j : ι) :
HomologicalComplex.d (().obj A) i j = 0
def HomologicalComplex.single (V : Type u) {ι : Type u_1} [] (c : ) (j : ι) :

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.

Instances For
@[simp]
theorem HomologicalComplex.singleObjXSelf_hom (V : Type u) {ι : Type u_1} [] (c : ) (j : ι) (A : V) :
().hom = CategoryTheory.eqToHom (_ : (if j = j then A else 0) = A)
@[simp]
theorem HomologicalComplex.singleObjXSelf_inv (V : Type u) {ι : Type u_1} [] (c : ) (j : ι) (A : V) :
().inv = CategoryTheory.eqToHom (_ : A = if j = j then A else 0)
def HomologicalComplex.singleObjXSelf (V : Type u) {ι : Type u_1} [] (c : ) (j : ι) (A : V) :
HomologicalComplex.X (().obj A) j A

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

Instances For
@[simp]
theorem HomologicalComplex.single_map_f_self (V : Type u) {ι : Type u_1} [] (c : ) (j : ι) {A : V} {B : V} (f : A B) :

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.

Instances For
@[simp]
theorem ChainComplex.single₀_obj_X_0 (V : Type u) (X : V) :
HomologicalComplex.X (().obj X) 0 = X
@[simp]
theorem ChainComplex.single₀_obj_X_succ (V : Type u) (X : V) (n : ) :
HomologicalComplex.X (().obj X) (n + 1) = 0
@[simp]
theorem ChainComplex.single₀_obj_X_d (V : Type u) (X : V) (i : ) (j : ) :
HomologicalComplex.d (().obj X) i j = 0
@[simp]
theorem ChainComplex.single₀_obj_X_dTo (V : Type u) (X : V) (j : ) :
HomologicalComplex.dTo (().obj X) j = 0
@[simp]
theorem ChainComplex.single₀_obj_x_dFrom (V : Type u) (X : V) (i : ) :
@[simp]
theorem ChainComplex.single₀_map_f_0 (V : Type u) {X : V} {Y : V} (f : X Y) :
@[simp]
theorem ChainComplex.single₀_map_f_succ (V : Type u) {X : V} {Y : V} (f : X Y) (n : ) :
HomologicalComplex.Hom.f (().map f) (n + 1) = 0

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

Instances For

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

Instances For
@[simp]
theorem ChainComplex.toSingle₀Equiv_symm_apply_f {V : Type u} (C : ) (X : V) (f : { f // }) (i : ) :
HomologicalComplex.Hom.f (().symm f) i = match i with | 0 => f | => 0
@[simp]
theorem ChainComplex.toSingle₀Equiv_apply_coe {V : Type u} (C : ) (X : V) (f : C ().obj X) :
↑(↑() f) =
def ChainComplex.toSingle₀Equiv {V : Type u} (C : ) (X : V) :
(C ().obj X) { f // }

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.

Instances For
theorem ChainComplex.to_single₀_ext {V : Type u} {C : } {X : V} (f : C ().obj X) (g : C ().obj X) (h : ) :
f = g
@[simp]
theorem ChainComplex.fromSingle₀Equiv_apply {V : Type u} (C : ) (X : V) (f : ().obj X C) :
@[simp]
theorem ChainComplex.fromSingle₀Equiv_symm_apply_f {V : Type u} (C : ) (X : V) (f : ) (i : ) :
HomologicalComplex.Hom.f (().symm f) i = match i with | 0 => f | => 0
def ChainComplex.fromSingle₀Equiv {V : Type u} (C : ) (X : V) :
(().obj X C) ()

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.

Instances For

single₀ is the same as single V _ 0.

Instances For

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.

Instances For
@[simp]
theorem CochainComplex.single₀_obj_X_0 (V : Type u) (X : V) :
HomologicalComplex.X (().obj X) 0 = X
@[simp]
theorem CochainComplex.single₀_obj_X_succ (V : Type u) (X : V) (n : ) :
HomologicalComplex.X (().obj X) (n + 1) = 0
@[simp]
theorem CochainComplex.single₀_obj_X_d (V : Type u) (X : V) (i : ) (j : ) :
HomologicalComplex.d (().obj X) i j = 0
@[simp]
theorem CochainComplex.single₀_obj_x_dFrom (V : Type u) (X : V) (j : ) :
@[simp]
theorem CochainComplex.single₀_obj_x_dTo (V : Type u) (X : V) (i : ) :
HomologicalComplex.dTo (().obj X) i = 0
@[simp]
theorem CochainComplex.single₀_map_f_0 (V : Type u) {X : V} {Y : V} (f : X Y) :
@[simp]
theorem CochainComplex.single₀_map_f_succ (V : Type u) {X : V} {Y : V} (f : X Y) (n : ) :
HomologicalComplex.Hom.f (().map f) (n + 1) = 0

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

Instances For

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

Instances For
def CochainComplex.fromSingle₀Equiv {V : Type u} (C : ) (X : V) :
(().obj X C) { f // }

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.

Instances For
theorem CochainComplex.from_single₀_ext {V : Type u} {C : } {X : V} (f : ().obj X C) (g : ().obj X C) (h : ) :
f = g

single₀ is the same as single V _ 0.

Instances For