Eichler's theorem: the decomposition into indecomposable summands

A positive definite integral lattice is an orthogonal sum of indecomposable sublattices in exactly one way. This file proves this for a reflexive bilinear form B on an arbitrary ℤ-module M whose values B x x on nonzero vectors are positive.

A vector is orthogonally irreducible when it is nonzero and is not the sum of two nonzero vectors orthogonal to each other. Since B (y + z) (y + z) = B y y + B z z when y and z are orthogonal, induction on the norm writes every vector as a sum of irreducible vectors. Join two irreducible vectors when they are not orthogonal; the spans of the connected components of this graph are the orthogonal components LinearMap.BilinForm.orthComponents B.

An irreducible vector of P ⊔ Q with P and Q orthogonal lies in P or in Q, and two non-orthogonal irreducible vectors lie in the same summand. Hence each component of the graph lies in one summand of any orthogonal decomposition, which gives both the indecomposability of the orthogonal components and the uniqueness of the decomposition.

Main definitions

• LinearMap.BilinForm.IsOrthIrreducible: a nonzero vector that is not the sum of two nonzero orthogonal vectors.
• LinearMap.BilinForm.IsOrthIndecomposable: a nonzero submodule that is not the sum of two nonzero orthogonal submodules.
• LinearMap.BilinForm.orthComponents: the spans of the connected components of the non-orthogonality graph on irreducible vectors.

Main results

• LinearMap.BilinForm.span_setOf_isOrthIrreducible: for a positive definite integral form the irreducible vectors span.
• LinearMap.BilinForm.isOrthIndecomposable_of_mem_orthComponents, LinearMap.BilinForm.pairwise_orthComponents and LinearMap.BilinForm.sSup_orthComponents: the orthogonal components are indecomposable, pairwise orthogonal, and span.
• LinearMap.BilinForm.eq_orthComponents_iff: Eichler's theorem. A set of submodules is a decomposition of M into pairwise orthogonal indecomposable submodules exactly when it is the set of orthogonal components.
• LinearMap.BilinForm.sSupIndep_orthComponents and LinearMap.BilinForm.finite_orthComponents: the sum is direct, and finite for a finitely generated module.

References

• M. Eichler, Note zur Theorie der Kristallgitter, Math. Ann. 125 (1952), 51–55.
• O. T. O'Meara, Introduction to Quadratic Forms, 105:1.
• J. Milnor and D. Husemoller, Symmetric Bilinear Forms, Chapter II, Theorem 6.4.

