Matrix presentations of linear codes

A matrix presents a linear code in either of two complementary ways. A generator matrix presents the span of its rows, implemented as the range of Matrix.vecMulLinear; a parity-check matrix presents the kernel of Matrix.mulVecLin. This file defines both constructions and the predicates saying that a matrix presents a specified code.

The API identifies membership with coefficient vectors or vanishing syndromes, computes both dimensions from matrix rank, and characterizes compatibility of a generator and a parity-check matrix by the matrix equation H * Gᵀ = 0. These facts are the linear-algebra interface used by systematic presentations, dual codes, and exact verification of named finite codes.

Row indices carry no coordinate meaning: invertible row operations leave both codes unchanged, a surjective row reindexing leaves the generated code unchanged, and the checked code depends only on the row space. A coordinate equivalence e : ι' ≃ ι transports both codes along LinearEquiv.funCongrLeft. The code checked by H is the orthogonal of the code generated by H for the standard dot product, so a generator matrix of C is a parity-check matrix of the Euclidean dual of C. A generator matrix with linearly independent rows is the same thing as a basis of the code, and encoding by it identifies messages with codewords. Dependent rows of a generator matrix may be deleted, and the systematic matrices [I | A] and [-Aᵀ | I] present the same code, one by its rows and the other by its syndromes, also after the coordinates are arranged by an equivalence ι ≃ ρ ⊕ τ singling out the information coordinates ρ.

Main definitions

• Matrix.generatedBy is the row code of a matrix.
• Matrix.checkedBy is the code with vanishing syndrome for a matrix.
• TauCeti.LinearCode.IsGeneratorMatrix and TauCeti.LinearCode.IsParityCheckMatrix record that either presentation gives a specified code.
• TauCeti.LinearCode.IsGeneratorMatrix.basis is the basis of a code formed by the rows of a generator matrix with linearly independent rows.

Main results

• Matrix.finrank_generatedBy and Matrix.finrank_checkedBy compute both dimensions from the matrix rank.
• Matrix.checkedBy_eq_orthogonal_generatedBy: checking by H is orthogonality to the rows of H.
• TauCeti.LinearCode.basisEquivFullRankGeneratorMatrix: bases of a code correspond to its generator matrices with linearly independent rows.
• TauCeti.LinearCode.IsGeneratorMatrix.encodingEquiv: such a generator matrix identifies messages with codewords by a ↦ a ᵥ* G.
• TauCeti.LinearCode.exists_isGeneratorMatrix: generator presentations with linearly independent rows exist.
• Matrix.generatedBy_one_fromCols_eq_checkedBy_fromCols_neg_transpose_one: [I | A] generates the code checked by [-Aᵀ | I].
• Matrix.exists_linearIndependent_generatedBy_submatrix: deleting dependent rows.

References

• W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes, Cambridge University Press, 2003, §§1.2–1.4 (generator and parity-check matrices, systematic form, syndromes).

def Matrix.generatedBy {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] (G : Matrix ρ ι F) : TauCeti.LinearCode F ι

The linear code generated by the rows of G. A coefficient vector a represents the codeword a ᵥ* G.

def Matrix.checkedBy {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ι] (H : Matrix ρ ι F) : TauCeti.LinearCode F ι

The linear code checked by H: its words are exactly those with zero syndrome H *ᵥ x.

theorem Matrix.generatedBy_def {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] (G : Matrix ρ ι F) : G.generatedBy = G.vecMulLinear.range

The code generated by G is the range of vector-matrix multiplication by G.

theorem Matrix.checkedBy_def {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ι] (H : Matrix ρ ι F) : H.checkedBy = H.mulVecLin.ker

The code checked by H is the kernel of matrix-vector multiplication by H.

def TauCeti.LinearCode.IsGeneratorMatrix {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] (C : LinearCode F ι) (G : Matrix ρ ι F) : Prop

