Documentation

TauCeti.NumberTheory.IntegralLattice.Localization.Ideals

Scale and norm ideals of a localized lattice #

The scale and norm ideals of the integral form on ℤ_p ⊗[ℤ] L are the extensions to ℤ_p of the corresponding ideals of L. In particular, their generators can be read directly from an integral Gram matrix. At an odd prime the ideals coincide, because 2 is a unit; at the dyadic prime their difference distinguishes the parity types of unimodular Jordan blocks. In particular a lattice is even exactly when its dyadic localization is (TauCeti.IntegralLattice.isEven_iff_forall_two_dvd_localIntegralForm_apply_self).

These are ideals of the integral localization, not of the completed rational space.

References #

source
@[reducible, inline]
noncomputable abbrev TauCeti.IntegralLattice.localScaleIdeal {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] :
Ideal ℤ_[p]

The ideal generated by pairings on the integral localization of L.

Instances For
    source
    @[reducible, inline]
    noncomputable abbrev TauCeti.IntegralLattice.localNormIdeal {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] :
    Ideal ℤ_[p]

    The ideal generated by self-pairings on the integral localization of L.

    Instances For
      source
      @[simp]
      theorem TauCeti.IntegralLattice.localScaleIdeal_eq_map {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] :
      L.localScaleIdeal p = Ideal.map (algebraMap ℤ ℤ_[p]) L.scaleIdeal

      Localization extends the integral scale ideal.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.localNormIdeal_eq_map {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [Fact (Nat.Prime p)] :
      L.localNormIdeal p = Ideal.map (algebraMap ℤ ℤ_[p]) L.normIdeal

      Localization extends the integral norm ideal.

      source
      theorem TauCeti.IntegralLattice.localNormIdeal_eq_localScaleIdeal {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) :
      L.localNormIdeal p = L.localScaleIdeal p

      At odd primes the local norm and scale ideals coincide.

      source
      theorem TauCeti.IntegralLattice.isEven_iff_localNormIdeal_le_span_two {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
      L.IsEven ↔ L.localNormIdeal 2 ≤ Ideal.span {2}

      Evenness is detected by the norm ideal at the dyadic localization.

      source
      theorem TauCeti.IntegralLattice.isEven_iff_forall_two_dvd_localIntegralForm_apply_self {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
      L.IsEven ↔ ∀ (x : L.LocalCarrier 2), 2 ∣ ((L.localIntegralForm 2) x) x

      Evenness is detected by the dyadic localization. A lattice is even exactly when every value B(x, x) of its localized integral form at 2 is divisible by 2 in ℤ_[2].

      source
      theorem TauCeti.IntegralLattice.IsEven.two_dvd_localIntegralForm_apply_self {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [Fact (Nat.Prime p)] (heven : L.IsEven) (x : L.LocalCarrier p) :
      2 ∣ ((L.localIntegralForm p) x) x

      The localizations of an even lattice are even. Every value B(x, x) of the localized integral form of an even lattice at a prime p is divisible by 2 in ℤ_[p].