Proposition (every chain complex of finitely generated free modules over a Bézout domain is the direct sum of some of its subcomplexes with at most two nonzero terms):
Let
be a chain complex whose objects are finitely generated free modules over a Bézout domain . This chain complex is then the countable direct sum of chain complexes of the form
- ,
where and .
(On the condition of the countable choice.)
Proof: We shall construct a direct sum decomposition
- ,
where . Once this is accomplished, we have in fact obtained a direct sum decomposition of the initial chain complex, because elements of are mapped to zero by , and elements of are mapped to due to the chain complex condition .
In order to achieve this decomposition, we invoke Dedekind's theorem for Bézout domains, which tells us that is finitely generated and free; indeed, it is finitely generated, since a generating set is given by the image (via ) of a generating set of . Let thus be a basis of . For each , we choose an arbitrary, but fixed , and then we define . This yields the desired direct sum decomposition. Indeed, , since whenever
for some elements of , applying to both sides of this equation and using its -linearity yields
- ,
which implies . Moreover, , since if is arbitrary, we may select such that
- ,
from which we may easily deduce that
- .
Proposition (every chain complex of finitely generated free modules over a Bézout domain splits as the direct sum of two types of elementary chain complexes):
Let
be a chain complex whose objects are finitely generated free modules over a Bézout domain . This chain complex is the countable direct sum of copies of the following two chain complexes:
- for an element , ie. the arrow represents the function which is given by multiplication by
(On the condition of the countable choice.)
Proof: Using the notation of the last theorem, we have , where is finitely generated and is sent to zero by .