Signature and definiteness of integral lattices

This file defines the radical and signature (n₊, n₀, n₋) of an integral symmetric lattice and the standard definiteness predicates. The indices of inertia are Mathlib's sigPos and sigNeg; the null index is the dimension of the kernel of the bilinear form.

Positive- and negative-semidefiniteness are expressed using Mathlib's bilinear-form predicates. The characteristic theorems relate every predicate both to the signature and to the usual elementwise inequalities. In particular, an indefinite lattice has vectors of both signs, and a degenerate lattice has a nonzero vector in its radical. The final section proves that an integral-lattice isometry transports the radical and preserves all three inertia indices and every definiteness predicate.

References

• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 1.

Main definitions

• TauCeti.IntegralLattice.radical: the kernel of the rational bilinear form.
• TauCeti.IntegralLattice.signature: the positive, null, and negative indices.
• TauCeti.IntegralLattice.IsPosSemidef and related definiteness predicates.
• TauCeti.IntegralLattice.isPosDef_ofGramMatrix_iff: a lattice presented by a Gram matrix is positive definite exactly when the matrix is, read over ℚ.
• TauCeti.IntegralLattice.Isometry.map_radical and the Isometry.sigPos_eq, sigNull_eq, and sigNeg_eq theorems: isometry invariance of the signature.

def TauCeti.IntegralLattice.radical {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Submodule ℚ V

The radical of an integral lattice is the kernel of its rational bilinear form.

Equations

• L.radical = LinearMap.ker L.form

@[simp]

theorem TauCeti.IntegralLattice.mem_radical_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : V) : x ∈ L.radical ↔ ∀ (y : V), (L.form x) y = 0

A vector lies in the radical of an integral lattice if and only if it annihilates all vectors under the rational bilinear form.

@[simp]

