Neighbors become isometric after adding a hyperbolic plane

Let L be an even lattice, p a positive integer and v ∈ L a vector whose norm is divisible by 2p², such that some lattice vector pairs with v coprimely to p. Then L ⊕ U ≅ L.neighbor p v ⊕ U, where U is the hyperbolic plane.

Write M = L.neighbor p v, b = v / p ∈ M and e, f for the standard isotropic basis of U. The vector z = p (b + e - (b · b / 2) f) of L ⊕ U is primitive and isotropic, and its orthogonal complement modulo z is identified with M by x + α e + β f ↦ x - α b. Choosing y ∈ L ⊕ U with z · y = 1 and correcting it to an isotropic vector, the plane spanned by z and y is a copy of U whose orthogonal complement is a copy of M. Assembled, this is an explicit rational isometry of M ⊕ U onto L ⊕ U carrying the integral carriers onto each other.

In particular two even unimodular lattices that are neighbors become isometric after adding U, although they need not be isometric themselves; this is how cancellation fails over ℤ.

Main results

• TauCeti.IntegralLattice.nonempty_isometry_orthogonalSum_hyperbolicPlane_neighbor: L ⊕ U ≅ L.neighbor p v ⊕ U.

References

• M. Kneser, Quadratische Formen, revised with R. Scharlau, Springer (2002), §28, for neighbors.
• J.-P. Serre, A Course in Arithmetic, Chapter V, for splitting off hyperbolic planes from indefinite unimodular lattices and the resulting failure of cancellation.

theorem TauCeti.IntegralLattice.nonempty_isometry_orthogonalSum_hyperbolicPlane_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) {w : ↥L.carrier} (hvw : IsCoprime ((L.integralForm v) w) ↑p) : Nonempty ((L.orthogonalSum hyperbolicPlane).Isometry ((neighbor p v hv).orthogonalSum hyperbolicPlane))

Neighbors become isometric after adding a hyperbolic plane. Let L be even and let v ∈ L have norm divisible by 2p², with some w ∈ L pairing with v coprimely to p. Then L ⊕ U and L.neighbor p v ⊕ U are isometric, where U is the hyperbolic plane.