Jordan splittings over a discrete valuation ring

Let R be a discrete valuation ring with uniformizer π. A Jordan splitting of a bilinear form B on an R-module M is a decomposition M = ⊕_i N_i into pairwise orthogonal submodules such that the restriction of B to N_i is π ^ i-modular: π ^ i times a perfect pairing (LinearMap.BilinForm.IsJordanSplitting). Thus each N_i carries the form π ^ i • C_i for a perfect pairing C_i; this is the Jordan decomposition of O'Meara 91C.

The main result is that every nondegenerate symmetric bilinear form on a finite module has a Jordan splitting (LinearMap.BilinForm.IsSymm.exists_isJordanSplitting). The constituents separate the form into its valuation scales, reducing its analysis to perfect pairings at each scale. This decomposition supports the local analysis and classification of integral forms, including the dyadic case, for instance R = ℤ_2, where constituents need not be diagonalizable.

A Jordan splitting is not unique, but the ranks of its constituents are invariants of the form (LinearMap.BilinForm.IsJordanSplitting.finrank_eq), and hence of its isometry class (LinearMap.BilinForm.IsJordanSplitting.finrank_eq_of_equivalent). This holds over every local domain R and every nonzero non-unit π, in particular at the dyadic prime. The vectors x with π ^ j ∣ B x y for all y are, modulo π M, exactly the sums of vectors of the constituents of index at least j. By Nakayama's lemma the sum of these constituents therefore has the same rank for any two splittings, and the rank of the j-th constituent is a difference of two such ranks.

On these vectors x, the form B agrees modulo π ^ (j + 1) with its values on the projections to the constituent N j (LinearMap.BilinForm.IsJordanSplitting.exists_pow_succ_dvd_sub): the form π ^ (-j) B modulo π factors through the residue form of the unimodular rescaling of N j. Comparing two splittings through these projections shows that their unimodular rescalings at each index have the same residue forms, which reduces the isometry of their constituents to that of these rescalings (LinearMap.BilinForm.IsJordanSplitting.equivalent_restrict_of_forall_unimodular). For symmetric forms on finite free modules over a Henselian local domain with finite residue field and two invertible, this decides their isometry class (LinearMap.BilinForm.IsJordanSplitting.equivalent_restrict_of_equivalent in TauCeti.LinearAlgebra.BilinearForm.Henselian). Without the Henselian hypothesis it fails: over ℤ localized at 3, the rank-one forms ⟨1⟩ and ⟨7⟩ have the same residue form but are not isometric.

When the neighbouring constituents N (j - 1) and N (j + 1) are even at their own scales, the self-pairings B x x of these vectors also agree with those of their projections modulo π ^ (j + 2). At π = 2 this is the extra precision that decides the isometry class of a dyadic constituent of type II between constituents of type II (LinearMap.BilinForm.IsJordanSplitting.equivalent_restrict_of_equivalent_of_even in TauCeti.LinearAlgebra.BilinearForm.Even.Henselian).

Main definitions

• LinearMap.BilinForm.IsJordanSplitting: a family N : ℕ → Submodule R M is a Jordan splitting of B with respect to π.

Main results

