Complexes of modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We provide some additional API to work with homological complexes in Module R.
theorem
Module.homology_ext
{R : Type v}
[ring R]
{L M N K : Module R}
{f : L ⟶ M}
{g : M ⟶ N}
(w : f ≫ g = 0)
{h k : homology f g w ⟶ K}
(w_1 : ∀ (x : ↥(linear_map.ker g)), ⇑h (⇑(category_theory.limits.cokernel.π (image_to_kernel f g w)) (⇑Module.to_kernel_subobject x)) = ⇑k (⇑(category_theory.limits.cokernel.π (image_to_kernel f g w)) (⇑Module.to_kernel_subobject x))) :
h = k
To prove that two maps out of a homology group are equal, it suffices to check they are equal on the images of cycles.
@[reducible]
noncomputable
def
Module.to_cycles
{R : Type v}
[ring R]
{ι : Type u_1}
{c : complex_shape ι}
{C : homological_complex (Module R) c}
{i : ι}
(x : ↥(linear_map.ker (C.d_from i))) :
Bundle an element C.X i such that C.d_from i x = 0 as a term of C.cycles i.
@[simp]
theorem
Module.cycles_map_to_cycles
{R : Type v}
[ring R]
{ι : Type u_1}
{c : complex_shape ι}
{C D : homological_complex (Module R) c}
(f : C ⟶ D)
{i : ι}
(x : ↥(linear_map.ker (C.d_from i))) :
⇑(cycles_map f i) (Module.to_cycles x) = Module.to_cycles ⟨⇑(f.f i) x.val, _⟩
@[reducible]
noncomputable
def
Module.to_homology
{R : Type v}
[ring R]
{ι : Type u_1}
{c : complex_shape ι}
{C : homological_complex (Module R) c}
{i : ι}
(x : ↥(linear_map.ker (C.d_from i))) :
Build a term of C.homology i from an element C.X i such that C.d_from i x = 0.
@[ext]
theorem
Module.homology_ext'
{R : Type v}
[ring R]
{ι : Type u_1}
{c : complex_shape ι}
{C : homological_complex (Module R) c}
{M : Module R}
(i : ι)
{h k : C.homology i ⟶ M}
(w : ∀ (x : ↥(linear_map.ker (C.d_from i))), ⇑h (Module.to_homology x) = ⇑k (Module.to_homology x)) :
h = k