Documentation

TauCeti.LinearAlgebra.IntegralLattice.Characteristic.Basic

Characteristic vectors of integral lattices #

A lattice vector is characteristic when pairing it with any lattice vector agrees modulo two with the latter's norm. This parity condition is the input to the characteristic-norm congruence for unimodular lattices. The results here give its behavior under evenness, isometries, translation by twice a vector, and orthogonal sums.

The congruences are in ℤ, using the integral restriction of the rational bilinear form, so the characteristic vectors of a lattice are those of that integral form in the sense of LinearMap.BilinForm.IsCharacteristic.

References #

source
def TauCeti.IntegralLattice.IsCharacteristicVector {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (w : ↥L.carrier) :
Prop

A vector is characteristic when its pairing with every lattice vector is congruent modulo two to that vector's norm.

Instances For
    source
    theorem TauCeti.IntegralLattice.isCharacteristicVector_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (w : ↥L.carrier) :
    L.IsCharacteristicVector w ↔ ∀ (x : ↥L.carrier), (L.integralForm w) x ≡ L.integralNorm x [ZMOD 2]

    The defining parity test for a characteristic vector.

    source
    theorem TauCeti.IntegralLattice.isCharacteristicVector_iff_forall_integralForm_eq_normParity {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (w : ↥L.carrier) :
    L.IsCharacteristicVector w ↔ ∀ (x : ↥L.carrier), ↑((L.integralForm w) x) = L.normParity x

    The characteristic condition says that pairing with the vector represents norm parity.

    source
    theorem TauCeti.IntegralLattice.isCharacteristicVector_iff_isCharacteristic {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (w : ↥L.carrier) :
    L.IsCharacteristicVector w ↔ L.integralForm.IsCharacteristic w

    The characteristic vectors of L are the characteristic vectors of its integral bilinear form.

    source
    theorem TauCeti.IntegralLattice.isEven_iff_isCharacteristicVector_zero {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    L.IsEven ↔ L.IsCharacteristicVector 0

    Zero is characteristic precisely when the lattice is even.

    source
    theorem TauCeti.IntegralLattice.IsCharacteristicVector.add_two_smul {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {w : ↥L.carrier} (hw : L.IsCharacteristicVector w) (v : ↥L.carrier) :
    L.IsCharacteristicVector (w + 2 • v)

    Adding twice a lattice vector preserves the characteristic parity condition.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.isCharacteristicVector_add_two_smul_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (w v : ↥L.carrier) :
    L.IsCharacteristicVector (w + 2 • v) ↔ L.IsCharacteristicVector w

    Translation by twice a lattice vector preserves and reflects the characteristic condition.

    source
    theorem TauCeti.IntegralLattice.IsCharacteristicVector.neg {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {w : ↥L.carrier} (hw : L.IsCharacteristicVector w) :
    L.IsCharacteristicVector (-w)

    A characteristic vector remains characteristic after changing its sign.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.isCharacteristicVector_neg_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (w : ↥L.carrier) :
    L.IsCharacteristicVector (-w) ↔ L.IsCharacteristicVector w

    Negation preserves and reflects the characteristic condition.

    source
    theorem TauCeti.IntegralLattice.IsCharacteristicVector.even_integralForm_sub {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {w₁ w₂ : ↥L.carrier} (h₁ : L.IsCharacteristicVector w₁) (h₂ : L.IsCharacteristicVector w₂) (x : ↥L.carrier) :
    Even ((L.integralForm (w₁ - w₂)) x)

    The pairing of the difference of two characteristic vectors with every lattice vector is even.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.Isometry.isCharacteristicVector_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) (w : ↥L.carrier) :
    M.IsCharacteristicVector (e.carrierEquiv w) ↔ L.IsCharacteristicVector w

    Isometries preserve and reflect characteristic vectors.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.isCharacteristicVector_orthogonalSum_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (w : ↥(L.orthogonalSum M).carrier) :
    (L.orthogonalSum M).IsCharacteristicVector w ↔ L.IsCharacteristicVector ((L.orthogonalSumFst M) w) ∧ M.IsCharacteristicVector ((L.orthogonalSumSnd M) w)

    A vector of an orthogonal sum is characteristic precisely when its two components are.

    source
    theorem TauCeti.IntegralLattice.IsCharacteristicVector.integralNorm_add_two_smul_modEq {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {w : ↥L.carrier} (hw : L.IsCharacteristicVector w) (v : ↥L.carrier) :
    L.integralNorm (w + 2 • v) ≡ L.integralNorm w [ZMOD 8]

    Translating a characteristic vector by twice a lattice vector changes its norm by a multiple of eight.