The Exercise

A classical linear code encodes $k$ bits into $n$ bits. Its generator matrix $G$ is an $n \times k$ matrix with entries in $\mathbb{Z}_2$: a message $x$ of $k$ bits is encoded as the codeword $Gx$, and the code is the set of all codewords. Exercise 10.15 is to show that adding one column of $G$ to another gives a generator matrix of the same code.

Column Addition

Let $M$ be a matrix with entries in a set carrying an addition, its rows labelled by some set and its columns by a set $C$. For columns $i$ and $j$ of $M$, the matrix $M^{(i\to j)}$ obtained by adding column $i$ to column $j$ is the matrix of the same shape whose column $j$ is the sum of columns $j$ and $i$ of $M$ and whose other columns are those of $M$: $$M^{(i\to j)}_{ab} = \begin{cases} M_{aj} + M_{ai}, & b = j,\\ M_{ab}, & b \neq j. \end{cases}$$(1)^✦

The Claim

The image of a matrix $M$ with entries in a commutative ring $R$ and columns labelled by a finite set $C$ is the set of vectors $Mx$ for $x$ in $R^C$, the space of column vectors with one entry in $R$ for each column of $M$.

With $R = \mathbb{Z}_2$ and $M = G$ this is the exercise.

What Is Checked

The claim is stated over the matrix $M^{(i\to j)}$ of (1). What the library proves about this construction is (2), for any two distinct columns.