Discriminant coset minima of orthogonal sums

Under the canonical identification A_(L ⊥ M) ≃ A_L × A_M, the norms in a discriminant coset are exactly the sums of norms in its two component cosets. Consequently, attained component minima add, and a vector attains their sum exactly when both components attain their minima. Iterating this result combines shortest-coset calculations for root lattices without losing attainment in the orthogonal sum.

The same holds for the orthogonal sum ⊥ i, L i of a finite family: under A_(⊥ i, L i) ≃ Π i, A_(L i), attained least norms r i of the component cosets sum to the attained least norm ∑ i, r i of the coset of the orthogonal sum, and a vector of that coset attains ∑ i, r i exactly when each of its coordinates attains r i. This is the form in which the shortest norm of a glue word is the sum of the shortest norms of its labels.

No positivity, evenness, or nondegeneracy assumption is required: the statements apply whenever the specified component cosets have least norms.

The construction uses discriminantGroupOrthogonalSumEquiv and orthogonalSumDualCarrierEquiv, respectively discriminantGroupPiEquiv and piDualCarrierEquiv, to keep the classes tied to the actual dual carriers.

References

• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §6 and Chapter 16, §1.

theorem TauCeti.IntegralLattice.setOf_form_self_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (a : L.DiscriminantGroup) (b : M.DiscriminantGroup) : {q : ℚ | ∃ (x : ↥(L.orthogonalSum M).dualCarrier), Submodule.Quotient.mk x = (L.discriminantGroupOrthogonalSumEquiv M).symm (a, b) ∧ ((L.orthogonalSum M).form ↑x) ↑x = q} = Set.image2 (fun (x1 x2 : ℚ) => x1 + x2) {q : ℚ | ∃ (x : ↥L.dualCarrier), Submodule.Quotient.mk x = a ∧ (L.form ↑x) ↑x = q} {q : ℚ | ∃ (y : ↥M.dualCarrier), Submodule.Quotient.mk y = b ∧ (M.form ↑y) ↑y = q}

The norms in a discriminant coset of an orthogonal sum are exactly the pairwise sums of norms in its component cosets.

theorem TauCeti.IntegralLattice.isLeast_form_self_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) {a : L.DiscriminantGroup} {b : M.DiscriminantGroup} {r s : ℚ} (hL : IsLeast {q : ℚ | ∃ (x : ↥L.dualCarrier), Submodule.Quotient.mk x = a ∧ (L.form ↑x) ↑x = q} r) (hM : IsLeast {q : ℚ | ∃ (y : ↥M.dualCarrier), Submodule.Quotient.mk y = b ∧ (M.form ↑y) ↑y = q} s) : IsLeast {q : ℚ | ∃ (x : ↥(L.orthogonalSum M).dualCarrier), Submodule.Quotient.mk x = (L.discriminantGroupOrthogonalSumEquiv M).symm (a, b) ∧ ((L.orthogonalSum M).form ↑x) ↑x = q} (r + s)

Attained least norms in two discriminant cosets add to the attained least norm of the corresponding coset of the orthogonal sum.

theorem TauCeti.IntegralLattice.form_self_orthogonalSum_eq_add_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) {a : L.DiscriminantGroup} {b : M.DiscriminantGroup} {r s : ℚ} (hL : r ∈ lowerBounds {q : ℚ | ∃ (x : ↥L.dualCarrier), Submodule.Quotient.mk x = a ∧ (L.form ↑x) ↑x = q}) (hM : s ∈ lowerBounds {q : ℚ | ∃ (y : ↥M.dualCarrier), Submodule.Quotient.mk y = b ∧ (M.form ↑y) ↑y = q}) (x : ↥(L.orthogonalSum M).dualCarrier) (hx : Submodule.Quotient.mk x = (L.discriminantGroupOrthogonalSumEquiv M).symm (a, b)) : ((L.orthogonalSum M).form ↑x) ↑x = r + s ↔ (L.form ↑((L.orthogonalSumDualCarrierEquiv M) x).1) ↑((L.orthogonalSumDualCarrierEquiv M) x).1 = r ∧ (M.form ↑((L.orthogonalSumDualCarrierEquiv M) x).2) ↑((L.orthogonalSumDualCarrierEquiv M) x).2 = s

A vector in a fixed discriminant coset attains the sum of component lower bounds exactly when both components attain their respective bounds.

Finite families

theorem TauCeti.IntegralLattice.isLeast_form_self_pi {ι : Type v} [Fintype ι] {U : ι → Type u} [(i : ι) → AddCommGroup (U i)] [(i : ι) → Module ℚ (U i)] (N : (i : ι) → IntegralLattice (U i)) {a : (i : ι) → (N i).DiscriminantGroup} {r : ι → ℚ} (h : ∀ (i : ι), IsLeast {q : ℚ | ∃ (x : ↥(N i).dualCarrier), Submodule.Quotient.mk x = a i ∧ ((N i).form ↑x) ↑x = q} (r i)) : IsLeast {q : ℚ | ∃ (x : ↥(pi N).dualCarrier), Submodule.Quotient.mk x = (discriminantGroupPiEquiv N).symm a ∧ ((pi N).form ↑x) ↑x = q} (∑ i : ι, r i)

Attained least norms r i in the discriminant cosets a i of a finite family of lattices sum to the attained least norm of the corresponding coset of the orthogonal sum ⊥ i, N i.

theorem TauCeti.IntegralLattice.form_self_pi_eq_sum_iff {ι : Type v} [Fintype ι] {U : ι → Type u} [(i : ι) → AddCommGroup (U i)] [(i : ι) → Module ℚ (U i)] (N : (i : ι) → IntegralLattice (U i)) {a : (i : ι) → (N i).DiscriminantGroup} {r : ι → ℚ} (h : ∀ (i : ι), r i ∈ lowerBounds {q : ℚ | ∃ (x : ↥(N i).dualCarrier), Submodule.Quotient.mk x = a i ∧ ((N i).form ↑x) ↑x = q}) (x : ↥(pi N).dualCarrier) (hx : Submodule.Quotient.mk x = (discriminantGroupPiEquiv N).symm a) : ((pi N).form ↑x) ↑x = ∑ i : ι, r i ↔ ∀ (i : ι), ((N i).form ↑((piDualCarrierEquiv N) x i)) ↑((piDualCarrierEquiv N) x i) = r i

A vector in a fixed discriminant coset of the orthogonal sum ⊥ i, N i attains the sum of component lower bounds exactly when each of its coordinates attains its bound.