Complexes of semisimple modules split

Let K be a homological complex of modules over a ring R, of any shape, whose terms are semisimple modules; for instance any complex of vector spaces over a division ring, or of modules over a semisimple ring. Every submodule of a semisimple module is a direct summand, and every submodule and quotient of a semisimple module is semisimple. So in every degree the inclusion of the cycles is a split monomorphism and the projection of the cycles onto the homology is a split epimorphism.

By HomologicalComplex.exists_homotopyEquiv_d_eq_zero, K is therefore chain homotopy equivalent to a complex with zero differentials, whose terms are the homology of K: over a division ring every complex is homotopy equivalent to its homology. This reduces statements about the homology of complexes of vector spaces, such as the Künneth theorem over a field, to complexes with zero differential.

Main results

• HomologicalComplex.isSplitMono_iCycles_of_isSemisimpleModule: the cycles of a semisimple term split off.
• HomologicalComplex.isSplitEpi_homologyπ_of_isSemisimpleModule: the homology in a degree with semisimple term splits off the cycles.

instance HomologicalComplex.isSplitMono_iCycles_of_isSemisimpleModule {R : Type u} [Ring R] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat R) c) (i : ι) [IsSemisimpleModule R ↑(K.X i)] : CategoryTheory.IsSplitMono (K.iCycles i)

The inclusion of the cycles into a semisimple term of a complex of modules is a split monomorphism.

instance HomologicalComplex.isSplitEpi_homologyπ_of_isSemisimpleModule {R : Type u} [Ring R] {ι : Type u_1} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat R) c) (i : ι) [IsSemisimpleModule R ↑(K.X i)] : CategoryTheory.IsSplitEpi (K.homologyπ i)

In a degree whose term is semisimple, the projection of the cycles of a complex of modules onto its homology is a split epimorphism: the cycles are a submodule of a semisimple module, hence semisimple.