Documentation

TauCeti.LinearAlgebra.IntegralLattice.TwoElementary

Even two-elementary lattices #

An even nondegenerate integral lattice L is 2-elementary when its discriminant group A_L = Lᵛ/L is (ℤ/2)^a. Nikulin attaches to it the invariants (δ; t₊, t₋, a), where (t₊, t₋) is the signature and δ = 0 exactly when the half-norm discriminant form q_L takes values in ½ℤ/ℤ. His Theorem 3.6.2 says that an even 2-elementary lattice with invariants (δ; t₊, t₋, a) exists exactly when seven arithmetic conditions hold:

  1. a ≤ t₊ + t₋;
  2. t₊ + t₋ + a ≡ 0 (mod 2);
  3. t₊ − t₋ ≡ 0 (mod 4) when δ = 0;
  4. δ = 0 and t₊ − t₋ ≡ 0 (mod 8) when a = 0;
  5. t₊ − t₋ ≡ ±1 (mod 8) when a = 1;
  6. δ = 0 when a = 2 and t₊ − t₋ ≡ 4 (mod 8);
  7. t₊ − t₋ ≡ 0 (mod 8) when δ = 0 and a = t₊ + t₋.

This file records the conditions as the structure TwoElementaryAdmissible, with one field per clause, and proves that they are necessary. Conditions 2 to 6 follow from Milgram's theorem sign q_L ≡ t₊ − t₋ (mod 8) together with the decomposition of a nondegenerate 2-elementary finite quadratic module into the generators q_θ^{(2)}(2), u^{(2)}(2) and v^{(2)}(2). Conditions 1 and 7 come from the lattice: since 2Lᵛ ⊆ L, the order 2^a of A_L divides the index 2^{t₊ + t₋} of 2Lᵛ in Lᵛ, and if they are equal then L = 2Lᵛ, so that Lᵛ with the doubled form is an integral unimodular lattice of the same signature, even when δ = 0.

The boundary clauses 4 to 7 cannot be dropped: the tuples (0; 4, 0, 0), (1; 3, 0, 1), (1; 4, 0, 2) and (0; 4, 0, 4) satisfy every condition before clause 4, 5, 6 and 7 respectively, and TauCeti.IntegralLattice.not_twoElementaryAdmissible_boundary_witnesses records that none of them is admissible.

Main definitions #

Main results #

References #

Nikulin's conditions #

source
structure TauCeti.IntegralLattice.TwoElementaryAdmissible (δ : ZMod 2) (tp tm a : ℕ) :
Prop

Nikulin's seven conditions on the invariants (δ; t₊, t₋, a) of an even 2-elementary lattice. Conditions 4 to 7 are boundary clauses at a = 0, a = 1, a = 2 and a = t₊ + t₋.

  • le_rank : a ≤ tp + tm

    (1) a ≤ t₊ + t₋.

  • parity : ↑(tp + tm + a) = 0

    (2) t₊ + t₋ + a ≡ 0 (mod 2).

  • four_of_delta_zero : δ = 0 → ↑(↑tp - ↑tm) = 0

    (3) t₊ − t₋ ≡ 0 (mod 4) when δ = 0.

  • unimodular_of_a_zero : a = 0 → δ = 0 ∧ ↑(↑tp - ↑tm) = 0

    (4) δ = 0 and t₊ − t₋ ≡ 0 (mod 8) when a = 0.

  • pm_one_of_a_one : a = 1 → ↑(↑tp - ↑tm) = 1 ∨ ↑(↑tp - ↑tm) = -1

    (5) t₊ − t₋ ≡ ±1 (mod 8) when a = 1.

  • delta_zero_of_a_two : a = 2 → ↑(↑tp - ↑tm) = 4 → δ = 0

    (6) δ = 0 when a = 2 and t₊ − t₋ ≡ 4 (mod 8).

  • eight_of_a_eq_rank : δ = 0 → a = tp + tm → ↑(↑tp - ↑tm) = 0

    (7) t₊ − t₋ ≡ 0 (mod 8) when δ = 0 and a = t₊ + t₋.

