Documentation

TauCeti.LinearAlgebra.IntegralLattice.Ideals

Scale and norm ideals of an integral lattice #

The scale ideal is generated by all integral pairings, and the norm ideal by all self-pairings. Polarization gives 2 𝔰(L) ≤ 𝔫(L) ≤ 𝔰(L). In particular, evenness says exactly that the norm ideal is contained in 2ℤ.

The ideal constructions and their algebraic properties are stated for bilinear forms over commutative rings, then specialized to integral lattices.

These ideals are the integral invariants used to distinguish the parity types of local Jordan constituents.

References #

source
@[reducible, inline]
noncomputable abbrev TauCeti.IntegralLattice.scaleIdeal {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
Ideal ℤ

The scale ideal of the integral form of a lattice.

Instances For
    source
    @[reducible, inline]
    noncomputable abbrev TauCeti.IntegralLattice.normIdeal {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    Ideal ℤ

    The norm ideal of the integral form of a lattice.

    Instances For
      source
      theorem TauCeti.IntegralLattice.normIdeal_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
      L.normIdeal = Ideal.span (Set.range ⇑L.integralNorm)

      The norm ideal as a span of self-pairing values.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.integralNorm_mem_normIdeal {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) :
      L.integralNorm x ∈ L.normIdeal

      Every integral norm lies in the norm ideal.

      source
      theorem TauCeti.IntegralLattice.normIdeal_le_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (I : Ideal ℤ) :
      L.normIdeal ≤ I ↔ ∀ (x : ↥L.carrier), L.integralNorm x ∈ I

      The norm ideal is the smallest ideal containing all integral norms.

      source
      theorem TauCeti.IntegralLattice.two_mul_integralForm_mem_normIdeal {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : ↥L.carrier) :
      2 * (L.integralForm x) y ∈ L.normIdeal

      Twice each integral pairing belongs to the norm ideal.

      source
      theorem TauCeti.IntegralLattice.normIdeal_eq_span_of_span {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {s : Set ↥L.carrier} (hs : Submodule.span ℤ s = ⊤) :
      L.normIdeal = Ideal.span (⇑L.integralNorm '' s ∪ Set.image2 (fun (x y : ↥L.carrier) => 2 * (L.integralForm x) y) s s)

      A spanning set generates the norm ideal through its norms and twice its pairings.

      source
      theorem TauCeti.IntegralLattice.normIdeal_eq_span_basis {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} (L : IntegralLattice V) (b : Module.Basis ι ℤ ↥L.carrier) :
      L.normIdeal = Ideal.span ((Set.range fun (i : ι) => L.integralNorm (b i)) ∪ Set.range fun (ij : ι × ι) => 2 * (L.integralForm (b ij.1)) (b ij.2))

      In a basis, the norm ideal is generated by diagonal Gram entries and twice every Gram entry. Including all ordered pairs avoids a choice of order on the index.

      source
      theorem TauCeti.IntegralLattice.span_singleton_two_mul_scaleIdeal_le_normIdeal {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
      Ideal.span {2} * L.scaleIdeal ≤ L.normIdeal

      Polarization yields 2 𝔰(L) ≤ 𝔫(L).

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

      The norm ideal lies in 2ℤ exactly when the lattice is even.

      source
      theorem TauCeti.IntegralLattice.scaleIdeal_le_of_integralForm_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) {M : IntegralLattice W} (f : ↥L.carrier →ₗ[ℤ] ↥M.carrier) (hf : ∀ (x y : ↥L.carrier), (L.integralForm x) y = (M.integralForm (f x)) (f y)) :
      L.scaleIdeal ≤ M.scaleIdeal

      A linear map preserving integral pairings gives containment of scale ideals.

      source
      theorem TauCeti.IntegralLattice.normIdeal_le_of_integralForm_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) {M : IntegralLattice W} (f : ↥L.carrier →ₗ[ℤ] ↥M.carrier) (hf : ∀ (x y : ↥L.carrier), (L.integralForm x) y = (M.integralForm (f x)) (f y)) :
      L.normIdeal ≤ M.normIdeal

      A linear map preserving integral pairings gives containment of norm ideals.

      source
      theorem TauCeti.IntegralLattice.scaleIdeal_le_of_form_eq_of_le {V : Type u} [AddCommGroup V] [Module ℚ V] (L M : IntegralLattice V) (hform : L.form = M.form) (hle : L.carrier ≤ M.carrier) :
      L.scaleIdeal ≤ M.scaleIdeal

      Inclusion of carriers with the same ambient form gives containment of scale ideals.

      source
      theorem TauCeti.IntegralLattice.normIdeal_le_of_form_eq_of_le {V : Type u} [AddCommGroup V] [Module ℚ V] (L M : IntegralLattice V) (hform : L.form = M.form) (hle : L.carrier ≤ M.carrier) :
      L.normIdeal ≤ M.normIdeal

      Inclusion of carriers with the same ambient form gives containment of norm ideals.

      source
      theorem TauCeti.IntegralLattice.Isometry.scaleIdeal_le {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) :
      L.scaleIdeal ≤ M.scaleIdeal

      An integral-lattice isometry maps scale ideals into one another.

      source
      theorem TauCeti.IntegralLattice.Isometry.scaleIdeal_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) :
      L.scaleIdeal = M.scaleIdeal

      An integral-lattice isometry preserves the scale ideal.

      source
      theorem TauCeti.IntegralLattice.Isometry.normIdeal_le {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) :
      L.normIdeal ≤ M.normIdeal

      An integral-lattice isometry maps norm ideals into one another.

      source
      theorem TauCeti.IntegralLattice.Isometry.normIdeal_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) :
      L.normIdeal = M.normIdeal

      An integral-lattice isometry preserves the norm ideal.