The Golay code as discriminant glue for Construction A

The extended binary Golay code is a quadratic-isotropic subgroup of the discriminant group of the zero-code lattice 2 ℤ²⁴. Gluing that subgroup gives the same integral lattice, in the same rational ambient space, as Construction A applied directly to the code. Its self-duality makes the code Lagrangian in the coordinate discriminant module, hence also in the discriminant group of 2 ℤ²⁴, so its orthogonal quotient is trivial. The glued lattice is even because its glue is quadratic-isotropic, by TauCeti.IntegralLattice.isEven_ofIsotropicSubgroup, and unimodular because its glue is Lagrangian, by TauCeti.IntegralLattice.isUnimodular_ofIsotropicSubgroup_iff_isLagrangian.

This identifies the code and lattice descriptions of the Golay construction through the actual discriminant subgroup, with no choice of an abstract lattice isomorphism. The final discriminant modules of the named lattice are also compared, by both bilinear and quadratic isometries, with the actual orthogonal quotients of the Golay code; those quotients are trivial because the code is Lagrangian, so both discriminant modules are trivial.

References

• 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.

theorem TauCeti.BinaryGolay.isIsotropic_codeInZeroLatticeDiscriminantQuadraticModule : ((ConstructionA.zeroLattice 2 (Fin 24)).discriminantQuadraticModule ⋯).IsIsotropic (ConstructionA.codeInZeroLatticeDiscriminantGroup 2 (Fin 24) (Submodule.toAddSubgroup code))

The Golay code defines a quadratic-isotropic subgroup of the discriminant group of the zero-code lattice 2 ℤ²⁴.

@[simp]

theorem TauCeti.BinaryGolay.ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup_eq_constructionALattice : (ConstructionA.zeroLattice 2 (Fin 24)).ofIsotropicSubgroup ⋯ (ConstructionA.codeInZeroLatticeDiscriminantGroup 2 (Fin 24) (Submodule.toAddSubgroup code)) isIsotropic_codeInZeroLatticeDiscriminantQuadraticModule = constructionALattice

Gluing 2 ℤ²⁴ along the Golay discriminant subgroup is literally the Golay Construction A lattice, with its halved dot product on the rational coordinate space.

theorem TauCeti.BinaryGolay.isLagrangian_code : ((FiniteBilinearModule.zmodStandard 2).coordinatePower (Fin 24)).IsLagrangian (Submodule.toAddSubgroup code)

The Golay code is Lagrangian in the binary coordinate discriminant module.

theorem TauCeti.BinaryGolay.isLagrangian_codeInZeroLatticeDiscriminantGroup : (ConstructionA.zeroLattice 2 (Fin 24)).discriminantBilinearModule.IsLagrangian (ConstructionA.codeInZeroLatticeDiscriminantGroup 2 (Fin 24) (Submodule.toAddSubgroup code))

The Golay code is Lagrangian in the discriminant group of the zero-code lattice 2 ℤ²⁴.

theorem TauCeti.BinaryGolay.natCard_orthogonalQuotient_code_eq_one : Nat.card (((FiniteBilinearModule.zmodStandard 2).coordinatePower (Fin 24)).orthogonalQuotient (Submodule.toAddSubgroup code)).carrier = 1

The orthogonal quotient of the Golay code in the binary coordinate discriminant module has one element: the code is its own Euclidean dual.

theorem TauCeti.BinaryGolay.isIsotropic_code : ((FiniteQuadraticModule.zmodStandard 2 ⋯).coordinatePower (Fin 24)).IsIsotropic (Submodule.toAddSubgroup code)

The binary coordinate discriminant form is quadratically isotropic on the Golay code.

theorem TauCeti.BinaryGolay.isEven_ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup : ((ConstructionA.zeroLattice 2 (Fin 24)).ofIsotropicSubgroup ⋯ (ConstructionA.codeInZeroLatticeDiscriminantGroup 2 (Fin 24) (Submodule.toAddSubgroup code)) isIsotropic_codeInZeroLatticeDiscriminantQuadraticModule).IsEven

Gluing 2 ℤ²⁴ along the Golay code gives an even lattice, because the glue is quadratic-isotropic.

theorem TauCeti.BinaryGolay.isUnimodular_ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup : ((ConstructionA.zeroLattice 2 (Fin 24)).ofIsotropicSubgroup ⋯ (ConstructionA.codeInZeroLatticeDiscriminantGroup 2 (Fin 24) (Submodule.toAddSubgroup code)) isIsotropic_codeInZeroLatticeDiscriminantQuadraticModule).IsUnimodular

Gluing 2 ℤ²⁴ along the Golay code gives a unimodular lattice, because the glue is Lagrangian.

noncomputable def TauCeti.BinaryGolay.discriminantBilinearOrthogonalQuotientIsometry : constructionALattice.discriminantBilinearModule.Isometry (((FiniteBilinearModule.zmodStandard 2).coordinatePower (Fin 24)).orthogonalQuotient (Submodule.toAddSubgroup code))

The discriminant bilinear module of the Golay Construction A lattice is the actual orthogonal quotient of its code.

noncomputable def TauCeti.BinaryGolay.discriminantQuadraticOrthogonalQuotientIsometry : (constructionALattice.discriminantQuadraticModule isEven_constructionALattice).Isometry (((FiniteQuadraticModule.zmodStandard 2 ⋯).coordinatePower (Fin 24)).orthogonalQuotient (Submodule.toAddSubgroup code) isIsotropic_code)

The discriminant quadratic module of the Golay Construction A lattice is the actual quadratic orthogonal quotient of its code.

instance TauCeti.BinaryGolay.subsingleton_discriminantBilinearModule : Subsingleton constructionALattice.discriminantBilinearModule.carrier

The discriminant bilinear group of the Golay lattice is trivial.

theorem TauCeti.BinaryGolay.natCard_discriminantBilinearModule_eq_one : Nat.card constructionALattice.discriminantBilinearModule.carrier = 1

The discriminant bilinear group of the Golay lattice has one element.

instance TauCeti.BinaryGolay.subsingleton_discriminantQuadraticModule : Subsingleton (constructionALattice.discriminantQuadraticModule isEven_constructionALattice).carrier

The discriminant quadratic group of the Golay lattice is trivial.