theorem TauCeti.IntegralLattice.radical_toQuadraticMap {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (LinearMap.BilinMap.toQuadraticMap L.form).radical = L.radical

The radical of the quadratic form associated to a lattice is its bilinear radical.

@[reducible, inline]

noncomputable abbrev TauCeti.IntegralLattice.sigPos {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ℕ

The positive index of inertia of an integral lattice.

Equations

• L.sigPos = sigPos (LinearMap.BilinMap.toQuadraticMap L.form)

@[reducible, inline]

noncomputable abbrev TauCeti.IntegralLattice.sigNull {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ℕ

The dimension of the radical of an integral lattice.

Equations

• L.sigNull = Module.finrank ℚ ↥L.radical

@[reducible, inline]

noncomputable abbrev TauCeti.IntegralLattice.sigNeg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ℕ

The negative index of inertia of an integral lattice.

Equations

• L.sigNeg = sigNeg (LinearMap.BilinMap.toQuadraticMap L.form)

@[reducible, inline]

noncomputable abbrev TauCeti.IntegralLattice.signature {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ℕ × ℕ × ℕ

The signature (n₊, n₀, n₋) of an integral lattice.

Equations

• L.signature = (L.sigPos, L.sigNull, L.sigNeg)

theorem TauCeti.IntegralLattice.signature_sum_eq_finrank {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.sigPos + L.sigNull + L.sigNeg = Module.finrank ℚ V

The positive, null, and negative indices exhaust the rank of the lattice.

@[reducible, inline]

abbrev TauCeti.IntegralLattice.IsPosDef {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Prop

An integral lattice is positive-definite when its quadratic form is positive on every nonzero vector.

Equations

• L.IsPosDef = (LinearMap.BilinMap.toQuadraticMap L.form).PosDef

@[reducible, inline]

abbrev TauCeti.IntegralLattice.IsPosSemidef {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Prop

An integral lattice is positive-semidefinite when its symmetric bilinear form is nonnegative.

Equations

• L.IsPosSemidef = L.form.IsPosSemidef

@[reducible, inline]

abbrev TauCeti.IntegralLattice.IsNegDef {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Prop

An integral lattice is negative-definite when the negative of its quadratic form is positive-definite.

Equations

• L.IsNegDef = (-LinearMap.BilinMap.toQuadraticMap L.form).PosDef

@[reducible, inline]

abbrev TauCeti.IntegralLattice.IsNegSemidef {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Prop

An integral lattice is negative-semidefinite when the negative of its symmetric bilinear form is positive-semidefinite.

Equations

• L.IsNegSemidef = (-L.form).IsPosSemidef

def TauCeti.IntegralLattice.IsDegenerate {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Prop

An integral lattice is degenerate when its radical is nontrivial.

Equations

• L.IsDegenerate = (L.radical ≠ ⊥)

def TauCeti.IntegralLattice.IsIndefinite {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Prop

An integral lattice is indefinite when both its positive and negative indices are nonzero.

Equations

• L.IsIndefinite = (0 < L.sigPos ∧ 0 < L.sigNeg)

theorem TauCeti.IntegralLattice.radical_eq_bot_iff_sigNull_eq_zero {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.radical = ⊥ ↔ L.sigNull = 0

The radical of an integral lattice is trivial if and only if its null index vanishes.

theorem TauCeti.IntegralLattice.isPosDef_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsPosDef ↔ ∀ (x : V), x ≠ 0 → 0 < (L.form x) x

Positive-definiteness has its usual elementwise characterization.

theorem TauCeti.IntegralLattice.isPosDef_ofGramMatrix_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) : (ofGramMatrix b G hG).IsPosDef ↔ (G.map Int.cast).PosDef

A lattice presented by a Gram matrix is positive definite exactly when the matrix is, read over ℚ. The form of ofGramMatrix b G hG is the bilinear form of G in the coordinates of b, so this is Mathlib's comparison of a quadratic map with the matrix of its bilinear form in a basis.

theorem TauCeti.IntegralLattice.isPosSemidef_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsPosSemidef ↔ ∀ (x : V), 0 ≤ (L.form x) x

Positive-semidefiniteness has its usual elementwise characterization.

theorem TauCeti.IntegralLattice.isNegDef_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsNegDef ↔ ∀ (x : V), x ≠ 0 → (L.form x) x < 0

Negative-definiteness has its usual elementwise characterization.

theorem TauCeti.IntegralLattice.isNegSemidef_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsNegSemidef ↔ ∀ (x : V), (L.form x) x ≤ 0

Negative-semidefiniteness has its usual elementwise characterization.

theorem TauCeti.IntegralLattice.isPosSemidef_iff_sigNeg_eq_zero {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsPosSemidef ↔ L.sigNeg = 0

Positive-semidefiniteness is equivalent to the vanishing of the negative index.

theorem TauCeti.IntegralLattice.isNegSemidef_iff_sigPos_eq_zero {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsNegSemidef ↔ L.sigPos = 0

Negative-semidefiniteness is equivalent to the vanishing of the positive index.

theorem TauCeti.IntegralLattice.isPosDef_iff_isPosSemidef_and_nondegenerate {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsPosDef ↔ L.IsPosSemidef ∧ L.form.Nondegenerate

Positive-definiteness is positive-semidefiniteness together with nondegeneracy.

theorem TauCeti.IntegralLattice.IsPosDef.isPosSemidef {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hL : L.IsPosDef) : L.IsPosSemidef

A positive-definite lattice is positive-semidefinite.

theorem TauCeti.IntegralLattice.isPosDef_iff_sigNull_eq_zero_and_sigNeg_eq_zero {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsPosDef ↔ L.sigNull = 0 ∧ L.sigNeg = 0

Positive-definiteness is equivalent to zero null and negative indices.

theorem TauCeti.IntegralLattice.isNegDef_iff_isNegSemidef_and_nondegenerate {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsNegDef ↔ L.IsNegSemidef ∧ L.form.Nondegenerate

Negative-definiteness is negative-semidefiniteness together with nondegeneracy.

theorem TauCeti.IntegralLattice.isNegDef_iff_sigPos_eq_zero_and_sigNull_eq_zero {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsNegDef ↔ L.sigPos = 0 ∧ L.sigNull = 0

Negative-definiteness is equivalent to zero positive and null indices.

theorem TauCeti.IntegralLattice.isDegenerate_iff_sigNull_pos {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsDegenerate ↔ 0 < L.sigNull

Degeneracy is equivalent to a positive null index.

theorem TauCeti.IntegralLattice.isDegenerate_iff_not_nondegenerate {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsDegenerate ↔ ¬L.form.Nondegenerate

A lattice is degenerate exactly when its bilinear form is not nondegenerate.

theorem TauCeti.IntegralLattice.isDegenerate_iff_exists_mem_radical_ne_zero {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsDegenerate ↔ ∃ x ∈ L.radical, x ≠ 0

A lattice is degenerate exactly when its radical contains a nonzero vector.

theorem TauCeti.IntegralLattice.isIndefinite_iff_not_semidef {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsIndefinite ↔ ¬L.IsPosSemidef ∧ ¬L.IsNegSemidef

Indefiniteness is equivalent to the failure of both semidefiniteness conditions.

theorem TauCeti.IntegralLattice.isIndefinite_iff_exists_pos_and_exists_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.IsIndefinite ↔ (∃ (x : V), 0 < (L.form x) x) ∧ ∃ (x : V), (L.form x) x < 0

An indefinite lattice has, and is characterized by, vectors of both signs.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.map_radical {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : Submodule.map (↑e.toLinearEquiv) L.radical = M.radical

An integral-lattice isometry maps the source radical onto the target radical.

theorem TauCeti.IntegralLattice.Isometry.sigPos_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.sigPos = M.sigPos

Isometric integral lattices have the same positive index.

theorem TauCeti.IntegralLattice.Isometry.sigNull_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.sigNull = M.sigNull

Isometric integral lattices have the same null index.

theorem TauCeti.IntegralLattice.Isometry.sigNeg_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.sigNeg = M.sigNeg

Isometric integral lattices have the same negative index.

theorem TauCeti.IntegralLattice.Isometry.signature_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.signature = M.signature

Isometric integral lattices have the same signature.

theorem TauCeti.IntegralLattice.Isometry.form_nondegenerate_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.form.Nondegenerate ↔ M.form.Nondegenerate

Nondegeneracy of the ambient form is invariant under integral-lattice isometry.

theorem TauCeti.IntegralLattice.Isometry.isNondegenerate_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.IsNondegenerate ↔ M.IsNondegenerate

The nondegeneracy mixin is invariant under integral-lattice isometry.

theorem TauCeti.IntegralLattice.Isometry.isNondegenerate {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) [L.IsNondegenerate] : M.IsNondegenerate

Transport the nondegeneracy mixin along an integral-lattice isometry.

theorem TauCeti.IntegralLattice.Isometry.isPosDef_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.IsPosDef ↔ M.IsPosDef

Positive-definiteness is invariant under integral-lattice isometry.

theorem TauCeti.IntegralLattice.Isometry.isPosSemidef_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.IsPosSemidef ↔ M.IsPosSemidef

Positive-semidefiniteness is invariant under integral-lattice isometry.

theorem TauCeti.IntegralLattice.Isometry.isNegDef_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.IsNegDef ↔ M.IsNegDef

Negative-definiteness is invariant under integral-lattice isometry.

theorem TauCeti.IntegralLattice.Isometry.isNegSemidef_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.IsNegSemidef ↔ M.IsNegSemidef

Negative-semidefiniteness is invariant under integral-lattice isometry.

theorem TauCeti.IntegralLattice.Isometry.isDegenerate_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.IsDegenerate ↔ M.IsDegenerate

Degeneracy is invariant under integral-lattice isometry.

theorem TauCeti.IntegralLattice.Isometry.isIndefinite_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.IsIndefinite ↔ M.IsIndefinite

Indefiniteness is invariant under integral-lattice isometry.