• LinearMap.BilinForm.IsJordanSplitting.hasFiniteSupport, LinearMap.BilinForm.IsJordanSplitting.finite_support_finrank: a finitely generated module has only finitely many nonzero Jordan constituents, hence only finitely many of nonzero rank.
• LinearMap.BilinForm.IsSymm.exists_isJordanSplitting: Jordan splittings exist.
• LinearMap.BilinForm.IsJordanSplitting.finrank_eq: any two Jordan splittings have constituents of equal rank.
• LinearMap.BilinForm.IsJordanSplitting.finrank_eq_of_equivalent: the ranks of the constituents are invariants of the isometry class of the form.
• LinearMap.BilinForm.IsJordanSplitting.finite, LinearMap.BilinForm.IsJordanSplitting.free: the constituents of a Jordan splitting of a finite module are finite, and over a local ring the constituents of a Jordan splitting of a finite flat module are free.
• LinearMap.BilinForm.IsJordanSplitting.finrank_biSup_Iic: the rank of the sum of the constituents of index at most j is the sum of their ranks.
• LinearMap.BilinForm.IsJordanSplitting.exists_pow_succ_dvd_sub: on the vectors pairing into π ^ j R, the form is congruent modulo π ^ (j + 1) to its pullback along the projection to the j-th constituent, and between neighbours even at their own scales its self-pairings are congruent modulo π ^ (j + 2).
• LinearMap.BilinForm.IsJordanSplitting.equivalent_restrict_of_forall_unimodular: through these congruences, the isometry of two constituents of isometric forms reduces to that of their unimodular rescalings.
• LinearMap.BilinForm.IsJordanSplitting.isCompl_biSup_Iic_biSup_Ici: the constituents of index at most j and those of index above j span complementary submodules.
• LinearMap.BilinForm.IsJordanSplitting.pow_succ_dvd_sub_apply_projectionOnto and LinearMap.BilinForm.IsJordanSplitting.two_mul_pow_succ_dvd_sub_apply_projectionOnto: projecting to the constituents of index at most j preserves the form modulo π ^ (j + 1), and the self-pairings modulo 2 * π ^ (j + 1) when 2 ∣ π and the constituent of index j + 1 is even at its own scale.
• LinearMap.BilinForm.IsJordanSplitting.exists_basis_restrict_biSup_Iic: the constituents of index at most j have a Gram matrix G and a symmetric H with G * H = π ^ j • 1.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §91C, for Jordan splittings, and 91:9, for the invariance of the ranks of their constituents.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 8, Lemma 4.1 and Theorem 4.1.

