Relabelling the coordinates of a linear code

Relabelling the coordinate set of a linear code along an equivalence is the most basic operation on codes, and every further construction is expected to commute with it. This file defines TauCeti.reindex as the image of the code under coordinate transport, and records membership, functoriality, the order and lattice laws, and invariance of the dimension and minimum distance.

The field is never assumed finite, and the coordinate types are finite only where minimum distance is involved.

Main declarations

• TauCeti.reindex: transport of a code along a coordinate equivalence.
• TauCeti.mem_reindex: membership characterization, with the direction of the equivalence explicit.
• TauCeti.finrank_reindex: relabelling coordinates preserves the dimension.
• TauCeti.hammingMinDist_reindex: relabelling coordinates preserves the minimum distance.
• TauCeti.isPermutationEquivalent_reindex: a reindexed code is permutation equivalent to the original one.

References

• W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes, Cambridge University Press, 2003, Chapter 1.

noncomputable def TauCeti.reindex {F : Type u_1} [Field F] {ι : Type u_2} {κ : Type u_3} (C : LinearCode F ι) (e : κ ≃ ι) : LinearCode F κ

Reindex a linear code along a coordinate equivalence. The equivalence points from the new coordinate type to the old one, so the transported word has value x (e j) at j.

theorem TauCeti.reindex_def {F : Type u_1} [Field F] {ι : Type u_2} {κ : Type u_3} (C : LinearCode F ι) (e : κ ≃ ι) : reindex C e = Submodule.map (↑(LinearEquiv.funCongrLeft F F e)) C

Reindexing is the image under coordinate transport.

@[simp]

theorem TauCeti.mem_reindex {F : Type u_1} [Field F] {ι : Type u_2} {κ : Type u_3} {C : LinearCode F ι} {e : κ ≃ ι} {y : κ → F} : y ∈ reindex C e ↔ ∃ x ∈ C, ∀ (j : κ), x (e j) = y j

Membership in a reindexed code, with the direction of the coordinate equivalence explicit.

@[simp]

theorem TauCeti.reindex_refl {F : Type u_1} [Field F] {ι : Type u_2} (C : LinearCode F ι) : reindex C (Equiv.refl ι) = C

Reindexing along the identity equivalence leaves a code unchanged.

@[simp]

theorem TauCeti.reindex_reindex {F : Type u_1} [Field F] {ι : Type u_2} {κ : Type u_3} {κ' : Type u_4} (C : LinearCode F ι) (e : κ ≃ ι) (f : κ' ≃ κ) : reindex (reindex C e) f = reindex C (f.trans e)

Successive changes of coordinates compose in their contravariant order.

theorem TauCeti.reindex_mono {F : Type u_1} [Field F] {ι : Type u_2} {κ : Type u_3} {C D : LinearCode F ι} (h : C ≤ D) (e : κ ≃ ι) : reindex C e ≤ reindex D e

Reindexing is monotone in the code.

@[simp]

theorem TauCeti.reindex_bot {F : Type u_1} [Field F] {ι : Type u_2} {κ : Type u_3} (e : κ ≃ ι) : reindex ⊥ e = ⊥

Reindexing sends the zero code to the zero code.

@[simp]

theorem TauCeti.reindex_top {F : Type u_1} [Field F] {ι : Type u_2} {κ : Type u_3} (e : κ ≃ ι) : reindex ⊤ e = ⊤

Reindexing sends the whole word space to the whole word space.

@[simp]

theorem TauCeti.reindex_sup {F : Type u_1} [Field F] {ι : Type u_2} {κ : Type u_3} (C D : LinearCode F ι) (e : κ ≃ ι) : reindex (C ⊔ D) e = reindex C e ⊔ reindex D e

Reindexing commutes with sums of codes.

@[simp]

theorem TauCeti.reindex_inf {F : Type u_1} [Field F] {ι : Type u_2} {κ : Type u_3} (C D : LinearCode F ι) (e : κ ≃ ι) : reindex (C ⊓ D) e = reindex C e ⊓ reindex D e

Reindexing commutes with intersections of codes.

theorem TauCeti.isPermutationEquivalent_reindex {F : Type u_1} [Field F] {ι : Type u_2} {κ : Type u_3} (C : LinearCode F ι) (e : κ ≃ ι) : IsPermutationEquivalent (reindex C e) C

Reindexing along a coordinate equivalence is exactly a permutation equivalence of codes.

@[simp]

theorem TauCeti.finrank_reindex {F : Type u_1} [Field F] {ι : Type u_2} {κ : Type u_3} (C : LinearCode F ι) (e : κ ≃ ι) : Module.finrank F ↥(reindex C e) = Module.finrank F ↥C

A coordinate equivalence preserves the dimension of a code.

@[simp]

theorem TauCeti.hammingMinDist_reindex {F : Type u_1} [Field F] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq F] (C : LinearCode F ι) (e : κ ≃ ι) : (↑(reindex C e)).hammingMinDist = (↑C).hammingMinDist

A coordinate equivalence preserves the minimum distance of a code, even for the zero code.