mathlib documentation

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
source
def homological_complex (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] (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 ℂ.)

source
def chain_complex (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] :
Type (max v u)

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

source
def cochain_complex (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] :
Type (max v u)

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

source
@[simp]
theorem homological_complex.d_squared {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} (C : homological_complex V b) (i : β) :
C.d i ≫ C.d (i + b) = 0
source
@[simp]
theorem homological_complex.d_squared_assoc {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} (C : homological_complex V b) (i : β) {X' : V} (f' : (category_theory.shift (category_theory.graded_object_with_shift b V) ^ 1).functor.obj C.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 ≫ C.d (i + b) ≫ f' = 0 ≫ f'
source
@[simp]
theorem homological_complex.comm_at_assoc {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} {C D : homological_complex V 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'
source
@[simp]
theorem homological_complex.comm_at {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} {C D : homological_complex V 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.

source
@[simp]
theorem homological_complex.comm_assoc {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} {C D : homological_complex V b} (f : C ⟶ D) {X' : category_theory.graded_object_with_shift b V} (f' : (category_theory.shift (category_theory.graded_object_with_shift b V) ^ 1).functor.obj D.X ⟶ X') :
C.d ≫ (category_theory.shift (category_theory.graded_object_with_shift b V) ^ 1).functor.map f.f ≫ f' = f.f ≫ D.d ≫ f'
source
@[simp]
theorem homological_complex.comm {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} {C D : homological_complex V b} (f : C ⟶ D) :
C.d ≫ (category_theory.shift (category_theory.graded_object_with_shift b V) ^ 1).functor.map f.f = f.f ≫ D.d
source
theorem homological_complex.eq_to_hom_d {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} (C : homological_complex V b) {i j : β} (h : i = j) :
category_theory.eq_to_hom _ ≫ C.d j = C.d i ≫ category_theory.eq_to_hom _
source
theorem homological_complex.eq_to_hom_d_assoc {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} (C : homological_complex V b) {i j : β} (h : i = j) {X' : V} (f' : (category_theory.shift (category_theory.graded_object_with_shift b V) ^ 1).functor.obj C.X j ⟶ X') :
category_theory.eq_to_hom _ ≫ C.d j ≫ f' = C.d i ≫ category_theory.eq_to_hom _ ≫ f'
source
theorem homological_complex.eq_to_hom_f {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} {C D : homological_complex V b} (f : C ⟶ D) {n m : β} (h : n = m) :
category_theory.eq_to_hom _ ≫ f.f m = f.f n ≫ category_theory.eq_to_hom _
source
theorem homological_complex.eq_to_hom_f_assoc {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} {C D : homological_complex V b} (f : C ⟶ D) {n m : β} (h : n = m) {X' : V} (f' : D.X m ⟶ X') :
category_theory.eq_to_hom _ ≫ f.f m ≫ f' = f.f n ≫ category_theory.eq_to_hom _ ≫ f'
source
def homological_complex.forget (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} :
homological_complex V b ⥤ category_theory.graded_object β V

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

source
@[protected, instance]
def homological_complex.inhabited {β : Type} [add_comm_group β] {b : β} :
inhabited (homological_complex (category_theory.discrete punit) b)
Equations
source
def category_theory.functor.map_homological_complex {β : Type} [add_comm_group β] {b : β} {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C ⥤ D) [F.additive] (Cs : homological_complex C b) :
homological_complex D b

Map a homological_complex with respect to an additive functor.

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

A functorial version of map_homological_complex.

Equations
source
@[simp]
theorem category_theory.functor.pushforward_homological_complex_map_f {β : Type} [add_comm_group β] {b : β} {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C ⥤ D) [F.additive] (X Y : homological_complex C b) (f : X ⟶ Y) (i : β) :
(F.pushforward_homological_complex.map f).f i = F.map (f.f i)