Euclidean duals of linear codes

A linear code on a finite coordinate type is a submodule of the corresponding function space. Its Euclidean dual consists of the words whose dot product with every codeword vanishes. This file gives that construction its order-theoretic API and proves that dot-product duality is an involution over a field. In particular, the dimensions of a code and its dual add to the number of coordinates, and over a finite field their cardinalities multiply to the cardinality of the whole word space.

A code is self-orthogonal when it lies in its Euclidean dual and self-dual when it equals it. These are predicates on the code itself rather than a new bundled type, so the full Submodule API stays available. Over a field, a self-orthogonal code has at most half the ambient dimension, with equality exactly for self-dual codes.

The dot-product convention and the resulting Euclidean dual follow Huffman and Pless, Fundamentals of Error-Correcting Codes, §§1.2–1.4.

def Submodule.euclideanDual {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] (C : Submodule R (ι → R)) : Submodule R (ι → R)

The Euclidean dual of a linear code: its orthogonal complement for the standard dot product.

@[simp]

theorem Submodule.mem_euclideanDual {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] {C : Submodule R (ι → R)} {y : ι → R} : y ∈ C.euclideanDual ↔ ∀ x ∈ C, x ⬝ᵥ y = 0

Membership in the Euclidean dual means having zero dot product with every codeword.

theorem Submodule.euclideanDual_eq_orthogonalBilin {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] (C : Submodule R (ι → R)) : C.euclideanDual = orthogonalBilin (dotProductBilin R R) C

The Euclidean dual is the orthogonal complement orthogonalBilin for the dot-product bilinear form.

theorem Submodule.mem_euclideanDual' {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] {C : Submodule R (ι → R)} {y : ι → R} : y ∈ C.euclideanDual ↔ ∀ x ∈ C, y ⬝ᵥ x = 0

Membership in the Euclidean dual can equivalently put the codeword on the right.

@[simp]

theorem Submodule.mem_euclideanDual_span {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] {s : Set (ι → R)} {y : ι → R} : y ∈ (span R s).euclideanDual ↔ ∀ ⦃x : ι → R⦄, x ∈ s → x ⬝ᵥ y = 0

A word is dual to a generated code exactly when it is orthogonal to every generator.

@[simp]

theorem Submodule.euclideanDual_bot_eq_top {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] : ⊥.euclideanDual = ⊤

The dual of the zero code is the whole word space.

@[simp]

theorem Submodule.euclideanDual_top_eq_bot {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] : ⊤.euclideanDual = ⊥

The dual of the whole word space is the zero code.

theorem Submodule.euclideanDual_antitone {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] : Antitone euclideanDual

Euclidean duality reverses inclusion.

theorem Submodule.le_euclideanDual_comm {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] {C D : Submodule R (ι → R)} : C ≤ D.euclideanDual ↔ D ≤ C.euclideanDual

Orthogonality of two codes is symmetric.

@[simp]

theorem Submodule.euclideanDual_sup {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] (C D : Submodule R (ι → R)) : (C ⊔ D).euclideanDual = C.euclideanDual ⊓ D.euclideanDual

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

Self-orthogonal and self-dual codes

def Submodule.IsSelfOrthogonal {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] (C : Submodule R (ι → R)) : Prop

A linear code is self-orthogonal when it is contained in its Euclidean dual, that is, when any two of its codewords have zero dot product.

def Submodule.IsSelfDual {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] (C : Submodule R (ι → R)) : Prop

A linear code is self-dual when it equals its Euclidean dual.

theorem Submodule.isSelfOrthogonal_iff_le {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] {C : Submodule R (ι → R)} : C.IsSelfOrthogonal ↔ C ≤ C.euclideanDual

Self-orthogonality is containment in the Euclidean dual.

theorem Submodule.isSelfOrthogonal_iff {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] {C : Submodule R (ι → R)} : C.IsSelfOrthogonal ↔ ∀ x ∈ C, ∀ y ∈ C, x ⬝ᵥ y = 0

A code is self-orthogonal exactly when any two of its words have zero dot product.

theorem Submodule.isSelfDual_iff {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] {C : Submodule R (ι → R)} : C.IsSelfDual ↔ C = C.euclideanDual

Self-duality is equality with the Euclidean dual.

theorem Submodule.IsSelfOrthogonal.le_euclideanDual {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] {C : Submodule R (ι → R)} (hC : C.IsSelfOrthogonal) : C ≤ C.euclideanDual

A self-orthogonal code is contained in its Euclidean dual.

theorem Submodule.IsSelfDual.euclideanDual_eq {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] {C : Submodule R (ι → R)} (hC : C.IsSelfDual) : C.euclideanDual = C

