Isometric orthogonal splitting of integral lattices

Orthogonally complementary submodules of an integral carrier give a decomposition of the entire lattice, including its rational ambient form. Each summand is realized by rationalizing the restricted integral form with IntegralLattice.ofIntegralForm; it need not span the original ambient space. The resulting isometry sends unit pure tensors to the sum of their underlying vectors, so the decomposition identifies the actual integral carriers.

A submodule whose restricted pairing is bijective is complementary to its orthogonal complement. Combining this with the isometry construction gives the unimodular splitting theorem without assuming nondegeneracy of the whole lattice.

Finally, an isometry of integral lattices carries orthogonal complements of sublattices to orthogonal complements of their images (TauCeti.IntegralLattice.Isometry.map_orthogonal).

The mathematical source is O. T. O'Meara, Introduction to Quadratic Forms, §82.

noncomputable def TauCeti.IntegralLattice.orthogonalSumIsometryOfIsCompl {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S T : Submodule ℤ ↥L.carrier) (h : IsCompl S T) (horth : T ≤ L.integralForm.orthogonal S) : ((ofIntegralForm (L.integralForm.restrict S) ⋯).orthogonalSum (ofIntegralForm (L.integralForm.restrict T) ⋯)).Isometry L

Orthogonally complementary integral submodules give an isometry from the orthogonal sum of their rationalized restricted forms onto the original lattice.

theorem TauCeti.IntegralLattice.orthogonalSumIsometryOfIsCompl_apply_one_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S T : Submodule ℤ ↥L.carrier) (h : IsCompl S T) (horth : T ≤ L.integralForm.orthogonal S) (s : ↥S) (t : ↥T) : (L.orthogonalSumIsometryOfIsCompl S T h horth) (1 ⊗ₜ[ℤ] s, 1 ⊗ₜ[ℤ] t) = ↑↑s + ↑↑t

On unit pure tensors the splitting isometry is addition of the original integral vectors.

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumIsometryOfIsCompl_apply_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S T : Submodule ℤ ↥L.carrier) (h : IsCompl S T) (horth : T ≤ L.integralForm.orthogonal S) (q r : ℚ) (s : ↥S) (t : ↥T) : (L.orthogonalSumIsometryOfIsCompl S T h horth) (q ⊗ₜ[ℤ] s, r ⊗ₜ[ℤ] t) = q • ↑↑s + r • ↑↑t

On arbitrary pure tensors the splitting isometry is the sum of the scalar multiples of the original vectors.

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumIsometryOfIsCompl_symm_apply_add {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S T : Submodule ℤ ↥L.carrier) (h : IsCompl S T) (horth : T ≤ L.integralForm.orthogonal S) (s : ↥S) (t : ↥T) : (L.orthogonalSumIsometryOfIsCompl S T h horth).symm (↑↑s + ↑↑t) = (1 ⊗ₜ[ℤ] s, 1 ⊗ₜ[ℤ] t)

The inverse splitting isometry recovers the two unit pure tensors from a sum of integral vectors in the two summands.

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumIsometryOfIsCompl_symm_apply_smul_add_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S T : Submodule ℤ ↥L.carrier) (h : IsCompl S T) (horth : T ≤ L.integralForm.orthogonal S) (q r : ℚ) (s : ↥S) (t : ↥T) : (L.orthogonalSumIsometryOfIsCompl S T h horth).symm (q • ↑↑s + r • ↑↑t) = (q ⊗ₜ[ℤ] s, r ⊗ₜ[ℤ] t)

The inverse splitting isometry recovers arbitrary pure tensors from the corresponding rational scalar multiples of vectors in the two summands.

noncomputable def TauCeti.IntegralLattice.orthogonalSplittingIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (h : Function.Bijective ⇑(L.integralForm.restrict S)) : ((ofIntegralForm (L.integralForm.restrict S) ⋯).orthogonalSum (ofIntegralForm (L.integralForm.restrict (L.integralForm.orthogonal S)) ⋯)).Isometry L

A submodule with perfect restricted integral pairing splits off isometrically, with its orthogonal complement rationalized in its own ambient space.

theorem TauCeti.IntegralLattice.orthogonalSplittingIsometry_apply_one_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (h : Function.Bijective ⇑(L.integralForm.restrict S)) (s : ↥S) (t : ↥(L.integralForm.orthogonal S)) : (L.orthogonalSplittingIsometry S h) (1 ⊗ₜ[ℤ] s, 1 ⊗ₜ[ℤ] t) = ↑↑s + ↑↑t

The unimodular splitting isometry sends unit pure tensors to the sum of their vectors.

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSplittingIsometry_apply_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (h : Function.Bijective ⇑(L.integralForm.restrict S)) (q r : ℚ) (s : ↥S) (t : ↥(L.integralForm.orthogonal S)) : (L.orthogonalSplittingIsometry S h) (q ⊗ₜ[ℤ] s, r ⊗ₜ[ℤ] t) = q • ↑↑s + r • ↑↑t

The unimodular splitting isometry sends arbitrary pure tensors to the sum of the corresponding rational scalar multiples of their vectors.

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSplittingIsometry_symm_apply_add {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (h : Function.Bijective ⇑(L.integralForm.restrict S)) (s : ↥S) (t : ↥(L.integralForm.orthogonal S)) : (L.orthogonalSplittingIsometry S h).symm (↑↑s + ↑↑t) = (1 ⊗ₜ[ℤ] s, 1 ⊗ₜ[ℤ] t)

The inverse unimodular splitting sends a sum of integral vectors in the summand and its orthogonal complement to their unit pure tensors.

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSplittingIsometry_symm_apply_smul_add_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (S : Submodule ℤ ↥L.carrier) (h : Function.Bijective ⇑(L.integralForm.restrict S)) (q r : ℚ) (s : ↥S) (t : ↥(L.integralForm.orthogonal S)) : (L.orthogonalSplittingIsometry S h).symm (q • ↑↑s + r • ↑↑t) = (q ⊗ₜ[ℤ] s, r ⊗ₜ[ℤ] t)

The inverse unimodular splitting recovers arbitrary pure tensors from rational scalar multiples of vectors in the summand and its orthogonal complement.

theorem TauCeti.IntegralLattice.Isometry.map_orthogonal {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (e : L.Isometry M) (S : Submodule ℤ ↥L.carrier) : Submodule.map (↑e.carrierEquiv) (L.integralForm.orthogonal S) = M.integralForm.orthogonal (Submodule.map (↑e.carrierEquiv) S)

An isometry carries the orthogonal complement of a sublattice onto the orthogonal complement of its image.