Documentation

TauCeti.LinearAlgebra.IntegralLattice.Overlattice.Index

The index and the discriminant of an overlattice #

Let L be an integral lattice and let L ≤ M ≤ Lᵛ be an intermediate carrier. This file computes the two numerical invariants of the gluing correspondence:

[M : L] = #(M / L) = |M / L ≤ A_L|,      disc(M) · [M : L]² = disc(L)  (for `M` integral).

The first equality is the index in the group-theoretic sense and holds for every intermediate carrier. The second needs M to be integral, so that M is itself an integral lattice and has a discriminant of its own; it says that enlarging a lattice by a subgroup of its discriminant group divides the discriminant by the square of the order of that subgroup. By the correspondence of TauCeti.LinearAlgebra.IntegralLattice.Overlattice.Isotropic, integrality of the carrier glued along a subgroup H of A_L is the vanishing of the discriminant pairing on H, that is the isotropy of H when L is nondegenerate. So this is the numerical half of Nikulin's gluing theory: an even lattice glued along an isotropic subgroup H has discriminant disc(L) / |H|², and is unimodular exactly when |H|² = disc(L).

The scaling law itself is not proved here: it is the general statement TauCeti.IntegralLattice.discriminant_eq_mul_relIndex_sq about an arbitrary pair of nested integral lattices sharing their ambient rational form, from TauCeti.LinearAlgebra.IntegralLattice.Index. What this file supplies is the identification of the index of an intermediate carrier with the order of the subgroup it cuts out in A_L.

The earlier overlattice theory packages a full integral intermediate carrier as an integral lattice in its own right through IntermediateCarrier.IsIntegral.toIntegralLattice, which keeps the ambient form and therefore preserves nondegeneracy; evenness of the carrier makes it an even lattice.

Main definitions #

Main results #

References #

The index of an intermediate carrier #

source
noncomputable def TauCeti.IntegralLattice.IntermediateCarrier.relIndex {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M N : ↑L.IntermediateCarrier) :
ℕ

The relative index of two intermediate carriers M N: the index of M ⊓ N in N, that is the order of the quotient group N / (M ⊓ N). When M ≤ N this is the index [N : M], the order of N / M.