A matrix is a generator matrix for C when its rows span C.

def TauCeti.LinearCode.IsParityCheckMatrix {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ι] (C : LinearCode F ι) (H : Matrix ρ ι F) : Prop

A matrix is a parity-check matrix for C when C is its kernel.

@[simp]

theorem TauCeti.LinearCode.isGeneratorMatrix_def {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] (C : LinearCode F ι) (G : Matrix ρ ι F) : C.IsGeneratorMatrix G ↔ G.generatedBy = C

G is a generator matrix for C exactly when the code generated by G is C.

@[simp]

theorem TauCeti.LinearCode.isParityCheckMatrix_def {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ι] (C : LinearCode F ι) (H : Matrix ρ ι F) : C.IsParityCheckMatrix H ↔ H.checkedBy = C

H is a parity-check matrix for C exactly when the code checked by H is C.

theorem Matrix.generatedBy_eq_span_rows {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] (G : Matrix ρ ι F) : G.generatedBy = Submodule.span F (Set.range G.row)

The generated code is the span of the rows.

@[simp]

theorem Matrix.mem_generatedBy_iff {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] {G : Matrix ρ ι F} {x : ι → F} : x ∈ G.generatedBy ↔ ∃ (a : ρ → F), vecMul a G = x

A word belongs to the code generated by G exactly when it is a linear combination of the rows, expressed as right multiplication by G.

theorem Matrix.row_mem_generatedBy {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] (G : Matrix ρ ι F) (r : ρ) : G.row r ∈ G.generatedBy

Every row of a matrix belongs to its generated code.

@[simp]

theorem Matrix.generatedBy_le_iff {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] {G : Matrix ρ ι F} {C : TauCeti.LinearCode F ι} : G.generatedBy ≤ C ↔ ∀ (r : ρ), G.row r ∈ C

The row code of G lies in C exactly when every row of G lies in C.

theorem Matrix.generatedBy_submatrix_equiv {F : Type u_1} {ι : Type u_2} {ι' : Type u_3} {ρ : Type u_4} [Field F] [Fintype ρ] (G : Matrix ρ ι F) (e : ι' ≃ ι) : (G.submatrix id ⇑e).generatedBy = Submodule.map (↑(LinearEquiv.funCongrLeft F F e)) G.generatedBy

Reindexing the coordinates along e transports the generated code along LinearEquiv.funCongrLeft.

@[simp]

theorem Matrix.mem_checkedBy_iff {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ι] {H : Matrix ρ ι F} {x : ι → F} : x ∈ H.checkedBy ↔ H.mulVec x = 0

A word belongs to the code checked by H exactly when its syndrome vanishes.

@[simp]

theorem Matrix.le_checkedBy_iff {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ι] {C : TauCeti.LinearCode F ι} {H : Matrix ρ ι F} : C ≤ H.checkedBy ↔ ∀ x ∈ C, H.mulVec x = 0

A code lies in the code checked by H exactly when H kills each of its words.

theorem Matrix.checkedBy_le_mul {F : Type u_1} {ι : Type u_2} {σ : Type u_6} {σ' : Type u_7} [Field F] [Fintype ι] [Fintype σ] (P : Matrix σ' σ F) (H : Matrix σ ι F) : H.checkedBy ≤ (P * H).checkedBy

Left multiplication can only enlarge the checked code.

theorem Matrix.checkedBy_mul_of_isUnit {F : Type u_1} {ι : Type u_2} {σ : Type u_6} [Field F] [Fintype ι] [Fintype σ] [DecidableEq σ] {P : Matrix σ σ F} (hP : IsUnit P) (H : Matrix σ ι F) : (P * H).checkedBy = H.checkedBy

Invertible row operations do not change the checked code.

