Row operations on generator matrices

Left multiplication changes the rows of a generator matrix by linear combinations and therefore cannot enlarge its generated code. If the left factor is invertible, this operation preserves the code. This file records that fact through the exact image formula for the generated code, so it can also be used for nonsquare coefficient matrices whose rows still span the whole coefficient space.

The second part treats deletion of a row. The matrix Matrix.deleteRow G r retains all rows of G except row r; it generates the same code precisely when the deleted row is generated by those remaining rows. In particular, every linearly dependent finite family of rows admits such a deletion. Together these results justify row reduction of generator matrices without changing the linear code they present.

Main results

• Matrix.generatedBy_mul_eq_map describes the code generated after left multiplication.
• Matrix.generatedBy_mul_eq_of_isUnit proves invariance under invertible row operations.
• Matrix.generatedBy_deleteRow_eq_iff characterizes when deleting one row preserves the code.
• Matrix.exists_deleteRow_generatedBy_eq_of_not_linearIndependent finds a redundant row in a linearly dependent generator family.

theorem Matrix.generatedBy_mul_eq_map {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} {σ : Type u_4} [Field F] [Fintype ρ] [Fintype σ] (A : Matrix σ ρ F) (G : Matrix ρ ι F) : (A * G).generatedBy = Submodule.map G.vecMulLinear A.generatedBy

Left multiplication maps the row code through right multiplication by the original matrix.

theorem Matrix.generatedBy_mul_le {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} {σ : Type u_4} [Field F] [Fintype ρ] [Fintype σ] (A : Matrix σ ρ F) (G : Matrix ρ ι F) : (A * G).generatedBy ≤ G.generatedBy

Taking linear combinations of the rows of G cannot enlarge its generated code.

theorem Matrix.generatedBy_mul_eq_of_generatedBy_eq_top {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} {σ : Type u_4} [Field F] [Fintype ρ] [Fintype σ] (A : Matrix σ ρ F) (G : Matrix ρ ι F) (hA : A.generatedBy = ⊤) : (A * G).generatedBy = G.generatedBy

A left factor whose rows span the whole coefficient space preserves the generated code.

theorem Matrix.generatedBy_mul_eq_of_surjective {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} {σ : Type u_4} [Field F] [Fintype ρ] [Fintype σ] (A : Matrix σ ρ F) (G : Matrix ρ ι F) (hA : Function.Surjective fun (v : σ → F) => vecMul v A) : (A * G).generatedBy = G.generatedBy

A surjective row operation preserves the generated code.

theorem Matrix.generatedBy_mul_eq_of_isUnit {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [Fintype ρ] [DecidableEq ρ] (A : Matrix ρ ρ F) (G : Matrix ρ ι F) (hA : IsUnit A) : (A * G).generatedBy = G.generatedBy

Invertible row operations preserve the code generated by a matrix.

theorem TauCeti.LinearCode.isGeneratorMatrix_mul_iff {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [Fintype ρ] [DecidableEq ρ] (C : LinearCode F ι) (A : Matrix ρ ρ F) (G : Matrix ρ ι F) (hA : IsUnit A) : C.IsGeneratorMatrix (A * G) ↔ C.IsGeneratorMatrix G

An invertible row operation preserves the property of being a generator matrix for C.

theorem TauCeti.LinearCode.IsGeneratorMatrix.mul_left {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [Fintype ρ] [DecidableEq ρ] {C : LinearCode F ι} {G : Matrix ρ ι F} (hG : C.IsGeneratorMatrix G) (A : Matrix ρ ρ F) (hA : IsUnit A) : C.IsGeneratorMatrix (A * G)

Applying an invertible row operation to a generator matrix gives another generator matrix.

theorem Matrix.generatedBy_submatrix_rows_le {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} {σ : Type u_4} [Field F] [Fintype ρ] [Fintype σ] (G : Matrix ρ ι F) (f : σ → ρ) : (G.submatrix f id).generatedBy ≤ G.generatedBy

Restricting or repeating rows along a map cannot enlarge the generated code.

theorem Matrix.generatedBy_submatrix_rows_eq_iff {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} {σ : Type u_4} [Field F] [Fintype ρ] [Fintype σ] (G : Matrix ρ ι F) (f : σ → ρ) : (G.submatrix f id).generatedBy = G.generatedBy ↔ ∀ (r : ρ), G.row r ∈ (G.submatrix f id).generatedBy

Rows selected along f generate the original code exactly when they generate every original row.

theorem Matrix.generatedBy_submatrix_rows_eq_of_surjective {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} {σ : Type u_4} [Field F] [Fintype ρ] [Fintype σ] (G : Matrix ρ ι F) (f : σ → ρ) (hf : Function.Surjective f) : (G.submatrix f id).generatedBy = G.generatedBy

Selecting rows along a surjective map, possibly with repetitions, preserves the generated code. In particular, this applies to reindexing the rows along an equivalence.

theorem Matrix.generatedBy_deleteRow_le {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [DecidableEq ρ] [Fintype ρ] (G : Matrix ρ ι F) (r : ρ) : (G.deleteRow r).generatedBy ≤ G.generatedBy

Deleting a row cannot enlarge the generated code.

theorem Matrix.generatedBy_deleteRow_eq_iff {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [DecidableEq ρ] [Fintype ρ] (G : Matrix ρ ι F) (r : ρ) : (G.deleteRow r).generatedBy = G.generatedBy ↔ G.row r ∈ (G.deleteRow r).generatedBy

Deleting row r preserves the generated code exactly when that row is generated by the remaining rows.

theorem Matrix.generatedBy_deleteRow_eq_of_row_mem {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [DecidableEq ρ] [Fintype ρ] (G : Matrix ρ ι F) (r : ρ) (hr : G.row r ∈ (G.deleteRow r).generatedBy) : (G.deleteRow r).generatedBy = G.generatedBy

A row generated by all the other rows can be deleted without changing the generated code.

theorem TauCeti.LinearCode.IsGeneratorMatrix.deleteRow {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [DecidableEq ρ] [Fintype ρ] {C : LinearCode F ι} {G : Matrix ρ ι F} (hG : C.IsGeneratorMatrix G) (r : ρ) (hr : G.row r ∈ (G.deleteRow r).generatedBy) : C.IsGeneratorMatrix (G.deleteRow r)

Deleting a redundant row from a generator matrix leaves a generator matrix for the same code.

theorem Matrix.exists_deleteRow_generatedBy_eq_of_not_linearIndependent {F : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Field F] [DecidableEq ρ] [Fintype ρ] (G : Matrix ρ ι F) (hG : ¬LinearIndependent F G.row) : ∃ (r : ρ), (G.deleteRow r).generatedBy = G.generatedBy

A linearly dependent finite row family contains a row that can be deleted without changing the generated code.