Equations
Instances For
    source
    noncomputable def TauCeti.IntegralLattice.IntermediateCarrier.index {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) :
    ℕ

    The index [M : L] of the lattice in an intermediate carrier, that is the order of the quotient group M / L.

    Equations
    Instances For
      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.relIndex_def {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M N : ↑L.IntermediateCarrier) :
      relIndex M N = (↑M).toAddSubgroup.relIndex (↑N).toAddSubgroup

      The relative index of intermediate carriers is their relative index as additive subgroups.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.index_def {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) :
      index M = L.carrier.toAddSubgroup.relIndex (↑M).toAddSubgroup

      The index of an intermediate carrier is its carrier's relative index over the original lattice.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.IntermediateCarrier.relIndex_bot_left {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) :
      relIndex ⊥ M = index M

      Relative index from the lattice itself is the index of an intermediate carrier.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.relIndex_eq_natCard_quotient {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M N : ↑L.IntermediateCarrier) :
      relIndex M N = Nat.card (↥↑N ⧸ (↑M).submoduleOf ↑N)

      The relative index of two intermediate carriers M N is the order of the quotient N / (M ⊓ N); when M ≤ N this is the order of N / M.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.index_eq_natCard_quotient {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) :
      index M = Nat.card (↥↑M ⧸ L.carrier.submoduleOf ↑M)

      The index of an intermediate carrier is the order of the quotient module M / L.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.IntermediateCarrier.relIndex_self {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) :
      relIndex M M = 1

      The relative index of an intermediate carrier in itself is one.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.relIndex_mul_relIndex {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M N P : ↑L.IntermediateCarrier} (hMN : M ≤ N) (hNP : N ≤ P) :
      relIndex M N * relIndex N P = relIndex M P

      The index is multiplicative in towers of intermediate carriers.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.index_mul_relIndex {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M N : ↑L.IntermediateCarrier} (h : M ≤ N) :
      index M * relIndex M N = index N

      The index of the smaller member of a chain times the relative index is the larger index.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.IntermediateCarrier.index_bot {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} :
      index ⊥ = 1

      The lattice itself has index one.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.IntermediateCarrier.relIndex_intermediateCarrierOfDiscriminantSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (H K : AddSubgroup L.DiscriminantGroup) :
      relIndex (L.intermediateCarrierOfDiscriminantSubgroup H) (L.intermediateCarrierOfDiscriminantSubgroup K) = H.relIndex K

      The relative index of two glued intermediate carriers is the relative index of the two subgroups of the discriminant group. Both sides are read off the same quotient of the dual carrier, so no finiteness and no containment of H in K is needed.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.relIndex_eq_relIndex_discriminantSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M N : ↑L.IntermediateCarrier) :
      relIndex M N = (L.discriminantSubgroup M).relIndex (L.discriminantSubgroup N)

      The relative index of two intermediate carriers is the relative index of their corresponding subgroups of the discriminant group.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.index_eq_natCard_discriminantSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) :
      index M = Nat.card ↥(L.discriminantSubgroup M)

      The index of an intermediate carrier is the order of the subgroup it cuts out in the discriminant group.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.IntermediateCarrier.index_intermediateCarrierOfDiscriminantSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (H : AddSubgroup L.DiscriminantGroup) :
      index (L.intermediateCarrierOfDiscriminantSubgroup H) = Nat.card ↥H

      The index of the overlattice attached to a subgroup of the discriminant group is the order of that subgroup.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.IntermediateCarrier.index_eq_one_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) :
      index M = 1 ↔ M = ⊥

      An intermediate carrier has index one exactly when it is the lattice itself.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.IntermediateCarrier.index_top {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] :
      index ⊤ = L.discriminant

      The index of the dual carrier is the discriminant of the lattice.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.index_pos {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) [Submodule.IsLattice ℚ ↑M] :
      0 < index M

      The index of a full intermediate carrier is positive.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.determinant_mul_index_sq {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} [Submodule.IsLattice ℚ ↑M] (hM : IsIntegral M) :
      hM.toIntegralLattice.determinant * ↑(index M) ^ 2 = L.determinant

      The signed determinant of an integral overlattice scales by the square of the index.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.discriminant_mul_index_sq {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} [Submodule.IsLattice ℚ ↑M] (hM : IsIntegral M) :
      hM.toIntegralLattice.discriminant * index M ^ 2 = L.discriminant

      The discriminant of an integral overlattice scales by the square of the index: disc(M) · [M : L]² = disc(L).

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.index_sq_dvd_discriminant {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} [Submodule.IsLattice ℚ ↑M] (hM : IsIntegral M) :
      index M ^ 2 ∣ L.discriminant

      The square of the index of an integral overlattice divides the discriminant.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.discriminant_eq_discriminant_div_index_sq {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} [Submodule.IsLattice ℚ ↑M] (hM : IsIntegral M) :
      hM.toIntegralLattice.discriminant = L.discriminant / index M ^ 2

      The discriminant of an integral overlattice is the exact quotient disc(L) / [M : L]².

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.isUnimodular_iff_index_sq_eq_discriminant {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M : ↑L.IntermediateCarrier} [Submodule.IsLattice ℚ ↑M] (hM : IsIntegral M) :
      hM.toIntegralLattice.IsUnimodular ↔ index M ^ 2 = L.discriminant

      An integral overlattice is unimodular exactly when the square of its index exhausts the discriminant of the lattice.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.discriminant_mul_natCard_sq {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {H : AddSubgroup L.DiscriminantGroup} [Submodule.IsLattice ℚ ↑(L.intermediateCarrierOfDiscriminantSubgroup H)] (hH : IsIntegral (L.intermediateCarrierOfDiscriminantSubgroup H)) :
      hH.toIntegralLattice.discriminant * Nat.card ↥H ^ 2 = L.discriminant

      The discriminant of the integral overlattice glued along a subgroup of the discriminant group: disc(L_H) · |H|² = disc(L).

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.isUnimodular_iff_natCard_sq_eq_discriminant {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {H : AddSubgroup L.DiscriminantGroup} [Submodule.IsLattice ℚ ↑(L.intermediateCarrierOfDiscriminantSubgroup H)] (hH : IsIntegral (L.intermediateCarrierOfDiscriminantSubgroup H)) :
      hH.toIntegralLattice.IsUnimodular ↔ Nat.card ↥H ^ 2 = L.discriminant

      The overlattice glued along a subgroup of the discriminant group is unimodular exactly when the square of the order of that subgroup is the discriminant.