Euclidean duals of derived codes

This file computes the Euclidean dual of the codes obtained from a linear code by the elementary constructions: puncturing, shortening, direct sums, reindexing, and linear (in particular monomial) equivalences of the coordinate space, and compares the automorphism groups of a code and of its dual.

For a set s of retained coordinates, puncturing and shortening are exchanged by duality: (puncture C s)^⊥ = shorten C^⊥ s and (shorten C s)^⊥ = puncture C^⊥ s. The dual of a direct sum is the direct sum of the duals. A linear equivalence of the coordinate space acts on the dual through its contragredient for the dot product. The contragredient of a monomial transformation which rescales coordinates by units u rescales by the inverse units u⁻¹ and relabels the coordinates in the same way; in particular, monomially (respectively permutation) equivalent codes have monomially (respectively permutation) equivalent duals, and a coordinate permutation preserves self-orthogonality and self-duality. A direct sum is self-orthogonal (respectively self-dual) exactly when both summands are.

Taking contragredients carries the monomial automorphisms of a code to those of its dual, and fixes every coordinate permutation. Over a field, where the dual of the dual is the code itself, a code and its dual therefore have the same permutation automorphism group and isomorphic monomial automorphism groups.

Main statements

• TauCeti.euclideanDual_puncture, TauCeti.euclideanDual_shorten: duality exchanges puncturing and shortening.
• Submodule.euclideanDual_directSum: the dual of a direct sum.
• Submodule.isSelfDual_directSum_iff: a direct sum is self-dual exactly when both summands are.
• TauCeti.euclideanDual_reindex: duality commutes with a change of coordinates.
• Submodule.euclideanDual_map_linearEquiv: the dual of the image of a code under a linear equivalence is the image of the dual under the contragredient.
• TauCeti.euclideanDual_map_monomialEquiv: the contragredient action of a monomial transformation on the dual.
• TauCeti.permutationAut_euclideanDual: a code and its dual have the same permutation automorphisms.
• TauCeti.mem_monomialAut_euclideanDual_iff, TauCeti.monomialAutEquivEuclideanDual: taking contragredients identifies the monomial automorphism groups of a code and of its dual.

References

• W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes, Cambridge University Press, 2003, Sections 1.5, 1.6 and 1.7.

@[simp]

theorem Submodule.euclideanDual_directSum {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] (C : Submodule R (ι → R)) (D : Submodule R (κ → R)) : (C.directSum D).euclideanDual = C.euclideanDual.directSum D.euclideanDual

The Euclidean dual of a direct sum is the direct sum of the Euclidean duals.

@[simp]

theorem Submodule.isSelfOrthogonal_directSum_iff {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} : (C.directSum D).IsSelfOrthogonal ↔ C.IsSelfOrthogonal ∧ D.IsSelfOrthogonal

A direct sum is self-orthogonal exactly when both summands are.

@[simp]

theorem Submodule.isSelfDual_directSum_iff {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} : (C.directSum D).IsSelfDual ↔ C.IsSelfDual ∧ D.IsSelfDual

A direct sum is self-dual exactly when both summands are.

@[simp]

theorem Submodule.euclideanDual_map_linearEquiv {R : Type u_1} {ι : Type u_2} {κ : Type u_3} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (C : Submodule R (ι → R)) (f : (ι → R) ≃ₗ[R] κ → R) : (map (↑f) C).euclideanDual = map (↑f.dotProductContragredient) C.euclideanDual

The Euclidean dual of the image of a code under a linear equivalence is the image of the dual under the contragredient equivalence.

@[simp]

theorem TauCeti.euclideanDual_puncture {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] (s : Set ι) [Fintype ↑s] (C : LinearCode F ι) : Submodule.euclideanDual (puncture C s) = shorten (Submodule.euclideanDual C) s

The Euclidean dual of a punctured code is the shortened Euclidean dual, with the same retained coordinates.

@[simp]

