Finiteness and dimension of homology of short complexes of modules

For a short complex X₁ ⟶ X₂ ⟶ X₃ of modules, its homology is the kernel of the second map modulo the range of the first. This file records two consequences of that description:

• over a ring for which the middle module is noetherian, the homology is finitely generated;
• over a division ring, when the middle term is finite-dimensional, the dimension of the homology plus the dimension of the range of the first map is the dimension of the kernel of the second.

References

• Charles A. Weibel, An Introduction to Homological Algebra, Sections 1.1 and 1.3.

theorem CategoryTheory.ShortComplex.finite_homology {k : Type u} [Ring k] (S : ShortComplex (ModuleCat k)) [IsNoetherian k ↑S.X₂] : Module.Finite k ↑S.homology

The homology of a short complex of modules with noetherian middle term is finitely generated.

theorem CategoryTheory.ShortComplex.finrank_homology_add_finrank_range_f {k : Type u} [DivisionRing k] (S : ShortComplex (ModuleCat k)) [Module.Finite k ↑S.X₂] : Module.finrank k ↑S.homology + Module.finrank k ↥(ModuleCat.Hom.hom S.f).range = Module.finrank k ↥(ModuleCat.Hom.hom S.g).ker

The homology of a short complex X₁ ⟶ X₂ ⟶ X₃ of vector spaces with X₂ finite-dimensional has dimension dim ker g - dim im f.