Additive codes in the Construction A discriminant group

The discriminant group of the zero-code Construction A lattice is canonically the coordinate alphabet (ℤ/m)^ι. This file transports an additive code through that canonical isometry, so the code becomes an actual subgroup of the discriminant group. The transport identifies bilinear orthogonal complements, bilinear isotropy, and the Lagrangian condition, and its inverse-image carrier is exactly the Construction A carrier of the original code. Gluing along a self-orthogonal code gives the Construction A integral lattice. The orthogonal-complement and isotropy statements use the finite bilinear-module presentation, while the carrier statement and the Lagrangian criterion use the quotient discriminant-group presentation required by the corresponding APIs. Quadratic isotropy is not treated here.

References:

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.4.
• W. Ebeling, Lattices and Codes, §§1.3 and 3.3.

Transport to the discriminant module

noncomputable def TauCeti.ConstructionA.codeInZeroLatticeDiscriminantBilinearModule (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) : AddSubgroup (zeroLattice m ι).discriminantBilinearModule.carrier

The additive code C as the inverse image under the canonical isometry from the zero-lattice discriminant group to the coordinate alphabet.

@[simp]

theorem TauCeti.ConstructionA.mem_codeInZeroLatticeDiscriminantBilinearModule_iff (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) {x : (zeroLattice m ι).discriminantBilinearModule.carrier} : x ∈ codeInZeroLatticeDiscriminantBilinearModule m ι C ↔ (discriminantIsometry m ι) x ∈ C

@[simp]

theorem TauCeti.ConstructionA.map_codeInZeroLatticeDiscriminantBilinearModule (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) : AddSubgroup.map (↑(discriminantIsometry m ι).toAddEquiv) (codeInZeroLatticeDiscriminantBilinearModule m ι C) = C

Reduction maps the transported discriminant subgroup back to the original code.

@[simp]

theorem TauCeti.ConstructionA.orthogonalComplement_codeInZeroLatticeDiscriminantBilinearModule (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) : (zeroLattice m ι).discriminantBilinearModule.orthogonalComplement (codeInZeroLatticeDiscriminantBilinearModule m ι C) = codeInZeroLatticeDiscriminantBilinearModule m ι ((AddSubgroup.toZModSubmodule m) C).euclideanDual.toAddSubgroup

The orthogonal complement of a transported code is the transport of its Euclidean dual.

theorem TauCeti.ConstructionA.intCast_mem_integralLattice_dualCarrier_iff (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) (z : ι → ℤ) : (fun (i : ι) => ↑(z i)) ∈ (integralLattice m C hC).dualCarrier ↔ (fun (i : ι) => ↑(z i)) ∈ ((FiniteBilinearModule.zmodStandard m).coordinatePower ι).orthogonalComplement C

An integer vector lies in the dual of the Construction A lattice exactly when its reduction lies in the orthogonal complement of the code in the coordinate alphabet.

@[simp]

theorem TauCeti.ConstructionA.isIsotropic_codeInZeroLatticeDiscriminantBilinearModule_iff (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) : (zeroLattice m ι).discriminantBilinearModule.IsIsotropic (codeInZeroLatticeDiscriminantBilinearModule m ι C) ↔ ((FiniteBilinearModule.zmodStandard m).coordinatePower ι).IsIsotropic C

Bilinear isotropy is preserved by the coordinate identification.

theorem TauCeti.ConstructionA.isIsotropic_codeInZeroLatticeDiscriminantBilinearModule_iff_le_euclideanDual (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) : (zeroLattice m ι).discriminantBilinearModule.IsIsotropic (codeInZeroLatticeDiscriminantBilinearModule m ι C) ↔ (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual

A code is bilinearly isotropic in the discriminant group exactly when it is self-orthogonal.

The inverse-image carrier

noncomputable def TauCeti.ConstructionA.codeInZeroLatticeDiscriminantGroup (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) : AddSubgroup (zeroLattice m ι).DiscriminantGroup

The same inverse-image code as a subgroup of the quotient discriminant group used by intermediate-carrier constructions.

@[simp]

theorem TauCeti.ConstructionA.mem_codeInZeroLatticeDiscriminantGroup_iff (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) {x : (zeroLattice m ι).DiscriminantGroup} : x ∈ codeInZeroLatticeDiscriminantGroup m ι C ↔ (discriminantEquiv m ι) x ∈ C

theorem TauCeti.ConstructionA.mem_codeInZeroLatticeDiscriminantGroup_iff_discriminantIsometry (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) {x : (zeroLattice m ι).DiscriminantGroup} : x ∈ codeInZeroLatticeDiscriminantGroup m ι C ↔ (discriminantIsometry m ι) x ∈ C

The quotient-group view has the same coordinate membership characterization as the finite-bilinear-module view, expressed through the canonical discriminant isometry.

theorem TauCeti.ConstructionA.codeInZeroLatticeDiscriminantGroup_eq_codeInZeroLatticeDiscriminantBilinearModule (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) : codeInZeroLatticeDiscriminantGroup m ι C = codeInZeroLatticeDiscriminantBilinearModule m ι C

The quotient-group and finite-bilinear-module views of a transported code are the same subgroup of the zero-lattice discriminant group.

theorem TauCeti.ConstructionA.isIsotropic_codeInZeroLatticeDiscriminantGroup (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : (zeroLattice m ι).discriminantBilinearModule.IsIsotropic (codeInZeroLatticeDiscriminantGroup m ι C)

The subgroup of the zero-lattice discriminant group transported from a self-orthogonal code is isotropic for the discriminant pairing.

@[simp]

theorem TauCeti.ConstructionA.isLagrangian_codeInZeroLatticeDiscriminantGroup_iff (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) : (zeroLattice m ι).discriminantBilinearModule.IsLagrangian (codeInZeroLatticeDiscriminantGroup m ι C) ↔ ((FiniteBilinearModule.zmodStandard m).coordinatePower ι).IsLagrangian C

The subgroup of the zero-lattice discriminant group transported from a code is Lagrangian exactly when the code is Lagrangian in the coordinate alphabet.

@[simp]

theorem TauCeti.ConstructionA.map_codeInZeroLatticeDiscriminantGroup (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) : AddSubgroup.map (↑(discriminantEquiv m ι).toAddEquiv) (codeInZeroLatticeDiscriminantGroup m ι C) = C

Reduction maps the transported discriminant subgroup back to the original code.

@[simp]

theorem TauCeti.ConstructionA.coe_intermediateCarrierOfDiscriminantSubgroup_codeInZeroLatticeDiscriminantGroup (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) : ↑((zeroLattice m ι).intermediateCarrierOfDiscriminantSubgroup (codeInZeroLatticeDiscriminantGroup m ι C)) = lattice m C

The inverse-image carrier of a transported code is its Construction A carrier.

theorem TauCeti.ConstructionA.toIntegralLattice_codeInZeroLatticeDiscriminantGroup_eq_integralLattice (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : ⋯.toIntegralLattice = integralLattice m C hC

Gluing the zero-code lattice along a self-orthogonal code gives Construction A. The integral overlattice of m ℤ^ι glued along the discriminant subgroup of C has the literal Construction A carrier and the same normalized dot-product form.