Kneser neighbors from isotropic vectors

Let L be an integral lattice, p a positive integer and v ∈ L a vector whose norm is divisible by p². Keep the vectors of L whose pairing with v is divisible by p, and adjoin v / p. The result L.neighbor p v is again an integral lattice on the same rational quadratic space. When some lattice vector pairs with v coprimely to p, the kept vectors are exactly L ∩ L.neighbor p v and have index p in both lattices, so L.neighbor p v is a Kneser p-neighbor of L. It is even when L is even and the norm of v is divisible by 2p².

A vector which is only isotropic modulo an odd p can be corrected: if w ∈ L pairs with v coprimely to p, then adding a suitable multiple of p w to v makes the norm divisible by p² without changing the kept vectors. So every vector of L that is isotropic modulo an odd p and pairs coprimely to p with some lattice vector produces a p-neighbor of L.

Main definitions

• TauCeti.IntegralLattice.neighborKernel: the vectors of L whose pairing with v lies in pℤ.
• TauCeti.IntegralLattice.neighbor: the lattice spanned by neighborKernel and v / p.

Main results

• TauCeti.IntegralLattice.isNeighbor_neighbor: L.neighbor p v is a p-neighbor of L when p² divides the norm of v and some w ∈ L pairs with v coprimely to p.
• TauCeti.IntegralLattice.isEven_neighbor: the neighbor of an even lattice is even when the norm of v is divisible by 2p².
• TauCeti.IntegralLattice.exists_dvd_integralNorm_add_smul: for odd p, a vector isotropic modulo p and pairing coprimely to p with some w ∈ L lifts to one isotropic modulo p².
• TauCeti.IntegralLattice.exists_isNeighbor_of_dvd_integralNorm: for odd p, a vector isotropic modulo p and pairing coprimely to p with some w ∈ L gives a p-neighbor meeting L in neighborKernel.
• TauCeti.IntegralLattice.exists_isNeighbor_of_not_dvd_discriminant: for an odd prime p ∤ det L, every v ∈ L ∖ p L isotropic modulo p gives a p-neighbor.

References

• M. Kneser, Klassenzahlen definiter quadratischer Formen, Arch. Math. 8 (1957), 241--250.
• J. Voight, Kneser's method of neighbors, arXiv:2308.11566, §3.

noncomputable def TauCeti.IntegralLattice.neighborCharacter {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) (v : ↥L.carrier) : ↥L.carrier →ₗ[ℤ] ZMod p

Pairing with v, reduced modulo p, as an additive character of the lattice.

@[simp]

theorem TauCeti.IntegralLattice.neighborCharacter_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) (v x : ↥L.carrier) : (L.neighborCharacter p v) x = ↑((L.integralForm v) x)

The neighbor character is the pairing with v modulo p.

noncomputable def TauCeti.IntegralLattice.neighborKernel {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) (v : ↥L.carrier) : Submodule ℤ V

The vectors of L whose pairing with v is divisible by p, as a submodule of the ambient space.

@[simp]

theorem TauCeti.IntegralLattice.coe_mem_neighborKernel_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) (v x : ↥L.carrier) : ↑x ∈ L.neighborKernel p v ↔ ↑p ∣ (L.integralForm v) x

A lattice vector lies in the neighbor kernel exactly when p divides its pairing with v.

theorem TauCeti.IntegralLattice.neighborKernel_le {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) (v : ↥L.carrier) : L.neighborKernel p v ≤ L.carrier

The neighbor kernel is contained in the original carrier.

theorem TauCeti.IntegralLattice.mem_neighborKernel_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) (v : ↥L.carrier) (x : V) : x ∈ L.neighborKernel p v ↔ ∃ (y : ↥L.carrier), ↑y = x ∧ ↑p ∣ (L.integralForm v) y

Membership in the neighbor kernel: its vectors are the lattice vectors whose pairing with v is divisible by p.

theorem TauCeti.IntegralLattice.neighborKernel_add_smul {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) (v w : ↥L.carrier) (t : ℤ) : L.neighborKernel p (v + (↑p * t) • w) = L.neighborKernel p v

The kernels of two vectors agree when the vectors agree modulo p L.

theorem TauCeti.IntegralLattice.smul_mem_neighborKernel {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) (v x : ↥L.carrier) : ↑p • ↑x ∈ L.neighborKernel p v

The neighbor kernel contains p L.

