mathlib3 documentation

algebra.homology.Module

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))) :
(C.cycles i)

Bundle an element C.X i such that C.d_from i x = 0 as a term of C.cycles i.

@[ext]
theorem Module.cycles_ext {R : Type v} [ring R] {ι : Type u_1} {c : complex_shape ι} {C : homological_complex (Module R) c} {i : ι} {x y : (C.cycles i)} (w : ((C.cycles i).arrow) x = ((C.cycles i).arrow) y) :
x = y
@[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))) :
@[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