Proposition (extending a single element of a free, finite-dimensional module over a Bézout domain to a basis):
Let be a Bézout domain, and let be the -dimensional free module over . Let be such that . Then there exist elements such that is a basis of .
Proof: We proceed by induction on . If , the statement becomes trivial, so that the induction base is handled. Let now a general be given; we reduce the claim to the same statement for .
Indeed, if is given, we may set
- ,
and then . Hence, there are elements such that
- .
We define
- ,
so that
- and ,
where for , as usual, denotes the vector whose every component is zero except the one in the -th place, which is one. From these equations it is evident that
- .
Also, and are linearly independent, because if there existed such that , then and in particular , so that either and and are linearly independent (almost) by definition, or , so that whenever (once again, if , then the vectors are automatically linearly independent). But this implies that for all , so that contrary to the assumption .
It now suffices to note that
by the first Noether isomorphism theorem applied to the homomorphism that forgets the first component, which reduces the dimension of the problem by one as we have .
Proof: We proceed by induction on , where is the cardinality of a minimum cardinality generating set of . Let be a minimum cardinality generating set of . Then we have a homomorphism
such that for , where is the element of whose every entry is zero, except for the -th entry, which is one. Since is surjective, the first isomorphism theorem implies that
- ,
where . If , then the claim is demonstrated. We lead to a contradiction. Indeed, in this case there is a nonzero vector . We denote and set . Then , for otherwise the image of in via the canonical projection would be a torsion element. Since we have , we may extend to a basis of , and then is generated by the images of via the canonical projection. Yet this contradicts the minimality of .
Proof: If is torsion-free, then every submodule of is torsion-free as well. Hence, as in the theorem's statement is torsion-free and finitely generated. Hence, there exists a basis of .
Proposition (basis extension over Bézout domains):
Let be a Bézout domain, and let be a torsion-free module over . If are linearly independent vectors in such that is torsion-free and finitely generated, then we find an and vectors such that the vectors constitute a basis of .
Proof: Since is torsion-free and finitely generated, upon choosing a generating set of minimal cardinality we obtain a basis of that module. We shall denote this basis by . If moreover
is the canonical projection, we choose a for each . We claim that is a basis. First, we prove that these vectors are linearly independent. Indeed, suppose that are such that
- .
Since is a homomorphism,
- ,
so that . Thus
- ,
which by virtue of the linear independence of implies .
It remains to show that is a generating set of . In order to do so, suppose that is arbitrary. We choose such that
- .
We further define , so that . But by the definition of , this means that , so that there are such that
- , hence ,
which shows that is a generating set of since was arbitrary.
Theorem (dimension formula):