The discriminant module of a Construction A lattice is C⊥ / C

Let C ≤ (ℤ/m)^ι be a self-orthogonal additive code. Inside the coordinate alphabet (ℤ/m)^ι, whose pairing is (x ⬝ᵥ y) / m, the orthogonal complement of C is its Euclidean dual C⊥, so the orthogonal quotient of C is the finite bilinear module C⊥ / C. This file identifies it with the discriminant bilinear module of the Construction A lattice P_m(C):

A_{P_m(C)} ≅ C⊥ / C.

The class of an integer vector z of the dual lattice P_m(C⊥) goes to the class of its coordinatewise reduction modulo m. When m is even and C is quadratically isotropic, so that P_m(C) is even, the same map is an isometry of finite quadratic modules for the half-norm convention.

The isometry is not computed afresh. The canonical coordinate isometry A_{L₀} ≅ (ℤ/m)^ι for the zero-code lattice L₀ = m ℤ^ι carries the transported subgroup of C onto C, the overlattice of L₀ glued along that subgroup is literally P_m(C), and the general comparison A_{L_H} ≅ H⊥ / H for an overlattice glued along an isotropic subgroup H does the rest.

Main declarations

• TauCeti.ConstructionA.discriminantBilinearOrthogonalQuotientIsometry: the isometry A_{P_m(C)} ≅ C⊥ / C of finite bilinear modules, with representative formula TauCeti.ConstructionA.discriminantBilinearOrthogonalQuotientIsometry_mk_intCast.
• TauCeti.ConstructionA.discriminantOrthogonalQuotientIsometry: the isometry of finite quadratic modules for an even modulus and a quadratically isotropic code, with representative formula TauCeti.ConstructionA.discriminantOrthogonalQuotientIsometry_mk_intCast.
• TauCeti.ConstructionA.natCard_orthogonalQuotient_coordinatePower_zmodStandard: the order of C⊥ / C is the discriminant of P_m(C).
• subsingleton_orthogonalQuotient_coordinatePower_zmodStandard_iff_isUnimodular: C⊥ / C is trivial exactly when P_m(C) is unimodular.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.4, Proposition 1.4.1.
• W. Ebeling, Lattices and Codes, §§1.3 and 3.3.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §3, and Chapter 7, §§8–9.

The bilinear isometry

noncomputable def TauCeti.ConstructionA.discriminantBilinearOrthogonalQuotientIsometry (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : (integralLattice m C hC).discriminantBilinearModule.Isometry (((FiniteBilinearModule.zmodStandard m).coordinatePower ι).orthogonalQuotient C)

The discriminant bilinear module of a Construction A lattice is C⊥ / C. For a self-orthogonal additive code C over ℤ/m, the discriminant bilinear module of P_m(C) is the orthogonal quotient of C in the coordinate alphabet (ℤ/m)^ι.

@[simp]

theorem TauCeti.ConstructionA.discriminantBilinearOrthogonalQuotientIsometry_mk_intCast (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) (z : ι → ℤ) (hz : (fun (i : ι) => ↑(z i)) ∈ (integralLattice m C hC).dualCarrier) : (discriminantBilinearOrthogonalQuotientIsometry m ι C hC) (Submodule.Quotient.mk ⟨fun (i : ι) => ↑(z i), hz⟩) = (((FiniteBilinearModule.zmodStandard m).coordinatePower ι).orthogonalQuotientMk C) ⟨fun (i : ι) => ↑(z i), ⋯⟩

The representative formula. The class in A_{P_m(C)} of an integer vector of the dual lattice goes to the class in C⊥ / C of its coordinatewise reduction modulo m.

theorem TauCeti.ConstructionA.natCard_orthogonalQuotient_coordinatePower_zmodStandard (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : Nat.card (((FiniteBilinearModule.zmodStandard m).coordinatePower ι).orthogonalQuotient C).carrier = (integralLattice m C hC).discriminant

The order of C⊥ / C is the discriminant of the Construction A lattice.

theorem TauCeti.ConstructionA.subsingleton_orthogonalQuotient_coordinatePower_zmodStandard_iff_isUnimodular (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (C : AdditiveCode (ZMod m) ι) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : Subsingleton (((FiniteBilinearModule.zmodStandard m).coordinatePower ι).orthogonalQuotient C).carrier ↔ (integralLattice m C hC).IsUnimodular

The orthogonal quotient of a self-orthogonal code is trivial exactly when its Construction A lattice is unimodular.

The quadratic isometry for an even modulus

noncomputable def TauCeti.ConstructionA.discriminantOrthogonalQuotientIsometry (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (hm : Even m) (C : AdditiveCode (ZMod m) ι) (hC : ((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).IsIsotropic C) : ((integralLattice m C ⋯).discriminantQuadraticModule ⋯).Isometry (((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).orthogonalQuotient C hC)

The discriminant quadratic module of an even Construction A lattice is C⊥ / C. Over an even modulus, for a quadratically isotropic code C, the discriminant quadratic module of the even lattice P_m(C) is the quadratic orthogonal quotient of C in the coordinate alphabet (ℤ/m)^ι, in the half-norm convention.

@[simp]

theorem TauCeti.ConstructionA.discriminantOrthogonalQuotientIsometry_mk_intCast (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (hm : Even m) (C : AdditiveCode (ZMod m) ι) (hC : ((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).IsIsotropic C) (z : ι → ℤ) (hz : (fun (i : ι) => ↑(z i)) ∈ (integralLattice m C ⋯).dualCarrier) : (discriminantOrthogonalQuotientIsometry m ι hm C hC) (Submodule.Quotient.mk ⟨fun (i : ι) => ↑(z i), hz⟩) = (((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).orthogonalQuotientMk C hC) ⟨fun (i : ι) => ↑(z i), ⋯⟩

The representative formula. The class in the discriminant quadratic module of P_m(C) of an integer vector of the dual lattice goes to the class in C⊥ / C of its coordinatewise reduction modulo m.