Even unimodular forms over Henselian local rings with residue field 𝔽₂

Let R be a Henselian local ring whose residue field has two elements, for instance ℤ_[2]. A symmetric bilinear form B over R is even when 2 divides every value B x x. This file classifies the even unimodular forms, which are the unimodular Jordan constituents of type II at the dyadic prime.

The binary forms come first. If B x y is a unit, then B has a pair e, f whose Gram matrix is either the hyperbolic plane !![0, 1; 1, 0] or !![2, 1; 1, 2]. Two orthogonal copies of !![2, 1; 1, 2] contain a hyperbolic pair, so an even unimodular form of rank at least four splits off a hyperbolic plane. Consequently, if -3 is not a square in R, two even unimodular forms of the same rank are isometric exactly when the product of their Gram determinants is a square. The hypothesis on -3 separates the two binary forms, whose determinants are -1 and 3.

Such a form is determined by its reduction, with no hypothesis on -3: if a linear map carries one even unimodular form to another modulo 𝔪, and their self-pairings modulo 2𝔪, then the forms are isometric. This is what makes a dyadic Jordan constituent of type II between neighbours of type II unique up to isometry (LinearMap.BilinForm.IsJordanSplitting.equivalent_restrict_of_equivalent_of_even).

This is the even half of the classification of unimodular lattices over ℤ₂; the odd unimodular forms, which are diagonalizable, are not treated here. The analogous statement when 2 is a unit is LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det.

Main results

• LinearMap.BilinForm.IsSymm.exists_hyperbolic_or_exists_two_one_one_two: a symmetric even form with a unit value B x y has a pair with Gram matrix !![0, 1; 1, 0] or !![2, 1; 1, 2].
• LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det_of_even: even unimodular forms of the same rank are isometric exactly when the product of their Gram determinants is a square.
• LinearMap.BilinForm.IsSymm.equivalent_of_sub_mem_maximalIdeal_of_even: even unimodular forms which agree up to a linear map modulo 𝔪, and on the diagonal modulo 2𝔪, are isometric.
• LinearMap.BilinForm.IsJordanSplitting.equivalent_restrict_of_equivalent_of_even: a dyadic Jordan constituent of type II whose neighbours are of type II is unique up to isometry.
• LinearMap.BilinForm.IsJordanSplitting.equivalent_iff_forall_equivalent_restrict_of_even: forms with a dyadic Jordan splitting all of whose constituents are of type II are isometric exactly when their constituents of each index are.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §93, for unimodular lattices over dyadic local rings, and 93:28 for the classification of lattices over unramified dyadic local rings.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 8, for integral forms over ℤ_2.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 15, §7, for the trains of a 2-adic symbol: a constituent of type II between constituents of type II forms a train by itself, so its sign is an invariant.

theorem LinearMap.BilinForm.IsSymm.exists_hyperbolic_or_exists_two_one_one_two {R : Type u_1} {M : Type u_2} [CommRing R] [HenselianLocalRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hR : Nat.card (IsLocalRing.ResidueField R) = 2) (hB : B.IsSymm) (heven : ∀ (x : M), 2 ∣ (B x) x) {x y : M} (hxy : IsUnit ((B x) y)) : ∃ (e : M) (f : M), (B e) f = 1 ∧ ((B e) e = 0 ∧ (B f) f = 0 ∨ (B e) e = 2 ∧ (B f) f = 2)

Binary even unimodular forms in residue characteristic two. Over a Henselian local ring whose residue field has two elements, let B be a symmetric form with every B x x divisible by 2. If B x y is a unit, then B has a pair e, f with B e f = 1 whose Gram matrix is either the hyperbolic plane !![0, 1; 1, 0] or !![2, 1; 1, 2].