theorem TauCeti.IntegralLattice.coe_mem_neighborKernel_self {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) {v : ↥L.carrier} (hv : ↑p ∣ L.integralNorm v) : ↑v ∈ L.neighborKernel p v

v lies in its own neighbor kernel when p divides its norm.

theorem TauCeti.IntegralLattice.neighborCharacter_surjective {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) {v w : ↥L.carrier} (hvw : IsCoprime ((L.integralForm v) w) ↑p) : Function.Surjective ⇑(L.neighborCharacter p v)

An integer coprime to p among the pairings with v makes the neighbor character onto.

theorem TauCeti.IntegralLattice.relIndex_neighborKernel {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) {v w : ↥L.carrier} (hvw : IsCoprime ((L.integralForm v) w) ↑p) : (L.neighborKernel p v).toAddSubgroup.relIndex L.carrier.toAddSubgroup = p

The neighbor kernel has index p in L when some lattice vector pairs with v coprimely to p.

instance TauCeti.IntegralLattice.isLattice_neighborKernel {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (p : ℕ) [NeZero p] (v : ↥L.carrier) : Submodule.IsLattice ℚ (L.neighborKernel p v)

The neighbor kernel is a full lattice in the ambient space, since it contains p L.

noncomputable def TauCeti.IntegralLattice.neighbor {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (p : ℕ) [NeZero p] (v : ↥L.carrier) (hv : ↑p ^ 2 ∣ L.integralNorm v) : IntegralLattice V

The neighbor of L along v. For p ≠ 0 and p² dividing the norm of v, the lattice spanned by the vectors of L whose pairing with v is divisible by p, together with v / p, with the form of L. It is a p-neighbor of L when some lattice vector pairs with v coprimely to p, by isNeighbor_neighbor.

theorem TauCeti.IntegralLattice.neighbor_carrier {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [NeZero p] {v : ↥L.carrier} (hv : ↑p ^ 2 ∣ L.integralNorm v) : (neighbor p v hv).carrier = L.neighborKernel p v ⊔ ℤ ∙ (↑p)⁻¹ • ↑v

The carrier of the neighbor is spanned by the neighbor kernel and v / p.

@[simp]

theorem TauCeti.IntegralLattice.neighbor_form {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [NeZero p] {v : ↥L.carrier} (hv : ↑p ^ 2 ∣ L.integralNorm v) : (neighbor p v hv).form = L.form

The neighbor carries the form of L.

theorem TauCeti.IntegralLattice.mem_neighbor_carrier_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [NeZero p] {v : ↥L.carrier} (hv : ↑p ^ 2 ∣ L.integralNorm v) (x : V) : x ∈ (neighbor p v hv).carrier ↔ ∃ y ∈ L.neighborKernel p v, ∃ (n : ℤ), y + n • (↑p)⁻¹ • ↑v = x

Membership in the neighbor: it consists of the vectors of the neighbor kernel plus integer multiples of v / p.

theorem TauCeti.IntegralLattice.neighborKernel_le_neighbor_carrier {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [NeZero p] {v : ↥L.carrier} (hv : ↑p ^ 2 ∣ L.integralNorm v) : L.neighborKernel p v ≤ (neighbor p v hv).carrier

The neighbor kernel is contained in the neighbor.

theorem TauCeti.IntegralLattice.inv_smul_mem_neighbor_carrier {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [NeZero p] {v : ↥L.carrier} (hv : ↑p ^ 2 ∣ L.integralNorm v) : (↑p)⁻¹ • ↑v ∈ (neighbor p v hv).carrier

The vector v / p belongs to the neighbor.

instance TauCeti.IntegralLattice.instIsNondegenerateNeighbor {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [NeZero p] {v : ↥L.carrier} (hv : ↑p ^ 2 ∣ L.integralNorm v) [L.IsNondegenerate] : (neighbor p v hv).IsNondegenerate

The neighbor of a nondegenerate lattice is nondegenerate.

theorem TauCeti.IntegralLattice.isPosDef_neighbor_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [NeZero p] {v : ↥L.carrier} (hv : ↑p ^ 2 ∣ L.integralNorm v) : (neighbor p v hv).IsPosDef ↔ L.IsPosDef

The neighbor is positive definite exactly when L is.

theorem TauCeti.IntegralLattice.isEven_neighbor {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [NeZero p] {v : ↥L.carrier} (hv : ↑p ^ 2 ∣ L.integralNorm v) (hL : L.IsEven) (hv₂ : 2 * ↑p ^ 2 ∣ L.integralNorm v) : (neighbor p v hv).IsEven

Neighbors of even lattices are even when the norm of v is divisible by 2p².

theorem TauCeti.IntegralLattice.zsmul_inv_smul_mem_carrier_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [NeZero p] {v w : ↥L.carrier} (hvw : IsCoprime ((L.integralForm v) w) ↑p) (k : ℤ) : k • (↑p)⁻¹ • ↑v ∈ L.carrier ↔ ↑p ∣ k

A multiple of v / p lies in L exactly when p divides the multiplier, as soon as some lattice vector pairs with v coprimely to p.

theorem TauCeti.IntegralLattice.carrier_inf_neighbor_carrier {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [NeZero p] {v : ↥L.carrier} (hv : ↑p ^ 2 ∣ L.integralNorm v) {w : ↥L.carrier} (hvw : IsCoprime ((L.integralForm v) w) ↑p) : L.carrier ⊓ (neighbor p v hv).carrier = L.neighborKernel p v

With a pairing coprime to p, the neighbor meets L exactly in the neighbor kernel.

theorem TauCeti.IntegralLattice.relIndex_neighborKernel_neighbor {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [NeZero p] {v : ↥L.carrier} (hv : ↑p ^ 2 ∣ L.integralNorm v) {w : ↥L.carrier} (hvw : IsCoprime ((L.integralForm v) w) ↑p) : (L.neighborKernel p v).toAddSubgroup.relIndex (neighbor p v hv).carrier.toAddSubgroup = p

With a pairing coprime to p, the neighbor kernel has index p in the neighbor.

theorem TauCeti.IntegralLattice.isNeighbor_neighbor {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [NeZero p] {v : ↥L.carrier} (hv : ↑p ^ 2 ∣ L.integralNorm v) {w : ↥L.carrier} (hvw : IsCoprime ((L.integralForm v) w) ↑p) : L.IsNeighbor (neighbor p v hv) p

The neighbor is a Kneser neighbor. If p² divides the norm of v and some lattice vector pairs with v coprimely to p, then L.neighbor p v is a p-neighbor of L.

theorem TauCeti.IntegralLattice.exists_dvd_integralNorm_add_smul {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} (hp : Odd p) {v w : ↥L.carrier} (hv : ↑p ∣ L.integralNorm v) (hvw : IsCoprime ((L.integralForm v) w) ↑p) : ∃ (t : ℤ), ↑p ^ 2 ∣ L.integralNorm (v + (↑p * t) • w)

Lifting isotropic vectors from p to p². For odd p, if p divides the norm of v and w pairs with v coprimely to p, then some v + p t w has norm divisible by p².

theorem TauCeti.IntegralLattice.exists_isNeighbor_of_dvd_integralNorm {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} (hp : Odd p) {v w : ↥L.carrier} (hv : ↑p ∣ L.integralNorm v) (hvw : IsCoprime ((L.integralForm v) w) ↑p) : ∃ (M : IntegralLattice V), L.IsNeighbor M p ∧ L.carrier ⊓ M.carrier = L.neighborKernel p v ∧ (L.IsEven → M.IsEven)

Kneser neighbors from isotropic vectors. For odd p, if p divides the norm of v and some lattice vector w pairs with v coprimely to p, then L has a p-neighbor M meeting L in the vectors whose pairing with v is divisible by p. If L is even, so is M.

theorem TauCeti.IntegralLattice.exists_isNeighbor_of_not_dvd_discriminant {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {p : ℕ} [L.IsNondegenerate] (hp : Nat.Prime p) (hp₂ : p ≠ 2) (hdisc : ¬p ∣ L.discriminant) {v : ↥L.carrier} (hv : ↑p ∣ L.integralNorm v) (hv₀ : (↑p)⁻¹ • ↑v ∉ L.carrier) : ∃ (M : IntegralLattice V), L.IsNeighbor M p ∧ L.carrier ⊓ M.carrier = L.neighborKernel p v ∧ (L.IsEven → M.IsEven)

Kneser neighbors at a prime not dividing the discriminant. Let p be an odd prime not dividing the discriminant of a nondegenerate lattice L, and let v ∈ L ∖ p L be isotropic modulo p. Then L has a p-neighbor M meeting L in the vectors whose pairing with v is divisible by p. If L is even, so is M.