The discriminant bilinear form of an integral overlattice

Let L be a nondegenerate integral lattice, not assumed even, and let L ≤ M ≤ Lᵛ be an integral intermediate carrier, that is an integral overlattice of L inside the common rational ambient space. The correspondence of TauCeti.LinearAlgebra.IntegralLattice.Overlattice.Isotropic attaches to M the subgroup H = M / L of the discriminant group A_L = Lᵛ / L, and integrality of M is exactly isotropy of H for the discriminant bilinear form. This file computes the discriminant bilinear module of M itself:

A_M ≅ H⊥ / H,   H = M / L ≤ A_L.

The proof is the composite

Mᵛ ↪ Lᵛ ↠ A_L,

which lands in H⊥ because the dual of an intermediate carrier corresponds to the orthogonal complement of its subgroup, is surjective onto H⊥ for the same reason, and whose fibre over H is exactly M. The composite therefore descends to an additive bijection A_M ≃ H⊥ / H, and it preserves the pairing because both sides are represented by B(x, y) modulo ℤ at the same pair of ambient vectors.

Two consequences are recorded. The order of H⊥ / H is the discriminant of M, and M is unimodular exactly when H⊥ / H is trivial — the quotient-side reading of the Lagrangian criterion of TauCeti.LinearAlgebra.IntegralLattice.Overlattice.Dual. The isometry is also restated for the overlattice L_H glued along a bilinear-isotropic subgroup H ≤ A_L, and it is natural: an isometry e : L ≅ L' transports everything in sight and the resulting square commutes.

This is the elementary intermediate-lattice analogue of the even-overlattice comparison of TauCeti.LinearAlgebra.IntegralLattice.Overlattice.OrthogonalQuotient.Quadratic, and must not be read as a statement about the quadratic discriminant form, which an odd lattice does not carry. The two comparisons descend the same map, the discriminant class IsIntegral.dualClassHom of a dual vector of M, along the bilinear and the quadratic orthogonal quotient of A_L respectively.

Main declarations

• TauCeti.IntegralLattice.IntermediateCarrier.discriminantBilinearOrthogonalQuotientIsometry: the isometry A_M ≅ H⊥ / H of finite bilinear modules.
• TauCeti.IntegralLattice.IntermediateCarrier.discriminantBilinearOrthogonalQuotientIsometry_mk: its value on the class of a vector of Mᵛ.
• TauCeti.IntegralLattice.IntermediateCarrier.natCard_discriminantBilinearOrthogonalQuotient and subsingleton_discriminantBilinearOrthogonalQuotient_iff_isUnimodular: the order of H⊥ / H is the discriminant of M, and M is unimodular exactly when H⊥ / H is trivial.
• TauCeti.IntegralLattice.discriminantBilinearOrthogonalQuotientIsometryOfSubgroup: the same isometry read as A_(L_H) ≅ H⊥ / H for a bilinear-isotropic subgroup H of A_L.
• TauCeti.IntegralLattice.Isometry.discriminantBilinearOrthogonalQuotientIsometry_naturality: the comparison isometry is natural under a lattice isometry.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.4, Proposition 1.4.1, which is the even refinement of the comparison proved here.
• W. Ebeling, Lattices and Codes, Chapter 1.

The comparison isometry

theorem TauCeti.IntegralLattice.IntermediateCarrier.pairing_discriminantBilinearModule_toIntegralLattice_mk {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) (y z : ↥hM.toIntegralLattice.dualCarrier) : (hM.toIntegralLattice.discriminantBilinearModule.pairing (Submodule.Quotient.mk y)) (Submodule.Quotient.mk z) = ↑((L.form ↑y) ↑z)

The pairing in A_M of the classes of two dual vectors of M is the ambient form modulo ℤ.

noncomputable def TauCeti.IntegralLattice.IntermediateCarrier.discriminantBilinearOrthogonalQuotientIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) : hM.toIntegralLattice.discriminantBilinearModule.Isometry (L.discriminantBilinearModule.orthogonalQuotient (L.discriminantSubgroup M))

The discriminant bilinear form of an integral overlattice. For an integral overlattice L ≤ M ≤ Lᵛ with subgroup H = M / L of the discriminant group of L, the discriminant bilinear module of M is H⊥ / H.

Neither L nor M is assumed even; this is the elementary bilinear analogue of Nikulin's Proposition 1.4.1.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.IntegralLattice.IntermediateCarrier.discriminantBilinearOrthogonalQuotientIsometry_mk {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) (y : ↥hM.toIntegralLattice.dualCarrier) : (discriminantBilinearOrthogonalQuotientIsometry hM) (Submodule.Quotient.mk y) = (L.discriminantBilinearModule.orthogonalQuotientMk (L.discriminantSubgroup M)) ⟨hM.dualClassHom y, ⋯⟩

The representative formula. The comparison isometry sends the class in A_M of a dual vector of M to the class in H⊥ / H of its discriminant class in A_L.

