Codes over ℤ/m as subgroups of a discriminant module

Words over ℤ/m are elements of the coordinate power of the standard alphabet TauCeti.FiniteBilinearModule.zmodStandard, whose pairing is xy / m. Summing that pairing over the coordinates gives

b(x, y) = (x ⬝ᵥ y) / m,

so an additive code and the codes orthogonal to it for the ℤ/m dot product are literally a subgroup of a finite bilinear module and its orthogonal complement. In particular a code is self-orthogonal exactly when it is isotropic, and self-dual exactly when it is Lagrangian.

When m is even the coordinate power of the quadratic alphabet adds the value

q(x) = (∑ i, lift (xᵢ)²) / (2m),

independent of the chosen integer lifts because each coordinate value is. At m = 2 each canonical representative is 0 or 1, hence equals its square, so q(x) is a quarter of the Hamming weight and quadratic isotropy of a binary code is exactly double evenness. These are the identifications through which a code becomes an isotropic subgroup of the discriminant module of a lattice.

Main declarations

• TauCeti.coordinatePower_zmodStandard_pairing and TauCeti.coordinatePower_zmodStandard_pairing_intCast: the coordinate pairing over ℤ/m is the dot product divided by m, including for arbitrary integer lifts.
• TauCeti.orthogonalComplement_coordinatePower_zmodStandard: the orthogonal complement of a code is its Euclidean dual.
• TauCeti.isIsotropic_coordinatePower_zmodStandard_iff_le_euclideanDual and TauCeti.isLagrangian_coordinatePower_zmodStandard_iff: isotropy is self-orthogonality and the Lagrangian condition is self-duality.
• TauCeti.coordinatePower_zmodStandard_quadratic: the coordinate quadratic value over an even ℤ/m is the sum of the squares of the coordinate lifts divided by 2m.
• TauCeti.coordinatePower_zmodStandard_quadratic_intCast_eq_zero_iff and TauCeti.isIsotropic_coordinatePower_zmodStandard_quadratic_intCast_iff: the same values and isotropy read off any coordinatewise integer lift.
• TauCeti.isIsotropic_coordinatePower_zmodStandard_quadratic_iff: quadratic isotropy over an even ℤ/m is divisibility of the sum of squared canonical representatives by 2m.
• TauCeti.isIsotropic_coordinatePower_zmodStandard_quadratic_iff_euclideanWeight: equivalently, divisibility of every Euclidean weight by 2m.
• TauCeti.isIsotropic_coordinatePower_zmodStandard_two_iff_isDoublyEven: over ℤ/2 quadratic isotropy is double evenness.

References

• W. Ebeling, Lattices and Codes, §§1.2–1.3, for binary codes, their weights, and the quadratic form wt / 4 modulo ℤ.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §3 and Chapter 7, §§8–9, for codes as glue groups in discriminant coordinates.

The bilinear coordinate power

