Semilinear equivalence of codes

A semilinear monomial transformation applies one automorphism of the alphabet to every coordinate, rescales by coordinate units, and permutes coordinates. Its induced equivalence of codes preserves dimension, cardinality, and Hamming data. This allows conjugate codes over a finite field to be compared without treating field conjugation as a linear map over that field. Over an alphabet whose only ring automorphism is the identity, such as ZMod n, semilinear equivalence is just monomial equivalence.

Use TauCeti.semilinearMonomialEquiv u e σ for the word transformation and TauCeti.IsSemilinearEquivalent C D for the induced relation on codes. The restriction to codewords is TauCeti.semilinearCodeEquiv u e σ h. Invariance of weight distributions and enumerators is in TauCeti.InformationTheory.Coding.Semilinear.WeightEnumerator.

The conventions extend TauCeti.monomialEquiv: the units are applied after the alphabet automorphism and before relabelling. Codes remain ordinary submodules, and their images are formed with Mathlib's semilinear Submodule.map. When using the semilinear map projections, make RingHomInvPair.of_ringEquiv and RingHomInvPair.of_ringEquiv_symm local instances, as in this file.

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

def TauCeti.semilinearMonomialEquiv {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] (u : ι → Rˣ) (e : ι ≃ κ) (σ : R ≃+* R) : (ι → R) ≃ₛₗ[↑σ] κ → R

Apply σ to the alphabet, multiply coordinate i by u i, then move it to e i.

@[simp]

theorem TauCeti.semilinearMonomialEquiv_apply {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] (u : ι → Rˣ) (e : ι ≃ κ) (σ : R ≃+* R) (x : ι → R) (j : κ) : (semilinearMonomialEquiv u e σ) x j = ↑(u (e.symm j)) * σ (x (e.symm j))

At coordinate j, apply the alphabet automorphism at e.symm j, then multiply by the unit at that source coordinate.

@[simp]

theorem TauCeti.semilinearMonomialEquiv_symm_apply {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] (u : ι → Rˣ) (e : ι ≃ κ) (σ : R ≃+* R) (y : κ → R) (i : ι) : (semilinearMonomialEquiv u e σ).symm y i = σ.symm (↑(u i)⁻¹ * y (e i))

To recover coordinate i, read coordinate e i, undo its unit scaling, then apply the inverse alphabet automorphism.

@[simp]

theorem TauCeti.semilinearMonomialEquiv_refl {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] (u : ι → Rˣ) (e : ι ≃ κ) : semilinearMonomialEquiv u e (RingEquiv.refl R) = monomialEquiv u e

The identity alphabet automorphism recovers the monomial transformation.

theorem TauCeti.semilinearMonomialEquiv_symm_apply_eq_apply {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] (u : ι → Rˣ) (e : ι ≃ κ) (σ : R ≃+* R) (y : κ → R) : (semilinearMonomialEquiv u e σ).symm y = (semilinearMonomialEquiv (fun (j : κ) => (Units.map σ.symm.toMonoidHom) (u (e.symm j))⁻¹) e.symm σ.symm) y

The inverse uses the inverse alphabet automorphism and its images of the inverse units.

@[simp]

