Documentation

TauCeti.LinearAlgebra.IntegralLattice.Overlattice.OrthogonalQuotient.Quadratic

The discriminant form of an even overlattice #

Let L be an even nondegenerate integral lattice and let L ≤ M ≤ Lᵛ be an even intermediate carrier, that is an even 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 evenness of M is exactly isotropy of H for the discriminant quadratic form. This file computes the discriminant quadratic module of M itself:

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

This is the last step of Nikulin's gluing recipe, and it is what identifies the discriminant form of a glued lattice without recomputing a dual lattice from scratch. 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 half-norm quadratic form because both sides are represented by B(x, x) / 2 modulo ℤ at the same ambient vector x.

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 quadratic-isotropic subgroup H ≤ A_L, which is the form in which the ADE glue calculations use it.

The comparison is natural. An isometry e : L ≅ L' transports the intermediate carrier M, and also restricts to an isometry of the overlattices themselves; the discriminant subgroups and their orthogonal complements correspond under the induced isometry of discriminant modules, and the square built from the two comparison isometries commutes.

The bilinear analogue, for a merely integral overlattice of a lattice that need not be even, is TauCeti.LinearAlgebra.IntegralLattice.Overlattice.OrthogonalQuotient.Bilinear; the discriminant class of a dual vector of M, which both comparisons are built from, is defined in TauCeti.LinearAlgebra.IntegralLattice.Overlattice.Dual.

Main declarations #

References #

The comparison isometry #

source
theorem TauCeti.IntegralLattice.IntermediateCarrier.quadratic_discriminantQuadraticModule_toIntegralLattice_mk {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsEven M) (y : ↥⋯.toIntegralLattice.dualCarrier) :
(⋯.toIntegralLattice.discriminantQuadraticModule ⋯).quadratic (Submodule.Quotient.mk y) = ↑((L.form ↑y) ↑y / 2)

The quadratic value in A_M of the class of a dual vector of M is the ambient half-norm.

source
noncomputable def TauCeti.IntegralLattice.IntermediateCarrier.discriminantOrthogonalQuotientIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hL : L.IsEven) (hM : IsEven M) :
(⋯.toIntegralLattice.discriminantQuadraticModule ⋯).Isometry ((L.discriminantQuadraticModule hL).orthogonalQuotient (L.discriminantSubgroup M) ⋯)

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

This is Nikulin's Proposition 1.4.1, in the half-norm ℚ/ℤ convention.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.IntegralLattice.IntermediateCarrier.discriminantOrthogonalQuotientIsometry_mk {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hL : L.IsEven) (hM : IsEven M) (y : ↥⋯.toIntegralLattice.dualCarrier) :
    (discriminantOrthogonalQuotientIsometry hL hM) (Submodule.Quotient.mk y) = ((L.discriminantQuadraticModule hL).orthogonalQuotientMk (L.discriminantSubgroup M) ⋯) ⟨⋯.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.

    source
    theorem TauCeti.IntegralLattice.IntermediateCarrier.quadratic_discriminantOrthogonalQuotientIsometry_mk {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hL : L.IsEven) (hM : IsEven M) (y : ↥⋯.toIntegralLattice.dualCarrier) :
    ((L.discriminantQuadraticModule hL).orthogonalQuotient (L.discriminantSubgroup M) ⋯).quadratic ((discriminantOrthogonalQuotientIsometry hL hM) (Submodule.Quotient.mk y)) = ↑((L.form ↑y) ↑y / 2)

    The quadratic value in H⊥ / H of the image of the class of a dual vector of M is the ambient half-norm.

    source
    theorem TauCeti.IntegralLattice.IntermediateCarrier.pairing_discriminantOrthogonalQuotientIsometry_mk {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hL : L.IsEven) (hM : IsEven M) (y z : ↥⋯.toIntegralLattice.dualCarrier) :
    (((L.discriminantQuadraticModule hL).orthogonalQuotient (L.discriminantSubgroup M) ⋯).pairing ((discriminantOrthogonalQuotientIsometry hL hM) (Submodule.Quotient.mk y))) ((discriminantOrthogonalQuotientIsometry hL 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 #

    source
    theorem TauCeti.IntegralLattice.IntermediateCarrier.natCard_orthogonalQuotient {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hL : L.IsEven) (hM : IsEven M) :
    Nat.card ((L.discriminantQuadraticModule hL).orthogonalQuotient (L.discriminantSubgroup M) ⋯).carrier = ⋯.toIntegralLattice.discriminant

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

    source
    theorem TauCeti.IntegralLattice.IntermediateCarrier.subsingleton_orthogonalQuotient_iff_isUnimodular {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hL : L.IsEven) (hM : IsEven M) :
    Subsingleton ((L.discriminantQuadraticModule hL).orthogonalQuotient (L.discriminantSubgroup M) ⋯).carrier ↔ ⋯.toIntegralLattice.IsUnimodular

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

    The comparison isometry read on subgroups #

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

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

    This is the form in which the ADE glue calculations use the comparison isometry.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.IntegralLattice.discriminantOrthogonalQuotientIsometryOfSubgroup_mk {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) {H : AddSubgroup L.DiscriminantGroup} (hH : (L.discriminantQuadraticModule hL).IsIsotropic H) :
      have hM := ⋯; ∀ (y : ↥⋯.toIntegralLattice.dualCarrier), (L.discriminantOrthogonalQuotientIsometryOfSubgroup hL hH) (Submodule.Quotient.mk y) = ((L.discriminantQuadraticModule hL).orthogonalQuotientMk H hH) ⟨⋯.dualClassHom y, ⋯⟩

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

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

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

      Naturality under a lattice isometry #

      source
      theorem TauCeti.IntegralLattice.Isometry.discriminantOrthogonalQuotientIsometry_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') (hL : L.IsEven) {P : ↑L.IntermediateCarrier} (hP : IntermediateCarrier.IsEven P) (q : ⋯.toIntegralLattice.DiscriminantGroup) :
      (IntermediateCarrier.discriminantOrthogonalQuotientIsometry ⋯ ⋯) (((e.toIntegralLatticeIsometry ⋯).discriminantQuadraticIsometry ⋯) q) = ((e.discriminantQuadraticIsometry hL).orthogonalQuotientEquiv ⋯ ⋯) ((IntermediateCarrier.discriminantOrthogonalQuotientIsometry hL 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.

      source
      theorem TauCeti.IntegralLattice.Isometry.discriminantOrthogonalQuotientIsometry_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') (hL : L.IsEven) {P : ↑L.IntermediateCarrier} (hP : IntermediateCarrier.IsEven P) :
      QuadraticMap.IsometryEquiv.trans ((e.toIntegralLatticeIsometry ⋯).discriminantQuadraticIsometry ⋯) (IntermediateCarrier.discriminantOrthogonalQuotientIsometry ⋯ ⋯) = QuadraticMap.IsometryEquiv.trans (IntermediateCarrier.discriminantOrthogonalQuotientIsometry hL hP) ((e.discriminantQuadraticIsometry hL).orthogonalQuotientEquiv ⋯ ⋯)

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