The genus of an integral lattice

Two integral lattices have the same genus when their real signatures agree and their integral localizations are isometric at every prime. This relation also makes sense for degenerate forms. The local condition concerns the actual forms on ℤ_p ⊗[ℤ] L, rather than just their extensions to ℚ_p.

The genus determines the signed determinant. Integral local isometry at p changes the determinant by the square of a unit of ℤ_p, so the absolute determinants have the same p-adic valuation at every prime and are therefore equal. The real signature fixes the sign, since the signed determinant is (-1) ^ n₋ times the absolute determinant. For nondegenerate lattices the absolute determinant is the order of the discriminant group Lᵛ / L, so the genus also determines that order.

The scale and norm ideals are genus invariants in the same way: their extensions to ℤ_p are the scale and norm ideals of the localization, and an ideal of ℤ is determined by its extensions to all ℤ_p.

For lattices with equal nonzero signed determinants, the local tests reduce to the finite set of prime factors of twice the absolute determinant. Outside that set, the local determinants are units at an odd prime, so the rank and determinant classification gives an isometry. The signature equality already supplies the rank equality.

The genus also fixes the rational quadratic space at every place. An integral local isometry extends to the completions, so lattices in one genus have isometric completed rational spaces ℚ_p ⊗[ℚ] V at every prime, while at the real place their signatures agree by definition. Combining these local isometries into an isometry of the rational forms over ℚ is the Hasse–Minkowski theorem and is not done here. Conversely, for lattices whose rational forms are isometric, the signature condition holds automatically, and the genus is decided by the integral localizations alone.

Main results

• TauCeti.IntegralLattice.SameGenus.determinant_eq: the genus determines the signed determinant.
• TauCeti.IntegralLattice.SameGenus.natCard_discriminantGroup_eq: lattices in one genus have discriminant groups of the same order.
• TauCeti.IntegralLattice.SameGenus.isEven_iff: lattices in one genus are even together.
• TauCeti.IntegralLattice.SameGenus.scaleIdeal_eq and TauCeti.IntegralLattice.SameGenus.normIdeal_eq: lattices in one genus have the same scale and norm ideals.
• TauCeti.IntegralLattice.SameGenus.completedRationalForm_equivalent: lattices in one genus have isometric completed rational spaces at every prime.
• TauCeti.IntegralLattice.sameGenus_iff_localIntegralForm_equivalent_primeFactors: for equal nonzero determinants, only the primes dividing twice the determinant need checking.
• TauCeti.IntegralLattice.sameGenus_iff_localIntegralForm_equivalent: on isometric rational spaces, the genus is decided by integral local isometry.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Chapter IX, for genera of lattices and the odd-prime unimodular classification.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 8, for integral local equivalence.

def TauCeti.IntegralLattice.SameGenus {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) : Prop

Two integral lattices have the same genus if their signatures agree and their integral local forms are isometric at every prime. No nondegeneracy assumption is imposed.

theorem TauCeti.IntegralLattice.sameGenus_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) : L.SameGenus M ↔ L.signature = M.signature ∧ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], (L.localIntegralForm p).Equivalent (M.localIntegralForm p)

The signature and integral local isometry conditions characterizing the genus relation.

theorem TauCeti.IntegralLattice.SameGenus.signature_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : L.signature = M.signature

Lattices in the same genus have equal real signatures.

theorem TauCeti.IntegralLattice.SameGenus.localIntegralForm_equivalent {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) (p : ℕ) [Fact (Nat.Prime p)] : (L.localIntegralForm p).Equivalent (M.localIntegralForm p)

Lattices in the same genus have isometric integral localizations at every prime.

theorem TauCeti.IntegralLattice.SameGenus.finrank_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : Module.finrank ℤ ↥L.carrier = Module.finrank ℤ ↥M.carrier

Lattices in the same genus have equal ranks.

theorem TauCeti.IntegralLattice.SameGenus.sigPos_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : L.sigPos = M.sigPos

Lattices in the same genus have the same positive index.

theorem TauCeti.IntegralLattice.SameGenus.sigNull_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : L.sigNull = M.sigNull

Lattices in the same genus have the same null index.

theorem TauCeti.IntegralLattice.SameGenus.sigNeg_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : L.sigNeg = M.sigNeg

