Documentation

TauCeti.LinearAlgebra.IntegralLattice.Overlattice.Dual

Duality for intermediate carriers of an integral lattice #

Let L be an integral lattice and let L ≤ M ≤ Lᵛ be an intermediate carrier. Its dual submodule Mᵛ = L.form.dualSubmodule M is again intermediate: it is contained in Lᵛ because L ≤ M, and it contains L because M ≤ Lᵛ and the form is symmetric. Passing to the dual is therefore order-reversing on the interval of intermediate carriers, and is an involution when the form is nondegenerate. This file identifies it under the correspondence with subgroups of the discriminant group A_L = Lᵛ / L:

Mᵛ / L = (M / L)⊥,   equivalently   (L_H)ᵛ = L_{H⊥}.

The proof is a calculation on representatives: a dual vector pairs integrally with every vector of M exactly when its discriminant class kills the class of every such vector.

Three consequences follow. Double duality (Mᵛ)ᵛ = M is the double orthogonal complement of a nondegenerate finite bilinear module. The orders of the two subgroups multiply to the order of A_L. Most importantly, an intermediate carrier is unimodular — it equals its own dual submodule — exactly when its subgroup of the discriminant group is Lagrangian. Combined with the correspondence between even overlattices and quadratic-isotropic subgroups, this is the last step of Nikulin's gluing recipe: gluing an even lattice along a Lagrangian isotropic subgroup produces an even unimodular overlattice.

The construction is natural: it commutes with transport along a lattice isometry, and it is computed componentwise on an orthogonal direct sum.

Main declarations #

References #

The dual of an intermediate carrier #

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

