Documentation

TauCeti.LinearAlgebra.IntegralLattice.Norm

Norms of integral lattices #

The norm of a vector in an integral lattice is its self-pairing under the lattice bilinear form. On lattice vectors this rational value has a canonical integral lift, the integral norm.

This file develops the rational and integral norm quadratic forms, their basic properties and polarization identities, and the set of lattice vectors having a prescribed norm. An integral-lattice isometry induces an isometry equivalence of the rational norm forms and preserves the integral norm on the carrier.

Main definitions #

Main results #

References #

Norms #

source
def TauCeti.IntegralLattice.norm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
QuadraticForm ℚ V

The rational quadratic form on ambient vectors given by self-pairing.

Equations
Instances For
    source
    theorem TauCeti.IntegralLattice.norm_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    L.norm = LinearMap.BilinMap.toQuadraticMap L.form

    The rational norm form is the quadratic form associated to the ambient bilinear form.

    source
    theorem TauCeti.IntegralLattice.nondegenerate_norm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] :
    QuadraticMap.Nondegenerate

    The ambient rational norm form of a nondegenerate integral lattice is nondegenerate.

    source
    theorem TauCeti.IntegralLattice.norm_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : V) :
    L.norm x = (L.form x) x

    Evaluating the rational norm of an ambient vector yields its self-pairing.

    source
    noncomputable def TauCeti.IntegralLattice.integralNorm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    QuadraticForm ℤ ↥L.carrier

    The canonical integer quadratic form induced on the lattice carrier.

    Equations
    Instances For
      source
      theorem TauCeti.IntegralLattice.integralNorm_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) :
      L.integralNorm x = (L.integralForm x) x

      Evaluating the integral norm of a lattice vector yields its integral self-pairing.

      source
      def TauCeti.IntegralLattice.Isometry.normIsometryEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) :
      QuadraticMap.IsometryEquiv L.norm M.norm

      An integral-lattice isometry, regarded as an isometry equivalence of the associated rational norm forms.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.IntegralLattice.Isometry.normIsometryEquiv_toLinearEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) :
        e.normIsometryEquiv.toLinearEquiv = e.toLinearEquiv

        The linear equivalence underlying the norm isometry is the original ambient equivalence.

        source
        @[simp]
        theorem TauCeti.IntegralLattice.Isometry.norm_apply {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (x : V) :
        M.norm (e x) = L.norm x

        An integral-lattice isometry preserves the rational norm.

        source
        @[simp]
        theorem TauCeti.IntegralLattice.Isometry.integralNorm_carrierEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (x : ↥L.carrier) :
        M.integralNorm (e.carrierEquiv x) = L.integralNorm x

        The carrier equivalence of an integral-lattice isometry preserves the integral norm.

        source
        @[simp]
        theorem TauCeti.IntegralLattice.integralNorm_cast {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) :
        ↑(L.integralNorm x) = L.norm ↑x

        The integral norm recovers the rational norm after coercion to ℚ.

        source
        @[simp]
        theorem TauCeti.IntegralLattice.norm_zero {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
        L.norm 0 = 0

        The rational norm of zero is zero.

        source
        theorem TauCeti.IntegralLattice.norm_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : V) :
        L.norm (-x) = L.norm x

        The rational norm is invariant under negation.

        source
        @[simp]
        theorem TauCeti.IntegralLattice.norm_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (a : ℚ) (x : V) :
        L.norm (a • x) = a ^ 2 * L.norm x

        Scaling an ambient vector squares its rational norm.

        source
        theorem TauCeti.IntegralLattice.norm_add {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : V) :
        L.norm (x + y) = L.norm x + L.norm y + 2 * (L.form x) y

        Polarization of the norm using symmetry of the lattice form.

        source
        theorem TauCeti.IntegralLattice.norm_sub {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : V) :
        L.norm (x - y) = L.norm x + L.norm y - 2 * (L.form x) y

        The subtraction form of the norm polarization identity.

        source
        @[simp]
        theorem TauCeti.IntegralLattice.integralNorm_zero {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
        L.integralNorm 0 = 0

        The integral norm of zero is zero.

        source
        theorem TauCeti.IntegralLattice.integralNorm_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) :
        L.integralNorm (-x) = L.integralNorm x

        The integral norm is invariant under negation.

        source
        @[simp]
        theorem TauCeti.IntegralLattice.integralNorm_zsmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (a : ℤ) (x : ↥L.carrier) :
        L.integralNorm (a • x) = a ^ 2 * L.integralNorm x

        Scaling a lattice vector by an integer scales its integral norm by the square.

        source
        theorem TauCeti.IntegralLattice.integralNorm_add {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : ↥L.carrier) :
        L.integralNorm (x + y) = L.integralNorm x + L.integralNorm y + 2 * (L.integralForm x) y

        Integral polarization of the norm.

        source
        noncomputable def TauCeti.IntegralLattice.normParity {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
        ↥L.carrier →+ ZMod 2

        The norm modulo two, as an additive character of the carrier.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.IntegralLattice.normParity_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) :
          L.normParity x = ↑(L.integralNorm x)

          The norm parity character evaluates to the norm modulo two.

          source
          theorem TauCeti.IntegralLattice.integralNorm_sub {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : ↥L.carrier) :
          L.integralNorm (x - y) = L.integralNorm x + L.integralNorm y - 2 * (L.integralForm x) y

          Integral polarization for a difference.

          Vectors of prescribed norm #

          source
          def TauCeti.IntegralLattice.vectorsOfNorm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (n : ℚ) :
          Set ↥L.carrier

          The lattice vectors having the prescribed rational norm.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.IntegralLattice.mem_vectorsOfNorm {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {n : ℚ} {x : ↥L.carrier} :
            x ∈ L.vectorsOfNorm n ↔ L.norm ↑x = n

            Membership condition for vectorsOfNorm.

            source
            theorem TauCeti.IntegralLattice.mem_vectorsOfNorm_intCast {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {n : ℤ} {x : ↥L.carrier} :
            x ∈ L.vectorsOfNorm ↑n ↔ L.integralNorm x = n

            Membership in vectorsOfNorm (n : ℚ) for an integer n is equivalent to having integral norm equal to n. This remains an explicit rewrite lemma because mem_vectorsOfNorm already simplifies its left-hand side, so tagging both lemmas would violate simpNF.

            source
            theorem TauCeti.IntegralLattice.mem_vectorsOfNorm_natCast {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {n : ℕ} {x : ↥L.carrier} :
            x ∈ L.vectorsOfNorm ↑n ↔ L.integralNorm x = ↑n

            Membership in vectorsOfNorm (n : ℚ) for a natural number n is equivalent to having integral norm equal to n.

            source
            theorem TauCeti.IntegralLattice.zero_mem_vectorsOfNorm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
            0 ∈ L.vectorsOfNorm 0

            The zero vector in an integral lattice has norm zero.

            source
            theorem TauCeti.IntegralLattice.neg_mem_vectorsOfNorm_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {n : ℚ} (x : ↥L.carrier) :
            -x ∈ L.vectorsOfNorm n ↔ x ∈ L.vectorsOfNorm n

            A lattice vector has norm n if and only if its negation does.

            source
            theorem TauCeti.IntegralLattice.Isometry.carrierEquiv_mem_vectorsOfNorm_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (x : ↥L.carrier) (n : ℚ) :
            e.carrierEquiv x ∈ M.vectorsOfNorm n ↔ x ∈ L.vectorsOfNorm n

            A carrier vector belongs to a prescribed norm set if and only if its image under an isometry does.

            source
            theorem TauCeti.IntegralLattice.vectorsOfNorm_eq_empty_of_forall_ne_intCast {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {n : ℚ} (hn : ∀ (z : ℤ), n ≠ ↑z) :
            L.vectorsOfNorm n = ∅

            If a rational number is not an integer, no lattice vector has that norm.