Rank-one integral lattices

The lattice rankOne a is ℤ ⊂ ℚ with bilinear form B(x,y) = axy, for any integer a. Integer representatives evaluate the integral form as akl and the integral norm as ak². Its rank is one, its signed determinant is a, and it is even exactly when a is even. It is unimodular exactly when a is a unit. The sign of a determines definiteness and signature, including the degenerate zero form.

This family includes odd lattices as well as the root lattices A₁ = ⟨2⟩ and ⟨-2⟩. Duality, the cyclic discriminant group, and the level are computed in TauCeti.LinearAlgebra.IntegralLattice.RankOne.Discriminant.

References

• W. Ebeling, Lattices and Codes, Chapter 1.

noncomputable def TauCeti.IntegralLattice.rankOne (a : ℤ) : IntegralLattice ℚ

The integral lattice ⟨a⟩: the integers in ℚ, with B(1,1) = a. The parameter may vanish, giving a degenerate lattice of rank one.

@[simp]

theorem TauCeti.IntegralLattice.mem_rankOne_carrier_iff (a : ℤ) (x : ℚ) : x ∈ (rankOne a).carrier ↔ ∃ (z : ℤ), ↑z = x

The carrier of ⟨a⟩ consists of the integers.

@[simp]

theorem TauCeti.IntegralLattice.rankOne_form_apply (a : ℤ) (x y : ℚ) : ((rankOne a).form x) y = ↑a * x * y

The bilinear form of ⟨a⟩ is axy.

@[simp]

theorem TauCeti.IntegralLattice.rankOne_norm_apply (a : ℤ) (x : ℚ) : (rankOne a).norm x = ↑a * x ^ 2

The norm of ⟨a⟩ is ax².

theorem TauCeti.IntegralLattice.integralForm_rankOne_eq {a : ℤ} (w x : ↥(rankOne a).carrier) {k l : ℤ} (hw : ↑w = ↑k) (hx : ↑x = ↑l) : ((rankOne a).integralForm w) x = a * k * l

Evaluate the integral restriction using integer representatives of actual carrier vectors.

theorem TauCeti.IntegralLattice.integralNorm_rankOne_eq {a : ℤ} (w : ↥(rankOne a).carrier) {k : ℤ} (hw : ↑w = ↑k) : (rankOne a).integralNorm w = a * k ^ 2

Evaluate the integral norm using an integer representative in the actual carrier.

@[simp]

theorem TauCeti.IntegralLattice.finrank_rankOne (a : ℤ) : Module.finrank ℤ ↥(rankOne a).carrier = 1

Every member of the family has rank one, including the zero form.

@[simp]

theorem TauCeti.IntegralLattice.isEven_rankOne_iff (a : ℤ) : (rankOne a).IsEven ↔ Even a

The lattice ⟨a⟩ is even exactly when a is even.

theorem TauCeti.IntegralLattice.isEven_rankOne_two_mul (m : ℤ) : (rankOne (2 * m)).IsEven

The rank-one lattice ⟨2m⟩ is even for every integer m.

@[simp]

theorem TauCeti.IntegralLattice.rankOne_determinant (a : ℤ) : (rankOne a).determinant = a

The signed determinant of ⟨a⟩ is a.

@[simp]

theorem TauCeti.IntegralLattice.rankOne_discriminant (a : ℤ) : (rankOne a).discriminant = a.natAbs

The nonnegative discriminant of ⟨a⟩ is |a|.

instance TauCeti.IntegralLattice.instIsNondegenerateRankOne (a : ℤ) [NeZero a] : (rankOne a).IsNondegenerate

Nonzero parameters give nondegenerate rank-one lattices.

theorem TauCeti.IntegralLattice.ofGramMatrix_singleton_eq_rankOne (a : ℤ) {c : ℤ} (hc : c = a) (h : (Matrix.of fun (x x_1 : Fin 1) => c).IsSymm) : ofGramMatrix (Module.Basis.singleton (Fin 1) ℚ) (Matrix.of fun (x x_1 : Fin 1) => c) h = rankOne a

The rank-one Gram-matrix lattice on the standard basis of ℚ with entry a is ⟨a⟩.

theorem TauCeti.IntegralLattice.rankOne_eq_neg_rankOne_neg (a : ℤ) : rankOne a = -rankOne (-a)

⟨a⟩ is the negative of ⟨-a⟩.

@[simp]

theorem TauCeti.IntegralLattice.isUnimodular_rankOne_iff (a : ℤ) : (rankOne a).IsUnimodular ↔ IsUnit a

The lattice ⟨a⟩ is unimodular exactly when a is a unit of ℤ.

theorem TauCeti.IntegralLattice.rankOne_two : rankOne 2 = a1

The positive rank-one root lattice is ⟨2⟩.

theorem TauCeti.IntegralLattice.rankOne_neg_two : rankOne (-2) = negativeA1

The negative rank-one root lattice is ⟨-2⟩.

theorem TauCeti.IntegralLattice.isPosDef_rankOne {a : ℤ} (ha : 0 < a) : (rankOne a).IsPosDef

A positive parameter gives a positive definite rank-one lattice.

theorem TauCeti.IntegralLattice.isNegDef_rankOne {a : ℤ} (ha : a < 0) : (rankOne a).IsNegDef

A negative parameter gives a negative definite rank-one lattice.

theorem TauCeti.IntegralLattice.rankOne_signature_of_pos {a : ℤ} (ha : 0 < a) : (rankOne a).signature = (1, 0, 0)

Positive rank-one lattices have signature (1,0,0).

theorem TauCeti.IntegralLattice.rankOne_signature_of_neg {a : ℤ} (ha : a < 0) : (rankOne a).signature = (0, 0, 1)

Negative rank-one lattices have signature (0,0,1).

@[simp]

theorem TauCeti.IntegralLattice.isPosDef_rankOne_iff (a : ℤ) : (rankOne a).IsPosDef ↔ 0 < a

Positive definiteness is equivalent to positivity of the parameter.

@[simp]

theorem TauCeti.IntegralLattice.isNegDef_rankOne_iff (a : ℤ) : (rankOne a).IsNegDef ↔ a < 0

Negative definiteness is equivalent to negativity of the parameter.

theorem TauCeti.IntegralLattice.isDegenerate_rankOne_zero : (rankOne 0).IsDegenerate

The zero parameter gives a degenerate rank-one lattice.

@[simp]

theorem TauCeti.IntegralLattice.rankOne_zero_signature : (rankOne 0).signature = (0, 1, 0)

The zero rank-one form has signature (0,1,0).