Lattices in the same genus have the same negative index.

theorem TauCeti.IntegralLattice.SameGenus.nonempty_linearEquiv {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : Nonempty (V ≃ₗ[ℚ] W)

Lattices in the same genus have isomorphic ambient spaces.

theorem TauCeti.IntegralLattice.SameGenus.isPosDef_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : L.IsPosDef ↔ M.IsPosDef

Positive definiteness is a property of the genus.

theorem TauCeti.IntegralLattice.SameGenus.isNegDef_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : L.IsNegDef ↔ M.IsNegDef

Negative definiteness is a property of the genus.

theorem TauCeti.IntegralLattice.SameGenus.isEven_iff {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : L.IsEven ↔ M.IsEven

Evenness is a genus invariant. Lattices in one genus have isometric dyadic localizations, and a lattice is even exactly when its dyadic localization is.

theorem TauCeti.IntegralLattice.SameGenus.scaleIdeal_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : L.scaleIdeal = M.scaleIdeal

The scale ideal is a genus invariant.

theorem TauCeti.IntegralLattice.SameGenus.normIdeal_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : L.normIdeal = M.normIdeal

The norm ideal is a genus invariant.

@[simp]

theorem TauCeti.IntegralLattice.SameGenus.refl {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.SameGenus L

Every integral lattice belongs to its own genus.

theorem TauCeti.IntegralLattice.SameGenus.symm {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : M.SameGenus L

The genus relation is symmetric.

theorem TauCeti.IntegralLattice.SameGenus.trans {V : Type u_1} {W : Type u_2} {U : Type u_3} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] [AddCommGroup U] [Module ℚ U] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} (h : L.SameGenus M) (h' : M.SameGenus N) : L.SameGenus N

The genus relation is transitive.

theorem TauCeti.IntegralLattice.SameGenus.determinant_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : L.determinant = M.determinant

Lattices in the same genus have equal signed determinants. No nondegeneracy assumption is needed: degenerate lattices in one genus both have determinant zero.

theorem TauCeti.IntegralLattice.SameGenus.natCard_discriminantGroup_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} [L.IsNondegenerate] (h : L.SameGenus M) : Nat.card L.DiscriminantGroup = Nat.card M.DiscriminantGroup

Lattices in one genus have discriminant groups of the same order.

theorem TauCeti.IntegralLattice.SameGenus.smul {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} {n : ℤ} (hn : n ≠ 0) (h : L.SameGenus M) : (n • L).SameGenus (n • M)

Scaling by a common nonzero integer preserves the genus relation.

theorem TauCeti.IntegralLattice.SameGenus.completedRationalForm_equivalent {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) (p : ℕ) [Fact (Nat.Prime p)] : (L.completedRationalForm p).Equivalent (M.completedRationalForm p)

Lattices in the same genus have isometric completed rational spaces: at every prime p the quadratic spaces ℚ_p ⊗[ℚ] V and ℚ_p ⊗[ℚ] W are isometric, since the integral local isometry extends to the completions.

theorem TauCeti.IntegralLattice.Isometry.sameGenus {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.SameGenus M

An integral-lattice isometry preserves the genus.

theorem TauCeti.IntegralLattice.sameGenus_iff_localIntegralForm_equivalent_primeFactors {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (hdet : L.determinant = M.determinant) (hdet0 : L.determinant ≠ 0) : L.SameGenus M ↔ L.signature = M.signature ∧ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], p ∈ (2 * L.determinant.natAbs).primeFactors → (L.localIntegralForm p).Equivalent (M.localIntegralForm p)

For lattices with equal nonzero signed determinants, equal signatures and integral local isometry at the prime factors of twice the absolute determinant characterize the genus. This is a finite family of local isometry conditions; no local classification at its primes is assumed.

theorem TauCeti.IntegralLattice.sameGenus_iff_localIntegralForm_equivalent {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (hform : L.form.Equivalent M.form) : L.SameGenus M ↔ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], (L.localIntegralForm p).Equivalent (M.localIntegralForm p)

On isometric rational spaces the genus is decided by the integral localizations. If the rational forms of L and M are isometric, then L and M lie in one genus exactly when their integral localizations are isometric at every prime: the rational isometry already supplies the equality of signatures.