Lean, informalized

Nielsen & Chuang · Chapter 10, Quantum error-correction · p. 447

Exercise 10.18 - The product of the parity check and generator matrices of one linear code is zero

A parity check matrix annihilates its generator matrix.

Hover over a blue or green term in the text, or a node in the graph, to find it in the other. Select it to read its declaration both in Lean and in words.

The Exercise

Messages are encoded with a generator matrix GG, which turns a message into a codeword, and received words are tested with a parity check matrix HH, which tells whether a word belongs to the code. The exercise is to show that a generator matrix and a parity check matrix of the same linear code satisfy HG=0HG = 0.✦

Linear Codes

The entries of all matrices are taken from a ring RR; for binary codes R=ℤ2R = \mathbb{Z}_2. The code generated by an m×nm \times n matrix GG with entries in RR is the set CGC_G of words in RmR^m of the form GxGx, the range of the linear map x↦Gxx \mapsto Gx on RnR^n: CG={Gx:x∈Rn}.C_G = \{\, Gx : x \in R^n \,\}.(1)

The kernel of an l×ml \times m matrix HH with entries in RR is the set of words in RmR^m that HH maps to zero: ker⁡H={y∈Rm:Hy=0}.\ker H = \{\, y \in R^m : Hy = 0 \,\}.(2)

The Claim

Theorem 1. Let GG be an m×nm \times n matrix and HH an l×ml \times m matrix, both with entries in a commutative ring RR. If the code generated by GG is the kernel of HH, CG=ker⁡HC_G = \ker H, then HG=0.HG = 0.(3)✦

A linear code is a submodule of RmR^m, a set of codewords closed under addition and scalar multiples from RR; when GG and HH are a generator matrix and a parity check matrix of one such code, CG=ker⁡HC_G = \ker H holds, and this is the exercise.

What Is Checked

The claim is stated over two matrices with entries in RR, of any sizes for which the product HGHG is defined, and over the two sets of words they determine: the code (1) generated by GG and the kernel (2) of HH. What the library proves about these constructions is the theorem above, display (3).