theorem TauCeti.euclideanDual_shorten {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] (s : Set ι) [Fintype ↑s] (C : LinearCode F ι) : Submodule.euclideanDual (shorten C s) = puncture (Submodule.euclideanDual C) s

The Euclidean dual of a shortened code is the punctured Euclidean dual, with the same retained coordinates.

@[simp]

theorem TauCeti.euclideanDual_punctureAt {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] (C : LinearCode F ι) (i : ι) : Submodule.euclideanDual (punctureAt C i) = shortenAt (Submodule.euclideanDual C) i

The Euclidean dual of the code punctured at i is the dual shortened at i.

@[simp]

theorem TauCeti.euclideanDual_shortenAt {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] (C : LinearCode F ι) (i : ι) : Submodule.euclideanDual (shortenAt C i) = punctureAt (Submodule.euclideanDual C) i

The Euclidean dual of the code shortened at i is the dual punctured at i.

theorem TauCeti.monomialEquiv_dotProduct {ι : Type u_2} {κ : Type u_3} {R : Type u_4} [CommSemiring R] [Fintype ι] [Fintype κ] (u : ι → Rˣ) (e : ι ≃ κ) (x : ι → R) (y : κ → R) : (monomialEquiv u e) x ⬝ᵥ y = x ⬝ᵥ (monomialEquiv u⁻¹ e).symm y

A monomial transformation is adjoint, for the dot product, to the inverse of the transformation with inverse scalars and the same relabelling.

@[simp]

theorem TauCeti.dotProductContragredient_monomialEquiv {ι : Type u_2} {κ : Type u_3} {R : Type u_4} [CommSemiring R] [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (u : ι → Rˣ) (e : ι ≃ κ) : (monomialEquiv u e).dotProductContragredient = monomialEquiv u⁻¹ e

The contragredient of a monomial transformation is the monomial transformation with the inverse scalars and the same relabelling.

theorem TauCeti.euclideanDual_map_monomialEquiv {ι : Type u_2} {κ : Type u_3} {R : Type u_4} [CommSemiring R] [Fintype ι] [Fintype κ] (u : ι → Rˣ) (e : ι ≃ κ) (C : Submodule R (ι → R)) : (Submodule.map (↑(monomialEquiv u e)) C).euclideanDual = Submodule.map (↑(monomialEquiv u⁻¹ e)) C.euclideanDual

The Euclidean dual of the image of a code under a monomial transformation is the image of the dual under the contragredient transformation, with inverse scalars.

theorem TauCeti.IsMonomialEquivalent.euclideanDual {ι : Type u_2} {κ : Type u_3} {R : Type u_4} [CommSemiring R] [Fintype ι] [Fintype κ] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsMonomialEquivalent C D) : IsMonomialEquivalent C.euclideanDual D.euclideanDual

Monomially equivalent codes have monomially equivalent Euclidean duals.

theorem TauCeti.IsPermutationEquivalent.euclideanDual {ι : Type u_2} {κ : Type u_3} {R : Type u_4} [CommSemiring R] [Fintype ι] [Fintype κ] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsPermutationEquivalent C D) : IsPermutationEquivalent C.euclideanDual D.euclideanDual

Permutation-equivalent codes have permutation-equivalent Euclidean duals.

theorem TauCeti.IsPermutationEquivalent.isSelfOrthogonal_iff {ι : Type u_2} {κ : Type u_3} {R : Type u_4} [CommSemiring R] [Fintype ι] [Fintype κ] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsPermutationEquivalent C D) : C.IsSelfOrthogonal ↔ D.IsSelfOrthogonal

Permutation equivalence preserves self-orthogonality.

theorem TauCeti.IsPermutationEquivalent.isSelfDual_iff {ι : Type u_2} {κ : Type u_3} {R : Type u_4} [CommSemiring R] [Fintype ι] [Fintype κ] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsPermutationEquivalent C D) : C.IsSelfDual ↔ D.IsSelfDual

Permutation equivalence preserves self-duality.

Automorphism groups of the Euclidean dual