def LinearMap.BilinForm.IsOrthIrreducible {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (x : M) : Prop

A vector is orthogonally irreducible for B when it is nonzero and is not the sum of two nonzero vectors y, z with B y z = 0.

def LinearMap.BilinForm.IsOrthIndecomposable {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (N : Submodule R M) : Prop

A submodule is orthogonally indecomposable for B when it is nonzero and is not the sum of two nonzero submodules orthogonal to each other.

def LinearMap.BilinForm.orthComponents {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : Set (Submodule R M)

The orthogonal components of B: the spans of the connected components of the graph on orthogonally irreducible vectors in which two vectors are joined when they are not orthogonal. For a positive definite integral form these are the summands of the unique decomposition into orthogonally indecomposable submodules (LinearMap.BilinForm.eq_orthComponents_iff).

theorem LinearMap.BilinForm.isOrthIrreducible_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {x : M} : B.IsOrthIrreducible x ↔ x ≠ 0 ∧ ∀ (y z : M), y + z = x → (B y) z = 0 → y = 0 ∨ z = 0

The defining property of an orthogonally irreducible vector.

theorem LinearMap.BilinForm.isOrthIndecomposable_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {N : Submodule R M} : B.IsOrthIndecomposable N ↔ N ≠ ⊥ ∧ ∀ (P Q : Submodule R M), P ≤ B.orthogonal Q → P ⊔ Q = N → P = ⊥ ∨ Q = ⊥

The defining property of an orthogonally indecomposable submodule.

theorem LinearMap.BilinForm.IsOrthIrreducible.ne_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {x : M} (hx : B.IsOrthIrreducible x) : x ≠ 0

An orthogonally irreducible vector is nonzero.

theorem LinearMap.BilinForm.IsOrthIrreducible.mem_or_mem_of_mem_sup {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {x : M} (hx : B.IsOrthIrreducible x) {P Q : Submodule R M} (hPQ : P ≤ B.orthogonal Q) (h : x ∈ P ⊔ Q) : x ∈ P ∨ x ∈ Q

An orthogonally irreducible vector of P ⊔ Q, where P is orthogonal to Q, lies in P or in Q.

theorem LinearMap.BilinForm.IsOrthIrreducible.exists_mem_of_sSup_eq_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {x : M} (hx : B.IsOrthIrreducible x) {S : Set (Submodule R M)} (hS : S.Pairwise fun (N N' : Submodule R M) => N ≤ B.orthogonal N') (htop : sSup S = ⊤) : ∃ N ∈ S, x ∈ N

An orthogonally irreducible vector lies in a member of every family of pairwise orthogonal submodules spanning M.

theorem LinearMap.BilinForm.pairwise_orthComponents {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} : B.orthComponents.Pairwise fun (N N' : Submodule R M) => N ≤ B.orthogonal N'

Distinct orthogonal components are orthogonal.

theorem LinearMap.BilinForm.sSupIndep_orthComponents {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (hani : (BilinMap.toQuadraticMap B).Anisotropic) : sSupIndep B.orthComponents

For an anisotropic form, the orthogonal components are independent.

theorem LinearMap.BilinForm.finite_orthComponents {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} [IsNoetherian R M] (hani : (BilinMap.toQuadraticMap B).Anisotropic) : B.orthComponents.Finite

For an anisotropic form on a Noetherian module, there are finitely many orthogonal components.

theorem LinearMap.BilinForm.isOrthIndecomposable_of_mem_orthComponents {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsRefl) (hani : (BilinMap.toQuadraticMap B).Anisotropic) {N : Submodule R M} (hN : N ∈ B.orthComponents) : B.IsOrthIndecomposable N

For a reflexive anisotropic form, each orthogonal component is orthogonally indecomposable.

theorem LinearMap.BilinForm.span_setOf_isOrthIrreducible {M : Type u_3} [AddCommGroup M] {B : LinearMap.BilinForm ℤ M} (hB : B.IsRefl) (hpos : (BilinMap.toQuadraticMap B).PosDef) : Submodule.span ℤ {x : M | B.IsOrthIrreducible x} = ⊤

For a reflexive positive definite integral form, every vector is a sum of orthogonally irreducible vectors.

theorem LinearMap.BilinForm.sSup_orthComponents {M : Type u_3} [AddCommGroup M] {B : LinearMap.BilinForm ℤ M} (hB : B.IsRefl) (hpos : (BilinMap.toQuadraticMap B).PosDef) : sSup B.orthComponents = ⊤

For a reflexive positive definite integral form, the orthogonal components span.

theorem LinearMap.BilinForm.eq_orthComponents_iff {M : Type u_3} [AddCommGroup M] {B : LinearMap.BilinForm ℤ M} (hB : B.IsRefl) (hpos : (BilinMap.toQuadraticMap B).PosDef) {S : Set (Submodule ℤ M)} : S = B.orthComponents ↔ (∀ N ∈ S, B.IsOrthIndecomposable N) ∧ (S.Pairwise fun (N N' : Submodule ℤ M) => N ≤ B.orthogonal N') ∧ sSup S = ⊤

Eichler's theorem. For a reflexive positive definite integral form, a set of submodules consists of pairwise orthogonal orthogonally indecomposable submodules spanning M exactly when it is the set of orthogonal components. In particular such a decomposition exists and is unique.

theorem LinearMap.BilinForm.isOrthIndecomposable_top_iff {M : Type u_3} [AddCommGroup M] {B : LinearMap.BilinForm ℤ M} (hB : B.IsRefl) (hpos : (BilinMap.toQuadraticMap B).PosDef) : B.IsOrthIndecomposable ⊤ ↔ B.orthComponents = {⊤}

For a reflexive positive definite integral form, M is orthogonally indecomposable exactly when it is its only orthogonal component.