Weight enumerators of semilinearly equivalent codes

Semilinearly equivalent codes have the same weight distribution, homogeneous weight enumerator, and one-variable weight polynomial. These invariants allow comparison of codes after uniform alphabet conjugation, coordinate scaling, and relabelling.

The conventions follow Huffman and Pless, Fundamentals of Error-Correcting Codes, §1.7.

theorem TauCeti.IsSemilinearEquivalent.weightDistribution_eq {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsSemilinearEquivalent C D) (w : ℕ) : (↑C).weightDistribution w = (↑D).weightDistribution w

Semilinearly equivalent codes have the same weight distribution.

theorem TauCeti.IsSemilinearEquivalent.weightEnumerator_eq {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsSemilinearEquivalent C D) : (↑C).weightEnumerator = (↑D).weightEnumerator

Semilinearly equivalent codes have the same homogeneous weight enumerator.

theorem TauCeti.IsSemilinearEquivalent.weightPolynomial_eq {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsSemilinearEquivalent C D) : (↑C).weightPolynomial = (↑D).weightPolynomial

Semilinearly equivalent codes have the same one-variable weight polynomial.