Definition 16: Dual Code

Given a classical [n, k, d]-code L ⊆ 𝔽₂^n (Def_3), the dual code is L⊥ = {w ∈ 𝔽₂^n : ⟨w, c⟩ = 0 for all c ∈ L}, where ⟨w, c⟩ = Σᵢ wᵢcᵢ is the standard 𝔽₂-dot product.

Main Results

• dualCode — the dual code L⊥ as a ClassicalCode
• mem_dualCode_iff — membership characterization via dot product
• mem_dualCode_iff' — symmetric characterization (commutativity of dot product)
• dualCodeEquivDualAnnihilator — L⊥ ≃ₗ L.code.dualAnnihilator
• dimension_dualCode — dim L⊥ = n - dim L
• dualCode_isNKDCode — L⊥ is an [n, n-k, d_{L⊥}]-code

Dual Code Definition

noncomputable def ClassicalCode.dualCode {n : ℕ} (𝒞 : ClassicalCode n) : ClassicalCode n

The dual code L⊥ = {w ∈ 𝔽₂^n : ⟨w, c⟩ = 0 for all c ∈ L}, where ⟨w, c⟩ = Σᵢ wᵢ cᵢ is the standard 𝔽₂-inner product. This is defined as the pullback of the dual annihilator L.code.dualAnnihilator ⊆ Dual(𝔽₂^n) through the canonical isomorphism dotProductEquiv : 𝔽₂^n ≃ₗ Dual(𝔽₂^n) given by v ↦ (w ↦ v ⬝ᵥ w).

Equations

• 𝒞.dualCode = { code := Submodule.comap (↑(dotProductEquiv 𝔽₂ (Fin n))) 𝒞.code.dualAnnihilator }

Membership Characterization

theorem ClassicalCode.mem_dualCode_iff {n : ℕ} (𝒞 : ClassicalCode n) (w : Fin n → 𝔽₂) : w ∈ 𝒞.dualCode.code ↔ ∀ c ∈ 𝒞.code, w ⬝ᵥ c = 0

Membership in the dual code: w ∈ L⊥ iff w ⬝ᵥ c = 0 for all c ∈ L.

theorem ClassicalCode.mem_dualCode_iff' {n : ℕ} (𝒞 : ClassicalCode n) (w : Fin n → 𝔽₂) : w ∈ 𝒞.dualCode.code ↔ ∀ c ∈ 𝒞.code, c ⬝ᵥ w = 0

The dual code is symmetric: w ∈ L⊥ iff c ⬝ᵥ w = 0 for all c ∈ L. Over 𝔽₂, w ⬝ᵥ c = c ⬝ᵥ w since 𝔽₂ is commutative.

Equivalence with Dual Annihilator

noncomputable def ClassicalCode.dualCodeEquivDualAnnihilator {n : ℕ} (𝒞 : ClassicalCode n) : ↥𝒞.dualCode.code ≃ₗ[𝔽₂] ↥𝒞.code.dualAnnihilator

The linear equivalence between ↥(dualCode 𝒞).code and ↥(𝒞.code.dualAnnihilator), obtained from dotProductEquiv. Since dualCode.code = dualAnnihilator.comap (dotProductEquiv), the restriction of dotProductEquiv gives the equivalence.

Equations

• 𝒞.dualCodeEquivDualAnnihilator = ⋯.mpr (⋯.mpr ((dotProductEquiv 𝔽₂ (Fin n)).symm.submoduleMap 𝒞.code.dualAnnihilator).symm)

Dimension Formula

theorem ClassicalCode.dimension_dualCode {n : ℕ} (𝒞 : ClassicalCode n) [FiniteDimensional 𝔽₂ (Fin n → 𝔽₂)] : 𝒞.dualCode.dimension = n - 𝒞.dimension

The dimension of the dual code: dim L⊥ = n - dim L. This follows from the dual annihilator dimension formula dim L + dim L.dualAnnihilator = dim 𝔽₂^n = n and the fact that dotProductEquiv preserves dimension.

Dual Code is an [n, n-k, d_{L⊥}]-code

theorem ClassicalCode.dualCode_isNKDCode {n : ℕ} (𝒞 : ClassicalCode n) [FiniteDimensional 𝔽₂ (Fin n → 𝔽₂)] : 𝒞.dualCode.IsNKDCode (n - 𝒞.dimension) 𝒞.dualCode.distance

The dual code is an [n, n-k, d_{L⊥}]-code, where k = dim L and d_{L⊥} is the minimum distance of the dual code.