Characteristic vectors of symmetric bilinear forms

Let B be a symmetric bilinear form over a commutative ring R. A vector w is characteristic for B when B w x ≡ B x x modulo 2 for every x.

Suppose that c ^ 2 ≡ c modulo 2 for every c : R, as for ℤ and ℤ_[2]. Then x ↦ B x x is linear modulo 2, so a perfect symmetric form on a free module has a characteristic vector. Any two characteristic vectors differ by twice a vector, and therefore their self-pairings agree modulo 8. If b is an orthogonal basis, then ∑ i, b i is characteristic, and its self-pairing is the trace ∑ i, B (b i) (b i) of the diagonal Gram matrix. Consequently that trace modulo 8 is an isometry invariant of a perfect symmetric form with an orthogonal basis. Over ℤ_[2] these are the odd unimodular forms, and the invariant is their oddity, one of the entries of the Conway–Sloane 2-adic symbol.

Main definitions

• LinearMap.BilinForm.IsCharacteristic: w is characteristic for B.

Main results

• LinearMap.BilinForm.IsSymm.exists_isCharacteristic: a perfect symmetric form on a free module has a characteristic vector.
• LinearMap.BilinForm.Equivalent.forall_two_dvd_apply_self_iff: isometric forms are even together.
• LinearMap.BilinForm.IsCharacteristic.isCharacteristic_iff_exists_eq_add_two_smul: the characteristic vectors form a single coset of twice the module.
• LinearMap.BilinForm.IsCharacteristic.eight_dvd_apply_self_sub_apply_self: characteristic vectors have the same self-pairing modulo 8.
• LinearMap.BilinForm.IsCharacteristic.eight_dvd_apply_self_of_forall_two_dvd: for an even form these self-pairings are divisible by 8.
• LinearMap.BilinForm.Equivalent.eight_dvd_sum_apply_self_sub_sum_apply_self: isometric perfect symmetric forms with orthogonal bases have diagonal Gram matrices with the same trace modulo 8.

References

• J. Milnor and D. Husemoller, Symmetric Bilinear Forms, Chapter II and Appendix 4.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 15, §7.

def LinearMap.BilinForm.IsCharacteristic {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (w : M) : Prop

A vector w is characteristic for B when B w x is congruent to B x x modulo 2 for every x.

theorem LinearMap.BilinForm.isCharacteristic_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {w : M} : B.IsCharacteristic w ↔ ∀ (x : M), 2 ∣ (B w) x - (B x) x

The defining parity test for a characteristic vector.

@[simp]

theorem LinearMap.BilinForm.isCharacteristic_zero_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} : B.IsCharacteristic 0 ↔ ∀ (x : M), 2 ∣ (B x) x

Zero is characteristic exactly when every self-pairing is even.

theorem LinearMap.BilinForm.IsCharacteristic.add_two_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {w : M} (hw : B.IsCharacteristic w) (v : M) : B.IsCharacteristic (w + 2 • v)

Adding twice a vector to a characteristic vector gives a characteristic vector.

@[simp]

theorem LinearMap.BilinForm.isCharacteristic_add_two_smul_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {w : M} (v : M) : B.IsCharacteristic (w + 2 • v) ↔ B.IsCharacteristic w

Translation by twice a vector preserves and reflects the characteristic condition.

@[simp]

theorem LinearMap.BilinForm.isCharacteristic_neg_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {w : M} : B.IsCharacteristic (-w) ↔ B.IsCharacteristic w

Negation preserves and reflects the characteristic condition.

theorem LinearMap.BilinForm.IsCharacteristic.two_dvd_apply_sub {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {w w' : M} (hw : B.IsCharacteristic w) (hw' : B.IsCharacteristic w') (x : M) : 2 ∣ (B (w - w')) x

The difference of two characteristic vectors pairs evenly with every vector.

@[simp]

