Documentation

TauCeti.LinearAlgebra.IntegralLattice.PosDef.Gram

Positive definiteness over ℤ, ℚ and ℝ #

An integral lattice is positive definite when its rational form is (TauCeti.IntegralLattice.IsPosDef). This file shows that the same condition can be read on every other model of the lattice form: on the integral norm form of the carrier, on the integral Gram matrix of any carrier basis, on that Gram matrix with its entries cast to ℝ, and on the base change of the rational form to ℝ. Base change holds more generally over any linearly ordered commutative rational algebra with an order-preserving structure map; the real matrix statement requires the order to be the star order of the trivial star.

The real Gram matrix is the form in which positive definiteness enters analytic arguments in Euclidean space, and the integral Gram matrix is the form in which it is checked on explicit lattices; these equivalences let either be used for IsPosDef. Ordered scalar extension uses LinearMap.BilinForm.posDef_toQuadraticMap_baseChange_iff. The Gram-matrix comparisons use rational congruence (TauCeti.Matrix.posDef_map_ratCast_iff) and clearing denominators (TauCeti.Matrix.posDef_map_intCast_iff).

Main results #

source
theorem TauCeti.IntegralLattice.isPosDef_iff_posDef_gramMatrix {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type u_2} [Finite ι] (b : Module.Basis ι ℤ ↥L.carrier) :
L.IsPosDef ↔ (L.gramMatrix b).PosDef

A lattice is positive definite exactly when the integral Gram matrix of a carrier basis is positive definite.

source
theorem TauCeti.IntegralLattice.isPosDef_iff_posDef_integralNorm {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
L.IsPosDef ↔ QuadraticMap.PosDef L.integralNorm

A lattice is positive definite exactly when its integral norm form is, that is, when every nonzero vector of the carrier has positive norm.

source
theorem TauCeti.IntegralLattice.IsPosDef.isPosDef_ofIntegralForm_restrict {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (S : Submodule ℤ ↥L.carrier) :
(ofIntegralForm (L.integralForm.restrict S) ⋯).IsPosDef

A sublattice of a positive definite lattice is positive definite, in the form of the rationalized restriction of the integral form to a submodule of the carrier.

source
theorem TauCeti.IntegralLattice.isPosDef_iff_posDef_baseChange {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {K : Type u_2} [CommRing K] [LinearOrder K] [IsStrictOrderedRing K] [Algebra ℚ K] [SMulPosStrictMono ℚ K] :
L.IsPosDef ↔ (LinearMap.BilinMap.toQuadraticMap (LinearMap.BilinForm.baseChange K L.form)).PosDef

A lattice is positive definite exactly when its real form is, and more generally when its rational form remains positive definite after base change to a linearly ordered commutative rational algebra whose structure map preserves order.

source
theorem TauCeti.IntegralLattice.isPosDef_iff_posDef_map_gramMatrix {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {K : Type u_2} [Field K] [LinearOrder K] [StarRing K] [StarOrderedRing K] {ι : Type u_3} [Finite ι] (b : Module.Basis ι ℤ ↥L.carrier) :
L.IsPosDef ↔ ((L.gramMatrix b).map Int.cast).PosDef

A lattice is positive definite exactly when its Gram matrix, cast to ℝ, is positive definite, and more generally its cast to any linearly ordered field K whose order is the star order of the trivial star.