The Euclidean dual of a self-dual code is the code itself.

theorem Submodule.IsSelfDual.isSelfOrthogonal {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] {C : Submodule R (ι → R)} (hC : C.IsSelfDual) : C.IsSelfOrthogonal

Every self-dual code is self-orthogonal.

theorem Submodule.IsSelfOrthogonal.mono {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] {C D : Submodule R (ι → R)} (hD : D.IsSelfOrthogonal) (hCD : C ≤ D) : C.IsSelfOrthogonal

Self-orthogonality passes to subcodes.

@[simp]

theorem Submodule.isSelfOrthogonal_bot {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] : ⊥.IsSelfOrthogonal

The zero code is self-orthogonal.

@[simp]

theorem Submodule.euclideanDual_euclideanDual {ι : Type u_2} [Fintype ι] {K : Type u_3} [Field K] (C : Submodule K (ι → K)) : C.euclideanDual.euclideanDual = C

Taking the Euclidean dual twice recovers the original code.

theorem Submodule.euclideanDual_le_euclideanDual_iff {ι : Type u_2} [Fintype ι] {K : Type u_3} [Field K] {C D : Submodule K (ι → K)} : C.euclideanDual ≤ D.euclideanDual ↔ D ≤ C

Dual inclusion is equivalent to inclusion in the opposite direction.

theorem Submodule.euclideanDual_injective {ι : Type u_2} [Fintype ι] {K : Type u_3} [Field K] : Function.Injective euclideanDual

Two codes have the same Euclidean dual exactly when they are equal.

@[simp]

theorem Submodule.euclideanDual_inf {ι : Type u_2} [Fintype ι] {K : Type u_3} [Field K] (C D : Submodule K (ι → K)) : (C ⊓ D).euclideanDual = C.euclideanDual ⊔ D.euclideanDual

The Euclidean dual of an intersection is the sum of the Euclidean duals.

theorem Submodule.finrank_add_finrank_euclideanDual {ι : Type u_2} [Fintype ι] {K : Type u_3} [Field K] (C : Submodule K (ι → K)) : Module.finrank K ↥C + Module.finrank K ↥C.euclideanDual = Fintype.card ι

The dimensions of a code and its Euclidean dual add to the number of coordinates.

theorem Submodule.IsSelfDual.two_mul_finrank_eq_card {ι : Type u_2} [Fintype ι] {K : Type u_3} [Field K] {C : Submodule K (ι → K)} (hC : C.IsSelfDual) : 2 * Module.finrank K ↥C = Fintype.card ι

A self-dual code has twice its dimension equal to its length.

theorem Submodule.IsSelfOrthogonal.two_mul_finrank_le_card {ι : Type u_2} [Fintype ι] {K : Type u_3} [Field K] {C : Submodule K (ι → K)} (hC : C.IsSelfOrthogonal) : 2 * Module.finrank K ↥C ≤ Fintype.card ι

A self-orthogonal code has dimension at most half the length.

theorem Submodule.IsSelfOrthogonal.isSelfDual_of_card_le_two_mul_finrank {ι : Type u_2} [Fintype ι] {K : Type u_3} [Field K] {C : Submodule K (ι → K)} (hC : C.IsSelfOrthogonal) (hdim : Fintype.card ι ≤ 2 * Module.finrank K ↥C) : C.IsSelfDual

A self-orthogonal code of half the ambient dimension is self-dual.

theorem Submodule.isSelfDual_iff_isSelfOrthogonal_and_two_mul_finrank_eq {ι : Type u_2} [Fintype ι] {K : Type u_3} [Field K] {C : Submodule K (ι → K)} : C.IsSelfDual ↔ C.IsSelfOrthogonal ∧ 2 * Module.finrank K ↥C = Fintype.card ι

A code is self-dual exactly when it is self-orthogonal and has half the ambient dimension.

theorem Submodule.natCard_mul_natCard_euclideanDual {ι : Type u_2} [Fintype ι] {K : Type u_3} [Field K] (C : Submodule K (ι → K)) : Nat.card ↥C * Nat.card ↥C.euclideanDual = Nat.card K ^ Fintype.card ι

Over a finite field, the cardinalities of a code and its Euclidean dual multiply to the cardinality of the whole word space.

theorem Submodule.IsSelfDual.natCard_eq {ι : Type u_2} [Fintype ι] {K : Type u_3} [Field K] {C : Submodule K (ι → K)} (hC : C.IsSelfDual) : Nat.card ↥C = Nat.card K ^ (Fintype.card ι / 2)

A self-dual code over a field with q elements has q^(n/2) words, where n is its length.