Definition 3: Classical Code

A classical, linear, binary code 𝒞 is a subspace of 𝔽₂^n. The number of encodable bits is k = dim 𝒞. The distance d is the minimum Hamming weight of any non-zero element of 𝒞 (with the convention d = 0 if 𝒞 = {0}). We call such a code an [n, k, d]-code.

A code can be specified as 𝒞 = ker ∂^C where ∂^C : 𝔽₂^n → 𝔽₂^m is the parity check matrix (an 𝔽₂-linear map), viewing the code as a two-term chain complex C = (C₁ →[∂^C] C₀) with C₁ = 𝔽₂^n and C₀ = 𝔽₂^m, so 𝒞 = Z₁(C) = ker ∂^C.

Main Definitions

• ClassicalCode — a classical linear binary code: a subspace of 𝔽₂^n
• ClassicalCode.dimension — the number of encodable bits k = dim 𝒞
• ClassicalCode.distance — the minimum Hamming weight of nonzero codewords
• ClassicalCode.IsNKDCode — the property of being an [n, k, d]-code
• ClassicalCode.ofParityCheck — construct a code from a parity check linear map
• ClassicalCode.parityCheckComplex — the two-term chain complex C₁ →[∂^C] C₀
• ClassicalCode.code_eq_ker — 𝒞 = ker ∂^C (definitional)
• ClassicalCode.code_eq_cycles_map — 𝒞 = Z₁(C) via the canonical iso

Classical code as a subspace of 𝔽₂^n

structure ClassicalCode (n : ℕ) : Type

A classical, linear, binary code is a subspace 𝒞 ⊆ 𝔽₂^n.

• code : Submodule 𝔽₂ (Fin n → 𝔽₂)

  The code as a submodule of 𝔽₂^n.

Code parameters

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

The number of encodable bits k = dim 𝒞.

Equations

• 𝒞.dimension = Module.finrank 𝔽₂ ↥𝒞.code

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

The distance of a code 𝒞: the minimum Hamming weight of any non-zero codeword. By convention, d = 0 when 𝒞 = {0} (the trivial code). We use sInf on ℕ, where sInf ∅ = 0 gives the correct convention for the trivial code.

Equations

• 𝒞.distance = sInf {w : ℕ | ∃ x ∈ 𝒞.code, x ≠ 0 ∧ hammingWeight x = w}

def ClassicalCode.IsNKDCode {n : ℕ} (𝒞 : ClassicalCode n) (k d : ℕ) : Prop

A code is an [n, k, d]-code if it has dimension k and distance d.

Equations

• 𝒞.IsNKDCode k d = (𝒞.dimension = k ∧ 𝒞.distance = d)

Code from parity check matrix

def ClassicalCode.ofParityCheck {n m : ℕ} (parityCheck : (Fin n → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) : ClassicalCode n

Construct a classical code from a parity check linear map ∂^C : 𝔽₂^n → 𝔽₂^m. The code is ker ∂^C.

Equations

• ClassicalCode.ofParityCheck parityCheck = { code := parityCheck.ker }

theorem ClassicalCode.code_eq_ker {n m : ℕ} (parityCheck : (Fin n → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) : (ofParityCheck parityCheck).code = parityCheck.ker

The code ker parityCheck is definitionally the kernel of the parity check map.

Two-term chain complex from parity check

noncomputable def ClassicalCode.parityCheckComplex {n m : ℕ} (parityCheck : (Fin n → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) : ChainComplex𝔽₂

The two-term chain complex C = (C₁ →[∂^C] C₀) associated to a parity check linear map ∂^C : 𝔽₂^n → 𝔽₂^m. This uses HomologicalComplex.double from Mathlib with C₁ = ModuleCat.of 𝔽₂ (Fin n → 𝔽₂) in degree 1 and C₀ = ModuleCat.of 𝔽₂ (Fin m → 𝔽₂) in degree 0, with the differential being ∂^C.

Equations

• ClassicalCode.parityCheckComplex parityCheck = HomologicalComplex.double (ModuleCat.ofHom parityCheck) ClassicalCode.parityCheckComplex._proof_4

Code equals cycles of the chain complex

noncomputable def ClassicalCode.parityCheckComplexXIso₁ {n m : ℕ} (parityCheck : (Fin n → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) : (parityCheckComplex parityCheck).X 1 ≅ ModuleCat.of 𝔽₂ (Fin n → 𝔽₂)

The isomorphism C.X 1 ≅ ModuleCat.of 𝔽₂ (Fin n → 𝔽₂) for the parity check complex.

Equations

• ClassicalCode.parityCheckComplexXIso₁ parityCheck = HomologicalComplex.doubleXIso₀ (ClassicalCode.pcMor✝ parityCheck) ClassicalCode.pcRel✝

theorem ClassicalCode.code_eq_cycles_map {n m : ℕ} (parityCheck : (Fin n → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) : (ofParityCheck parityCheck).code = Submodule.map (ModuleCat.Hom.hom (parityCheckComplexXIso₁ parityCheck).hom) ((parityCheckComplex parityCheck).cycles 1)