# mathlibdocumentation

algebra.homology.chain_complex

# Chain complexes #

We define a chain complex in V as a differential ℤ-graded object in V.

This is fancy language for the obvious definition, and it seems we can use it straightforwardly:

example (C : chain_complex V) : C.X 5 ⟶ C.X 6 := C.d 5

def homological_complex (V : Type u) {β : Type} (b : β) :
Type (max v u)

A homological_complex V b for b : β is a (co)chain complex graded by β, with differential in grading b.

(We use the somewhat cumbersome homological_complex to avoid the name conflict with ℂ.)

def chain_complex (V : Type u)  :
Type (max v u)

A chain complex in V is "just" a differential ℤ-graded object in V, with differential graded -1.

def cochain_complex (V : Type u)  :
Type (max v u)

A cochain complex in V is "just" a differential ℤ-graded object in V, with differential graded +1.

@[simp]
theorem homological_complex.d_squared {V : Type u} {β : Type} {b : β} (C : b) (i : β) :
C.d i C.d (i + b) = 0
@[simp]
theorem homological_complex.d_squared_assoc {V : Type u} {β : Type} {b : β} (C : b) (i : β) {X' : V} (f' : (({to_fun := λ (b_1 : β), b_1 - b, inv_fun := λ (b_1 : β), b_1 + b, left_inv := _, right_inv := _}.symm) i) X') :
C.d i C.d (i + b) f' = 0 f'
@[simp]
theorem homological_complex.comm_at_assoc {V : Type u} {β : Type} {b : β} {C D : b} (f : C D) (i : β) {X' : V} (f' : D.X (({to_fun := λ (b_1 : β), b_1 - b, inv_fun := λ (b_1 : β), b_1 + b, left_inv := _, right_inv := _}.symm) i) X') :
C.d i f.f (i + b) f' = f.f i D.d i f'
@[simp]
theorem homological_complex.comm_at {V : Type u} {β : Type} {b : β} {C D : b} (f : C D) (i : β) :
C.d i f.f (i + b) = f.f i D.d i

A convenience lemma for morphisms of cochain complexes, picking out one component of the commutation relation.

@[simp]
theorem homological_complex.comm_assoc {V : Type u} {β : Type} {b : β} {C D : b} (f : C D) (f' : X') :
C.d f' = f.f D.d f'
@[simp]
theorem homological_complex.comm {V : Type u} {β : Type} {b : β} {C D : b} (f : C D) :
C.d = f.f D.d
theorem homological_complex.eq_to_hom_d {V : Type u} {β : Type} {b : β} (C : b) {i j : β} (h : i = j) :
=
theorem homological_complex.eq_to_hom_d_assoc {V : Type u} {β : Type} {b : β} (C : b) {i j : β} (h : i = j) {X' : V} (f' : X') :
C.d j f' = C.d i
theorem homological_complex.eq_to_hom_f {V : Type u} {β : Type} {b : β} {C D : b} (f : C D) {n m : β} (h : n = m) :
=
theorem homological_complex.eq_to_hom_f_assoc {V : Type u} {β : Type} {b : β} {C D : b} (f : C D) {n m : β} (h : n = m) {X' : V} (f' : D.X m X') :
f.f m f' = f.f n
def homological_complex.forget (V : Type u) {β : Type} {b : β} :

The forgetful functor from cochain complexes to graded objects, forgetting the differential.

@[instance]
def homological_complex.inhabited {β : Type} {b : β} :
Equations
def category_theory.functor.map_homological_complex {β : Type} {b : β} {C : Type u_1} {D : Type u_2} (F : C D) [F.additive] (Cs : b) :

Map a homological_complex with respect to an additive functor.

Equations
@[simp]
theorem category_theory.functor.map_homological_complex_X {β : Type} {b : β} {C : Type u_1} {D : Type u_2} (F : C D) [F.additive] (Cs : b) (i : β) :
(F.map_homological_complex Cs).X i = F.obj (Cs.X i)
@[simp]
theorem category_theory.functor.map_homological_complex_d {β : Type} {b : β} {C : Type u_1} {D : Type u_2} (F : C D) [F.additive] (Cs : b) (i : β) :
(F.map_homological_complex Cs).d i = F.map (Cs.d i)
@[simp]
theorem category_theory.functor.pushforward_homological_complex_obj {β : Type} {b : β} {C : Type u_1} {D : Type u_2} (F : C D) [F.additive] (Cs : b) :
def category_theory.functor.pushforward_homological_complex {β : Type} {b : β} {C : Type u_1} {D : Type u_2} (F : C D) [F.additive] :

A functorial version of map_homological_complex.

Equations
@[simp]
theorem category_theory.functor.pushforward_homological_complex_map_f {β : Type} {b : β} {C : Type u_1} {D : Type u_2} (F : C D) [F.additive] (X Y : b) (f : X Y) (i : β) :
i = F.map (f.f i)