Tensor Product of Free Modules is Free

Theorem

Let $A$ be a commutative ring with unity.

Let $F$ and $F'$ be free $A$-modules.

Then the tensor product $F \otimes_A F'$ is a free $A$-module.

Proof

By Free Module is Isomorphic to Free Module on Set there are sets $I$ and $I'$ and isomorphisms $\Psi : A^{\paren I} \to F$ and $\Psi' : A^{\paren {I'} } \to F'$.

By Tensor Product Distributes over Direct Sum, there is an isomorphism:

$\ds A^{\paren I} \otimes_A A^{\paren {I'} } \cong \bigoplus_{i \mathop \in I} \bigoplus_{i' \mathop \in I'} A$

By Direct Sum of Direct Sums is Direct Sum, there is an isomorphism:

$\ds \bigoplus_{i \mathop \in I} \bigoplus_{i' \mathop \in I'} A \cong \bigoplus_{\tuple {i, i'} \mathop \in I \times I'} A$

Hence $A^{\paren I} \otimes_A A^{\paren {I'} } \cong A^{\paren {I \times I'} }$ by definition of $A^{\paren {I \times I'} }$.

By Free Module on Set is Free $A^{\paren {I \times I'} }$ is free.

By Module Isomorphic to Free Module is Free $A^{\paren I} \otimes_A A^{\paren {I'} }$ is free.

$\blacksquare$