Generator matrices and parity-check matrices

The rows of a matrix generate a linear code, while the same matrix checks the Euclidean dual of that code. This identifies the kernel presentation by a parity-check matrix with the orthogonal complement of its row space and makes conversion between generator and parity-check matrices literal: no transpose or choice of coordinates is needed.

For every finite-length code, a basis of its Euclidean dual therefore gives a full-row-rank parity-check matrix. The number of its rows is the codimension of the original code.

The conventions follow Huffman and Pless, Fundamentals of Error-Correcting Codes, Sections 1.2--1.4.

Main results

• Matrix.checkedBy_eq_euclideanDual_generatedBy identifies a matrix kernel with the orthogonal complement of its row space.
• LinearCode.isGeneratorMatrix_iff_isParityCheckMatrix_euclideanDual converts generator matrices into parity-check matrices for the dual code.
• LinearCode.isParityCheckMatrix_of_basis_euclideanDual: a basis of the dual code gives a parity-check matrix, and LinearCode.exists_isParityCheckMatrix uses it to construct one with linearly independent rows.
• Matrix.generatedBy_isSelfOrthogonal_iff_mul_transpose_eq_zero: the code generated by the rows of G is self-orthogonal exactly when G * Gᵀ = 0; Matrix.generatedBy_isSelfDual_of_mul_transpose_eq_zero_and_card_le adds a dimension hypothesis to conclude that the generated code is self-dual.

@[simp]

theorem Matrix.checkedBy_eq_euclideanDual_generatedBy {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [Fintype ι] [Fintype ρ] (H : Matrix ρ ι F) : H.checkedBy = Submodule.euclideanDual H.generatedBy

The code checked by a matrix is the Euclidean dual of the code generated by its rows.

theorem Matrix.checkedBy_eq_iff_generatedBy_eq {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [Fintype ι] {σ : Type u_4} [Fintype ρ] [Fintype σ] (H : Matrix ρ ι F) (H' : Matrix σ ι F) : H.checkedBy = H'.checkedBy ↔ H.generatedBy = H'.generatedBy

Two matrices check the same code exactly when their rows span the same code.

theorem Matrix.generatedBy_isSelfOrthogonal_iff_mul_transpose_eq_zero {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [Fintype ι] [Fintype ρ] (G : Matrix ρ ι F) : Submodule.IsSelfOrthogonal G.generatedBy ↔ G * G.transpose = 0

The code generated by a matrix is self-orthogonal exactly when the rows of the matrix are pairwise orthogonal, i.e. when G * Gᵀ = 0.

theorem Matrix.generatedBy_isSelfDual_of_mul_transpose_eq_zero_and_card_le {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [Fintype ι] [Fintype ρ] (G : Matrix ρ ι F) (hgram : G * G.transpose = 0) (hdim : Fintype.card ι ≤ 2 * G.rank) : Submodule.IsSelfDual G.generatedBy

A matrix whose rows are pairwise orthogonal and which has half the ambient dimension as many independent rows generates a self-dual code.

theorem TauCeti.LinearCode.isGeneratorMatrix_iff_isParityCheckMatrix_euclideanDual {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [Fintype ι] {C : LinearCode F ι} {G : Matrix ρ ι F} [Fintype ρ] : C.IsGeneratorMatrix G ↔ IsParityCheckMatrix (Submodule.euclideanDual C) G

A matrix generates C exactly when it checks the Euclidean dual of C.

theorem TauCeti.LinearCode.isParityCheckMatrix_iff_isGeneratorMatrix_euclideanDual {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [Fintype ι] {C : LinearCode F ι} {H : Matrix ρ ι F} [Fintype ρ] : C.IsParityCheckMatrix H ↔ IsGeneratorMatrix (Submodule.euclideanDual C) H

A matrix checks C exactly when it generates the Euclidean dual of C.

theorem TauCeti.LinearCode.isParityCheckMatrix_of_basis_euclideanDual {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [Fintype ι] {C : LinearCode F ι} (b : Module.Basis ρ F ↥(Submodule.euclideanDual C)) : C.IsParityCheckMatrix (Matrix.of fun (r : ρ) => ↑(b r))

The matrix whose rows are the vectors of a basis of the Euclidean dual of C is a parity-check matrix for C.

theorem TauCeti.LinearCode.exists_isParityCheckMatrix {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] (C : LinearCode F ι) : ∃ (H : Matrix (Fin (Fintype.card ι - Module.finrank F ↥C)) ι F), C.IsParityCheckMatrix H ∧ LinearIndependent F H.row

Every finite-length linear code has a parity-check matrix whose rows form a basis of the Euclidean dual. Its row type has cardinality equal to the codimension of the code.