Documentation

TauCeti.LinearAlgebra.IntegralLattice.Neighbor.Basic

Kneser neighbors #

Two integral lattices L and M on the same rational quadratic space are p-neighbors when their intersection L ∩ M has index p in each of them. Neighbor steps are the moves of Kneser's method for exploring a genus. This file defines the relation, proves that it is symmetric, that 1-neighbors are equal, and that neighbors have equal determinants: the determinant of L ∩ M is both p² det L and p² det M. In particular a neighbor of a unimodular lattice is unimodular.

The intersection L ∩ M is the integral lattice TauCeti.IntegralLattice.inf from TauCeti.LinearAlgebra.IntegralLattice.Restriction, carrying the form of L.

Main definitions #

Main results #

References #

source
structure TauCeti.IntegralLattice.IsNeighbor {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L M : IntegralLattice V) (p : ℕ) :
Prop

Kneser neighbors. Integral lattices L and M on the same rational quadratic space are p-neighbors when their intersection has index p in each of them, that is [L : L ∩ M] = [M : L ∩ M] = p.

Instances For
    source
    theorem TauCeti.IntegralLattice.IsNeighbor.symm {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} {p : ℕ} (h : L.IsNeighbor M p) :
    M.IsNeighbor L p

    The neighbor relation is symmetric.

    source
    theorem TauCeti.IntegralLattice.isNeighbor_comm {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} {p : ℕ} :
    L.IsNeighbor M p ↔ M.IsNeighbor L p

    M is a p-neighbor of L exactly when L is a p-neighbor of M.

    source
    theorem TauCeti.IntegralLattice.IsNeighbor.transport {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} {p : ℕ} {W : Type u_2} [AddCommGroup W] [Module ℚ W] (h : L.IsNeighbor M p) (e : V ≃ₗ[ℚ] W) :
    (L.transport e).IsNeighbor (M.transport e) p

    Neighbors transport along rational linear equivalences. Transporting two p-neighbors along the same equivalence of their ambient spaces gives p-neighbors.

    source
    theorem TauCeti.IntegralLattice.IsNeighbor.ne_zero {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} {p : ℕ} (h : L.IsNeighbor M p) :
    p ≠ 0

    The common index of two neighbors is nonzero, since the intersection of two lattices on the same rational space has finite index in each.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.isNeighbor_one_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} :
    L.IsNeighbor M 1 ↔ L = M

    Two integral lattices are 1-neighbors exactly when they are equal.

    source
    theorem TauCeti.IntegralLattice.IsNeighbor.determinant_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} {p : ℕ} (h : L.IsNeighbor M p) :
    L.determinant = M.determinant

    Neighbors have equal determinants. The intersection L ∩ M has determinant [L : L ∩ M]² det L = [M : L ∩ M]² det M, and both indices equal the nonzero integer p.

    source
    theorem TauCeti.IntegralLattice.IsNeighbor.discriminant_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} {p : ℕ} (h : L.IsNeighbor M p) :
    L.discriminant = M.discriminant

    Neighbors have equal discriminants.

    source
    theorem TauCeti.IntegralLattice.IsNeighbor.isUnimodular {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} {p : ℕ} (h : L.IsNeighbor M p) (hL : L.IsUnimodular) :
    M.IsUnimodular

    Neighbors of unimodular lattices are unimodular, since neighbors have equal discriminants.

    source
    theorem TauCeti.IntegralLattice.IsNeighbor.isUnimodular_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} {p : ℕ} (h : L.IsNeighbor M p) :
    L.IsUnimodular ↔ M.IsUnimodular

    Two neighbors are unimodular together.