Discriminant forms of coordinate powers

The coordinate power L^ι is the orthogonal sum of the constant family at L, so the canonical equivalence TauCeti.IntegralLattice.discriminantGroupPiEquiv specialises to

A_(L^ι) ≃ (A_L)^ι,

which sends the class of x to the family of classes of its coordinates. This file proves that it is an isometry from the discriminant pairing of L^ι to the coordinate power of the discriminant pairing of L, and, when L is even, of the half-norm discriminant quadratic modules.

Composing with a coordinatewise alphabet isometry gives the interface through which codes enter lattice constructions: an isometry A ≅ A_L from a finite quadratic alphabet induces an isometry from the coordinate module A^ι to the actual discriminant module of the orthogonal sum L^ι. An additive code C ≤ A^ι is carried to a subgroup of A_(L^ι), and quadratic isotropy and the Lagrangian condition transfer along this isometry by TauCeti.FiniteQuadraticModule.Isometry.isIsotropic_map_iff and TauCeti.FiniteQuadraticModule.Isometry.isLagrangian_map_iff.

Main declarations

• TauCeti.IntegralLattice.discriminantBilinearIsometryCoordinatePower: the equivalence A_(L^ι) ≃ (A_L)^ι is an isometry of finite bilinear modules.
• TauCeti.IntegralLattice.discriminantQuadraticIsometryCoordinatePower: for even L, it is an isometry of finite quadratic modules, the constant-family case of TauCeti.IntegralLattice.discriminantQuadraticIsometryPi.
• TauCeti.FiniteQuadraticModule.Isometry.coordinatePowerDiscriminant: the isometry A^ι ≅ A_(L^ι) induced by an alphabet isometry A ≅ A_L, with the bilinear analogue TauCeti.FiniteBilinearModule.Isometry.coordinatePowerDiscriminant.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.1.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §3.
• TauCeti/LinearAlgebra/IntegralLattice/Discriminant/Operations.lean: the binary orthogonal-sum isometries A_(L ⊥ M) ≃ A_L × A_M (discriminantBilinearIsometryOrthogonalSum and discriminantQuadraticIsometryOrthogonalSum). The isometries of this file are their analogue for the ι-fold orthogonal sum L^ι.

The discriminant bilinear module