structure LinearMap.BilinForm.IsJordanSplitting {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (π : R) (N : ℕ → Submodule R M) : Prop

A family N of submodules is a Jordan splitting of B with respect to π when M is the internal direct sum of the N i, these are pairwise orthogonal, and the restriction of B to N i is π ^ i-modular.

• isInternal : DirectSum.IsInternal N

  The module is the internal direct sum of the constituents.

• apply_eq_zero (i j : ℕ) : i ≠ j → ∀ x ∈ N i, ∀ y ∈ N j, (B x) y = 0

  Distinct constituents are orthogonal.

• isModular (i : ℕ) : (B.restrict (N i)).IsModular (π ^ i)

  The i-th constituent is π ^ i-modular.

theorem LinearMap.BilinForm.IsJordanSplitting.congr {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {M' : Type u_3} [AddCommMonoid M'] [Module R M'] {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) (e : M ≃ₗ[R] M') : ((BilinForm.congr e) B).IsJordanSplitting π fun (i : ℕ) => Submodule.map (↑e) (N i)

A Jordan splitting is transported by a linear equivalence, mapping every constituent.

@[simp]

theorem LinearMap.BilinForm.isJordanSplitting_congr_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {M' : Type u_3} [AddCommMonoid M'] [Module R M'] {π : R} {N : ℕ → Submodule R M} (e : M ≃ₗ[R] M') : (((congr e) B).IsJordanSplitting π fun (i : ℕ) => Submodule.map (↑e) (N i)) ↔ B.IsJordanSplitting π N

Jordan splitting is invariant under a linear equivalence of the underlying module.

theorem LinearMap.BilinForm.IsJordanSplitting.map_isometryEquiv {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {M' : Type u_3} [AddCommMonoid M'] [Module R M'] {B' : LinearMap.BilinForm R M'} {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) (e : B.IsometryEquiv B') : B'.IsJordanSplitting π fun (i : ℕ) => Submodule.map (↑e.toLinearEquiv) (N i)

A Jordan splitting is transported along an isometry, mapping every constituent.

theorem LinearMap.BilinForm.IsJordanSplitting.pow_dvd_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) {i : ℕ} {x : M} (hx : x ∈ N i) (y : M) : π ^ i ∣ (B x) y

Every value of B at a vector of the constituent N i of a Jordan splitting is divisible by π ^ i.

theorem LinearMap.BilinForm.IsJordanSplitting.apply_dfinsuppSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} [(i : ℕ) → (x : ↥(N i)) → Decidable (x ≠ 0)] (h : B.IsJordanSplitting π N) (f : Π₀ (i : ℕ), ↥(N i)) (i : ℕ) (y : ↥(N i)) : (B (f.sum fun (x : ℕ) (z : ↥(N x)) => ↑z)) ↑y = (B ↑(f i)) ↑y

Pairing a recomposed vector with the i-th constituent only sees its i-th component.

theorem LinearMap.BilinForm.IsJordanSplitting.hasFiniteSupport {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} [Module.Finite R M] {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) : {i : ℕ | N i ≠ ⊥}.Finite

A Jordan splitting of a finitely generated module has finitely many nonzero constituents.

theorem LinearMap.BilinForm.IsJordanSplitting.finite_support_finrank {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} [Nontrivial R] [Module.Finite R M] {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) : (Function.support fun (i : ℕ) => Module.finrank R ↥(N i)).Finite

A Jordan splitting of a finitely generated module has finitely many constituents of nonzero rank.

theorem LinearMap.BilinForm.IsModular.isJordanSplitting {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {i : ℕ} (h : B.IsModular (π ^ i)) : B.IsJordanSplitting π fun (j : ℕ) => if j = i then ⊤ else ⊥

A modular form is its own Jordan splitting. A π ^ i-modular form has the Jordan splitting whose constituent of index i is the whole module and whose other constituents are zero.

theorem LinearMap.BilinForm.isJordanSplitting_reverse {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {N : ℕ → Submodule R M} {π : R} (hN : DirectSum.IsInternal N) {D : LinearMap.BilinForm R M} {m : ℕ} (htop : ∀ (i : ℕ), m < i → N i = ⊥) (horth : ∀ (i k : ℕ), i ≠ k → ∀ x ∈ N i, ∀ y ∈ N k, (D x) y = 0) (hmod : ∀ k ≤ m, (D.restrict (N (m - k))).IsModular (π ^ k)) : D.IsJordanSplitting π fun (k : ℕ) => if k ≤ m then N (m - k) else ⊥

Reversing a Jordan splitting. Let N be an internal direct sum decomposition of M with N i = ⊥ for i > m, and let D be a form for which the N i are orthogonal and N (m - k) is π ^ k-modular for k ≤ m. Then k ↦ N (m - k), extended by ⊥, is a Jordan splitting of D.

theorem LinearMap.BilinForm.IsSymm.exists_isJordanSplitting {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} [IsDomain R] [IsDiscreteValuationRing R] [Module.Finite R M] (hB : B.IsSymm) (hnd : B.Nondegenerate) {π : R} (hπ : Irreducible π) : ∃ (N : ℕ → Submodule R M), B.IsJordanSplitting π N

Jordan splittings exist. Over a discrete valuation ring with uniformizer π, every nondegenerate symmetric bilinear form on a finite module is an orthogonal direct sum of submodules N i on which the form is π ^ i-modular. Nondegeneracy forces the module to be torsion-free.

Uniqueness of the ranks of the constituents

theorem LinearMap.BilinForm.IsJordanSplitting.pow_dvd_apply_of_mem_biSup {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) {j : ℕ} {x : M} (hx : x ∈ ⨆ i ∈ Set.Ici j, N i) (y : M) : π ^ j ∣ (B x) y

The vectors of the constituents of index at least j of a Jordan splitting pair into π ^ j R.

theorem LinearMap.BilinForm.IsJordanSplitting.mem_biSup_sup_smul_top {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) (hπ : π ∈ nonZeroDivisors R) {j : ℕ} {x : M} (hx : ∀ (y : M), π ^ j ∣ (B x) y) : x ∈ (⨆ i ∈ Set.Ici j, N i) ⊔ Ideal.span {π} • ⊤

A vector pairing into π ^ j R lies in the constituents of index at least j, modulo π. If π is a non-zero-divisor and every value B x y is divisible by π ^ j, then x is the sum of a vector of the constituents of index at least j of a Jordan splitting and a vector of π M.

theorem LinearMap.BilinForm.IsJordanSplitting.finrank_eq {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} [IsDomain R] [IsLocalRing R] [Module.Finite R M] {N' : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) (h' : B.IsJordanSplitting π N') (hπ : π ≠ 0) (hπ' : ¬IsUnit π) (j : ℕ) : Module.finrank R ↥(N j) = Module.finrank R ↥(N' j)

The ranks of the constituents of a Jordan splitting are invariants of the form. Over a local domain, any two Jordan splittings of a bilinear form on a finite module with respect to the same nonzero non-unit π have constituents of equal rank at every index.

theorem LinearMap.BilinForm.IsJordanSplitting.finrank_eq_of_equivalent {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} [IsDomain R] [IsLocalRing R] {M' : Type u_5} [AddCommGroup M'] [Module R M'] [Module.Finite R M'] {B' : LinearMap.BilinForm R M'} {N' : ℕ → Submodule R M'} (h : B.IsJordanSplitting π N) (h' : B'.IsJordanSplitting π N') (hB : B.Equivalent B') (hπ : π ≠ 0) (hπ' : ¬IsUnit π) (j : ℕ) : Module.finrank R ↥(N j) = Module.finrank R ↥(N' j)

The ranks of the Jordan constituents are isometry invariants. Over a local domain, if a bilinear form is isometric to a bilinear form on a finite module, then Jordan splittings of the two forms with respect to the same nonzero non-unit π have constituents of equal rank at every index.

The constituents as modules, and their residue forms

theorem LinearMap.BilinForm.IsJordanSplitting.isCompl_biSup_ne {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) (j : ℕ) : IsCompl (N j) (⨆ (i : ℕ), ⨆ (_ : i ≠ j), N i)

Each constituent of a Jordan splitting is complementary to the sum of the others.

theorem LinearMap.BilinForm.IsJordanSplitting.finite {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} [Module.Finite R M] (h : B.IsJordanSplitting π N) (j : ℕ) : Module.Finite R ↥(N j)

The constituents of a Jordan splitting of a finite module are finite.

theorem LinearMap.BilinForm.IsJordanSplitting.free {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} [IsLocalRing R] [Module.Flat R M] [Module.Finite R M] (h : B.IsJordanSplitting π N) (j : ℕ) : Module.Free R ↥(N j)

The constituents of a Jordan splitting of a finite flat module over a local ring are free, being finite flat direct summands.

theorem LinearMap.BilinForm.IsJordanSplitting.finrank_biSup_Iic {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} [IsLocalRing R] [Module.Flat R M] [Module.Finite R M] (h : B.IsJordanSplitting π N) (j : ℕ) : Module.finrank R ↥(⨆ i ∈ Set.Iic j, N i) = ∑ i ≤ j, Module.finrank R ↥(N i)

The rank of the sum of the constituents of index at most j of a Jordan splitting of a finite flat module over a local ring is the sum of their ranks.

theorem LinearMap.BilinForm.IsJordanSplitting.exists_pow_succ_dvd_sub {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) (hπ : π ∈ nonZeroDivisors R) (j : ℕ) : ∃ (f : M →ₗ[R] ↥(N j)), (∀ (x : ↥(N j)), f ↑x = x) ∧ (∀ (x y : M), (∀ (z : M), π ^ j ∣ (B x) z) → (∀ (z : M), π ^ j ∣ (B y) z) → π ^ (j + 1) ∣ (B x) y - (B ↑(f x)) ↑(f y)) ∧ ((∀ w ∈ N (j - 1), π ^ j ∣ (B w) w) → (∀ w ∈ N (j + 1), π ^ (j + 2) ∣ (B w) w) → ∀ (x : M), (∀ (z : M), π ^ j ∣ (B x) z) → π ^ (j + 2) ∣ (B x) x - (B ↑(f x)) ↑(f x))

The residue form of a Jordan constituent. Let N be a Jordan splitting of B with respect to a non-zero-divisor π. On the vectors x with π ^ j ∣ B x z for all z, the form B agrees modulo π ^ (j + 1) with its value on the projections to the constituent N j along the other constituents. Thus the form π ^ (-j) B modulo π on these vectors is pulled back from the residue form of the unimodular rescaling of N j.

If moreover the neighbouring constituents N (j - 1) and N (j + 1) are even at their own scales (the first condition is vacuous for j = 0), then the self-pairings B x x of these vectors agree with those of their projections modulo π ^ (j + 2). At π = 2 this says that for a constituent of type II between two constituents of type II, the quadratic residue form x ↦ 2 ^ (-j - 1) B x x modulo 2 is also pulled back from that constituent. In general the self-pairings need not be divisible by π ^ (j + 1); only their differences are controlled.

theorem LinearMap.BilinForm.IsJordanSplitting.equivalent_restrict_of_forall_unimodular {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} [IsDomain R] [IsLocalRing R] [Module.Free R M] [Module.Finite R M] {M' : Type u_5} [AddCommGroup M'] [Module R M'] {B' : LinearMap.BilinForm R M'} {N' : ℕ → Submodule R M'} (h : B.IsJordanSplitting π N) (h' : B'.IsJordanSplitting π N') (hB : B.IsSymm) (hBB' : B.Equivalent B') (hπ : π ≠ 0) (hπ' : ¬IsUnit π) (j : ℕ) (H : ∀ (C : LinearMap.BilinForm R ↥(N j)) (C' : LinearMap.BilinForm R ↥(N' j)), C.IsSymm → C'.IsSymm → (∀ (x y : ↥(N j)), π ^ j * (C x) y = (B ↑x) ↑y) → ∀ {n : ℕ} (b : Module.Basis (Fin n) R ↥(N j)) (b' : Module.Basis (Fin n) R ↥(N' j)), IsUnit ((toMatrix b) C).det → IsUnit ((toMatrix b') C').det → ∀ (φ : ↥(N' j) →ₗ[R] ↥(N j)), (∀ (x y : ↥(N' j)), π ∣ (C' x) y - (C (φ x)) (φ y)) → ((∀ w ∈ N (j - 1), π ^ j ∣ (B w) w) → (∀ w ∈ N (j + 1), π ^ (j + 2) ∣ (B w) w) → ∀ (x : ↥(N' j)), π ^ 2 ∣ (C' x) x - (C (φ x)) (φ x)) → C.Equivalent C') : (B.restrict (N j)).Equivalent (B'.restrict (N' j))

Comparing Jordan constituents through their unimodular rescalings. Over a local domain, let B be a symmetric form on a finite free module, isometric to a form B', and let N and N' be Jordan splittings of B and B' with respect to the same nonzero non-unit π. To show that the constituents N j and N' j are isometric, it suffices to show that their unimodular rescalings C and C' (with π ^ j C = B on N j) are isometric, knowing that they are symmetric with unit Gram determinants in bases of the same size, and that a linear map φ (the projection to N j along the other constituents, pulled back by the isometry) carries C' to C modulo π, and on the diagonal modulo π ^ 2 when the neighbouring constituents of N j are even at their own scales.

theorem LinearMap.BilinForm.IsJordanSplitting.isCompl_biSup_Iic_biSup_Ici {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) (j : ℕ) : IsCompl (⨆ i ∈ Set.Iic j, N i) (⨆ i ∈ Set.Ici (j + 1), N i)

The sums of the constituents of a Jordan splitting of index at most j and at least j + 1 are complementary.

theorem LinearMap.BilinForm.IsJordanSplitting.pow_succ_dvd_sub_apply_projectionOnto {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) (j : ℕ) (x y : M) : π ^ (j + 1) ∣ (B x) y - (B ↑(((⨆ i ∈ Set.Iic j, N i).projectionOnto (⨆ i ∈ Set.Ici (j + 1), N i) ⋯) x)) ↑(((⨆ i ∈ Set.Iic j, N i).projectionOnto (⨆ i ∈ Set.Ici (j + 1), N i) ⋯) y)

Projecting to the sum of the constituents of index at most j, along those of index above j, preserves the form modulo π ^ (j + 1).

theorem LinearMap.BilinForm.IsJordanSplitting.two_mul_pow_succ_dvd_apply_self_of_mem_biSup {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) (h2 : 2 ∣ π) {j : ℕ} (hnext : ∀ w ∈ N (j + 1), 2 * π ^ (j + 1) ∣ (B w) w) {x : M} (hx : x ∈ ⨆ i ∈ Set.Ici (j + 1), N i) : 2 * π ^ (j + 1) ∣ (B x) x

When 2 ∣ π and the constituent of index j + 1 of a Jordan splitting is even at its own scale, the self-pairings of the vectors of the constituents of index above j are divisible by 2 * π ^ (j + 1): the constituent of index j + 1 is even, and the pairings on the others are divisible by π ^ (j + 2).

theorem LinearMap.BilinForm.IsJordanSplitting.two_mul_pow_succ_dvd_sub_apply_projectionOnto {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} (h : B.IsJordanSplitting π N) (h2 : 2 ∣ π) {j : ℕ} (hnext : ∀ w ∈ N (j + 1), 2 * π ^ (j + 1) ∣ (B w) w) (x : M) : 2 * π ^ (j + 1) ∣ (B x) x - (B ↑(((⨆ i ∈ Set.Iic j, N i).projectionOnto (⨆ i ∈ Set.Ici (j + 1), N i) ⋯) x)) ↑(((⨆ i ∈ Set.Iic j, N i).projectionOnto (⨆ i ∈ Set.Ici (j + 1), N i) ⋯) x)

Projecting to the sum of the constituents of index at most j, along those of index above j, preserves the self-pairings modulo 2 * π ^ (j + 1) when 2 ∣ π and the constituent of index j + 1 is even at its own scale.

theorem LinearMap.BilinForm.IsJordanSplitting.exists_basis_restrict_biSup_Iic {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} {N : ℕ → Submodule R M} [IsDomain R] [IsLocalRing R] [Module.Free R M] [Module.Finite R M] (h : B.IsJordanSplitting π N) (hB : B.IsSymm) (hπ : π ≠ 0) (j : ℕ) : ∃ (ι : Type) (x : Fintype ι) (x_1 : DecidableEq ι) (b : Module.Basis ι R ↥(⨆ i ∈ Set.Iic j, N i)) (H : Matrix ι ι R), (toMatrix b) (B.restrict (⨆ i ∈ Set.Iic j, N i)) * H = π ^ j • 1 ∧ H.IsSymm ∧ (2 ∣ π → (∀ w ∈ N j, 2 * π ^ j ∣ (B w) w) → ∀ (i : ι), 2 ∣ H i i)

Over a local domain, the sum of the constituents of index at most j of a Jordan splitting of a symmetric form on a finite free module has a Gram matrix G and a symmetric matrix H with G * H = π ^ j • 1. When 2 ∣ π and the constituent of index j is even at its own scale, H has even diagonal.