Construction A and its dual lattice

For an additive code C ≤ (ZMod m)^ι, ConstructionA.lattice m C is the submodule of ℚ^ι consisting of integer vectors whose reductions lie in C. The ambient form is ConstructionA.form m x y = (∑ i, x i * y i) / m. This rational model becomes the usual Construction A lattice after scaling real coordinates by 1 / √m.

When the coordinate type is finite and m ≠ 0, the carrier is a full lattice for every code. Its dual carrier is literally the carrier constructed from the dual code, so integrality is equivalent to self-orthogonality of the code, and the resulting integral lattice is unimodular exactly when the code is self-dual. Additive codes over ZMod m are canonically submodules through AddSubgroup.toZModSubmodule; their dual here is the existing Submodule.euclideanDual, transported back to an additive subgroup. The carrier and the form are defined for every modulus m : ℕ (at m = 0 the form is zero); the results that divide by the modulus assume [NeZero m], and no primality hypothesis is needed. For m ≠ 0 the normalized form is positive definite, so every Construction A lattice is definite. At m = 1, the construction is the integer coordinate lattice with the ordinary dot product, and the same results apply.

References

• W. Ebeling, Lattices and Codes, §1.3, for binary Construction A.
• M. Harada, A. Munemasa, and B. Venkov, Classification of ternary extremal self-dual codes of length 28, §2, for the general positive-modulus normalization and the self-dual-to-unimodular implication.
• A. Munemasa and H. Tamura, The codes and the lattices of Hadamard matrices, §4, for the integrality criterion over ZMod m.

def TauCeti.ConstructionA.lattice {ι : Type u_1} (m : ℕ) (C : AddSubgroup (ι → ZMod m)) : Submodule ℤ (ι → ℚ)

The rational carrier of Construction A: the integer vectors reducing to the additive code C modulo m.

theorem TauCeti.ConstructionA.mem_lattice (m : ℕ) {ι : Type u_1} {C : AddSubgroup (ι → ZMod m)} {x : ι → ℚ} : x ∈ lattice m C ↔ ∃ (z : ι → ℤ), (fun (i : ι) => ↑(z i)) ∈ C ∧ (fun (i : ι) => ↑(z i)) = x

Membership in the Construction A carrier is given by an integer lift of a codeword.

@[simp]

theorem TauCeti.ConstructionA.intCast_mem_lattice (m : ℕ) {ι : Type u_1} {C : AddSubgroup (ι → ZMod m)} (z : ι → ℤ) : (fun (i : ι) => ↑(z i)) ∈ lattice m C ↔ (fun (i : ι) => ↑(z i)) ∈ C

An integer vector belongs to Construction A exactly when its reduction is a codeword.

theorem TauCeti.ConstructionA.exists_eq_val_add_mul (m : ℕ) {ι : Type u_1} [NeZero m] {C : AddSubgroup (ι → ZMod m)} {x : ι → ℚ} (hx : x ∈ lattice m C) : ∃ c ∈ C, ∃ (z : ι → ℤ), x = fun (i : ι) => ↑(c i).val + ↑m * ↑(z i)

For a nonzero modulus, every Construction A vector is c + m z, where c is the lift of a codeword with coordinates in [0, m).

@[simp]

theorem TauCeti.ConstructionA.lattice_le_lattice_iff (m : ℕ) {ι : Type u_1} {C D : AddSubgroup (ι → ZMod m)} : lattice m C ≤ lattice m D ↔ C ≤ D

Inclusion of Construction A carriers is equivalent to inclusion of codes.

theorem TauCeti.ConstructionA.single_mem_lattice (m : ℕ) {ι : Type u_1} [DecidableEq ι] (C : AddSubgroup (ι → ZMod m)) (i : ι) : Pi.single i ↑m ∈ lattice m C

The scaled coordinate vectors m eᵢ belong to every Construction A carrier.

instance TauCeti.ConstructionA.isLattice (m : ℕ) {ι : Type u_1} [NeZero m] [Finite ι] (C : AddSubgroup (ι → ZMod m)) : Submodule.IsLattice ℚ (lattice m C)

For a nonzero modulus and finite coordinates, every Construction A carrier is a full, finitely generated integer lattice.

def TauCeti.ConstructionA.form {ι : Type u_1} [Fintype ι] (m : ℕ) : LinearMap.BilinForm ℚ (ι → ℚ)

The rational bilinear form of Construction A, normalized by dividing the dot product by the modulus.

@[simp]

theorem TauCeti.ConstructionA.form_apply (m : ℕ) {ι : Type u_1} [Fintype ι] (x y : ι → ℚ) : ((form m) x) y = x ⬝ᵥ y / ↑m

The form is the dot product divided by the modulus.

theorem TauCeti.ConstructionA.form_isSymm (m : ℕ) {ι : Type u_1} [Fintype ι] : (form m).IsSymm

The Construction A form is symmetric.

theorem TauCeti.ConstructionA.form_nondegenerate (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] : (form m).Nondegenerate

The Construction A form is nondegenerate.

theorem TauCeti.ConstructionA.form_posDef (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] : (LinearMap.BilinMap.toQuadraticMap (form m)).PosDef

