Splitting off a vector of unit norm

A nonzero integral vector generates a cyclic lattice with Gram matrix consisting of its norm. This file identifies the rationalized restricted form on that cyclic submodule with the Gram-matrix lattice on ℚ, sending 1 to the unit tensor of the chosen vector.

If the norm is a unit of ℤ, hence 1 or -1, the cyclic lattice splits off orthogonally. The resulting isometry identifies the entire integral lattice with ⟨1⟩ or ⟨-1⟩ plus its orthogonal complement. Neither nondegeneracy nor definiteness of the ambient form is needed. These splittings allow unit-norm vectors to be removed in classification arguments.

The construction uses LinearEquiv.toSpanNonzeroSingleton, the abstract-form dictionary IntegralLattice.ofIntegralForm, and the orthogonal splitting isometry. The mathematical source is O. T. O'Meara, Introduction to Quadratic Forms, §82.

noncomputable def TauCeti.IntegralLattice.spanSingletonIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) (hx : x ≠ 0) : (ofGramMatrix (Module.Basis.singleton (Fin 1) ℚ) (Matrix.of fun (x_1 x_2 : Fin 1) => (L.integralForm x) x) ⋯).Isometry (ofIntegralForm (L.integralForm.restrict (ℤ ∙ x)) ⋯)

The cyclic lattice generated by a nonzero integral vector has one-entry Gram matrix equal to its norm. The isometry sends 1 to the unit tensor of the vector.

@[simp]

theorem TauCeti.IntegralLattice.spanSingletonIsometry_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) (hx : x ≠ 0) (q : ℚ) : (L.spanSingletonIsometry x hx) q = q ⊗ₜ[ℤ] ⟨x, ⋯⟩

The cyclic isometry sends a rational scalar to the corresponding pure tensor.

@[simp]

theorem TauCeti.IntegralLattice.spanSingletonIsometry_symm_apply_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) (hx : x ≠ 0) (q : ℚ) : (L.spanSingletonIsometry x hx).symm (q ⊗ₜ[ℤ] ⟨x, ⋯⟩) = q

The inverse cyclic isometry recovers the coefficient of a pure tensor.

theorem TauCeti.IntegralLattice.determinant_eq_integralForm_mul_determinant_orthogonal {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) (hxx : (L.integralForm x) x ≠ 0) (hdvd : ∀ (y : ↥L.carrier), (L.integralForm x) x ∣ (L.integralForm x) y) : L.determinant = (L.integralForm x) x * (ofIntegralForm (L.integralForm.restrict (L.integralForm.orthogonal (ℤ ∙ x))) ⋯).determinant

If the nonzero norm of x divides every pairing with x, then L is the orthogonal sum of ℤ x and its orthogonal complement, so its determinant is the norm of x times the determinant of that complement.

noncomputable def TauCeti.IntegralLattice.unitNormSplittingIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) (hx : IsUnit ((L.integralForm x) x)) : ((ofGramMatrix (Module.Basis.singleton (Fin 1) ℚ) (Matrix.of fun (x_1 x_2 : Fin 1) => (L.integralForm x) x) ⋯).orthogonalSum (ofIntegralForm (L.integralForm.restrict (L.integralForm.orthogonal (ℤ ∙ x))) ⋯)).Isometry L

A vector of norm 1 or -1 splits off its canonical rank-one Gram-matrix lattice. The other summand is the rationalized integral orthogonal complement of the vector.

@[simp]

theorem TauCeti.IntegralLattice.unitNormSplittingIsometry_apply_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) (hx : IsUnit ((L.integralForm x) x)) (q r : ℚ) (t : ↥(L.integralForm.orthogonal (ℤ ∙ x))) : (L.unitNormSplittingIsometry x hx) (q, r ⊗ₜ[ℤ] t) = q • ↑x + r • ↑↑t

The splitting sends the rank-one coordinate to its multiple of the chosen vector, and a pure tensor in the orthogonal complement to its underlying scalar multiple.

@[simp]

theorem TauCeti.IntegralLattice.unitNormSplittingIsometry_symm_apply_smul_add_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) (hx : IsUnit ((L.integralForm x) x)) (q r : ℚ) (t : ↥(L.integralForm.orthogonal (ℤ ∙ x))) : (L.unitNormSplittingIsometry x hx).symm (q • ↑x + r • ↑↑t) = (q, r ⊗ₜ[ℤ] t)

The inverse splitting recovers the rank-one coordinate and the pure tensor in the orthogonal complement.

@[simp]

theorem TauCeti.IntegralLattice.unitNormSplittingIsometry_symm_apply_fst {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.carrier) (hx : IsUnit ((L.integralForm x) x)) (y : V) : ((L.unitNormSplittingIsometry x hx).symm y).1 = (L.form ↑x) y / ↑((L.integralForm x) x)

The first inverse coordinate is the orthogonal projection coefficient, on every rational ambient vector.