theorem LinearMap.BilinForm.IsometryEquiv.isCharacteristic_apply_iff {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] {B : LinearMap.BilinForm R M} {w : M} {C : LinearMap.BilinForm R M'} (f : B.IsometryEquiv C) : C.IsCharacteristic (f w) ↔ B.IsCharacteristic w

An isometry identifies the characteristic vectors of the two forms.

theorem LinearMap.BilinForm.Equivalent.forall_two_dvd_apply_self_iff {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R M'} (h : B.Equivalent C) : (∀ (x : M), 2 ∣ (B x) x) ↔ ∀ (y : M'), 2 ∣ (C y) y

Isometric forms are even together. 0 is characteristic for B exactly when it is for an isometric form, so 2 divides every B x x exactly when it divides every C y y.

theorem LinearMap.BilinForm.IsSymm.isCharacteristic_iff_forall_basis {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {w : M} (hB : B.IsSymm) (h2 : ∀ (c : R), 2 ∣ c ^ 2 - c) {ι : Type u_4} (b : Module.Basis ι R M) : B.IsCharacteristic w ↔ ∀ (i : ι), 2 ∣ (B w) (b i) - (B (b i)) (b i)

Characteristic vectors are tested on a basis. If c ^ 2 ≡ c modulo 2 for every c : R, then for a symmetric form it suffices to test the characteristic condition on the vectors of a basis.

theorem LinearMap.BilinForm.IsSymm.exists_isCharacteristic {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} [Module.Free R M] [IsPerfPair B] (hB : B.IsSymm) (h2 : ∀ (c : R), 2 ∣ c ^ 2 - c) : ∃ (w : M), B.IsCharacteristic w

Existence of characteristic vectors. If c ^ 2 ≡ c modulo 2 for every c : R, then a perfect symmetric form on a free module has a characteristic vector.

theorem LinearMap.BilinForm.IsCharacteristic.exists_eq_add_two_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {w w' : M} [Module.Free R M] [IsPerfPair B] (hw : B.IsCharacteristic w) (hw' : B.IsCharacteristic w') : ∃ (v : M), w' = w + 2 • v

Two characteristic vectors differ by twice a vector when the form is perfect and the module is free.

theorem LinearMap.BilinForm.IsCharacteristic.isCharacteristic_iff_exists_eq_add_two_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {w w' : M} [Module.Free R M] [IsPerfPair B] (hw : B.IsCharacteristic w) : B.IsCharacteristic w' ↔ ∃ (v : M), w' = w + 2 • v

The characteristic vectors form a coset of twice the module. For a perfect form on a free module, once w is characteristic, the characteristic vectors are exactly the vectors w + 2 • v.

theorem LinearMap.BilinForm.IsSymm.eight_dvd_apply_add_two_smul_sub {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {w : M} (hB : B.IsSymm) (hw : B.IsCharacteristic w) (v : M) : 8 ∣ (B (w + 2 • v)) (w + 2 • v) - (B w) w

Translating a characteristic vector by twice a vector changes its self-pairing by a multiple of 8.

theorem LinearMap.BilinForm.IsCharacteristic.eight_dvd_apply_self_sub_apply_self {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {w w' : M} [Module.Free R M] [IsPerfPair B] (hB : B.IsSymm) (hw : B.IsCharacteristic w) (hw' : B.IsCharacteristic w') : 8 ∣ (B w') w' - (B w) w

The self-pairing of a characteristic vector is well defined modulo 8. For a perfect symmetric form on a free module, any two characteristic vectors have self-pairings congruent modulo 8.

theorem LinearMap.BilinForm.IsCharacteristic.eight_dvd_apply_self_of_forall_two_dvd {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {w : M} [Module.Free R M] [IsPerfPair B] (hw : B.IsCharacteristic w) (heven : ∀ (x : M), 2 ∣ (B x) x) : 8 ∣ (B w) w

Even forms have characteristic norms divisible by 8. If 2 divides every B x x, then 0 is characteristic, so for a perfect form on a free module every characteristic vector has self-pairing divisible by 8.

theorem LinearMap.BilinForm.iIsOrtho.isCharacteristic_sum {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {ι : Type u_4} [Fintype ι] (h2 : ∀ (c : R), 2 ∣ c ^ 2 - c) {b : Module.Basis ι R M} (hb : B.iIsOrtho ⇑b) : B.IsCharacteristic (∑ i : ι, b i)

The sum of an orthogonal basis is characteristic when c ^ 2 ≡ c modulo 2 for every c : R.

theorem LinearMap.BilinForm.Equivalent.eight_dvd_sum_apply_self_sub_sum_apply_self {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] {B : LinearMap.BilinForm R M} {ι : Type u_4} [Fintype ι] {C : LinearMap.BilinForm R M'} (h : B.Equivalent C) [IsPerfPair B] (h2 : ∀ (c : R), 2 ∣ c ^ 2 - c) {κ : Type u_5} [Fintype κ] {b : Module.Basis ι R M} {c : Module.Basis κ R M'} (hb : B.iIsOrtho ⇑b) (hc : C.iIsOrtho ⇑c) : 8 ∣ ∑ j : κ, (C (c j)) (c j) - ∑ i : ι, (B (b i)) (b i)

The trace of a diagonal Gram matrix modulo 8 is an isometry invariant. Let c ^ 2 ≡ c modulo 2 for every c : R, as over ℤ and ℤ_[2]. If a perfect form B is isometric to C, and b and c are orthogonal bases for B and C, then the traces ∑ i, B (b i) (b i) and ∑ j, C (c j) (c j) agree modulo 8. Over ℤ_[2] this is the invariance of the oddity of an odd unimodular form.