The normalized Construction A form is positive definite.

@[simp]

theorem TauCeti.ConstructionA.form_single_right (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] [DecidableEq ι] (x : ι → ℚ) (i : ι) : ((form m) x) (Pi.single i ↑m) = x i

Pairing with m eᵢ reads off the ith coordinate.

theorem TauCeti.ConstructionA.form_intCast_mem_one_iff (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (x y : ι → ℤ) : (((form m) fun (i : ι) => ↑(x i)) fun (i : ι) => ↑(y i)) ∈ 1 ↔ ((fun (i : ι) => ↑(x i)) ⬝ᵥ fun (i : ι) => ↑(y i)) = 0

Integrality of the Construction A pairing on integer vectors is precisely orthogonality of their reductions modulo m.

@[simp]

theorem TauCeti.ConstructionA.dualSubmodule_lattice (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) : (form m).dualSubmodule (lattice m C) = lattice m ((AddSubgroup.toZModSubmodule m) C).euclideanDual.toAddSubgroup

The dual of a Construction A carrier is the Construction A carrier of the Euclidean dual code, as an equality of submodules of the same rational coordinate space.

@[simp]

theorem TauCeti.ConstructionA.lattice_le_dualSubmodule_iff (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) : lattice m C ≤ (form m).dualSubmodule (lattice m C) ↔ (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual

The Construction A form is integral on its carrier exactly when the additive code is self-orthogonal for the dot product modulo m.

def TauCeti.ConstructionA.integralLattice (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : IntegralLattice (ι → ℚ)

Construction A as an integral lattice, under the exact self-orthogonality hypothesis.

@[simp]

theorem TauCeti.ConstructionA.integralLattice_carrier (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : (integralLattice m C hC).carrier = lattice m C

The underlying carrier of the bundled Construction A lattice.

@[simp]

theorem TauCeti.ConstructionA.integralLattice_form (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : (integralLattice m C hC).form = form m

The ambient form of the bundled Construction A lattice.

@[simp]

theorem TauCeti.ConstructionA.integralLattice_norm (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) (x : ι → ℚ) : (integralLattice m C hC).norm x = x ⬝ᵥ x / ↑m

The norm of a Construction A vector is its dot product with itself, divided by the modulus.

theorem TauCeti.ConstructionA.integralLattice_norm_intCast (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) (z : ι → ℤ) : ((integralLattice m C hC).norm fun (i : ι) => ↑(z i)) = ↑(∑ i : ι, z i ^ 2) / ↑m

The norm of a rational vector with integer coordinates is the sum of the squares of those coordinates, divided by the modulus.

@[simp]

theorem TauCeti.ConstructionA.integralLattice_dualCarrier (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : (integralLattice m C hC).dualCarrier = lattice m ((AddSubgroup.toZModSubmodule m) C).euclideanDual.toAddSubgroup

The dual carrier of the bundled Construction A lattice is the carrier of the dual code.

instance TauCeti.ConstructionA.isNondegenerate_integralLattice (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : (integralLattice m C hC).IsNondegenerate

A self-orthogonal code gives a nondegenerate integral lattice.

theorem TauCeti.ConstructionA.isPosDef_integralLattice (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : (integralLattice m C hC).IsPosDef

Construction A always produces a positive-definite lattice.

theorem TauCeti.ConstructionA.isUnimodular_integralLattice_iff (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : (integralLattice m C hC).IsUnimodular ↔ (AddSubgroup.toZModSubmodule m) C = ((AddSubgroup.toZModSubmodule m) C).euclideanDual

An integral Construction A lattice is unimodular exactly when its code is self-dual.

Linear codes

theorem TauCeti.ConstructionA.toZModSubmodule_toAddSubgroup_le_euclideanDual_iff (m : ℕ) {ι : Type u_1} [Fintype ι] (C : Submodule (ZMod m) (ι → ZMod m)) : (AddSubgroup.toZModSubmodule m) C.toAddSubgroup ≤ ((AddSubgroup.toZModSubmodule m) C.toAddSubgroup).euclideanDual ↔ C.IsSelfOrthogonal

For a linear code over ZMod m, the integrality hypothesis of Construction A is self-orthogonality of the code.

theorem TauCeti.ConstructionA.isUnimodular_integralLattice_toAddSubgroup_iff (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] (C : Submodule (ZMod m) (ι → ZMod m)) (hC : C.IsSelfOrthogonal) : (integralLattice m C.toAddSubgroup ⋯).IsUnimodular ↔ C.IsSelfDual

The Construction A lattice of a self-orthogonal linear code over ZMod m is unimodular exactly when the code is self-dual.

theorem TauCeti.ConstructionA.isUnimodular_integralLattice_toAddSubgroup_of_isSelfDual (m : ℕ) {ι : Type u_1} [Fintype ι] [NeZero m] {C : Submodule (ZMod m) (ι → ZMod m)} (hC : C.IsSelfDual) : (integralLattice m C.toAddSubgroup ⋯).IsUnimodular

The Construction A lattice of a self-dual linear code over ZMod m is unimodular.