The dual submodule of an intermediate carrier L ≤ M ≤ Lᵛ, which is again an intermediate carrier.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.IntegralLattice.IntermediateCarrier.coe_dual {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) :
    ↑(dual M) = L.form.dualSubmodule ↑M

    The underlying submodule of the dual carrier is the dual submodule.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.IntermediateCarrier.dual_bot {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} :
    dual ⊥ = ⊤

    The dual of the smallest intermediate carrier, the carrier of L itself, is the largest one, the dual carrier.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.IntermediateCarrier.dual_top {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] :
    dual ⊤ = ⊥

    The dual of the largest intermediate carrier, the dual carrier, is the carrier of L.

    source
    theorem TauCeti.IntegralLattice.IntermediateCarrier.dual_le_dual {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M N : ↑L.IntermediateCarrier} (h : M ≤ N) :
    dual N ≤ dual M

    Passing to the dual carrier reverses inclusions.

    source
    theorem TauCeti.IntegralLattice.IntermediateCarrier.le_dual_comm {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {M N : ↑L.IntermediateCarrier} :
    M ≤ dual N ↔ N ≤ dual M

    Passing to the dual carrier is an adjunction: one carrier lies in the dual of a second exactly when the second lies in the dual of the first.

    source
    theorem TauCeti.IntegralLattice.IntermediateCarrier.isIntegral_iff_le_dual {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) :
    IsIntegral M ↔ M ≤ dual M

    Integrality is containment in the dual. An intermediate carrier is integral exactly when it is contained in its own dual carrier.

    The dual carrier and the orthogonal complement #

    source
    theorem TauCeti.IntegralLattice.IntermediateCarrier.mem_discriminantSubgroup_dual_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (M : ↑L.IntermediateCarrier) (a : L.DiscriminantGroup) :
    a ∈ L.discriminantSubgroup (dual M) ↔ ∀ b ∈ L.discriminantSubgroup M, (L.discriminantPairing a) b = 0

    A discriminant class belongs to the subgroup of the dual carrier exactly when it is orthogonal to the whole subgroup of the original carrier.

    source
    theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.toIntegralLattice_dualCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) :
    hM.toIntegralLattice.dualCarrier = ↑(dual M)

    The dual carrier of the lattice carried by an integral intermediate carrier is the dual intermediate carrier.

    source
    theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.dualCarrier_le {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) :
    hM.toIntegralLattice.dualCarrier ≤ L.dualCarrier

    Since L ≤ M, the dual carrier of M is contained in the dual carrier of L.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.IntermediateCarrier.discriminantSubgroup_dual {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] (M : ↑L.IntermediateCarrier) :
    L.discriminantSubgroup (dual M) = L.discriminantBilinearModule.orthogonalComplement (L.discriminantSubgroup M)

    The dual of an intermediate carrier is the orthogonal complement of its subgroup. Under the correspondence between intermediate carriers and subgroups of the discriminant group, taking the dual submodule corresponds to taking the orthogonal complement in the discriminant bilinear module.

    source
    noncomputable def TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.dualClassHom {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) :
    ↥hM.toIntegralLattice.dualCarrier →ₗ[ℤ] L.DiscriminantGroup

    The discriminant class in A_L of a vector of the dual carrier of an integral intermediate carrier.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.dualClassHom_apply {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) (y : ↥hM.toIntegralLattice.dualCarrier) :
      hM.dualClassHom y = Submodule.Quotient.mk ⟨↑y, ⋯⟩
      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.dualClassHom_mem_orthogonalComplement {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) (y : ↥hM.toIntegralLattice.dualCarrier) :
      hM.dualClassHom y ∈ L.discriminantBilinearModule.orthogonalComplement (L.discriminantSubgroup M)

      The discriminant class of a vector of Mᵛ is orthogonal to H = M / L, because the dual of an intermediate carrier corresponds to the orthogonal complement of its subgroup.

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

      Double duality for intermediate carriers.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.dual_injective {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] :
      Function.Injective dual

      Passing to the dual carrier is injective.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.IntermediateCarrier.dual_le_dual_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M N : ↑L.IntermediateCarrier} :
      dual M ≤ dual N ↔ N ≤ M

      Passing to the dual carrier reflects inclusions as well as reversing them.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.card_discriminantSubgroup_mul_card_discriminantSubgroup_dual {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] (M : ↑L.IntermediateCarrier) :
      Nat.card ↥(L.discriminantSubgroup M) * Nat.card ↥(L.discriminantSubgroup (dual M)) = Nat.card L.DiscriminantGroup

      The orders of the subgroups attached to an intermediate carrier and to its dual multiply to the order of the discriminant group.

      Unimodular intermediate carriers and Lagrangian subgroups #

      source
      @[simp]
      theorem TauCeti.IntegralLattice.IntermediateCarrier.dual_eq_self_iff_isLagrangian {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] (M : ↑L.IntermediateCarrier) :
      dual M = M ↔ L.discriminantBilinearModule.IsLagrangian (L.discriminantSubgroup M)

      An intermediate carrier is unimodular exactly when its subgroup is Lagrangian. Here unimodularity is the equality Mᵛ = M of an intermediate carrier with its own dual submodule, matching TauCeti.IntegralLattice.IsUnimodular for the lattice which M carries.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.isUnimodular_toIntegralLattice_iff_dual_eq_self {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] {M : ↑L.IntermediateCarrier} (hM : IsIntegral M) :
      hM.toIntegralLattice.IsUnimodular ↔ dual M = M

      The lattice carried by an integral intermediate carrier is unimodular exactly when the carrier is its own dual.

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

      An integral overlattice is unimodular exactly when its discriminant subgroup is Lagrangian. For an integral intermediate carrier L ≤ M ≤ Lᵛ, the lattice M is unimodular exactly when M / L equals its orthogonal complement in the discriminant group of L.

      The correspondence read on subgroups #

      source
      @[simp]
      theorem TauCeti.IntegralLattice.dual_intermediateCarrierOfDiscriminantSubgroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (H : AddSubgroup L.DiscriminantGroup) :
      IntermediateCarrier.dual (L.intermediateCarrierOfDiscriminantSubgroup H) = L.intermediateCarrierOfDiscriminantSubgroup (L.discriminantBilinearModule.orthogonalComplement H)

      The dual of a glued overlattice is the overlattice glued along the orthogonal complement: (L_H)ᵛ = L_{H⊥}.

      source
      theorem TauCeti.IntegralLattice.dual_intermediateCarrierOfDiscriminantSubgroup_eq_self_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (H : AddSubgroup L.DiscriminantGroup) :
      IntermediateCarrier.dual (L.intermediateCarrierOfDiscriminantSubgroup H) = L.intermediateCarrierOfDiscriminantSubgroup H ↔ L.discriminantBilinearModule.IsLagrangian H

      The overlattice glued along H is unimodular exactly when H is Lagrangian. For an even lattice L and a quadratic-isotropic subgroup H, the glued overlattice L_H is even by TauCeti.IntegralLattice.isEven_intermediateCarrierOfDiscriminantSubgroup_iff, so this is the criterion for L_H to be an even unimodular overlattice of L.

      source
      theorem TauCeti.IntegralLattice.isUnimodular_ofIsotropicSubgroup_iff_isLagrangian {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) :
      (L.ofIsotropicSubgroup hL H hH).IsUnimodular ↔ L.discriminantBilinearModule.IsLagrangian H

      The glued overlattice is unimodular exactly when the glue is Lagrangian. For an even lattice L and a quadratic-isotropic subgroup H of its discriminant group, the even overlattice L_H is unimodular exactly when H = H⊥ for the discriminant pairing.

      Naturality #

      source
      @[simp]
      theorem TauCeti.IntegralLattice.Isometry.intermediateCarrierEquiv_dual {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (P : ↑L.IntermediateCarrier) :
      e.intermediateCarrierEquiv (IntermediateCarrier.dual P) = IntermediateCarrier.dual (e.intermediateCarrierEquiv P)

      Transport along an isometry commutes with duality of intermediate carriers.

      Orthogonal direct sums #

      source
      @[simp]
      theorem TauCeti.IntegralLattice.dual_orthogonalSumIntermediateCarrier {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (P : ↑L.IntermediateCarrier) (Q : ↑M.IntermediateCarrier) :
      IntermediateCarrier.dual (L.orthogonalSumIntermediateCarrier M P Q) = L.orthogonalSumIntermediateCarrier M (IntermediateCarrier.dual P) (IntermediateCarrier.dual Q)

      Duality of intermediate carriers is componentwise on an orthogonal direct sum.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.IntermediateCarrier.mem_dualCarrier_orthogonalSum_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} [L.IsNondegenerate] [M.IsNondegenerate] {P : ↑L.IntermediateCarrier} {Q : ↑M.IntermediateCarrier} (hP : IsIntegral P) (hQ : IsIntegral Q) (x : V × W) :
      x ∈ ⋯.toIntegralLattice.dualCarrier ↔ x.1 ∈ hP.toIntegralLattice.dualCarrier ∧ x.2 ∈ hQ.toIntegralLattice.dualCarrier

      Dual vectors of an assembled overlattice are componentwise.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.fst_mem_dualCarrier_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} [L.IsNondegenerate] [M.IsNondegenerate] {P : ↑L.IntermediateCarrier} {Q : ↑M.IntermediateCarrier} (hP : IsIntegral P) (hQ : IsIntegral Q) (y : ↥⋯.toIntegralLattice.dualCarrier) :
      (↑y).1 ∈ hP.toIntegralLattice.dualCarrier

      The first component of a dual vector of the assembled overlattice is a dual vector of the first overlattice.

      source
      theorem TauCeti.IntegralLattice.IntermediateCarrier.snd_mem_dualCarrier_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} [L.IsNondegenerate] [M.IsNondegenerate] {P : ↑L.IntermediateCarrier} {Q : ↑M.IntermediateCarrier} (hP : IsIntegral P) (hQ : IsIntegral Q) (y : ↥⋯.toIntegralLattice.dualCarrier) :
      (↑y).2 ∈ hQ.toIntegralLattice.dualCarrier

      The second component of a dual vector of the assembled overlattice is a dual vector of the second overlattice.