Instances For
    source
    theorem TauCeti.IntegralLattice.not_twoElementaryAdmissible_boundary_witnesses :
    ¬TwoElementaryAdmissible 0 4 0 0 ∧ ¬TwoElementaryAdmissible 1 3 0 1 ∧ ¬TwoElementaryAdmissible 1 4 0 2 ∧ ¬TwoElementaryAdmissible 0 4 0 4

    The four boundary witnesses are not admissible: (0; 4, 0, 0), (1; 3, 0, 1), (1; 4, 0, 2) and (0; 4, 0, 4) fail conditions 4, 5, 6 and 7 respectively.

    Even lattices of level dividing two #

    source
    theorem TauCeti.IntegralLattice.four_dvd_sigPos_sub_sigNeg_of_level_dvd_two {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (h2 : L.level ∣ 2) :
    4 ∣ ↑L.sigPos - ↑L.sigNeg

    An even lattice of level dividing 2 has signature divisible by 4. The level divides 2 exactly when q_L takes values in ½ℤ/ℤ, so the Gauss-sum invariant of q_L is 0 or 4, and by Milgram's theorem it is t₊ − t₋ modulo 8.

    source
    theorem TauCeti.IntegralLattice.four_dvd_finrank_of_level_dvd_two {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : L.IsEven) (h2 : L.level ∣ 2) (hP : L.IsPosDef) :
    4 ∣ Module.finrank ℚ V

    The rank of a positive definite even lattice of level dividing 2 is divisible by 4.

    Necessity of Nikulin's conditions #

    source
    theorem TauCeti.IntegralLattice.twoElementaryAdmissible_sigPos_sigNeg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) {a : ℕ} (e : L.DiscriminantGroup ≃+ (Fin a → ZMod 2)) {δ : ZMod 2} (hδ : δ = 0 ↔ ∀ (x : L.DiscriminantGroup), (L.discriminantQuadraticMap hL) x + (L.discriminantQuadraticMap hL) x = 0) :
    TwoElementaryAdmissible δ L.sigPos L.sigNeg a

    The invariants of an even 2-elementary lattice satisfy Nikulin's conditions. If the discriminant group of an even nondegenerate lattice L is (ℤ/2)^a, and δ = 0 exactly when q_L takes values in ½ℤ/ℤ, then (δ; t₊, t₋, a) satisfies TwoElementaryAdmissible.

    source
    def TauCeti.IntegralLattice.TwoElementaryLatticeWithInvariants (δ : ZMod 2) (tp tm a : ℕ) :
    Prop

    An even 2-elementary lattice with invariants (δ; t₊, t₋, a) exists. It is a nondegenerate even lattice in ℚ^{t₊ + t₋} of signature (t₊, 0, t₋) whose discriminant group is (ℤ/2)^a, and δ = 0 exactly when its half-norm discriminant form takes values in ½ℤ/ℤ.

    Instances For
      source
      theorem TauCeti.IntegralLattice.twoElementaryLatticeWithInvariants_iff {δ : ZMod 2} {tp tm a : ℕ} :
      TwoElementaryLatticeWithInvariants δ tp tm a ↔ ∃ (L : IntegralLattice (Fin (tp + tm) → ℚ)) (_ : L.IsNondegenerate) (hev : L.IsEven), L.signature = (tp, 0, tm) ∧ Nonempty (L.DiscriminantGroup ≃+ (Fin a → ZMod 2)) ∧ (δ = 0 ↔ ∀ (x : L.DiscriminantGroup), (L.discriminantQuadraticMap hev) x + (L.discriminantQuadraticMap hev) x = 0)

      The defining characterization of TwoElementaryLatticeWithInvariants: introduce and eliminate the existence predicate through its lattice witness.

      source
      theorem TauCeti.IntegralLattice.TwoElementaryLatticeWithInvariants.twoElementaryAdmissible {δ : ZMod 2} {tp tm a : ℕ} (h : TwoElementaryLatticeWithInvariants δ tp tm a) :
      TwoElementaryAdmissible δ tp tm a

      The necessity half of Nikulin's Theorem 3.6.2: the invariants of an even 2-elementary lattice satisfy his seven conditions.