theorem TauCeti.IntegralLattice.IntermediateCarrier.pairing_discriminantBilinearOrthogonalQuotientIsometry_mk {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) (y z : ↥hM.toIntegralLattice.dualCarrier) : ((L.discriminantBilinearModule.orthogonalQuotient (L.discriminantSubgroup M)).pairing ((discriminantBilinearOrthogonalQuotientIsometry hM) (Submodule.Quotient.mk y))) ((discriminantBilinearOrthogonalQuotientIsometry hM) (Submodule.Quotient.mk z)) = ↑((L.form ↑y) ↑z)

The pairing in H⊥ / H of the images of the classes of two dual vectors of M is the ambient form modulo ℤ.

Numerical consequences

theorem TauCeti.IntegralLattice.IntermediateCarrier.natCard_discriminantBilinearOrthogonalQuotient {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) : Nat.card (L.discriminantBilinearModule.orthogonalQuotient (L.discriminantSubgroup M)).carrier = hM.toIntegralLattice.discriminant

The order of H⊥ / H is the discriminant of the overlattice.

theorem TauCeti.IntegralLattice.IntermediateCarrier.subsingleton_discriminantBilinearOrthogonalQuotient_iff_isUnimodular {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) : Subsingleton (L.discriminantBilinearModule.orthogonalQuotient (L.discriminantSubgroup M)).carrier ↔ hM.toIntegralLattice.IsUnimodular

An integral overlattice is unimodular exactly when H⊥ / H is trivial.

The comparison isometry read on subgroups

noncomputable def TauCeti.IntegralLattice.discriminantBilinearOrthogonalQuotientIsometryOfSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {H : AddSubgroup L.DiscriminantGroup} (hH : L.discriminantBilinearModule.IsIsotropic H) : have hM := ⋯; hM.toIntegralLattice.discriminantBilinearModule.Isometry (L.discriminantBilinearModule.orthogonalQuotient H)

The discriminant bilinear form of a glued integral overlattice: A_(L_H) ≅ H⊥ / H for a bilinear-isotropic subgroup H of the discriminant group of a nondegenerate integral lattice.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.IntegralLattice.discriminantBilinearOrthogonalQuotientIsometryOfSubgroup_mk {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {H : AddSubgroup L.DiscriminantGroup} (hH : L.discriminantBilinearModule.IsIsotropic H) : have hM := ⋯; ∀ (y : ↥hM.toIntegralLattice.dualCarrier), (L.discriminantBilinearOrthogonalQuotientIsometryOfSubgroup hH) (Submodule.Quotient.mk y) = (L.discriminantBilinearModule.orthogonalQuotientMk H) ⟨hM.dualClassHom y, ⋯⟩

The subgroup-level comparison isometry sends a representative to its discriminant class in H⊥ / H.

theorem TauCeti.IntegralLattice.natCard_discriminantBilinearOrthogonalQuotient_of_subgroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {H : AddSubgroup L.DiscriminantGroup} (hH : L.discriminantBilinearModule.IsIsotropic H) : have hM := ⋯; Nat.card (L.discriminantBilinearModule.orthogonalQuotient H).carrier = hM.toIntegralLattice.discriminant

The order of H⊥ / H is the discriminant of the overlattice glued along H.

Naturality under a lattice isometry

theorem TauCeti.IntegralLattice.Isometry.discriminantBilinearOrthogonalQuotientIsometry_naturality_apply {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {W : Type u_1} [AddCommGroup W] [Module ℚ W] {L' : IntegralLattice W} [L'.IsNondegenerate] (e : L.Isometry L') {P : ↑L.IntermediateCarrier} (hP : IntermediateCarrier.IsIntegral P) (q : hP.toIntegralLattice.DiscriminantGroup) : (IntermediateCarrier.discriminantBilinearOrthogonalQuotientIsometry ⋯) ((e.toIntegralLatticeIsometry hP).discriminantBilinearIsometry q) = (e.discriminantBilinearIsometry.orthogonalQuotientEquiv ⋯) ((IntermediateCarrier.discriminantBilinearOrthogonalQuotientIsometry hP) q)

Naturality of the comparison isometry A_M ≅ H⊥ / H, on a discriminant class. The equation identifies comparison after transport on A_M with transport after comparison.

theorem TauCeti.IntegralLattice.Isometry.discriminantBilinearOrthogonalQuotientIsometry_naturality {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {W : Type u_1} [AddCommGroup W] [Module ℚ W] {L' : IntegralLattice W} [L'.IsNondegenerate] (e : L.Isometry L') {P : ↑L.IntermediateCarrier} (hP : IntermediateCarrier.IsIntegral P) : (e.toIntegralLatticeIsometry hP).discriminantBilinearIsometry.trans (IntermediateCarrier.discriminantBilinearOrthogonalQuotientIsometry ⋯) = (IntermediateCarrier.discriminantBilinearOrthogonalQuotientIsometry hP).trans (e.discriminantBilinearIsometry.orthogonalQuotientEquiv ⋯)

Naturality of the comparison isometry A_M ≅ H⊥ / H. An isometry e : L ≅ L' of nondegenerate integral lattices transports an integral intermediate carrier P of L to one of L', and the square built from the two comparison isometries, the induced isometry of the discriminant bilinear modules of the two overlattices, and the transported orthogonal quotient commutes.