theorem TauCeti.semilinearMonomialEquiv_trans_apply {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {μ : Type u_4} [CommSemiring R] (u : ι → Rˣ) (v : κ → Rˣ) (e : ι ≃ κ) (f : κ ≃ μ) (σ τ : R ≃+* R) (x : ι → R) : (semilinearMonomialEquiv v f τ) ((semilinearMonomialEquiv u e σ) x) = (semilinearMonomialEquiv (fun (i : ι) => v (e i) * (Units.map τ.toMonoidHom) (u i)) (e.trans f) (σ.trans τ)) x

Composition conjugates the first scaling by the second alphabet automorphism.

@[simp]

theorem TauCeti.support_semilinearMonomialEquiv {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] (u : ι → Rˣ) (e : ι ≃ κ) (σ : R ≃+* R) (x : ι → R) : Function.support ((semilinearMonomialEquiv u e σ) x) = ⇑e '' Function.support x

Semilinear monomial transformations transport support by their coordinate equivalence.

@[simp]

theorem TauCeti.hammingNorm_semilinearMonomialEquiv {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq R] (u : ι → Rˣ) (e : ι ≃ κ) (σ : R ≃+* R) (x : ι → R) : hammingNorm ((semilinearMonomialEquiv u e σ) x) = hammingNorm x

A semilinear monomial transformation preserves Hamming weight.

@[simp]

theorem TauCeti.hammingDist_semilinearMonomialEquiv {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq R] (u : ι → Rˣ) (e : ι ≃ κ) (σ : R ≃+* R) (x y : ι → R) : hammingDist ((semilinearMonomialEquiv u e σ) x) ((semilinearMonomialEquiv u e σ) y) = hammingDist x y

A semilinear monomial transformation preserves Hamming distance.

def TauCeti.IsSemilinearEquivalent {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] (C : Submodule R (ι → R)) (D : Submodule R (κ → R)) : Prop

Codes are semilinearly equivalent when a semilinear monomial transformation carries one onto the other. The alphabet automorphism is shared by all coordinates.

theorem TauCeti.isSemilinearEquivalent_iff {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} : IsSemilinearEquivalent C D ↔ ∃ (σ : R ≃+* R) (u : ι → Rˣ) (e : ι ≃ κ), Submodule.map (↑(semilinearMonomialEquiv u e σ)) C = D

Characterize semilinear equivalence by a semilinear image equality.

def TauCeti.semilinearCodeEquiv {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (u : ι → Rˣ) (e : ι ≃ κ) (σ : R ≃+* R) (h : Submodule.map (↑(semilinearMonomialEquiv u e σ)) C = D) : ↥C ≃ₛₗ[↑σ] ↥D

A semilinear monomial transformation mapping one code onto another restricts to a semilinear equivalence between their codewords.

@[simp]

theorem TauCeti.coe_semilinearCodeEquiv_apply {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (u : ι → Rˣ) (e : ι ≃ κ) (σ : R ≃+* R) (h : Submodule.map (↑(semilinearMonomialEquiv u e σ)) C = D) (x : ↥C) : ↑((semilinearCodeEquiv u e σ h) x) = (semilinearMonomialEquiv u e σ) ↑x

The induced code equivalence acts by the ambient semilinear monomial transformation.

@[simp]

theorem TauCeti.coe_semilinearCodeEquiv_symm_apply {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (u : ι → Rˣ) (e : ι ≃ κ) (σ : R ≃+* R) (h : Submodule.map (↑(semilinearMonomialEquiv u e σ)) C = D) (y : ↥D) : ↑((semilinearCodeEquiv u e σ h).symm y) = (semilinearMonomialEquiv u e σ).symm ↑y

The inverse code equivalence acts by the inverse ambient semilinear transformation.

theorem TauCeti.IsMonomialEquivalent.isSemilinearEquivalent {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsMonomialEquivalent C D) : IsSemilinearEquivalent C D

Monomial equivalence is semilinear equivalence with the identity alphabet automorphism.

theorem TauCeti.IsSemilinearEquivalent.refl {R : Type u_1} {ι : Type u_2} [CommSemiring R] (C : Submodule R (ι → R)) : IsSemilinearEquivalent C C

Semilinear equivalence of codes is reflexive.

theorem TauCeti.IsSemilinearEquivalent.symm {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsSemilinearEquivalent C D) : IsSemilinearEquivalent D C

Semilinear equivalence of codes is symmetric.

theorem TauCeti.IsSemilinearEquivalent.trans {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {μ : Type u_4} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} {E : Submodule R (μ → R)} (h : IsSemilinearEquivalent C D) (h' : IsSemilinearEquivalent D E) : IsSemilinearEquivalent C E

Semilinear equivalence of codes is transitive.

theorem TauCeti.IsSemilinearEquivalent.card_eq {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsSemilinearEquivalent C D) : Nat.card ↥C = Nat.card ↥D

Semilinearly equivalent codes have the same cardinality.

theorem TauCeti.IsSemilinearEquivalent.finrank_eq {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsSemilinearEquivalent C D) : Module.finrank R ↥C = Module.finrank R ↥D

Semilinearly equivalent codes have the same dimension.

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

Semilinearly equivalent codes have the same minimum Hamming distance.

@[simp]

theorem TauCeti.isSemilinearEquivalent_iff_isMonomialEquivalent {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} [Subsingleton (R ≃+* R)] : IsSemilinearEquivalent C D ↔ IsMonomialEquivalent C D

When the identity is the only ring automorphism of the alphabet, as for ZMod n, semilinear equivalence is monomial equivalence.