Documentation

TauCeti.LinearAlgebra.IntegralLattice.ConstructionA.Code.Quadratic

Quadratically isotropic codes in the Construction A discriminant group #

For an even modulus, the discriminant group of the zero-code Construction A lattice carries a quadratic form. The coordinate isometry identifies quadratic isotropy of the subgroup attached to a code with quadratic isotropy of the code in the standard coordinate alphabet. Consequently, gluing the zero-code lattice along this subgroup gives exactly the existing Construction A integral lattice, not merely an abstractly isometric copy. The general gluing criterion then says that the glued lattice is unimodular exactly when the code is Lagrangian, that is, equal to its own orthogonal complement in the coordinate alphabet.

This supplies the quadratic refinement of the bilinear code transport in TauCeti.LinearAlgebra.IntegralLattice.ConstructionA.Code.Basic.

Main declarations #

References #

source
theorem TauCeti.ConstructionA.isIsotropic_codeInZeroLatticeDiscriminantQuadraticModule_iff (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (hm : Even m) (C : AdditiveCode (ZMod m) ι) :
((zeroLattice m ι).discriminantQuadraticModule ⋯).IsIsotropic (codeInZeroLatticeDiscriminantGroup m ι C) ↔ ((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).IsIsotropic C

A code transported into the zero lattice's discriminant group is quadratically isotropic exactly when the original code is quadratically isotropic in the standard coordinate alphabet.

source
theorem TauCeti.ConstructionA.isIsotropic_codeInZeroLatticeDiscriminantQuadraticModule_iff_isEven (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (hm : Even m) (C : AdditiveCode (ZMod m) ι) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) :
((zeroLattice m ι).discriminantQuadraticModule ⋯).IsIsotropic (codeInZeroLatticeDiscriminantGroup m ι C) ↔ (integralLattice m C hC).IsEven

Quadratic isotropy of the transported discriminant subgroup is equivalent to evenness of the associated Construction A integral lattice.

source
theorem TauCeti.ConstructionA.isIsotropic_codeInZeroLatticeDiscriminantQuadraticModule_two_iff_isDoublyEven (ι : Type u_1) [Fintype ι] (C : LinearCode (ZMod 2) ι) :
((zeroLattice 2 ι).discriminantQuadraticModule ⋯).IsIsotropic (codeInZeroLatticeDiscriminantGroup 2 ι (Submodule.toAddSubgroup C)) ↔ BinaryCode.IsDoublyEven C

Over the binary alphabet, the subgroup transported into the zero lattice's discriminant quadratic module is isotropic exactly when the linear code is doubly even.

source
theorem TauCeti.ConstructionA.ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup_eq_integralLattice (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (hm : Even m) (C : AdditiveCode (ZMod m) ι) (hC : ((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).IsIsotropic C) :
(zeroLattice m ι).ofIsotropicSubgroup ⋯ (codeInZeroLatticeDiscriminantGroup m ι C) ⋯ = integralLattice m C ⋯

Gluing the zero-code lattice along the discriminant subgroup of a quadratically isotropic code gives its Construction A integral lattice. Both lattices have the literal Construction A carrier inside ι → ℚ and the same normalized dot-product form.

source
theorem TauCeti.ConstructionA.isUnimodular_ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup_iff (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (hm : Even m) (C : AdditiveCode (ZMod m) ι) (hC : ((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).IsIsotropic C) :
((zeroLattice m ι).ofIsotropicSubgroup ⋯ (codeInZeroLatticeDiscriminantGroup m ι C) ⋯).IsUnimodular ↔ ((FiniteBilinearModule.zmodStandard m).coordinatePower ι).IsLagrangian C

Gluing along a code gives a unimodular lattice exactly when the code is Lagrangian. For an even modulus and a quadratically isotropic code C, the overlattice of the zero-code lattice m ℤ^ι glued along the discriminant subgroup of C is unimodular exactly when C equals its orthogonal complement in the coordinate alphabet (ℤ/m)^ι.