Documentation

TauCeti.NumberTheory.IntegralLattice.Cancellation

Cancellation fails over ℤ #

The two even unimodular positive definite lattices E₈ ⊕ E₈ and D₁₆⁺ of rank sixteen are not isometric, but they become isometric after adding a hyperbolic plane:

E₈ ⊕ E₈ ⊕ U ≅ D₁₆⁺ ⊕ U.

So L ⊕ N ≅ M ⊕ N does not imply L ≅ M for integral lattices, in contrast with Witt cancellation over a field.

The proof is explicit. Split the coordinates of ℚ¹⁶ into two blocks of eight, and let v be the vector with entries 1 on the first block and 0 on the second. It lies in D₁₆⁺, has norm 8, and pairs oddly with e₁ + e₉, so its two-neighbor M is defined and is an even neighbor of D₁₆⁺. Placing the eight E₈ glue roots TauCeti.IntegralLattice.e8GlueRoot of D₈⁺ in each block gives sixteen vectors of M with Gram matrix that of E₈ ⊕ E₈; since E₈ ⊕ E₈ is unimodular and M is integral they span M, so M ≅ E₈ ⊕ E₈. The general theorem TauCeti.IntegralLattice.nonempty_isometry_orthogonalSum_hyperbolicPlane_neighbor then gives D₁₆⁺ ⊕ U ≅ M ⊕ U.

Main results #

References #

source
theorem TauCeti.IntegralLattice.nonempty_isometry_orthogonalSum_hyperbolicPlane_e8PowLattice :
Nonempty (((e8PowLattice 2).orthogonalSum hyperbolicPlane).Isometry ((checkerboardPlusLattice (8 * 2) ⋯).orthogonalSum hyperbolicPlane))

E₈ ⊕ E₈ ⊕ U ≅ D₁₆⁺ ⊕ U. Adding the hyperbolic plane U makes the two non-isometric even unimodular lattices of rank sixteen isometric.

source
theorem TauCeti.IntegralLattice.not_forall_nonempty_isometry_of_orthogonalSum :
¬∀ (L M : IntegralLattice (Fin (8 * 2) → ℚ)) (N : IntegralLattice (Fin 2 → ℚ)), Nonempty ((L.orthogonalSum N).Isometry (M.orthogonalSum N)) → Nonempty (L.Isometry M)

Cancellation fails over ℤ. There are integral lattices L, M and N with L ⊕ N ≅ M ⊕ N but L ≇ M: take L = E₈ ⊕ E₈, M = D₁₆⁺ and N = U.