theorem TauCeti.dotProductContragredient_eq_self_of_mem_permutationGroup {ι : Type u_2} {R : Type u_4} [CommSemiring R] [Fintype ι] [DecidableEq ι] {f : (ι → R) ≃ₗ[R] ι → R} (hf : f ∈ permutationGroup R ι) : f.dotProductContragredient = f

The contragredient of a coordinate permutation is the permutation itself.

theorem TauCeti.dotProductContragredient_mem_monomialGroup_iff {ι : Type u_2} {R : Type u_4} [CommSemiring R] [Fintype ι] [DecidableEq ι] {f : (ι → R) ≃ₗ[R] ι → R} : f.dotProductContragredient ∈ monomialGroup R ι ↔ f ∈ monomialGroup R ι

The contragredient of a linear automorphism is monomial exactly when the automorphism is.

theorem TauCeti.dotProductContragredient_mem_monomialAut_euclideanDual {ι : Type u_2} {R : Type u_4} [CommSemiring R] [Fintype ι] {C : Submodule R (ι → R)} [DecidableEq ι] {f : (ι → R) ≃ₗ[R] ι → R} (hf : f ∈ monomialAut C) : f.dotProductContragredient ∈ monomialAut C.euclideanDual

The contragredient of a monomial automorphism of a code is a monomial automorphism of its Euclidean dual.

theorem TauCeti.permutationAut_le_permutationAut_euclideanDual {ι : Type u_2} {R : Type u_4} [CommSemiring R] [Fintype ι] {C : Submodule R (ι → R)} : permutationAut C ≤ permutationAut C.euclideanDual

A permutation automorphism of a code is a permutation automorphism of its Euclidean dual.

@[simp]

theorem TauCeti.permutationAut_euclideanDual {ι : Type u_2} {K : Type u_4} [Field K] [Fintype ι] (C : Submodule K (ι → K)) : permutationAut C.euclideanDual = permutationAut C

A linear code and its Euclidean dual have the same permutation automorphisms.

theorem TauCeti.mem_monomialAut_euclideanDual_iff {ι : Type u_2} {K : Type u_4} [Field K] [Fintype ι] [DecidableEq ι] {C : Submodule K (ι → K)} {f : (ι → K) ≃ₗ[K] ι → K} : f ∈ monomialAut C.euclideanDual ↔ f.dotProductContragredient ∈ monomialAut C

A linear automorphism is a monomial automorphism of the Euclidean dual of a linear code exactly when its contragredient is a monomial automorphism of the code.

def TauCeti.monomialAutEquivEuclideanDual {ι : Type u_2} {K : Type u_4} [Field K] [Fintype ι] [DecidableEq ι] (C : Submodule K (ι → K)) : ↥(monomialAut C) ≃* ↥(monomialAut C.euclideanDual)

The monomial automorphism groups of a linear code and of its Euclidean dual are isomorphic, by taking contragredients.

@[simp]

theorem TauCeti.coe_monomialAutEquivEuclideanDual_apply {ι : Type u_2} {K : Type u_4} [Field K] [Fintype ι] [DecidableEq ι] (C : Submodule K (ι → K)) (f : ↥(monomialAut C)) : ↑((monomialAutEquivEuclideanDual C) f) = (↑f).dotProductContragredient

@[simp]

theorem TauCeti.coe_monomialAutEquivEuclideanDual_symm_apply {ι : Type u_2} {K : Type u_4} [Field K] [Fintype ι] [DecidableEq ι] (C : Submodule K (ι → K)) (f : ↥(monomialAut C.euclideanDual)) : ↑((monomialAutEquivEuclideanDual C).symm f) = (↑f).dotProductContragredient

@[simp]

theorem TauCeti.euclideanDual_reindex {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Field F] [Fintype ι] [Fintype κ] (C : LinearCode F ι) (e : κ ≃ ι) : Submodule.euclideanDual (reindex C e) = reindex (Submodule.euclideanDual C) e

Euclidean duality commutes with a change of coordinates.