theorem Matrix.checkedBy_submatrix_equiv {F : Type u_1} {ι : Type u_2} {ι' : Type u_3} {σ : Type u_6} [Field F] [Fintype ι] [Fintype ι'] (H : Matrix σ ι F) (e : ι' ≃ ι) : (H.submatrix id ⇑e).checkedBy = Submodule.map (↑(LinearEquiv.funCongrLeft F F e)) H.checkedBy

Reindexing the coordinates along e transports the checked code along LinearEquiv.funCongrLeft.

theorem Matrix.isGeneratorMatrix_generatedBy {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] (G : Matrix ρ ι F) : G.generatedBy.IsGeneratorMatrix G

Every matrix is a generator matrix for its generated code.

theorem Matrix.isParityCheckMatrix_checkedBy {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ι] (H : Matrix ρ ι F) : H.checkedBy.IsParityCheckMatrix H

Every matrix is a parity-check matrix for its checked code.

@[simp]

theorem Matrix.finrank_generatedBy {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] [Fintype ι] (G : Matrix ρ ι F) : Module.finrank F ↥G.generatedBy = G.rank

The dimension of the code generated by a matrix is the rank of that matrix.

@[simp]

theorem Matrix.finrank_checkedBy {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ι] (H : Matrix ρ ι F) : Module.finrank F ↥H.checkedBy = Fintype.card ι - H.rank

The dimension of the code checked by a matrix is the number of coordinates minus the rank of that matrix.

theorem Matrix.generatedBy_le_checkedBy_iff {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} {σ : Type u_6} [Field F] [Fintype ρ] [Fintype ι] {G : Matrix ρ ι F} {H : Matrix σ ι F} : G.generatedBy ≤ H.checkedBy ↔ H * G.transpose = 0

The rows of G satisfy all checks in H exactly when H * Gᵀ = 0.

theorem Matrix.checkedBy_eq_orthogonal_generatedBy {F : Type u_1} {ι : Type u_2} {σ : Type u_6} [Field F] [Fintype ι] [Fintype σ] (H : Matrix σ ι F) : H.checkedBy = LinearMap.BilinForm.orthogonal (dotProductBilin F F) H.generatedBy

A word is checked by H exactly when it is orthogonal, for the dot product, to every word generated by H.

theorem Matrix.checkedBy_eq_of_generatedBy_eq {F : Type u_1} {ι : Type u_2} {σ : Type u_6} {σ' : Type u_7} [Field F] [Fintype ι] [Fintype σ] [Fintype σ'] {H : Matrix σ ι F} {H' : Matrix σ' ι F} (h : H.generatedBy = H'.generatedBy) : H.checkedBy = H'.checkedBy

The code checked by a matrix depends only on its row space.

theorem Matrix.generatedBy_one_fromCols_eq_checkedBy_fromCols_neg_transpose_one {F : Type u_1} {ρ : Type u_4} {τ : Type u_8} [Field F] [Fintype ρ] [Fintype τ] [DecidableEq ρ] [DecidableEq τ] (A : Matrix ρ τ F) : (fromCols 1 A).generatedBy = ((-A.transpose).fromCols 1).checkedBy

The systematic generator matrix [I | A] and the systematic parity-check matrix [-Aᵀ | I] present the same code.

theorem Matrix.generatedBy_one_fromCols_eq_checkedBy_fromCols_neg_transpose_one_submatrix {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} {τ : Type u_8} [Field F] [Fintype ι] [Fintype ρ] [DecidableEq ρ] [DecidableEq τ] (A : Matrix ρ τ F) (e : ι ≃ ρ ⊕ τ) : ((fromCols 1 A).submatrix id ⇑e).generatedBy = (((-A.transpose).fromCols 1).submatrix id ⇑e).checkedBy

Systematic form relative to an information set: if the coordinates are split as ρ ⊕ τ by e, with the information coordinates ρ, then [I | A] and [-Aᵀ | I] with columns arranged by e still present the same code.

theorem Matrix.exists_linearIndependent_generatedBy_submatrix {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] (G : Matrix ρ ι F) : ∃ (s : Finset ρ), LinearIndependent F (G.submatrix Subtype.val id).row ∧ (G.submatrix Subtype.val id).generatedBy = G.generatedBy

Deleting dependent rows: some linearly independent subfamily of the rows of G generates the same code.

theorem TauCeti.LinearCode.isGeneratorMatrix_iff_forall {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] {C : LinearCode F ι} {G : Matrix ρ ι F} : C.IsGeneratorMatrix G ↔ (∀ x ∈ C, ∃ (a : ρ → F), Matrix.vecMul a G = x) ∧ ∀ (a : ρ → F), Matrix.vecMul a G ∈ C

A matrix generates C exactly when every word of C has a coefficient vector and every represented word belongs to C.

theorem TauCeti.LinearCode.isParityCheckMatrix_iff_mem {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ι] {C : LinearCode F ι} {H : Matrix ρ ι F} : C.IsParityCheckMatrix H ↔ ∀ (x : ι → F), x ∈ C ↔ H.mulVec x = 0

A matrix is a parity-check matrix for C exactly when vanishing of the syndrome characterizes membership in C.

theorem TauCeti.LinearCode.IsGeneratorMatrix.isParityCheckMatrix_orthogonal {F : Type u_1} {ι : Type u_2} {σ : Type u_6} [Field F] [Fintype ι] [Fintype σ] {C : LinearCode F ι} {G : Matrix σ ι F} (hG : C.IsGeneratorMatrix G) : IsParityCheckMatrix (LinearMap.BilinForm.orthogonal (dotProductBilin F F) C) G

A generator matrix of C is a parity-check matrix of the Euclidean dual of C.

theorem TauCeti.LinearCode.card_eq_finrank_of_isGeneratorMatrix_of_linearIndependent {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] {C : LinearCode F ι} {G : Matrix ρ ι F} (hG : C.IsGeneratorMatrix G) (hli : LinearIndependent F G.row) : Fintype.card ρ = Module.finrank F ↥C

A full-row-rank generator matrix for C has one row per dimension of C.

Bases and generator matrices with linearly independent rows

noncomputable def TauCeti.LinearCode.IsGeneratorMatrix.basis {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] {C : LinearCode F ι} {G : Matrix ρ ι F} (hG : C.IsGeneratorMatrix G) (hli : LinearIndependent F G.row) : Module.Basis ρ F ↥C

The rows of a generator matrix for C with linearly independent rows form a basis of C.

@[simp]

theorem TauCeti.LinearCode.IsGeneratorMatrix.coe_basis_apply {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] {C : LinearCode F ι} {G : Matrix ρ ι F} (hG : C.IsGeneratorMatrix G) (hli : LinearIndependent F G.row) (r : ρ) : ↑((hG.basis hli) r) = G.row r

The basis vectors given by a generator matrix are its rows.

noncomputable def TauCeti.LinearCode.IsGeneratorMatrix.encodingEquiv {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] {C : LinearCode F ι} {G : Matrix ρ ι F} (hG : C.IsGeneratorMatrix G) (hli : LinearIndependent F G.row) : (ρ → F) ≃ₗ[F] ↥C

Encoding by a generator matrix for C with linearly independent rows: the linear equivalence between messages and codewords sending a message a to a ᵥ* G.

@[simp]

theorem TauCeti.LinearCode.IsGeneratorMatrix.coe_encodingEquiv_apply {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] {C : LinearCode F ι} {G : Matrix ρ ι F} (hG : C.IsGeneratorMatrix G) (hli : LinearIndependent F G.row) (a : ρ → F) : ↑((hG.encodingEquiv hli) a) = Matrix.vecMul a G

Encoding multiplies the message by the generator matrix.

@[simp]

theorem TauCeti.LinearCode.IsGeneratorMatrix.vecMul_encodingEquiv_symm_apply {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] {C : LinearCode F ι} {G : Matrix ρ ι F} (hG : C.IsGeneratorMatrix G) (hli : LinearIndependent F G.row) (x : ↥C) : Matrix.vecMul ((hG.encodingEquiv hli).symm x) G = ↑x

Decoding a codeword gives the unique message whose encoding is that codeword.

theorem TauCeti.LinearCode.isGeneratorMatrix_of_basis {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] {C : LinearCode F ι} (b : Module.Basis ρ F ↥C) : C.IsGeneratorMatrix (Matrix.of fun (r : ρ) => ↑(b r))

The matrix whose rows are the vectors of a basis of C is a generator matrix for C.

theorem TauCeti.LinearCode.linearIndependent_row_of_basis {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] {C : LinearCode F ι} (b : Module.Basis ρ F ↥C) : LinearIndependent F (Matrix.of fun (r : ρ) => ↑(b r)).row

The matrix whose rows are the vectors of a basis has linearly independent rows.

noncomputable def TauCeti.LinearCode.basisEquivFullRankGeneratorMatrix {F : Type u_1} {ι : Type u_2} [Field F] (C : LinearCode F ι) (ρ : Type u_9) [Fintype ρ] : Module.Basis ρ F ↥C ≃ { G : Matrix ρ ι F // C.IsGeneratorMatrix G ∧ LinearIndependent F G.row }

Bases of C indexed by ρ correspond exactly to generator matrices for C with row type ρ and linearly independent rows: a basis corresponds to the matrix whose rows are its vectors.

@[simp]

theorem TauCeti.LinearCode.coe_basisEquivFullRankGeneratorMatrix_apply {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] {C : LinearCode F ι} (b : Module.Basis ρ F ↥C) : ↑((C.basisEquivFullRankGeneratorMatrix ρ) b) = Matrix.of fun (r : ρ) => ↑(b r)

The generator matrix attached to a basis has the basis vectors as its rows.

@[simp]

theorem TauCeti.LinearCode.basisEquivFullRankGeneratorMatrix_symm_apply {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] {C : LinearCode F ι} (G : { G : Matrix ρ ι F // C.IsGeneratorMatrix G ∧ LinearIndependent F G.row }) : (C.basisEquivFullRankGeneratorMatrix ρ).symm G = ⋯.basis ⋯

The basis attached to a generator matrix with linearly independent rows is formed by its rows.

theorem TauCeti.LinearCode.exists_isGeneratorMatrix {F : Type u_1} {ι : Type u_2} [Field F] [Finite ι] (C : LinearCode F ι) : ∃ (G : Matrix (Fin (Module.finrank F ↥C)) ι F), C.IsGeneratorMatrix G ∧ LinearIndependent F G.row

Every finite-length linear code has a generator matrix with one row per dimension, and those rows are linearly independent.

theorem TauCeti.LinearCode.card_eq_card_sub_finrank_of_isParityCheckMatrix_of_linearIndependent {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} [Field F] [Fintype ρ] [Fintype ι] {C : LinearCode F ι} {H : Matrix ρ ι F} (hH : C.IsParityCheckMatrix H) (hli : LinearIndependent F H.row) : Fintype.card ρ = Fintype.card ι - Module.finrank F ↥C

A full-row-rank parity-check matrix for C has length - dim C rows.

theorem TauCeti.LinearCode.IsGeneratorMatrix.mul_transpose_eq_zero {F : Type u_1} {ι : Type u_2} {ρ : Type u_4} {σ : Type u_6} [Field F] [Fintype ρ] [Fintype ι] {C : LinearCode F ι} {G : Matrix ρ ι F} {H : Matrix σ ι F} (hG : C.IsGeneratorMatrix G) (hH : C.IsParityCheckMatrix H) : H * G.transpose = 0

A generator matrix and a parity-check matrix for the same code satisfy H * Gᵀ = 0.