theorem LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det_of_even {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [HenselianLocalRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R N} (hR : Nat.card (IsLocalRing.ResidueField R) = 2) (h3 : ¬IsSquare (-3)) (hB : B.IsSymm) (hC : C.IsSymm) (hBeven : ∀ (x : M), 2 ∣ (B x) x) (hCeven : ∀ (x : N), 2 ∣ (C x) x) {n : ℕ} (b : Module.Basis (Fin n) R M) (c : Module.Basis (Fin n) R N) (hBdet : IsUnit ((toMatrix b) B).det) (hCdet : IsUnit ((toMatrix c) C).det) : B.Equivalent C ↔ IsSquare (((toMatrix b) B).det * ((toMatrix c) C).det)

Classification of even unimodular forms in residue characteristic two. Let R be a Henselian local ring whose residue field has two elements and in which -3 is not a square, for instance ℤ_[2]. Two symmetric forms with every B x x divisible by 2 and with unit Gram determinants in bases of the same size are isometric exactly when the product of those determinants is a square.

theorem LinearMap.BilinForm.IsSymm.equivalent_of_sub_mem_maximalIdeal_of_even {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [HenselianLocalRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (hR : Nat.card (IsLocalRing.ResidueField R) = 2) {C : LinearMap.BilinForm R M} {C' : LinearMap.BilinForm R N} (hC : C.IsSymm) (hC' : C'.IsSymm) (heven : ∀ (x : M), 2 ∣ (C x) x) {n : ℕ} (b : Module.Basis (Fin n) R M) (b' : Module.Basis (Fin n) R N) (hdet : IsUnit ((toMatrix b) C).det) (hdet' : IsUnit ((toMatrix b') C').det) (φ : N →ₗ[R] M) (hφ : ∀ (x y : N), (C' x) y - (C (φ x)) (φ y) ∈ IsLocalRing.maximalIdeal R) (hφ₂ : ∀ (x : N), (C' x) x - (C (φ x)) (φ x) ∈ Ideal.span {2} * IsLocalRing.maximalIdeal R) : C.Equivalent C'

An even unimodular form is determined by its reduction. Let R be a Henselian local ring whose residue field has two elements, for instance ℤ_[2], and let C and C' be symmetric forms with unit Gram determinants in bases of the same size, with every C x x divisible by 2. If a linear map φ carries C' to C modulo 𝔪, and the self-pairings modulo 2𝔪, that is C' x y - C (φ x) (φ y) ∈ 𝔪 and C' x x - C (φ x) (φ x) ∈ 2𝔪 for all x and y, then C and C' are isometric. Thus C is determined by its reduction modulo 𝔪 together with its self-pairings modulo 2𝔪; when 2 is a non-zero-divisor, as in ℤ_[2], these amount to the residue of the quadratic form x ↦ C x x / 2. The condition on the diagonal cannot be dropped: !![0, 1; 1, 0] and !![2, 1; 1, 2] agree modulo 2, but they are not isometric over ℤ_[2].

theorem LinearMap.BilinForm.IsJordanSplitting.equivalent_restrict_of_equivalent_of_even {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [HenselianLocalRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsDomain R] {B : LinearMap.BilinForm R M} {B' : LinearMap.BilinForm R N} {S : ℕ → Submodule R M} {S' : ℕ → Submodule R N} (hR : Nat.card (IsLocalRing.ResidueField R) = 2) (h20 : 2 ≠ 0) [Module.Free R M] [Module.Finite R M] (hS : B.IsJordanSplitting 2 S) (hS' : B'.IsJordanSplitting 2 S') (hB : B.IsSymm) (hBB' : B.Equivalent B') {j : ℕ} (hj : ∀ x ∈ S j, 2 ^ (j + 1) ∣ (B x) x) (hprev : ∀ x ∈ S (j - 1), 2 ^ j ∣ (B x) x) (hnext : ∀ x ∈ S (j + 1), 2 ^ (j + 2) ∣ (B x) x) : (B.restrict (S j)).Equivalent (B'.restrict (S' j))

Dyadic Jordan constituents of type II between constituents of type II are unique. Let R be a Henselian local domain whose residue field has two elements and in which 2 ≠ 0, for instance ℤ_[2]. Let B be a symmetric form on a finite free module, isometric to a form B', and let S and S' be Jordan splittings of B and B' with respect to 2. Suppose that the constituent S j is even at its own scale (of type II), and so are its neighbours S (j - 1) and S (j + 1); the condition on S (j - 1) is vacuous for j = 0, and zero constituents are of type II. Then the constituents S j and S' j are isometric.

Without the condition on the neighbours, constituents of type II are not unique: over ℤ_[2] the forms !![0, 1; 1, 0] ⊥ ⟨2⟩ and !![2, 1; 1, 2] ⊥ ⟨-6⟩ are isometric, while their constituents !![0, 1; 1, 0] and !![2, 1; 1, 2] of index 0, both of type II, are not: the ratio -3 of their determinants is not a square. Here the neighbour ⟨2⟩ is of type I.

theorem LinearMap.BilinForm.IsJordanSplitting.equivalent_iff_forall_equivalent_restrict_of_even {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [HenselianLocalRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsDomain R] {B : LinearMap.BilinForm R M} {B' : LinearMap.BilinForm R N} {S : ℕ → Submodule R M} {S' : ℕ → Submodule R N} (hR : Nat.card (IsLocalRing.ResidueField R) = 2) (h20 : 2 ≠ 0) [Module.Free R M] [Module.Finite R M] (hS : B.IsJordanSplitting 2 S) (hS' : B'.IsJordanSplitting 2 S') (hB : B.IsSymm) (heven : ∀ (j : ℕ), ∀ x ∈ S j, 2 ^ (j + 1) ∣ (B x) x) : B.Equivalent B' ↔ ∀ (j : ℕ), (B.restrict (S j)).Equivalent (B'.restrict (S' j))

Classification of dyadic forms whose Jordan constituents are all of type II. Let R be a Henselian local domain whose residue field has two elements and in which 2 ≠ 0, for instance ℤ_[2], and let B be a symmetric form on a finite free module with a Jordan splitting S with respect to 2 in which every constituent is even at its own scale. Then B is isometric to a form B' with a Jordan splitting S' exactly when their constituents of each index are isometric. Over ℤ_[2] the constituents are classified by their rank and determinant square class (LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det_of_even).