theorem TauCeti.coordinatePower_zmodStandard_pairing {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (x y : ι → ZMod m) : (((FiniteBilinearModule.zmodStandard m).coordinatePower ι).pairing x) y = (ZMod.toRatAddCircle m) (x ⬝ᵥ y)

The pairing of two words over ℤ/m is their dot product, divided by m.

theorem TauCeti.coordinatePower_zmodStandard_pairing_intCast {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (a b : ι → ℤ) : ((((FiniteBilinearModule.zmodStandard m).coordinatePower ι).pairing fun (i : ι) => ↑(a i)) fun (i : ι) => ↑(b i)) = ↑((∑ i : ι, ↑(a i) * ↑(b i)) / ↑m)

The pairing of two words over ℤ/m, computed using arbitrary coordinatewise integer lifts.

theorem TauCeti.coordinatePower_zmodStandard_pairing_eq_zero_iff {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (x y : ι → ZMod m) : (((FiniteBilinearModule.zmodStandard m).coordinatePower ι).pairing x) y = 0 ↔ x ⬝ᵥ y = 0

Two words over ℤ/m are orthogonal for the coordinate pairing exactly when their dot product vanishes.

theorem TauCeti.mem_orthogonalComplement_coordinatePower_zmodStandard_iff {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (C : AdditiveCode (ZMod m) ι) (x : ι → ZMod m) : x ∈ ((FiniteBilinearModule.zmodStandard m).coordinatePower ι).orthogonalComplement C ↔ ∀ y ∈ C, x ⬝ᵥ y = 0

The orthogonal complement of an additive code over ℤ/m consists of the words with zero dot product against every codeword.

@[simp]

theorem TauCeti.orthogonalComplement_coordinatePower_zmodStandard {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (C : AdditiveCode (ZMod m) ι) : ((FiniteBilinearModule.zmodStandard m).coordinatePower ι).orthogonalComplement C = ((AddSubgroup.toZModSubmodule m) C).euclideanDual.toAddSubgroup

The orthogonal complement of an additive code over ℤ/m is its Euclidean dual.

theorem TauCeti.isIsotropic_coordinatePower_zmodStandard_iff {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (C : AdditiveCode (ZMod m) ι) : ((FiniteBilinearModule.zmodStandard m).coordinatePower ι).IsIsotropic C ↔ ∀ x ∈ C, ∀ y ∈ C, x ⬝ᵥ y = 0

An additive code over ℤ/m is isotropic exactly when any two of its words are orthogonal.

@[simp]

theorem TauCeti.isIsotropic_coordinatePower_zmodStandard_iff_le_euclideanDual {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (C : AdditiveCode (ZMod m) ι) : ((FiniteBilinearModule.zmodStandard m).coordinatePower ι).IsIsotropic C ↔ (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual

Isotropy of a code over ℤ/m is self-orthogonality.

@[simp]

theorem TauCeti.isLagrangian_coordinatePower_zmodStandard_iff {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (C : AdditiveCode (ZMod m) ι) : ((FiniteBilinearModule.zmodStandard m).coordinatePower ι).IsLagrangian C ↔ (AddSubgroup.toZModSubmodule m) C = ((AddSubgroup.toZModSubmodule m) C).euclideanDual

The Lagrangian condition for a code over ℤ/m is self-duality.

The quadratic coordinate power for an even modulus

theorem TauCeti.coordinatePower_zmodStandard_quadratic {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (hm : Even m) (x : ι → ZMod m) : ((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).quadratic x = ↑((∑ i : ι, ↑(x i).val ^ 2) / (2 * ↑m))

The quadratic value of a word over an even ℤ/m is the sum of the squares of its coordinate representatives, divided by 2m.

theorem TauCeti.coordinatePower_zmodStandard_quadratic_intCast {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (hm : Even m) (z : ι → ℤ) : (((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).quadratic fun (i : ι) => ↑(z i)) = ↑((∑ i : ι, ↑(z i) ^ 2) / (2 * ↑m))

The quadratic value of a word over an even ℤ/m is computed by any coordinatewise integer lift: the sum of the squares of the lifts, divided by 2m.

theorem TauCeti.coordinatePower_zmodStandard_quadratic_intCast_eq_zero_iff {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (hm : Even m) (z : ι → ℤ) : (((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).quadratic fun (i : ι) => ↑(z i)) = 0 ↔ 2 * ↑m ∣ ∑ i : ι, z i ^ 2

The quadratic value of a word over an even ℤ/m vanishes exactly when 2m divides the sum of the squares of a coordinatewise integer lift.

theorem TauCeti.isIsotropic_coordinatePower_zmodStandard_quadratic_intCast_iff {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (hm : Even m) (C : AdditiveCode (ZMod m) ι) : ((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).IsIsotropic C ↔ ∀ (z : ι → ℤ), (fun (i : ι) => ↑(z i)) ∈ C → 2 * ↑m ∣ ∑ i : ι, z i ^ 2

Quadratic isotropy of an additive code over an even ℤ/m means that 2m divides the sum of the squares of every coordinatewise integer lift of a codeword.

theorem TauCeti.isIsotropic_coordinatePower_zmodStandard_quadratic_iff {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (hm : Even m) (C : AdditiveCode (ZMod m) ι) : ((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).IsIsotropic C ↔ ∀ x ∈ C, 2 * m ∣ ∑ i : ι, (x i).val ^ 2

Quadratic isotropy of an additive code over an even ℤ/m means that the sum of the squares of the canonical representatives of every codeword is divisible by 2m.

theorem TauCeti.isIsotropic_coordinatePower_zmodStandard_quadratic_iff_euclideanWeight {ι : Type u_1} [Fintype ι] (m : ℕ) [NeZero m] (hm : Even m) (C : AdditiveCode (ZMod m) ι) : ((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).IsIsotropic C ↔ ∀ x ∈ C, 2 * m ∣ euclideanWeight x

Quadratic isotropy of an additive code over an even ℤ/m means that every codeword has Euclidean weight divisible by 2m.

theorem TauCeti.coordinatePower_zmodStandard_two_quadratic {ι : Type u_1} [Fintype ι] (x : ι → ZMod 2) : ((FiniteQuadraticModule.zmodStandard 2 ⋯).coordinatePower ι).quadratic x = ↑(↑(hammingNorm x) / 4)

The quadratic value of a binary word is a quarter of its Hamming weight.

theorem TauCeti.isIsotropic_coordinatePower_zmodStandard_two_iff {ι : Type u_1} [Fintype ι] (C : AdditiveCode (ZMod 2) ι) : ((FiniteQuadraticModule.zmodStandard 2 ⋯).coordinatePower ι).IsIsotropic C ↔ ∀ x ∈ C, 4 ∣ hammingNorm x

Quadratic isotropy of a binary code is double evenness of its Hamming weights.

theorem TauCeti.isIsotropic_coordinatePower_zmodStandard_two_iff_isDoublyEven {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) : ((FiniteQuadraticModule.zmodStandard 2 ⋯).coordinatePower ι).IsIsotropic (Submodule.toAddSubgroup C) ↔ BinaryCode.IsDoublyEven C

A binary linear code is quadratically isotropic in the standard coordinate discriminant module exactly when it is doubly even.