noncomputable def TauCeti.IntegralLattice.discriminantBilinearIsometryCoordinatePower {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (ι : Type v) [Fintype ι] [L.IsNondegenerate] : (L.coordinatePower ι).discriminantBilinearModule.Isometry (L.discriminantBilinearModule.coordinatePower ι)

The equivalence A_(L^ι) ≃ (A_L)^ι of discriminant groups is an isometry from the discriminant pairing of L^ι to the coordinate power of the discriminant pairing of L.

@[simp]

theorem TauCeti.IntegralLattice.discriminantBilinearIsometryCoordinatePower_toAddEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (ι : Type v) [Fintype ι] [L.IsNondegenerate] : (L.discriminantBilinearIsometryCoordinatePower ι).toAddEquiv = (discriminantGroupPiEquiv fun (x : ι) => L).toAddEquiv

The underlying additive equivalence of the coordinate-power discriminant-bilinear isometry is the canonical equivalence A_(L^ι) ≃ (A_L)^ι of discriminant groups.

@[simp]

theorem TauCeti.IntegralLattice.discriminantBilinearIsometryCoordinatePower_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (ι : Type v) [Fintype ι] [L.IsNondegenerate] (x : (L.coordinatePower ι).DiscriminantGroup) : (L.discriminantBilinearIsometryCoordinatePower ι) x = (discriminantGroupPiEquiv fun (x : ι) => L) x

The coordinate-power discriminant-bilinear isometry acts through the canonical equivalence A_(L^ι) ≃ (A_L)^ι of discriminant groups.

The discriminant quadratic module

noncomputable def TauCeti.IntegralLattice.discriminantQuadraticIsometryCoordinatePower {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (ι : Type v) [Fintype ι] [L.IsNondegenerate] (hL : L.IsEven) : ((L.coordinatePower ι).discriminantQuadraticModule ⋯).Isometry ((L.discriminantQuadraticModule hL).coordinatePower ι)

For an even lattice L, the equivalence A_(L^ι) ≃ (A_L)^ι of discriminant groups is an isometry from the half-norm discriminant quadratic module of L^ι to the coordinate power of the discriminant quadratic module of L.

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticIsometryCoordinatePower_toAddEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (ι : Type v) [Fintype ι] [L.IsNondegenerate] (hL : L.IsEven) : (L.discriminantQuadraticIsometryCoordinatePower ι hL).toAddEquiv = (discriminantGroupPiEquiv fun (x : ι) => L).toAddEquiv

The underlying additive equivalence of the coordinate-power discriminant-quadratic isometry is the canonical equivalence A_(L^ι) ≃ (A_L)^ι of discriminant groups.

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticIsometryCoordinatePower_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (ι : Type v) [Fintype ι] [L.IsNondegenerate] (hL : L.IsEven) (x : (L.coordinatePower ι).DiscriminantGroup) : (L.discriminantQuadraticIsometryCoordinatePower ι hL) x = (discriminantGroupPiEquiv fun (x : ι) => L) x

The coordinate-power discriminant-quadratic isometry acts through the canonical equivalence A_(L^ι) ≃ (A_L)^ι of discriminant groups.

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticIsometryCoordinatePower_toFiniteBilinearModule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (ι : Type v) [Fintype ι] [L.IsNondegenerate] (hL : L.IsEven) : (L.discriminantQuadraticIsometryCoordinatePower ι hL).toFiniteBilinearModule = L.discriminantBilinearIsometryCoordinatePower ι

Forgetting the quadratic maps from the coordinate-power discriminant isometry recovers the coordinate-power discriminant-bilinear isometry.

Coordinate alphabets

noncomputable def TauCeti.FiniteBilinearModule.Isometry.coordinatePowerDiscriminant {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {A : FiniteBilinearModule} (f : A.Isometry L.discriminantBilinearModule) (ι : Type v) [Fintype ι] : (A.coordinatePower ι).Isometry (L.coordinatePower ι).discriminantBilinearModule

An isometry A ≅ A_L from a finite bilinear alphabet to the discriminant bilinear module of a nondegenerate lattice induces, coordinatewise, an isometry from the coordinate module A^ι to the discriminant bilinear module of the orthogonal sum L^ι.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.coordinatePowerDiscriminant_apply {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {ι : Type v} [Fintype ι] {A : FiniteBilinearModule} (f : A.Isometry L.discriminantBilinearModule) (x : ι → A.carrier) : (f.coordinatePowerDiscriminant ι) x = (L.discriminantBilinearIsometryCoordinatePower ι).symm ((f.coordinatePower ι) x)

The coordinatewise bilinear alphabet isometry applies the alphabet isometry in each coordinate and then identifies (A_L)^ι with A_(L^ι).

noncomputable def TauCeti.FiniteQuadraticModule.Isometry.coordinatePowerDiscriminant {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {hL : L.IsEven} {A : FiniteQuadraticModule} (f : A.Isometry (L.discriminantQuadraticModule hL)) (ι : Type v) [Fintype ι] : (A.coordinatePower ι).Isometry ((L.coordinatePower ι).discriminantQuadraticModule ⋯)

An isometry A ≅ A_L from a finite quadratic alphabet to the discriminant module of an even lattice induces, coordinatewise, an isometry from the coordinate module A^ι to the discriminant module of the orthogonal sum L^ι.

@[simp]

theorem TauCeti.FiniteQuadraticModule.Isometry.coordinatePowerDiscriminant_apply {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {hL : L.IsEven} {ι : Type v} [Fintype ι] {A : FiniteQuadraticModule} (f : A.Isometry (L.discriminantQuadraticModule hL)) (x : ι → A.carrier) : (f.coordinatePowerDiscriminant ι) x = (QuadraticMap.IsometryEquiv.symm (L.discriminantQuadraticIsometryCoordinatePower ι hL)) ((f.coordinatePower ι) x)

The coordinatewise quadratic alphabet isometry applies the alphabet isometry in each coordinate and then identifies (A_L)^ι with A_(L^ι).

@[simp]

theorem TauCeti.FiniteQuadraticModule.Isometry.discriminantGroupPiEquiv_coordinatePowerDiscriminant_apply {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {hL : L.IsEven} {ι : Type v} [Fintype ι] {A : FiniteQuadraticModule} (f : A.Isometry (L.discriminantQuadraticModule hL)) (x : ι → A.carrier) (i : ι) : (IntegralLattice.discriminantGroupPiEquiv fun (x : ι) => L) ((f.coordinatePowerDiscriminant ι) x) i = f (x i)

In each coordinate of (A_L)^ι, the coordinatewise quadratic alphabet isometry is the alphabet isometry applied to that coordinate.