Unimodular symmetric forms and Jordan splittings over Henselian local rings

Over a Henselian local ring with finite residue field and two invertible, symmetric forms with unit Gram determinant are classified by their rank and their determinant modulo squares. The determinant may be computed in any caller-provided basis. The conclusion is an isometry over the coefficient ring, preserving the bilinear forms themselves.

Diagonalization over the local ring gives an orthogonal basis with unit coefficients. The unit diagonal classification then identifies the forms. This applies to ℤ_p for odd p, including forms which arise by localizing an integral lattice that is unimodular only at p.

Such a form is already determined by its reduction modulo the maximal ideal: if a linear map carries one form to the other modulo 𝔪, the two determinants differ by a unit whose residue is a square, hence by a square. Applied to the unimodular rescalings of the constituents of two Jordan splittings, compared through the projections between them, this shows that the constituents of a Jordan splitting are unique up to isometry, and that a symmetric form over a Henselian local domain with finite residue field and two invertible is classified by the isometry classes of its Jordan constituents, that is, by the rank and the determinant square class of each of them.

Main results

• LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det: unimodular forms are classified by rank and determinant square class.
• LinearMap.BilinForm.IsSymm.equivalent_of_sub_mem_maximalIdeal: unimodular forms which agree modulo the maximal ideal up to a linear map are isometric.
• LinearMap.BilinForm.IsJordanSplitting.equivalent_restrict_of_equivalent: isometric forms have isometric Jordan constituents at every index.
• LinearMap.BilinForm.IsJordanSplitting.equivalent_iff_forall_equivalent_restrict: forms are isometric exactly when their Jordan constituents are.

References

• O. T. O'Meara, Introduction to Quadratic Forms, 92:1--92:2.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 8.

theorem LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [HenselianLocalRing R] [Finite (IsLocalRing.ResidueField R)] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R N} (hB : B.IsSymm) (hC : C.IsSymm) (h2 : IsUnit 2) {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)

Unimodular classification at odd residue characteristic. Symmetric forms with unit Gram determinants on modules with bases of the same size are integrally isometric exactly when the product of those determinants is a square. The bases and hence the determinant representatives are arbitrary; positive rank is not required.

theorem LinearMap.BilinForm.IsSymm.equivalent_of_sub_mem_maximalIdeal {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [HenselianLocalRing R] [Finite (IsLocalRing.ResidueField R)] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {C : LinearMap.BilinForm R M} {C' : LinearMap.BilinForm R N} (hC : C.IsSymm) (hC' : C'.IsSymm) (h2 : IsUnit 2) {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) : C.Equivalent C'

A unimodular form is determined by its reduction. Let C and C' be symmetric forms with unit Gram determinants in bases of the same size, over a Henselian local ring with finite residue field and two invertible. If a linear map φ carries C' to C modulo the maximal ideal, that is C' x y - C (φ x) (φ y) ∈ 𝔪 for all x and y, then C and C' are isometric.

theorem LinearMap.BilinForm.IsJordanSplitting.equivalent_restrict_of_equivalent {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [HenselianLocalRing R] [Finite (IsLocalRing.ResidueField R)] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsDomain R] {B : LinearMap.BilinForm R M} {B' : LinearMap.BilinForm R N} {π : R} {S : ℕ → Submodule R M} {S' : ℕ → Submodule R N} [Module.Free R M] [Module.Finite R M] (hS : B.IsJordanSplitting π S) (hS' : B'.IsJordanSplitting π S') (hB : B.IsSymm) (h2 : IsUnit 2) (hπ : π ≠ 0) (hπ' : ¬IsUnit π) (hBB' : B.Equivalent B') (j : ℕ) : (B.restrict (S j)).Equivalent (B'.restrict (S' j))

Jordan constituents are unique up to isometry at odd residue characteristic. Over a Henselian local domain with finite residue field and two invertible, let B be a symmetric form on a finite free module, isometric to a form B'. Then for Jordan splittings S of B and S' of B' with respect to the same nonzero non-unit π, the constituents S j and S' j are isometric at every index j. In particular the constituents of a Jordan splitting do not depend on the splitting up to isometry.

theorem LinearMap.BilinForm.IsJordanSplitting.equivalent_iff_forall_equivalent_restrict {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [HenselianLocalRing R] [Finite (IsLocalRing.ResidueField R)] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsDomain R] {B : LinearMap.BilinForm R M} {B' : LinearMap.BilinForm R N} {π : R} {S : ℕ → Submodule R M} {S' : ℕ → Submodule R N} [Module.Free R M] [Module.Finite R M] (hS : B.IsJordanSplitting π S) (hS' : B'.IsJordanSplitting π S') (hB : B.IsSymm) (h2 : IsUnit 2) (hπ : π ≠ 0) (hπ' : ¬IsUnit π) : B.Equivalent B' ↔ ∀ (j : ℕ), (B.restrict (S j)).Equivalent (B'.restrict (S' j))

Jordan splittings classify forms at odd residue characteristic. Over a Henselian local domain with finite residue field and two invertible, let B be a symmetric form on a finite free module, and let S and S' be Jordan splittings of B and B' with respect to the same nonzero non-unit π. Then B and B' are isometric exactly when their constituents of each index are isometric. Each constituent is π ^ j times a unimodular form, classified by its rank and the square class of its determinant (LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det).