The homology of a complex #
Given C : homological_complex V c, we have C.cycles i and C.boundaries i,
both defined as subobjects of C.X i.
We show these are functorial with respect to chain maps,
as C.cycles_map f i and C.boundaries_map f i.
As a consequence we construct homology_functor i : homological_complex V c ⥤ V,
computing the i-th homology.
@[reducible]
noncomputable
def
homological_complex.cycles
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
[category_theory.limits.has_kernels V]
(i : ι) :
category_theory.subobject (C.X i)
The cycles at index i, as a subobject.
theorem
homological_complex.cycles_eq_kernel_subobject
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
[category_theory.limits.has_kernels V]
{i j : ι}
(r : c.rel i j) :
C.cycles i = category_theory.limits.kernel_subobject (C.d i j)
noncomputable
def
homological_complex.cycles_iso_kernel
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
[category_theory.limits.has_kernels V]
{i j : ι}
(r : c.rel i j) :
↑(C.cycles i) ≅ category_theory.limits.kernel (C.d i j)
The underlying object of C.cycles i is isomorphic to kernel (C.d i j),
for any j such that rel i j.
Equations
- C.cycles_iso_kernel r = (C.cycles i).iso_of_eq (category_theory.limits.kernel_subobject (C.d i j)) _ ≪≫ category_theory.limits.kernel_subobject_iso (C.d i j)
theorem
homological_complex.cycles_eq_top
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
[category_theory.limits.has_kernels V]
{i : ι}
(h : ¬c.rel i (c.next i)) :
@[reducible]
noncomputable
def
homological_complex.boundaries
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_images V]
(C : homological_complex V c)
(j : ι) :
category_theory.subobject (C.X j)
The boundaries at index i, as a subobject.
theorem
homological_complex.boundaries_eq_image_subobject
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
{i j : ι}
(r : c.rel i j) :
C.boundaries j = category_theory.limits.image_subobject (C.d i j)
noncomputable
def
homological_complex.boundaries_iso_image
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
{i j : ι}
(r : c.rel i j) :
↑(C.boundaries j) ≅ category_theory.limits.image (C.d i j)
The underlying object of C.boundaries j is isomorphic to image (C.d i j),
for any i such that rel i j.
Equations
- C.boundaries_iso_image r = (C.boundaries j).iso_of_eq (category_theory.limits.image_subobject (C.d i j)) _ ≪≫ category_theory.limits.image_subobject_iso (C.d i j)
theorem
homological_complex.boundaries_eq_bot
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
(C : homological_complex V c)
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_object V]
{j : ι}
(h : ¬c.rel (c.prev j) j) :
C.boundaries j = ⊥
theorem
homological_complex.boundaries_le_cycles
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
(C : homological_complex V c)
(i : ι) :
C.boundaries i ≤ C.cycles i
@[reducible]
noncomputable
def
homological_complex.boundaries_to_cycles
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
(C : homological_complex V c)
(i : ι) :
↑(C.boundaries i) ⟶ ↑(C.cycles i)
The canonical map from boundaries i to cycles i.
@[simp]
theorem
homological_complex.image_to_kernel_as_boundaries_to_cycles
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
(C : homological_complex V c)
(i : ι)
(h : C.boundaries i ≤ C.cycles i) :
(C.boundaries i).of_le (C.cycles i) h = C.boundaries_to_cycles i
Prefer boundaries_to_cycles.
@[reducible]
noncomputable
def
homological_complex.homology
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
[category_theory.limits.has_cokernels V]
(C : homological_complex V c)
(i : ι) :
V
The homology of a complex at index i.
Computing the cycles is functorial.
@[reducible]
noncomputable
def
cycles_map
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_kernels V]
{C₁ C₂ : homological_complex V c}
(f : C₁ ⟶ C₂)
(i : ι) :
The morphism between cycles induced by a chain map.
@[simp]
theorem
cycles_map_arrow_assoc
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_kernels V]
{C₁ C₂ : homological_complex V c}
(f : C₁ ⟶ C₂)
(i : ι)
{X' : V}
(f' : C₂.X i ⟶ X') :
@[simp]
theorem
cycles_map_arrow_apply
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_kernels V]
{C₁ C₂ : homological_complex V c}
(f : C₁ ⟶ C₂)
(i : ι)
[I : category_theory.concrete_category V]
(x : ↥↑(C₁.cycles i)) :
@[simp]
theorem
cycles_map_arrow
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_kernels V]
{C₁ C₂ : homological_complex V c}
(f : C₁ ⟶ C₂)
(i : ι) :
@[simp]
theorem
cycles_map_id
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_kernels V]
{C₁ : homological_complex V c}
(i : ι) :
@[simp]
theorem
cycles_map_comp
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_kernels V]
{C₁ C₂ C₃ : homological_complex V c}
(f : C₁ ⟶ C₂)
(g : C₂ ⟶ C₃)
(i : ι) :
cycles_map (f ≫ g) i = cycles_map f i ≫ cycles_map g i
@[simp]
theorem
cycles_functor_map
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_kernels V]
(i : ι)
(C₁ C₂ : homological_complex V c)
(f : C₁ ⟶ C₂) :
(cycles_functor V c i).map f = cycles_map f i
noncomputable
def
cycles_functor
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_kernels V]
(i : ι) :
homological_complex V c ⥤ V
Cycles as a functor.
Equations
- cycles_functor V c i = {obj := λ (C : homological_complex V c), ↑(C.cycles i), map := λ (C₁ C₂ : homological_complex V c) (f : C₁ ⟶ C₂), cycles_map f i, map_id' := _, map_comp' := _}
Instances for cycles_functor
@[simp]
theorem
cycles_functor_obj
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_kernels V]
(i : ι)
(C : homological_complex V c) :
(cycles_functor V c i).obj C = ↑(C.cycles i)
Computing the boundaries is functorial.
@[reducible]
noncomputable
def
boundaries_map
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
{C₁ C₂ : homological_complex V c}
(f : C₁ ⟶ C₂)
(i : ι) :
↑(C₁.boundaries i) ⟶ ↑(C₂.boundaries i)
The morphism between boundaries induced by a chain map.
noncomputable
def
boundaries_functor
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
(i : ι) :
homological_complex V c ⥤ V
Boundaries as a functor.
Equations
- boundaries_functor V c i = {obj := λ (C : homological_complex V c), ↑(C.boundaries i), map := λ (C₁ C₂ : homological_complex V c) (f : C₁ ⟶ C₂), category_theory.limits.image_subobject_map (homological_complex.hom.sq_to f i), map_id' := _, map_comp' := _}
Instances for boundaries_functor
@[simp]
theorem
boundaries_functor_obj
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
(i : ι)
(C : homological_complex V c) :
(boundaries_functor V c i).obj C = ↑(C.boundaries i)
@[simp]
theorem
boundaries_functor_map
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
(i : ι)
(C₁ C₂ : homological_complex V c)
(f : C₁ ⟶ C₂) :
The boundaries_to_cycles morphisms are natural.
@[simp]
theorem
boundaries_to_cycles_naturality_assoc
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
{C₁ C₂ : homological_complex V c}
(f : C₁ ⟶ C₂)
(i : ι)
{X' : V}
(f' : ↑(C₂.cycles i) ⟶ X') :
boundaries_map f i ≫ C₂.boundaries_to_cycles i ≫ f' = C₁.boundaries_to_cycles i ≫ cycles_map f i ≫ f'
@[simp]
theorem
boundaries_to_cycles_naturality
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{c : complex_shape ι}
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
{C₁ C₂ : homological_complex V c}
(f : C₁ ⟶ C₂)
(i : ι) :
boundaries_map f i ≫ C₂.boundaries_to_cycles i = C₁.boundaries_to_cycles i ≫ cycles_map f i
@[simp]
theorem
boundaries_to_cycles_nat_trans_app
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
(i : ι)
(C : homological_complex V c) :
(boundaries_to_cycles_nat_trans V c i).app C = C.boundaries_to_cycles i
noncomputable
def
boundaries_to_cycles_nat_trans
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
(i : ι) :
boundaries_functor V c i ⟶ cycles_functor V c i
The natural transformation from the boundaries functor to the cycles functor.
Equations
- boundaries_to_cycles_nat_trans V c i = {app := λ (C : homological_complex V c), C.boundaries_to_cycles i, naturality' := _}
noncomputable
def
homology_functor
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
(i : ι) :
homological_complex V c ⥤ V
The i-th homology, as a functor to V.
Equations
- homology_functor V c i = {obj := λ (C : homological_complex V c), C.homology i, map := λ (C₁ C₂ : homological_complex V c) (f : C₁ ⟶ C₂), homology.map _ _ (homological_complex.hom.sq_to f i) (homological_complex.hom.sq_from f i) _, map_id' := _, map_comp' := _}
Instances for homology_functor
@[simp]
theorem
homology_functor_obj
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
(i : ι)
(C : homological_complex V c) :
(homology_functor V c i).obj C = C.homology i
@[simp]
theorem
homology_functor_map
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
(i : ι)
(C₁ C₂ : homological_complex V c)
(f : C₁ ⟶ C₂) :
(homology_functor V c i).map f = homology.map _ _ (homological_complex.hom.sq_to f i) (homological_complex.hom.sq_from f i) _
@[simp]
theorem
graded_homology_functor_obj
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
(C : homological_complex V c)
(i : ι) :
(graded_homology_functor V c).obj C i = C.homology i
noncomputable
def
graded_homology_functor
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V] :
The homology functor from ι-indexed complexes to ι-graded objects in V.
Equations
- graded_homology_functor V c = {obj := λ (C : homological_complex V c) (i : ι), C.homology i, map := λ (C C' : homological_complex V c) (f : C ⟶ C') (i : ι), (homology_functor V c i).map f, map_id' := _, map_comp' := _}
@[simp]
theorem
graded_homology_functor_map
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
(C C' : homological_complex V c)
(f : C ⟶ C')
(i : ι) :
(graded_homology_functor V c).map f i = (homology_functor V c i).map f