Discriminant forms of orthogonal sums of finite families #
The dual carrier of the orthogonal sum ⊥ i, L i of a finite family of integral lattices consists
of the families whose values lie in the dual carriers of the summands. Passing to quotients
coordinatewise gives the canonical equivalence
A_(⊥ i, L i) ≃ Π i, A_(L i),
which sends the class of x to the family of classes of its coordinates. When every summand is
even and nondegenerate, this file proves that it is an isometry from the half-norm discriminant
quadratic module of the orthogonal sum to the orthogonal sum
TauCeti.FiniteQuadraticModule.pi of the discriminant quadratic modules of the summands.
Composing with summandwise alphabet isometries A_i ≅ A_(L i) gives the interface through which
glue words enter lattice constructions: an isometry from the coordinate module Π i, A_i to the
actual discriminant module of the orthogonal sum
(TauCeti.IntegralLattice.discriminantQuadraticIsometryPiOfIsometry). That isometry is natural
for coordinatewise isometries of the summands and for reindexing of the family, so glue words of a
reducible root system transform as expected under componentwise isometries of the root lattices
and permutations of the components.
Main declarations #
TauCeti.IntegralLattice.dualCarrier_pi: the dual carrier of an orthogonal sum is the product of the dual carriers.TauCeti.IntegralLattice.discriminantGroupPiEquiv:A_(⊥ i, L i) ≃ Π i, A_(L i).TauCeti.IntegralLattice.discriminantQuadraticIsometryPi: for even nondegenerate summands, this equivalence is an isometry of finite quadratic modules.TauCeti.IntegralLattice.discriminantQuadraticIsometryPiOfIsometry: the isometryΠ i, A_i ≅ A_(⊥ i, L i)induced by summandwise isometriesA_i ≅ A_(L i), with coordinatesTauCeti.IntegralLattice.discriminantGroupPiEquiv_discriminantQuadraticIsometryPiOfIsometry.discriminantQuadraticIsometry_pi_discriminantQuadraticIsometryPiOfIsometryanddiscriminantQuadraticIsometry_piCongrLeft_discriminantQuadraticIsometryPiOfIsometry, inTauCeti.IntegralLattice: naturality of that isometry under coordinatewise isometries (TauCeti.IntegralLattice.Isometry.pi) and under reindexing (TauCeti.IntegralLattice.Isometry.piCongrLeft).
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/CoordinatePower.lean: the coordinate-power isometriesA_(L^ι) ≃ (A_L)^ι, obtained as the constant-family case of the isometries here.
The dual carrier #
A family lies in the dual carrier of an orthogonal sum exactly when each of its values lies in the dual carrier of its summand.
The dual carrier of an orthogonal sum is the product of the dual carriers.
The dual carrier of an orthogonal sum is canonically the product of the dual carriers.
Instances For
The dual-carrier equivalence of an orthogonal sum reads off the coordinates.
The inverse dual-carrier equivalence of an orthogonal sum assembles the coordinates.
Under the dual-carrier equivalence, the embedded carrier of an orthogonal sum is the product of the embedded carriers.
The discriminant group #
The discriminant group of an orthogonal sum is canonically the product of the discriminant groups of its summands.
Instances For
The orthogonal-sum discriminant-group equivalence maps a representative to the family of classes of its coordinates.
The inverse orthogonal-sum discriminant-group equivalence sends a family of classes to the class of the assembled representative.
The discriminant quadratic module #
For even nondegenerate summands, the orthogonal-sum equivalence of discriminant groups is an
isometry from the half-norm discriminant quadratic module of ⊥ i, L i to the orthogonal sum of
the discriminant quadratic modules of the summands.
Instances For
The orthogonal-sum discriminant-quadratic isometry acts through the canonical equivalence of discriminant groups.
The inverse orthogonal-sum discriminant-quadratic isometry acts through the inverse of the canonical equivalence of discriminant groups.
Summandwise alphabets #
Summandwise isometries A_i ≅ A_(L i) from finite quadratic alphabets to the discriminant
modules of even nondegenerate lattices induce an isometry from the orthogonal sum Π i, A_i to
the discriminant module of the orthogonal sum ⊥ i, L i.
Instances For
The isometry induced by summandwise alphabet isometries applies them coordinatewise and then
identifies Π i, A_(L i) with A_(⊥ i, L i).
The class induced by summandwise alphabet isometries has as coordinate in the discriminant group of each summand the image of the corresponding letter.
Naturality #
The identification A_(⊥ i, L i) ≃ Π i, A_(L i) is natural for the two kinds of isometries of
orthogonal sums: coordinatewise isometries of the summands, and reindexing of the family by an
equivalence of index types. For glue words of a reducible root system these are a componentwise
isometry of the root lattices and a permutation of the components.
The discriminant class of an orthogonal sum of isometries has as coordinates the images of the coordinates of the original class.
Naturality of the summandwise alphabet isometry under coordinatewise isometries. Let
a i : A_i ≅ A_(L i) and b i : B_i ≅ A_(M i) be alphabet isometries, and g i : A_i → B_i
maps compatible with isometries f i : L i ≅ M i. Then the orthogonal sum of the f i
transports the class of an alphabet family x to the class of i ↦ g i (x i).
Reindexing an orthogonal sum by σ : κ ≃ ι moves the coordinate in position k of a
discriminant class to position σ k.
On discriminant groups the one-summand isometry extracts the unique component.
Naturality of the summandwise alphabet isometry under reindexing. Reindexing the
orthogonal sum by σ : κ ≃ ι transports the class of an alphabet family x over κ to the class
of the reindexed family Equiv.piCongrLeft A σ x over ι.