FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024)
FC11 — Peters & Sterk, Symmetric and Quadratic Forms.
This chapter contains 70 definitions, 8 theorems, 7 propositions, 13 lemmas, 3 corollaries, 27 examples, 12 constructions, 11 remarks and 4 conventions.
Of the 155 statements checked against Lean, 49 are formalized somewhere and 106 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 106 | 68% | A documented search found no Lean statement of it anywhere. |
| in lean-categories | 37 | 24% | This repository states and proves it. |
| in Mathlib | 9 | 6% | Mathlib states and proves it. |
| in another Lean project | 3 | 2% | Some other Lean development has it; using it means porting that code. |
| checked in total | 155 |
- Canonical source block: FC11 Peters–Sterk Chapter 1, “Symmetric and Quadratic Forms, an Overview”,
FC11-C01-U001–FC11-C01-U155, 155 units, in exact canonical order from FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024). - Project code baseline:
A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19(Apache-2.0, Lean 4.33.0). No project Lean source changed while this chapter was audited. - Pinned Mathlib:
P=db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean 4.33.0). Current upstream Mathlib source was checked atH=71a80585ee495fc24472fd0eaffc89d94e4fd8d6. Targeted Mathlib history was inspected from the local full Git checkout; open-PR searches included the form/lattice families and found, among others, PR #42719 on totally isotropic subspaces, which does not close the unmatched Witt/lattice bundles. - Search services: dated LeanSearch query captures cover linear/symmetric/quadratic forms, integral lattices, primitivity, index/discriminant, parity, reflections, Witt theory, dual/discriminant forms, gluing, local/genus/Hasse theory, dyadic forms, finiteness/Hermite, Nikulin/Niemeier, mass and theta-series families. Loogle captures cover orthogonal, discriminant, primitive/saturated, reflective, Witt, unimodular, Hermite, genus and theta vocabulary.
- Package discovery: Reservoir application/search data were captured and inspected. The local formalization-source atlas was checked across all registered sources, including
formal-conjectures@b123bb89b5978ae6b648159e430c4e4dce161b97. Broad GitHub Lean code search captures cover bilinear/quadratic forms, primitive lattices, reflections, discriminant forms, overlattices, dyadic forms, Nikulin, Witt decomposition, Niemeier and Hermite families. - Reference-port source used by three rows:
TauCeti@98a6bfc9f3cb4ab3a159d83858ce546d1e543c1b(Apache-2.0), Lean 4.34.0-rc2 with Mathlibe21ec05048292b3de86d4cf1987e2208171a5642. Its integral-lattice index, overlattice/isotropic-subgroup, orthogonal-quotient and naturality declarations are mathematically compatible but require a source port to the project toolchain, so they arereference-port, notpackage-import. - Strict whole-row semantics were used. A row is positive only when the cited existing declarations cover the full source unit without a substantive reconstruction. Partial ingredients remain
unmatched; the rational-discriminant/binary-form remark was explicitly demoted on that basis during verification. - Route totals for C01:
mathlib9,project-existing37,package-import0,reference-port3,unmatched106. - Negative result scope: every
unmatchedrow recordsN=2026-09-07through its provenance field. The negative result applies only to the inspected revisions/search surfaces above and is not a claim about future Mathlib/project/package state.
Definition / construction
A symmetric bilinear form on a \(k\)-vector space \(V\) is a bilinear map \(b:V\times V\to k\) with \(b(x,y)=b(y,x)\).
Formalized. Mathlib/LinearAlgebra/BilinearForm/Basic.lean::LinearMap.BilinForm; Mathlib/LinearAlgebra/BilinearForm/Properties.lean::LinearMap.BilinForm.IsSymm — Specialize the scalar ring to the source field; IsSymm is precisely interchange of the two arguments, with no positivity hypothesis.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition / construction
The Gram matrix of a bilinear form \(b\) in a basis \(E=(e_i)\) is \(B_E=(b(e_i,e_j))\).
Formalized. Mathlib/LinearAlgebra/Matrix/BilinearForm.lean::LinearMap.BilinForm.toMatrix — The basis-indexed matrix evaluates to the pairings of basis vectors; no nondegeneracy is required.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition / construction
A quadratic form on a \(k\)-vector space \(V\) is a map \(q:V\to k\) with \(q(ax)=a^2q(x)\) whose polarization \(b_q(x,y)=q(x+y)-q(x)-q(y)\) is bilinear.
Formalized. Mathlib/LinearAlgebra/QuadraticForm/Basic.lean::QuadraticForm, QuadraticMap.ofPolar — The ring constructor uses quadratic homogeneity and bilinearity of the unhalved polar map, including characteristic two.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition / construction
The polar form of a quadratic form \(q\) is \(b_q(x,y)=q(x+y)-q(x)-q(y)\).
Formalized. Mathlib/LinearAlgebra/QuadraticForm/Basic.lean::QuadraticMap.polar, QuadraticMap.polarBilin — Use the unhalved polar, not associated (which divides by two).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Remark 1.1.1
Remark 1.1.1. The Gram matrix presentation of a polar form is non-unique; the same notions extend to forms over finite-rank free modules; over \(\mathbf Z\), polar forms of integral quadratic forms correspond to even symmetric forms.
Not formalized. Quadratic maps, matrices and parity exist separately. The entire bundle includes nonunique representing matrices over general rings and the integral even-polar correspondence; the latter is not supplied by the inverse-two associated-map API over Z.
Definition / construction
A symmetric form is non-degenerate when its Gram matrix is invertible. Under a basis change \(B_F=C^{\mathsf T}B_EC\), so non-degeneracy is basis independent.
Formalized. Mathlib/LinearAlgebra/Matrix/BilinearForm.lean::LinearMap.BilinForm.nondegenerate_iff_det_ne_zero, LinearMap.BilinForm.toMatrix_mul_basis_toMatrix — For finite-dimensional spaces over a field, determinant nonzero is matrix invertibility. The basis-change identity is the exact transpose-congruence formula and establishes basis independence.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition / construction / notation
For a non-degenerate symmetric form, the determinant of a Gram matrix is well defined modulo non-zero squares; its class in \(k^\times/(k^\times)^2\) is the discriminant \(\operatorname{disc}(b)\).
Not formalized. Candidate determinant square-class owners need comparison between arbitrary symmetric bilinear forms and diagonal quadratic presentations; do not replace the signed square class with absolute determinant.
Definition / construction
An inner product space is a vector space equipped with a non-degenerate symmetric bilinear form.
Formalized. LeanCategories/Modules/Bilinear/Valued/Fixed.lean::RadicalFreeSymBilinModuleCat — The source uses inner product to mean a nondegenerate symmetric bilinear form. This is not Mathlib InnerProductSpace, which adds positivity. Take the field-valued full subcategory.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Proposition 1.1.2
Proposition 1.1.2. The form \(^ { b }\) is non-degenerate if and only if for any non-zero \(x \in V\) there exists \(y \in V\) with \(b ( x , y ) = 1\) (equivalently: \(y \mapsto b ( x , y )\) is non-trivial).
Not formalized. Nondegeneracy gives a nonzero pairing; the source asserts the normalized value one in both directions. No exact normalized equivalence has yet been identified in the inspected declarations.
Definition / construction
The orthogonal complement of \(S\subset V\) is \(S^\perp=\{x:b(x,S)=0\}\); the radical is \(V^\perp\).
Formalized. Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean::LinearMap.BilinForm.orthogonal, LinearMap.BilinForm.orthogonal_top_eq_ker — The source is symmetric, so the side used in the annihilation convention is immaterial. Taking the full subspace gives the radical.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition / construction
A set of vectors is orthogonal if distinct vectors pair to zero.
Formalized. Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean::LinearMap.BilinForm.IsOrthoᵢ — Pairwise distinct indices have zero pairing; specialize the index type to the source set when a set rather than a family is used.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Lemma 1.1.3
Lemma 1.1.3. Let ?? be a subspace of \(V\) and let \(^ { b }\) be a symmetric bilinear form on \(V\) . 1. ?? is non-degenerate if and only if the radical of \(b\) is \(\{ 0 \}\) . In the case \(b\) is non-degenerate, \(\dim S ^ { \perp } + \dim S = \dim V\) . Moreover, \(( S ^ { \bot } ) ^ { \bot } = S\) . 2. If ?? and \(b | _ { S }\) are non-degenerate, then \(S \oplus S ^ { \perp } = V\) and \(b | _ { S ^ { \perp } }\) is non-degenerate. Conversely, if \(b\) is non-degenerate and \(V = S \oplus S ^ { \perp }\) , then ?? restricts nondegenerately to \(S\) and \(S ^ { \perp }\) .
Not formalized. The dimension and double-orthogonal theorems and nondegenerate-restriction/complement criterion are present. Verify the complementary restriction clause against the full multi-clause source lemma before counting the bundle.
Convention / notation
An orthogonal direct sum is denoted by \(V=V_1\perp V_2\) (or the book’s orthogonal-sum symbol).
Formalized. LeanCategories/Lattices/Valued/Constructions.lean::finiteFormOrthogonalSum — The underlying module is a product, with the sum of pairings and zero cross terms; over a field finite products are the indicated orthogonal direct sums.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Proposition 1.1.4
Proposition 1.1.4. Let \(k\) have characteristic different from 2. Then every inner product space \(( V , b )\) of positive dimension has a basis in which the Gram matrix is diagonal.
Formalized. Mathlib/LinearAlgebra/QuadraticForm/Basic.lean::LinearMap.BilinForm.exists_orthogonal_basis — The theorem assumes finite dimension, symmetry and invertibility of two, but not nondegeneracy. The source nondegenerate case is a specialization; diagonal entries are nonzero by the nondegenerate orthogonal-basis criterion.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Remark 1.1.5
Remark 1.1.5. The technique used in the proof of the preceding proposition shows that every quadratic form in characteristic different from 2 is diagonalizable; if there is a non-zero radical, say of dimension \(n\) , all diagonalized forms have precisely \(n\) zeros on the diagonal. If \(k\) is a field of characteristic 2, this is no longer true. Consider for example the so-called hyperbolic plane over \(k\) , \(U = k \cdot e \oplus k \cdot f\) with bilinear form given by \(b ( e , e ) = b ( f , f ) = 0\) , \(b ( e , f ) = 1\) . Since \(b ( x , x ) = 0\) for all \(x \in U\) , this form is not diagonalizable.
Not formalized. Degenerate diagonalization is available. The characteristic-two hyperbolic example is defined and proved alternating/nonzero, but its non-diagonalizability and the complete nullity comparison are not packaged by the inspected counterexample theorem (which instead disproves injectivity of polarization).
Definition / construction / notation
Finally a word about the comparison of forms. A metric linear map between two \(k\) -vector spaces \(V , V ^ { \prime }\) equipped with symmetric bilinear forms, say \(( V , b )\) and \(( V ^ { \prime } , b ^ { \prime } )\) , is a linear map \(f\) for which \(b ^ { \prime } ( f ( x ) , f ( y ) ) = b ( x , y )\) for all \(x , y \in V\) . If \(b\) is non-degenerate, \(f\) is injective. If, moreover, \(f\) is bijective, then \(b ^ { \prime }\) is also nondegenerate and \(f\) is called an isometry. Two inner product spaces are said to be isometric if there exists an isometry between them.
Not formalized. Form-preserving linear maps and categorical isomorphisms exist. This bundled paragraph additionally proves injectivity from nondegeneracy of the source and transfers nondegeneracy through a bijection; the map constructor alone is not that result.
Definition / construction / notation
An integral symmetric lattice is a finite-rank free \(\mathbf Z\)-module \(L\) equipped with an integral symmetric bilinear form \(b\).
Formalized. LeanCategories/Lattices/Valued/Arithmetic.lean::FiniteFreeLatticeCat — Specialize both scalar and value modules to Z. Unlike IntegralLatticeCat alone, this owner includes the required finite free carrier.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Remark 1.2.1
Remark 1.2.1. 1. If \(( L , b )\) is an integral lattice of rank two, the form \(^ { b }\) is also called a binary form. 2. If instead of being \(\mathbb { Z }\) -valued, \(^ { b }\) has values in \(\mathbb { Q }\) , the above argument shows that the determinant of a Gram matrix for \(^ { b }\) is still independent of the choice of a basis for \(L\) . This rational number will also be called “discriminant” of \(^ { b }\) and denoted as \(\operatorname { d i s c } ( b ) \in \mathbb { Q }\) . For the sake of simplicity we prefer to work with \(\mathbb { Z }\) -valued forms. This restriction occasionally necessitates however to adapt an argument slightly.
Not formalized. The project has rank and integral Gram determinants, but this remark also names binary forms and treats a Q-valued form on a free Z-lattice whose rational Gram determinant is exactly basis-independent. The inspected integral-lattice determinant owner does not supply that whole convention/result bundle.
Definition / construction
An integral lattice is non-degenerate when its bilinear form is non-degenerate over \(\mathbf Q\), and unimodular when its Gram determinant is a unit \(\pm1\).
Formalized. LeanCategories/Lattices/Valued/MetricDual.lean::IsFractionFieldNondegenerate, IsUnimodular, isFractionFieldPerfect_iff_determinant_ne_zero — Use the rationalized nondegeneracy predicate; unimodularity is perfection of the integral pairing, not merely nonsingularity over Q. The determinant-unit criterion must accompany the owner.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction
An integral symmetric lattice is even if \(b(x,x)\) is even for every \(x\), and odd otherwise.
Formalized. LeanCategories/Lattices/Valued/ScaleAndEvenness.lean::IsEven, IsOdd — Evenness is membership of every self-pairing in the ideal (2); over Z this is precisely even integer norm. Odd means its negation.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction
A sublattice is a free subgroup equipped with the restricted form.
Formalized. LeanCategories/Lattices/Valued/Sublattice.lean::formedSublattice — The submodule carries the restricted symmetric bilinear form. Over Z a submodule of a finite free carrier is finite free; no nondegeneracy of the restriction is assumed.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Lemma 1.2.2
Lemma 1.2.2. If \(L\) is a non-degenerate lattice and \(L ^ { \prime } \subset L\) a sublattice of finite index, then \[ \operatorname { d i s c } ( L ^ { \prime } ) = [ L : L ^ { \prime } ] ^ { 2 } \cdot \operatorname { d i s c } ( L ) . \]
Formalized. TauCeti/LinearAlgebra/IntegralLattice/Index.lean::TauCeti.IntegralLattice.determinant_eq_mul_relIndex_sq — Exact signed formula det(S)=det(L)[L:S]^2 for integral lattices sharing the rational form, with inclusion of carriers. Transport abstract lattices into their rationalization. TauCeti discriminant is the absolute determinant; use determinant here.
Searched: TauCeti@98a6bfc9f3cb4ab3a159d83858ce546d1e543c1b; Apache-2.0; Lean 4.34.0-rc2; Mathlib e21ec05048292b3de86d4cf1987e2208171a5642; source port required for project Lean 4.33.0
Remark 1.2.3
Remark 1.2.3. One can also use matrices to describe sublattices. For instance, if \(\{ e _ { 1 } , \ldots , e _ { n } \}\) is a basis of \(L\) , then a sublattice \(L ^ { \prime }\) of finite index can be described as the span of \(v _ { 1 } , \ldots , v _ { n }\) , where \(\begin{array} { r } { v _ { i } = \sum _ { j = 1 } ^ { n } a _ { i j } e _ { j } } \end{array}\) , \(i = 1 , \ldots , n\) , and where the matrix \(A = ( a _ { i j } )\) has integer entries and non-zero determinant. Using the basis \(\pmb { E } ^ { \prime }\) as in the proof of the lemma, one derives that \(\left[ L : L ^ { \prime } \right] = | \operatorname* { d e t } ( A ) |\) .
Not formalized. LeanSearch identifies AddSubgroup.relIndex_eq_natAbs_det as the exact candidate; resolve its actual defining path and assumptions before accepting the row.
Definition 1.2.4
Definition 1.2.4. A submodule or sublattice \(S\) of \(L\) is called primitive 1 if one of the following equivalent assertions is true. 1. For \(x \in L\) , if the non-zero integral multiple \(n x\) belongs to \(S\) , then \(x\) belongs to \(S\) ; 2. \(L / S\) is free of torsion; 3. Any basis for \(S\) can be extended to a basis for \(L\) ; 4. For some submodule \(S ^ { \prime }\) of \(L\) one has \(L = S \oplus S ^ { \prime }\) .
Not formalized. Native primitivity is torsion-freeness of the quotient and is equivalent to saturation. The full source bundle also includes extension of an arbitrary basis and direct-summand equivalence; these must not be inferred from only the saturation theorem.
Definition / construction
A vector of a free module is primitive if it can be extended to a basis.
Not formalized. Primitivity of a cyclic submodule exists; the source specifically defines a primitive vector through extension to an integral basis. No dedicated basis-extension equivalence was identified.
Definition / construction
The primitive closure of a sublattice \(S\subset L\) is \((S\otimes\mathbf Q)\cap L\); \(S\) is primitive when it equals its primitive closure.
Not formalized. The annihilator-based saturation and its primitivity equivalence are implemented. The bundled identity with the intersection of L and its rational subspace is not supplied by that theorem.
Convention / notation
For a lattice \(S\), write \(S_{\mathbf Q}=S\otimes_{\mathbf Z}\mathbf Q\) for its associated rational quadratic space.
Formalized. LeanCategories/Lattices/Valued/BaseChange.lean::baseChangeIntegral, baseChangeIntegralCarrierEquiv, baseChangeIntegral_pairing_tmul — Specializing integral scalar extension to Z -> Q gives the tensor carrier S_Q and the Q-bilinear extension of the pairing exactly.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction
An integral quadratic form is a quadratic form on a free finite-rank \(\mathbf Z\)-module taking values in \(\mathbf Z\); its polarization is integral and even on the diagonal.
Formalized. Mathlib/LinearAlgebra/QuadraticForm/Basic.lean::QuadraticForm, QuadraticMap.polarBilin, QuadraticMap.polar_self — Specialize to a finite free Z-module. polar_self is twice q(x), establishing the evenness of the polar lattice, including the factor-of-two convention.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition / construction
An integral quadratic lattice is a finite-rank free \(\mathbf Z\)-module equipped with an integral quadratic form.
Formalized. LeanCategories/Modules/Quadratic/Valued/Subcategories.lean::FiniteFreeQuadModuleCat; LeanCategories/Modules/Quadratic/Valued/Fixed.lean::QuadModuleCat.form — Specializing the finite-free quadratic-module subcategory to R=W=Z gives exactly a finite-rank free Z-module equipped with an integral quadratic form.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Proposition 1.2.5
Proposition 1.2.5. The polar form of an integral quadratic form is even and, conversely, every even form \(b\) is the polar form of the integral quadratic form \(\begin{array} { r } { q ( x ) = \frac { 1 } { 2 } b ( x , x ) } \end{array}\) .
Not formalized. Evenness predicates and closure under addition/scalars do not give the integral quadratic map q=b(x,x)/2 and the inverse correspondence as a Lean implementation. Inverse-two constructions over a field do not apply over Z.
Remark 1.2.6
Remark 1.2.6. If \(B = ( b _ { i j } )\) is a real symmetric matrix of size \(n \times n\) , there is a corresponding symmetric form \(b ( x , y )\) defined by \(\textstyle \sum _ { i , j = 1 } ^ { n } b _ { i j } x _ { i } y _ { j }\) . Note that \(b ( x , x ) =\) \(\textstyle \sum _ { i , j = 1 } ^ { n } b _ { i j } x _ { i } x _ { j }\) has integral values on \(\oplus ^ { n } \mathbb { Z }\) precisely if \(b _ { i i } \in \mathbb { Z }\) , \(2 b _ { i j } \in \mathbb { Z }\) if \(i \neq j\) . Unfortunately, \(\operatorname* { d e t } B\) then need not be integral. For instance the matrix \(\left( { \begin{array} { l l } { 1 } & { { \frac { 1 } { 2 } } } \\ { { \frac { 1 } { 2 } } } & { 1 } \end{array} } \right)\) having determinant \(3 / 4\) would then represent the quadratic form \(x ^ { 2 } + x y + y ^ { 2 }\) . In cases where a matrix will be used to define an integral lattice, we shall therefore adhere to Kneser’s convention from [122], i.e., as in formula (1.1) a quadratic form \(\begin{array} { r } { ( x _ { 1 } , \ldots , x _ { n } ) \mapsto \sum _ { 1 \leq i \leq j \leq n } q _ { i j } x _ { i } x _ { j } } \end{array}\) corresponds to the upper triangular matrix \(Q \ : = \ : ( q _ { i j } )\) and conversely. Then the quadratic form is integral if and only if \(Q\) has integral entries and its polar form corresponds to \(B = Q + Q ^ { \mathsf { T } }\) , a form with even integral entries on the diagonal and with \(\operatorname* { d e t } B\) integral. Thus \(x ^ { 2 } + x y + y ^ { 2 }\) corresponds to a polar form with Gram matrix \(\left( \begin{array} { c c } { { 2 } } & { { 1 } } \\ { { 1 } } & { { 2 } } \end{array} \right)\) . One could also consider quadratic forms \(\textstyle \sum _ { i , j = 1 } ^ { n } q _ { i j } x _ { i } x _ { j }\) , starting from a symmetric integral matrix ( \(q _ { i j }\) ). J.W. Cassels [36] calls such forms classically integral after Gauß. However, this excludes forms like \(x ^ { 2 } + x y + y ^ { 2 }\) .
Not formalized. The whole unit includes triangular coefficient conventions, polar matrix Q+transpose Q, half-integral versus classically integral forms and the specified binary example. Generic symmetric Gram constructors do not cover this bundle.
Definition / construction
For a sublattice \(S\subset L\), its lattice orthogonal complement is \(S^\perp=L\cap(S_{\mathbf Q})^\perp\); the radical is \(L^\perp\).
Formalized. LeanCategories/Lattices/Valued/Sublattice.lean::orthogonalSubmodule; LeanCategories/Modules/Bilinear/Valued/Fixed.lean::BilinModuleCat.leftRadical — Use the integral orthogonal submodule and kernel of the adjoint; symmetry identifies the left/right conventions. The rational-intersection characterization needs an explicit comparison if treated as a theorem.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction
A vector is isotropic if its quadratic value is zero; a subspace is isotropic if the form vanishes identically on it.
Not formalized. Quadratic isotropy and bilinear total isotropy must be compared in the exact source characteristic convention. Do not substitute vanishing of q for vanishing of b in characteristic two.
Lemma 1.3.1
Lemma 1.3.1. Let \(( L , b )\) be a non-degenerate lattice. 1. If \(S _ { 1 } \subset S _ { 2 } \subset L\) , then \(S _ { 1 } ^ { \bot } \supset S _ { 2 } ^ { \bot }\) . 2. The orthogonal complement \(T = S ^ { \perp }\) of any sublattice \(S\) is primitive and \(T ^ { \perp }\) is the primitive closure of \(S\) . Furthermore, (a) \(\operatorname { r a n k } ( S ) + \operatorname { r a n k } ( T ) = \operatorname { r a n k } ( L )\) and if \(b | _ { S }\) is non-degenerate then \(S \cap T =\) \(\{ 0 \}\) . (b) If \(b | _ { S }\) is non-degenerate, then \(S \oplus T\) is a sublattice of \(L\) of finite index, say ??. If, moreover, \(S\) is primitive and \(0 < \mathrm { r a n k } ( S ) < \mathrm { r a n k } ( L )\) , then there are integers \(c _ { S } , c _ { T }\) such that \[ \begin{array} { r l } & { \operatorname { d i s c } ( S ) = e \cdot c _ { S } } \\ & { \operatorname { d i s c } ( T ) = e \cdot c _ { T } } \\ & { \operatorname { d i s c } ( L ) = c _ { S } c _ { T } . } \end{array} \] In particular, \(L\) is unimodular if and only if \(| \operatorname { d i s c } ( S ) |\) and \(| \operatorname { d i s c } ( S ^ { \bot } ) |\) are equal to \(e = [ L : S \oplus S ^ { \perp } ]\) .
Not formalized. The source lemma bundles primitivity of perpendiculars, double perpendicular equals saturation, ranks/intersections, finite-index discriminant formulas and a unimodularity equivalence. Available separate constructors and the index formula do not constitute the full bundle.
Remark 1.3.2
Remark 1.3.2. Let \(S \subset L\) be a non-degenerate sublattice of a non-degenerate lattice \(L\) . Instead of \(T = S ^ { \perp }\) , suppose \(T \subset L\) is only known to be orthogonal to \(S\) . Then \(S \cap T = \{ 0 \}\) , since \(S\) is non-degenerate. Suppose that in addition \(S \oplus T\) has finite index in \(L\) . Then \(T = S ^ { \perp }\) if and only if \(T\) is primitive in \(L\) , and a similar assertion holds for \(T\) . Contrary to what happens for inner product spaces, a non-degenerate sublattice does not always split off orthogonally.
Not formalized. The full claim compares complementary-rank sublattices, primitive equality with the full perpendicular and failure of integral orthogonal splitting. Field-level IsCompl results omit the integral assertion.
Example / comparison
Example 1.3.3. The hyperbolic lattice is the rank two \(\mathbb { Z }\) -module \(\mathbb { Z } ^ { 2 }\) equipped with the form with Gram matrix \(\left( \begin{array} { c c } { { 0 } } & { { 1 } } \\ { { 1 } } & { { 0 } } \end{array} \right)\) . Take for \(S\) the lattice spanned by the non-isotropic vector \(( 1 , 1 )\) with orthogonal complement \(\mathbb { Z } \cdot ( 1 , - 1 )\) . The vectors \(( k , 0 )\) and \(( 0 , \ell )\) for \(k\) and \(\ell\) odd do not belong to \(S \oplus S ^ { \perp }\) .
Not formalized. The specified index-two sublattice generated by (1,1) and (1,-1), with non-splitting comparison, is not an identified theorem in the hyperbolic-plane constructor.
Definition / construction / notation
A non-degenerate lattice is decomposable if it has a non-trivial orthogonal direct-sum decomposition \(L=S\oplus S^\perp\); otherwise it is indecomposable.
Not formalized. Orthogonal summands and irreducible root lattices are present, but irreducibility of a root graph is not the source predicate of orthogonal indecomposability for every nondegenerate integral lattice.
Corollary 1.3.4
Corollary 1.3.4. If \(S\) is a unimodular sublattice of a non-degenerate lattice \(L\) , then \(L = S \oplus S ^ { \perp }\) . If, moreover, \(L\) is unimodular, then \(S ^ { \perp }\) is unimodular.
Not formalized. The inspected orthogonal-sum isometries assume a complement. They do not establish that a unimodular integral sublattice supplies one, nor the additional unimodularity of the perpendicular.
Definition / construction
The signature of a real symmetric form is the pair of numbers of positive and negative entries in a diagonal normal form.
Formalized. LeanCategories/Lattices/Valued/Signature.lean::signature, signature_eq_matrixSignature — The source pair is the positive and negative entries of the native triple (positive,negative,nullity). For nondegenerate forms the third entry is zero.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction / notation
The signature of a real symmetric form is the pair \((r,s)\) of positive and negative squares in a diagonalization; for a non-degenerate lattice its index is \(\tau(b)=r-s\).
Not formalized. Signature counts exist; this unit also owns the signed integer index tau=r-s. No canonical signed-index owner was identified, and the natural subtraction of two Nat counts would be incorrect.
Definition / construction
A real symmetric form is positive/negative definite or semidefinite according to the signs of its values; otherwise a non-degenerate form is indefinite.
Formalized. LeanCategories/Lattices/Valued/Signature.lean::signature, IsPositiveDefiniteSignature, IsNegativeDefiniteSignature, IsPositiveSemidefiniteSignature, IsNegativeSemidefiniteSignature, IsIndefiniteSignature — Applied to a finite real symmetric form, the signature predicates encode exactly the sign definitions; on a nondegenerate form the remaining case with both signed ranks nonzero is indefinite.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Convention / notation
The rank-one lattice with Gram matrix \((a)\) is denoted \(\langle a\rangle\).
Formalized. LeanCategories/Lattices/Valued/Standard.lean::rankOneLattice — The parameter is the Gram coefficient a itself, unlike TauCeti rankOne which uses Gram coefficient 2m. Include a=0 unless the local source assumption excludes it.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Convention / notation
For a lattice \(L\) and scalar \(m\), \(L(m)\) denotes the same module with its form multiplied by \(m\).
Formalized. LeanCategories/Lattices/Valued/Constructions.lean::scaleLattice — scaleLattice keeps the carrier and multiplies the form by the scalar, exactly the source L(m) construction.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction / notation
In the examples we often use a dot to denote symmetric bilinear forms and so, instead of \(b ( v , w )\) , we write \(v \cdot w\) .
Formalized. LeanCategories/Modules/Bilinear/Valued/Fixed.lean::BilinModuleCat.pairing — The dot is source notation for the existing pairing and creates no new structure or theorem. Do not reuse a Euclidean dot-product owner with extra assumptions.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Example / comparison
The hyperbolic plane \(U=\mathbf Ze\oplus\mathbf Zf\) has \(e\cdot f=1\) and \(e^2=f^2=0\), hence discriminant \(-1\); it is the polar lattice of the quadratic form \(x_1e+x_2f\mapsto x_1x_2\) and is even.
Not formalized. The even unimodular hyperbolic Gram model is present. The whole example additionally identifies it as the unhalved polar of the integral cross-product quadratic form and records signed discriminant -1; retain all clauses.
Definition / construction
A weighted graph with prescribed vertex and edge pairings determines its graph lattice via the corresponding Gram matrix.
Not formalized. A generic Gram-matrix constructor is available, but no weighted-graph-to-lattice owner with the prescribed diagonal and edge weights was identified. Root-base graphs go in the opposite direction.
Definition / construction
A root is a vector whose associated reflection preserves the lattice; a root lattice is a lattice generated by its roots.
Not formalized. The general reflection-preserving root predicate exists. The native small-norm root-lattice owner is generated by norms ±1,±2 and is narrower than the source lattice generated by all reflective roots.
Definition / construction
The Dynkin diagram records a chosen root basis and their pairings.
Not formalized. The graph records nonzero pairing adjacency of chosen roots. The source Dynkin diagram records all requisite pairing data; verify the exact simply-laced/source assumptions rather than equating any unweighted graph to a Dynkin datum.
Example / comparison
For \(4\mid n\), let \(E^{(0)}\subset\mathbf Z^n\) be the even-norm sublattice and put \(\Gamma_n=\mathbf Z(\tfrac12,\ldots,\tfrac12)+E^{(0)}\). Then \(\Gamma_n\) is unimodular; it is even exactly when \(8\mid n\).
Not formalized. TauCeti supplies the dimension-eight half-vector extension. The source quantifies over every n divisible by four and proves unimodularity and the evenness criterion 8 divides n. D8+ alone is a strict special case.
Definition / construction / notation
A homomorphism of integral lattices is a module homomorphism preserving the bilinear forms. A bijective lattice homomorphism is an isometry, and two lattices joined by one are isometric.
Formalized. LeanCategories/Modules/Bilinear/Valued/Fixed.lean::BilinModuleCat.Hom, BilinModuleCat.isoMk, BilinModuleCat.linearEquivOfIso — The full lattice subcategory inherits form-preserving linear maps; bijective such maps are equivalent to categorical isomorphisms. No manual refinement of the underlying category is needed.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction
An isometry of determinant \(1\) is a rotation; one of determinant \(-1\) is a reflection.
Not formalized. The source calls every determinant-minus-one automorphism a reflection. Hyperplane-reflection constructors do not define that whole component; no pair of determinant ±1 predicates was identified.
Example / comparison
The lattice \(\Gamma _ { 8 }\) is isometric to \(E _ { 8 }\) . To see this, one takes as a basis for \(\Gamma _ { 8 }\) the roots \[ \begin{array} { r l r } { \alpha _ { 0 } } & { = } & { ( 1 , 1 , 0 , 0 , 0 , 0 , 0 , 0 , 0 , 0 ) , } \\ { \alpha _ { 1 } } & { = } & { ( \frac { 1 } { 2 } , - \frac { 1 } { 2 } , - \frac { 1 } { 2 } , - \frac { 1 } { 2 } , - \frac { 1 } { 2 } , - \frac { 1 } { 2 } , \frac { 1 } { 2 } ) , } \\ { \alpha _ { 2 } } & { = } & { ( - 1 , 1 , 0 , 0 , 0 , 0 , 0 , 0 ) , } \\ { \alpha _ { 3 } } & { = } & { ( 0 , - 1 , 1 , 0 , 0 , 0 , 0 , 0 ) , } \\ { \alpha _ { 4 } } & { = } & { ( 0 , 0 , - 1 , 1 , 0 , 0 , 0 , 0 ) , } \\ { \alpha _ { 5 } } & { = } & { ( 0 , 0 , 0 , - 1 , 1 , 0 , 0 , 0 ) , } \\ { \alpha _ { 6 } } & { = } & { ( 0 , 0 , 0 , 0 , - 1 , 1 , 0 , 0 ) , } \\ { \alpha _ { 7 } } & { = } & { ( 0 , 0 , 0 , 0 , 0 , - 1 , 1 , 0 ) , } \end{array} \]
Not formalized. An E8–D8+ isometry candidate exists. The canonical source row contains malformed OCR coordinates in its explicit basis; the exact intended basis must be normalized from the source before counting the complete example.
Example / comparison
and checks that these give the Dynkin diagram \(E _ { 8 }\) (see Fig. 1.4.1) discussed earlier. 2. The two unimodular positive definite lattices \(E _ { 8 } \oplus E _ { 8 }\) and \(\Gamma _ { 1 6 }\) of rank 16 are not isometric. Indeed, \(E _ { 8 } \oplus E _ { 8 }\) is a root lattice, but this is not the case for \(\Gamma _ { 1 6 }\) . To see this, observe that the function \(\begin{array} { r } { \sum _ { i = 1 } ^ { 1 6 } ( x _ { i } + \frac { 1 } { 2 } ) ^ { 2 } = 2 } \end{array}\) has no solution since the minimum of the left-hand side is 4, hence the only roots are \(\pm e _ { j } \pm e _ { k }\) , \(j \neq k\) , where \(\{ e _ { 1 } , \ldots , e _ { 1 6 } \}\) is the standard basis of \(\mathbb { Q } ^ { 1 6 }\) . However, the vector \(e \ = \ ( \textstyle { \frac { 1 } { 2 } } , \ldots , \textstyle { \frac { 1 } { 2 } } )\) is not in the sublattice generated by these roots. A similar statement is true for all lattices \(\Gamma _ { 8 m }\) with \(m \geq 2\) : for \(m \geq 2\) the lattice \(\Gamma _ { 8 m }\) is not a root lattice. One of the purposes of lattice theory is to classify lattices up to isometry. To this end we need isometry invariants. Here are the most obvious ones:
Not formalized. No complete E8⊕E8 versus Gamma16 nonisometry proof and all-m≥2 Gamma8m non-root-lattice statement found in these sources. An E8 construction or n=8 isometry is not this comparison.
Lemma 1.5.2
Lemma 1.5.2. For non-degenerate lattices the discriminant, index and parity are isometry invariants.
Not formalized. Determinant, signature and parity invariance have owners. The bundled signed index needs the r-s integer convention from U040; do not count natural subtraction or determinant-square-class invariance as signed determinant invariance.
Corollary 1.5.3
Corollary 1.5.3. Let \(a , a ^ { \prime } \in \mathbb { Z }\) . The lattices \(\langle a \rangle\) and \(\langle { a ^ { \prime } } \rangle\) are isometric if and only if \(a = a ^ { \prime }\) .
Not formalized. The rank-one constructor exists, but the all-a,a-prime integral isometry iff coefficient equality (including zero) is not an identified classification theorem.
Definition / construction
The isometry group \(O(L)\) consists of all lattice automorphisms preserving the form.
Formalized. LeanCategories/Lattices/Valued/OrthogonalGroup.lean::OrthogonalGroup — The elements are bijective linear self-maps preserving the bilinear form, with composition as multiplication.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Construction / comparison
An isometry \(f:L\to L\prime\) induces an isomorphism \(O(L)\to O(L\prime)\) by conjugation, \(\varphi\mapsto f\varphi f^{-1}\).
Formalized. LeanCategories/Lattices/Valued/Mass.lean::FiniteProjectiveLatticeCat.orthogonalGroupCongr — The multiplicative equivalence is conjugation by the lattice isometry; no definiteness assumption is imposed on this construction.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Lemma 1.5.4
Lemma 1.5.4. If \(L\) is an integral lattice, then for all \(k \in \mathbb { Z }\) , \(k \neq 0\) , the lattice \(L ( k )\) has the same automorphism group as \(L\) .
Not formalized. The source asserts equality/equivalence of full orthogonal groups after any nonzero integral scaling. The generic group and scale constructors alone are not that cancellation theorem.
Remark 1.5.5
Remark 1.5.5. If \(^ { b }\) is an even integral form, then \(b\) is the polar form of an integral quadratic form \(q\) . A lattice automorphism preserving \(q\) of course preserves \(^ { b }\) , but the converse is also true: an isometry (an automorphism preserving \(^ { b }\) ) also preserves \(q\) since \(\begin{array} { r } { q ( x ) = \frac { 1 } { 2 } b ( x , x ) } \end{array}\) . So we can and shall use the notation \(\mathrm { O } ( b )\) and \({ \mathrm { O } } ( q )\) interchangeably.
Not formalized. The exact integral half-norm construction and equivalence between all b-isometries and q-isometries is required. A field theorem dividing by two does not alone construct the integral q.
Definition / construction / notation
For \(x\) with \(b(x,x)\ne0\), the hyperplane reflection is \(\sigma_x(y)=y-2b(x,y)b(x,x)^{-1}x\); it is a lattice isometry when it preserves \(L\).
Formalized. LeanCategories/ForMathlib/QuadraticReflection.lean::LeanCategories.ForMathlib.reflection, LeanCategories.ForMathlib.reflection_apply — Apply to Q(v)=b(v,v) over Q: polar(Q)=2b, giving exactly y-2b(x,y)/b(x,x) x. The integral-lattice condition is that this rational involution preserves the integral carrier.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Construction / comparison
For a primitive non-isotropic vector \(x\in L\), the rational hyperplane reflection \(\sigma_x\) preserves \(L\) exactly when \(2b(x,y)\in b(x,x)\mathbf Z\) for every \(y\in L\).
Not formalized. The divisibility-based reflective predicate is a candidate, but the converse from preservation of the lattice uses primitivity of x. Verify that exact iff rather than only the sufficient divisibility construction.
Definition / construction
A \(k\)-root is a root of square \(k\).
Not formalized. The source k-root is a general reflective root together with norm k, for arbitrary k. Do not use the narrower native IsRoot predicate, which hardcodes four norms. A canonical all-k root owner was not identified.
Lemma 1.5.6
Lemma 1.5.6. Let \(( L , b )\) be a lattice. The reflection in a hyperplane orthogonal to a vector \(x \in L\) with \(b ( x , x ) = \pm 1\) or with \(b ( x , x ) = \pm 2\) preserves the lattice. All such vectors \(x\) are roots.
Formalized. LeanCategories/Lattices/Valued/RootLattice.lean::FiniteProjectiveLatticeCat.isReflective_of_isRoot — The native IsRoot alternatives are exactly norms ±1 or ±2; isReflective_of_isRoot handles all four and constructs the integral reflective structure. Reflection.lean alone handles only ±2.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Construction / comparison
Lattice isometries preserve \(k\)-roots and conjugate their reflections: \(\sigma_{\varphi(x)}=\varphi\sigma_x\varphi^{-1}\). Hence the subgroup generated by reflections in \(k\)-roots is normal in \(O(L)\).
Not formalized. The source combines preservation of all k-roots, the conjugation identity and normality of the subgroup generated by those reflections. Individual reflections and orthogonal-group constructors are insufficient.
Definition / construction
The Weyl group of a lattice is the subgroup of its isometry group generated by root reflections.
Not formalized. A Weyl-group owner must use the source collection of root reflections and its indicated norm/sign convention. Root-system Weyl groups and the source lattice subgroup require an explicit identification.
Definition / construction / notation
and will be referred to as the Weyl group of \(L\) . This is somewhat ambiguous, but the context makes clear whether \(\epsilon = 1\) or \(^ { - 1 }\) . If the lattice is definite, there is of course no confusion about signs. A lattice spanned by its \(k\) -roots (for all possible \(k\) ) is called a root lattice. Examples of root lattices can be found in Sections 4.1 and 4.2.
Not formalized. The source allows all k-roots, while the inspected native root-lattice owner uses small-norm roots. This difference is part of the definition, not a harmless specialization.
Definition / construction
A Witt decomposition of the rational quadratic space of a lattice is an orthogonal decomposition \(L_{\mathbf Q}=\widehat U\perp S\) with \(\widehat U\) containing the isotropic vectors and \(S\) anisotropic. The Witt index is \(\frac12\dim\widehat U\); over \(\mathbf R\) it equals \(\min(r,s)\) for signature \((r,s)\).
Not formalized. Witt decomposition data and line cancellation exist. The full source bundle includes the Witt index and its real value min(r,s); neither follows by unpacking the data structure. The phrase contains isotropic vectors denotes the hyperbolic part, not containment of every ambient isotropic vector.
Definition / construction / notation
where \(\hat { U }\) is an even-dimensional space which contains the isotropic vectors while \(S\) contains none. This decomposition is unique up to isometry. In particular, half the dimension of \(\widehat { U }\) is an invariant of \(L _ { \mathbb { Q } }\) , the Witt index , \({ \sf W } _ { \tau } ( L _ { \mathbb { Q } } )\) . This invariant can be defined for \(L _ { \mathbb { R } }\) as well. Here \({ \sf W } _ { \tau } ( L _ { \mathbb { R } } )\) is related to the signature \(( r , s ) \colon \mathsf { W } _ { \tau } ( L _ { \mathbb { R } } ) = \operatorname* { m i n } ( r , s )\) .
Not formalized. Line cancellation is a reusable ingredient, but no complete uniqueness of Witt decomposition, invariance of its index, and real signature formula was identified as a full bundle.
Definition / construction
The dual module of a lattice is \(L^*=\{x\in L_{\mathbf Q}:b(x,L)\subset\mathbf Z\}\); with the induced form it is the dual lattice.
Formalized. LeanCategories/Lattices/Valued/MetricDual.lean::metricDual, rieszDualLattice — The dual is the integral-pairing submodule of the rationalized carrier. Distinguish it from the abstract algebraic dual; the Riesz comparison supplies the relation under nondegeneracy.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction
The correlation morphism sends \(x\) to the functional \(b(x,-)\).
Formalized. LeanCategories/Lattices/Valued/MetricDual.lean::toAlgebraicDual; LeanCategories/Modules/Bilinear/Valued/Fixed.lean::BilinModuleCat.adjoint — The correlation is x↦b(x,-), using symmetry if an opposite convention is chosen.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Lemma 1.6.1
Lemma 1.6.1. For an integral lattice the correlation morphism \(b _ { L }\) is injective if and only if \(L\) is non-degenerate, and \(b _ { L }\) is an isomorphism if and only if \(L\) is unimodular.
Formalized. LeanCategories/Modules/Bilinear/Valued/Fixed.lean::BilinModuleCat.isLeftNondegenerate_iff_adjoint_injective, BilinModuleCat.isPerfect_iff_adjoint_bijective_of_isSymmetric; LeanCategories/Lattices/Valued/MetricDual.lean::isPerfect_iff_isUnimodular — Over finite free integral lattices, nondegeneracy means injective correlation and unimodularity means bijective correlation. The symmetric hypothesis is explicit.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction
For a sublattice \(S\subset L\), the map \(\beta_S:L\to S^*\) sends \(x\) to \([y\mapsto b(x,y)]\); its kernel is \(S^\perp\), so it induces an injection \(L/S^\perp\hookrightarrow S^*\).
Not formalized. The restricted correlation and perpendicular kernel can be built from existing maps, but no exact lattice quotient injection L/S-perp into S-dual was identified.
Lemma 1.6.2
Lemma 1.6.2. Let \(S \subset L\) be a sublattice. If \(S\) is primitive and \(L\) unimodular, the morphism \(\beta _ { S } : L / S ^ { \perp } \longrightarrow S ^ { * }\) is an isomorphism of \(\mathbb { Z }\) -modules.
Not formalized. Primitive S in unimodular L must give surjectivity onto S-dual and the quotient isomorphism L/S-perp ≃ S-dual. Generic first-isomorphism tools alone do not establish the primitive extension of functionals.
Remark: Remark
Remark. The variant \(\beta _ { S }\) of the correlation morphism is to be discussed in generality in Section 6.2.
Not formalized. The beta-map remarks refer to the quotient/perpendicular comparison in U072–073; no complete implementation of that source-specific comparison has been identified.
Definition / construction
The discriminant group of a non-degenerate lattice is \(\operatorname{dg}_L=L^*/L\).
Formalized. LeanCategories/Lattices/Valued/Discriminant.lean::discriminantGroup — The carrier is the metric dual modulo the embedded lattice, under rational nondegeneracy; it is not the determinant square-class group.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Construction / comparison
If \(d_1,\ldots,d_n\) are the elementary divisors of \(L\subset L^*\), then \(|\operatorname{dg}_L|=[L^*:L]=|\operatorname{disc}(L)|\).
Formalized. LeanCategories/Lattices/Valued/SmithNormalForm.lean::defectEquivPiZMod, natCard_defect_eq_natAbs_determinant; LeanCategories/Lattices/Valued/Discriminant.lean::discriminantCarrierEquivDefect — The canonical discriminant carrier is transported to the cokernel of the adjoint; SNF supplies its cyclic factors and cardinality equal to the absolute signed Gram determinant. Finite rank and rational perfection are explicit assumptions.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction
The length \(\ell(G)\) of a finite abelian group is its minimal number of generators; for a discriminant group one has \(\ell(\operatorname{dg}_L)\le\operatorname{rank}(L)\).
Not formalized. The decomposition supplies generators, but a canonical minimal-number-of-generators length and its bound by rank were not identified. An elementary p-rank is not the length of an arbitrary finite abelian group.
Definition / construction
For non-degenerate \(L\), the correlation isomorphism transports the rational bilinear form to \(L_{\mathbf Q}^*\) and yields a correlation map \(L_{\mathbf Q}^*\to(L_{\mathbf Q}^*)^*\). The natural evaluation map \(\lambda:L_{\mathbf Q}\to(L_{\mathbf Q}^*)^*\) is used to compare these maps and the lattice inclusions.
Not formalized. The Riesz dual and bidual comparison are candidates. The full unit also transports the form by the correlation; inspect the double-dual identification rather than identifying abstract and embedded duals without a map.
Lemma 1.6.3
Lemma 1.6.3. Let \(L\) be a non-degenerate integral lattice. 1. If one identifies \(L _ { \mathbb { Q } }\) with \(L _ { \mathbb { Q } } ^ { * }\) using the correlation map, then \(L ^ { * }\) is the free ℤ-module inside \(L _ { \mathbb { Q } }\) consisting of those \(y \in L _ { \mathbb { Q } }\) for which \(b _ { \mathbb { Q } } ( y , L ) \subset \mathbb { Z }\) . 2. If \(A = b _ { E }\) is the Gram matrix of \(b\) with respect to the basis \(\pmb { { \cal E } }\) , then \(A ^ { - 1 }\) is the Gram matrix of \(b _ { \mathbb { Q } }\) with respect to the dual basis \(E ^ { * }\) . 3. Under the identification of \(L _ { \mathbb { Q } } = L _ { \mathbb { Q } } ^ { * }\) given by the correlation map, \(A\) , respectively \(A ^ { - 1 }\) , is also the matrix expressing the \(\mathbb { Q }\) -basis \(\pmb { { \cal E } }\) in \(E ^ { * }\) , or the other way around. 4. \(b _ { L _ { \mathbb { Q } } ^ { * } } \circ b _ { L _ { \mathbb { Q } } } = \lambda\) . Under this map \(L\) and \(( L ^ { * } ) ^ { * }\) become identified.
Not formalized. The source bundles inverse Gram matrix, changes of dual bases and evaluation identification with the double dual. No single complete bundle has yet been verified.
Definition 1.6.4
Definition 1.6.4. Let \(( L , b )\) be a non-degenerate integral lattice. The discriminant bilinear form is the \(\mathbb { Q } / \mathbb { Z }\) -valued bilinear form on the discriminant group of \(L\) given by \[ b _ { L } ^ { \# } : \mathrm { d } \mathrm { g } _ { L } \times \mathrm { d } \mathrm { g } _ { L } \to \mathbb { Q } / \mathbb { Z } , \quad ( \bar { x } , \bar { y } ) \mapsto b _ { \mathbb { Q } } ( x , y ) \mathrm { m o d } \mathbb { Z } . \]
Formalized. LeanCategories/Lattices/Valued/Discriminant.lean::discriminantBilinMap, discriminantBilinMap_mk — The induced pairing takes values in the rational value quotient Q/Z and is computed by the rational pairing of lifts.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Construction / comparison
The discriminant bilinear form \(b_L^\#\) is well defined on \(L^*/L\) and is non-degenerate.
Formalized. LeanCategories/Lattices/Valued/Discriminant.lean::discriminantBilinObject_isNondegenerate — Quotient well-definedness is intrinsic to discriminantBilinMap; nondegeneracy of the induced pairing is a theorem, under the source finite/rational-nonsingularity assumptions.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition 1.6.5
Definition 1.6.5. Let \(q\) be a non-degenerate quadratic form with polar form \(^ { b }\) . Extending \(q\) in a \(\mathbb { Q }\) -quadratic fashion to \(L _ { \mathbb { Q } }\) , we have the discriminant quadratic form: \[ q _ { L } ^ { \# } : \mathrm { d g } _ { L } \mathbb { Q } / \mathbb { Z } , \quad \bar { x } \mapsto q _ { \mathbb { Q } } ( x ) \bmod \mathbb { Z } . \]
Not formalized. Choose the source half-norm Q/Z convention. The native discriminantQuadraticMap in Discriminant.lean instead polarizes to twice the bilinear form and must not be silently substituted.
Construction / comparison
If \(b\) is even, then \(q(x)=\frac12b(x,x)\) is integral and induces a discriminant quadratic form on \(L^*/L\).
Not formalized. The source asserts the half-norm quadratic discriminant refinement of an even lattice. Verify either TauCeti halfNorm or explicit inverse-doubling transport from native Q/2Z.
Definition / construction
The pairs \((\operatorname{dg}_L,b_L^\#)\) and \((\operatorname{dg}_L,q_L^\#)\) are respectively symmetric and quadratic torsion groups.
Not formalized. Candidate bundled finite bilinear and quadratic modules must be checked for the exact polar, finiteness and nonsingularity requirements.
Remark 1.6.6
Remark 1.6.6. In the literature (e.g. in [171]) often a different convention is used, namely \(\boldsymbol { q } _ { L } ^ { \# } ( \boldsymbol { x } ) = \boldsymbol { b } _ { \mathbb { Q } } ( \boldsymbol { x } , \boldsymbol { x } )\) mod \(2 \mathbb { Z }\) , i.e., we get a \(\mathbb { Q } / 2 \mathbb { Z }\) -valued form instead of a \(\mathbb { Q } / \mathbb { Z }\) - valued form. This is equivalent to our approach since multiplication by 2 induces an isomorphism \(\mathbb { Q } / \mathbb { Z } { \stackrel { \simeq } { \to } } \mathbb { Q } / 2 \mathbb { Z }\) which links the two.
Formalized. LeanCategories/Lattices/Valued/DiscriminantQuadratic.lean::doubleValueEquiv — The map multiplies rational representatives by two, identifying Q/Z with Q/2Z. Its inverse converts full norm modulo 2Z to the source half norm modulo Z; this is a value-group equivalence, not division in the finite discriminant carrier.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition 1.6.7
Definition 1.6.7. A non-zero subgroup of a torsion group is called isotropic with respect to a symmetric bilinear form (respectively a quadratic form) if the bilinear form (quadratic form) is identically zero on the subgroup.
Not formalized. Bilinear isotropy means vanishing of all pairings; quadratic isotropy means vanishing of the quadratic map. Preserve any nonzero-subgroup convention in the source; the zero subgroup may be permitted by library predicates.
Example / comparison
Let us consider the rank one module \(\mathbb { Z } e\) with form given by \(b ( e , e ) = a\) , \(a \neq 0\) , i.e., \(\langle a \rangle\) . The dual module is generated by \(\varepsilon ^ { * } = a ^ { - 1 } e\) and \(b _ { \mathbb { Q } } ( \varepsilon ^ { * } , \varepsilon ^ { * } ) = a ^ { - 2 } \cdot a = a ^ { - 1 }\) . Hence the discriminant group \(a ^ { - 1 } \mathbb { Z } e / \mathbb { Z } e \simeq \mathbb { Z } / a \mathbb { Z }\) is equipped with the bilinear form which takes the value \(a ^ { - 1 }\) mod \(\mathbb { Z }\) on the pair \(( \overline { { \varepsilon ^ { * } } } , \overline { { \varepsilon ^ { * } } } )\) . For the quadratic form \(q\) associated with the rank one forms \(\langle a \rangle\) with \(a\) even, this goes as follows. With \(e\) and \(\varepsilon ^ { * }\) as before, one has \(\begin{array} { r } { q ( e ) = \frac { 1 } { 2 } a } \end{array}\) since \(\begin{array} { r } { q ( e ) = \frac { 1 } { 2 } b ( e , e ) } \end{array}\) , and so \(q ( \varepsilon ^ { * } ) = q ( a ^ { - 1 } e ) = a ^ { - 2 } \cdot { \textstyle \frac { 1 } { 2 } } a = { \textstyle \frac { 1 } { 2 } } a ^ { - 1 } = { \textstyle \frac { 1 } { 2 } } b _ { \mathbb { Q } } ( \varepsilon ^ { * } , \varepsilon ^ { * } )\) . On the level of the discriminant group \(a ^ { - 1 } \mathbb { Z } e / \mathbb { Z } e\) this equality induces the equality \(\begin{array} { r } { q ( \varepsilon ^ { * } ) = \frac { 1 } { 2 } b _ { \mathbb { Q } } ( \varepsilon ^ { * } , \varepsilon ^ { * } ) } \end{array}\) in the value group \(\mathbb { Q } / \mathbb { Z }\) .
Not formalized. TauCeti rankOne m has Gram coefficient 2m. It verifies the even-a part with a=2m, but does not cover the source arbitrary odd-a bilinear rank-one assertion. Preserve this strict scope difference.
Example / comparison
\(^ { 2 }\) . If \(L\) is any non-degenerate lattice, then the dual module of \(L ( k )\) equals \(k ^ { - 1 } L ^ { * }\) Indeed, for \(x \in L _ { \mathbb { Q } }\) we have \[ \begin{array} { l l l } { x \in L ( k ) ^ { * } } & { \iff } & { k \cdot b ( x , y ) \in \mathbb { Z } } & { \forall y \in L } \\ & { \iff } & { b ( k \cdot x , y ) \in \mathbb { Z } } & { \forall y \in L } \\ & { \iff } & { k \cdot x \in L ^ { * } . } \end{array} \] Suppose that \(L\) is in addition unimodular of rank \(n\) . Then \(L = L ^ { * }\) , hence \(L ( k ) ^ { * } =\) \(k ^ { - 1 } L\) . Hence all elementary divisors of the discriminant group of \(L ( k )\) are equal to \(k\) so that \(\mathsf { d g } _ { L ( k ) } = k ^ { - 1 } L / L \simeq \oplus ^ { n } \mathbb { Z } / k \mathbb { Z }\) . In this case, all entries of the Gram matrix of \({ \mathsf { d g } } _ { L ( k ) }\) are in \(k ^ { - 1 } { \mathbb { Z } } / { \mathbb { Z } }\) and so the discriminant form of \(L ( k )\) is \(k ^ { - 1 } { \mathbb { Z } } / { \mathbb { Z } }\) -valued. Let us next explain how to find the discriminant group from the Gram matrix \(A\) of \(L\) with respect to an \(L\) -basis \(\pmb { { \cal E } }\) . We just observed that the rows (and columns, by symmetry) of \(A ^ { - 1 }\) express the dual basis \(\pmb { E } ^ { * }\) for \(L ^ { * }\) in the basis \(\pmb { { \cal E } }\) for \(L\) . Elementary row and column operations that are unimodular correspond to new bases for \(L\) and for \(L ^ { * }\) (viewed as ℤ-modules). Hence suitable bases can be found so that \(A\) is equivalent to a diagonal form. We shall show that using elementary row and column operations carefully, the diagonal elements give the elementary divisors of \(L ^ { * } / L\) : Step 1: since \(A\) is non-singular, no column is zero and by a row operation we move a non-zero entry \(A _ { 1 }\) to place \(( 1 , 1 )\) . Using integral row and column addition, replace the other entries in the first column and row by 0 or by a non-zero element with absolute value \(< | A _ { 1 } |\) . Step 2: repeat step 1 with such a non-zero element, and so on until all entries in the first column and row are 0 except the (new) entry \(A _ { 1 , 1 }\) . Step 3: if there is a non-zero entry \(A _ { i , j }\) , \(i , j \ge 2\) , that is not divisible by \(A _ { 1 , 1 }\) we add the \(i\) -the row to the first and start step 1 and 2 anew. Repeating this step makes all entries \(A _ { 1 , j }\) , \(j \geq 2\) , \(A _ { i , 1 }\) , \(i \geq 2\) zero, and makes the entries \(A _ { i , j }\) , \(i , j \geq 2\) , divisible by \(A _ { 1 , 1 }\) . Step 4: repeat steps 1–3 with the matrix \(( A _ { i , j } ) , i , j \ge 2\) .
Not formalized. Scaled duals and SNF exist. The unit also asks for the resulting discriminant pairing and the source computational prescription, including the unimodular special case; no complete comparison was identified.
Example / comparison
Example 1.6.9. On \(L = \mathbb { Z } e _ { 1 } \oplus \mathbb { Z } e _ { 2 } \oplus \mathbb { Z } e _ { 3 }\) consider the even form \(b _ { A }\) given by the Gram matrix \(A = { \left( \begin{array} { l l l } { - 2 } & { 1 } & { 0 } \\ { 1 } & { 2 } & { 1 } \\ { 0 } & { 1 } & { - 2 } \end{array} \right) } .\) The form \(b _ { A }\) is also the polar form of an integral quadratic form \(q _ { A }\) « ¬. It is best to exchange rows 1 and 2 so that the first column and row can be handled quickly, yielding \({ \left( \begin{array} { l l l } { 1 } & { 0 } & { 0 } \\ { 0 } & { 5 } & { 2 } \\ { 0 } & { 1 } & { - 2 } \end{array} \right) } .\) Now we repeat the steps for \(\left( { \begin{array} { c c } { 5 } & { 2 } \\ { 1 } & { - 2 } \end{array} } \right)\) by first exchanging rows \(1\) and 2. Finally we arrive at \(\left( { \begin{array} { c c c } { 1 } & { 0 } & { 0 } \\ { 0 } & { 1 } & { 0 } \\ { 0 } & { 0 } & { 1 2 } \end{array} } \right)\) so that \(\mathrm { d g } _ { L } \simeq \mathbb { Z } / 1 2 \mathbb { Z } \simeq \mathbb { Z } / 2 ^ { 2 } \mathbb { Z } \times \mathbb { Z } / 3 \mathbb { Z }\) « ¬. The third column of the inverse matrix \(\begin{array} { r } { A ^ { - 1 } = \frac { 1 } { 1 2 } \left( \begin{array} { c c c } { - 5 } & { 2 } & { 1 } \\ { 2 } & { 4 } & { 2 } \\ { 1 } & { 2 } & { - 5 } \end{array} \right) } \end{array}\) represents a vector \(e _ { 3 } ^ { * } \in L ^ { * }\) which is obviously of order 12 \(L\) so mumod gen and \({ \mathsf { d g } } _ { L }\) hen tmod discriminant forms are given by. \(\begin{array} { r } { b _ { A , \mathbb { Q } } ( e _ { 3 } ^ { * } , e _ { 3 } ^ { * } ) = \frac { 7 } { 1 2 } } \end{array}\) \(\mathbb { Z }\) \(\begin{array} { r } { q _ { A , \mathbb { Q } } ( e _ { 3 } ) = \frac { 7 } { 2 4 } } \end{array}\) \(\mathbb { Z }\)
Not formalized. The specified rank-three determinant-12 example, cyclic generator and values 7/12 and 7/24 are not an identified formal example. A generic matrix constructor is not this computed comparison.
Definition / construction
For a non-degenerate integral lattice with elementary divisors \(d_1\mid\cdots\mid d_r\), choose a basis of \(L^*\) adapted so that \(e_i=d_i\varepsilon_i^*\) for \(i\le r\) and the classes of \(\varepsilon_1^*,\ldots,\varepsilon_r^*\) generate the discriminant group.
Not formalized. SNF of the adjoint is available. The source additionally identifies adapted dual bases and discriminant generators with their form coefficients; this is not merely the cokernel decomposition.
Definition / construction / notation
The set \(s\) is called an ordered basis of \({ \mathsf { d g } } _ { L }\) and we shall investigate the shape of the Gram matrix \(B _ { S }\) of the discriminant form on such a basis \(\pmb { S }\) . First note that since \(b _ { \mathbb { Q } } ( e _ { i } , \varepsilon _ { j } ^ { * } ) \in \mathbb { Z }\) , \(b _ { \mathbb { Q } } ( \varepsilon _ { i } ^ { * } , \varepsilon _ { j } ^ { * } ) = { d _ { i } } ^ { - 1 } b _ { \mathbb { Q } } ( e _ { i } , \varepsilon _ { j } ^ { * } ) \in { d _ { i } } ^ { - 1 } \mathbb { Z }\) for \(i , j = 1 , \dots , r\) . Secondly, all \(d _ { i }\) divide \(d _ { r }\) and so \(B _ { S }\) is \(d _ { r } ^ { - 1 } \mathbb { Z } / \mathbb { Z }\) -valued and, by the preceding remarks, is represented by the \(\mathbb { Q }\) -valued matrix \[ B ^ { \prime } = \left( \begin{array} { l l l l l } { \displaystyle \frac { \beta _ { 1 1 } } { d _ { 1 } } } & { \displaystyle \frac { \beta _ { 1 2 } } { d _ { 1 } } } & { \cdots } & { \displaystyle \frac { \beta _ { 1 r } } { d _ { 1 } } } \\ { \displaystyle \frac { \beta _ { 2 1 } } { d _ { 1 } } } & { \displaystyle \frac { \beta _ { 2 2 } } { d _ { 2 } } } & { \cdots } & { \displaystyle \frac { \beta _ { 2 r } } { d _ { 2 } } } \\ { \vdots } & { \ddots } & { \vdots } & { \vdots } \\ { \displaystyle \frac { \beta _ { r 1 } } { d _ { 1 } } } & { \displaystyle \frac { \beta _ { r 2 } } { d _ { 2 } } } & { \cdots } & { \displaystyle \frac { \beta _ { r r } } { d _ { r } } } \end{array} \right) \quad \mathrm { f o r ~ c e r t a i n ~ } \beta _ { i j } = \beta _ { j i } \in \mathbb { Z } . \]
Not formalized. No canonical matrix representation of the finite discriminant pairing with the specified denominator convention was identified.
Construction / comparison
For an ordered basis adapted to the elementary divisors \(d_1\mid\cdots\mid d_r\) of a discriminant group, the Gram matrix of the discriminant bilinear form has its \(i\)-th row and column in \(d_i^{-1}\mathbf Z/\mathbf Z\). For an even lattice the associated discriminant quadratic matrix has diagonal entries in \((2d_r)^{-1}\mathbf Z/\mathbf Z\).
Not formalized. The row/column denominator and even-diagonal denominator constraints for a general finite quadratic module require the complete source matrix statement, not only a cyclic example.
Remark 1.6.10
Remark 1.6.10. Of course, the form \(b _ { \mathbb { Q } }\) on \(L _ { \mathbb { Q } } ^ { * }\) does not in general assume integral values on \(L ^ { * }\) , but, as we have seen, if \(d\) is the largest elementary divisor of \({ \mathsf { d g } } _ { L }\) , then \(d \cdot b _ { \mathbb { Q } } | L ^ { * }\) is integer valued. More generally, if \(\rho \in \mathbb { Z }\) , \(\rho > 0\) , is such that \(\rho \cdot b _ { \mathbb { Q } } | L ^ { * }\) assumes integral values, we can consider the lattice \(L ^ { * } ( \rho )\) , that is, \(L ^ { * }\) equipped with \(\rho \cdot b _ { \mathbb { Q } }\) . Example 1.6.8.2 can be generalized to this situation by expressing the elementary divisors of the discriminant group of \(L ^ { * } ( \rho )\) in terms of the elementary divisors \(d _ { 1 } , \ldots , d _ { r }\) of \({ \mathsf { d g } } _ { L }\) , where these satisfy the usual divisibility relations \(d _ { 1 } | d _ { 2 } | \cdots | d _ { r }\) . To start with, the dual module of \(L ^ { * } ( \rho )\) equals \(1 / \rho \cdot ( L ^ { * } ) ^ { * }\) . There is a basis \(\{ \varepsilon _ { 1 } ^ { * } , \ldots , \varepsilon _ { n } ^ { * } \}\) for \(L ^ { * }\) such that \[ \pmb { { \cal E } } = \{ \varepsilon _ { 1 } = d _ { 1 } \varepsilon _ { 1 } ^ { * } , \ldots , \varepsilon _ { r } = d _ { r } \varepsilon _ { r } ^ { * } , \varepsilon _ { r + 1 } ^ { * } , \ldots , \varepsilon _ { n } ^ { * } \} \] is a basis for \(L \subset L ^ { * }\) . We identify \(L\) and its double dual using the composition \(b _ { L _ { 0 } ^ { * } } \circ b _ { L _ { \mathbb { Q } } }\) of the correlation maps. \(( \mathrm { S o } L ^ { \ast } ( \rho ) ^ { \ast } / L ^ { \ast } ( \rho )\) is isomorphic to \(\scriptstyle { \frac { 1 } { \rho } } L / L ^ { * } ( \rho )\) .) Since \(1 / \rho \cdot E\) is a basis of \(( L ^ { * } ( \rho ) ) ^ { * } = 1 / \rho \cdot L \subset 1 / \rho \cdot L ^ { * }\) , we see that \(d _ { 1 } ^ { * } = \rho / d _ { 1 } , \ldots , d _ { r } ^ { * } =\) \(\rho / d _ { r } , d _ { r + 1 } ^ { * } = \rho , \ldots , d _ { n } ^ { * } = \rho\) yield the elementary divisors of \(\mathrm { d } \mathrm { g } _ { L ^ { * } ( \rho ) }\) by leaving out terms for which \(d _ { j } = \rho\) . The discriminant quadratic form of \(^ { b }\) takes values in \(( 2 d ) ^ { - 1 } \mathbb { Z } / \mathbb { Z }\) , while the discriminant quadratic form for the lattice \(L ^ { * } ( \rho )\) takes values in \(( 2 \rho ) ^ { - 1 } \mathbb { Z } / \mathbb { Z }\) .
Not formalized. No full scaled-dual elementary-divisor transformation d_i↦rho/d_i with its source hypotheses was identified.
Lemma 1.7.1
Lemma 1.7.1. Neighbouring lattices of a non-degenerate lattice \(N\) have the same discriminant. For odd primes \(p\) the \(\boldsymbol { p }\) -primary part of the discriminant group of \(a\) neighbour of \(N\) is isomorphic to the \(p\) -primary part of \(N ^ { * } / N\) . In particular, discriminant groups of neighbouring lattices with odd discriminant are all isomorphic.
Not formalized. Neighbor lattices and their odd-primary discriminant comparison are not supplied by general genus-invariance declarations.
Example / comparison
For the even-coordinate-sum sublattice \(E^{(0)}\subset\mathbf Z^n\), if \(n\) is odd then \((E^{(0)})^*/E^{(0)}\cong\mathbf Z/4\mathbf Z\); if \(n\) is even its three non-zero classes all have order \(2\).
Not formalized. Resolve the generic D_n discriminant-group isomorphisms and rank restrictions; the odd-rank cyclic-four and even-rank Klein-four cases must both be present.
Example / comparison
If \(L\) is odd unimodular, its even sublattice \(L^{(0)}\) has index \(2\) and sits in \(L^{(0)}\subset L=L^*\subset(L^{(0)})^*\). For \(W=\langle1\rangle\oplus\langle-1\rangle\), the two other unimodular neighbours of \(W^{(0)}\simeq U(2)\) are both isometric to \(U\).
Not formalized. The whole example needs index-two even part of every odd unimodular lattice plus explicit U(2) and alternate-neighbor identifications. Evenness predicates alone are not this result.
Definition 1.7.2
Definition 1.7.2. A 2-elementary even lattice is a type \(\boldsymbol { \mathit { I } }\) lattice if its discriminant quadratic form is \({ \frac { 1 } { 2 } } \mathbb { Z } / \mathbb { Z }\) -valued and it is a type \(\pi\) lattice otherwise, i.e., its discriminant quadratic form takes at least one value in \(\scriptstyle { { \frac { 1 } { 4 } } \mathbb { Z } } / \mathbb { Z } - { \frac { 1 } { 2 } } \mathbb { Z } / \mathbb { Z }\) .
Not formalized. The native annihilator-based elementary predicates do not define the type-I/type-II dichotomy for dyadic finite quadratic forms and its denominator criterion.
Construction / comparison
For a type-I \(2\)-elementary even lattice, the polar discriminant form is non-degenerate and \(\dim W_L\) is even; type-II lattices do not carry the same induced \(\mathbf F_2\) inner-product structure.
Not formalized. Individual Klein-four models do not establish the general type-I symplectic F2 form, even-dimensionality and contrast with type II.
Example / comparison
The hyperbolic lattice \(U(2)\) is a type-I \(2\)-elementary even lattice, whereas \(\langle2\rangle\) is type II, since its discriminant quadratic form takes the value \(1/4\) on a generator.
Not formalized. The U(2) and <2> constructors do not by themselves prove their respective type-I/type-II discriminant classifications.
Example / comparison
Example 1.7.3. For a finite group \(G\) acting isometrically on a non-degenerate lattice \(L\), the invariant lattice \(L^G\) and coinvariant lattice \(L_G=(L^G)^\perp\) are primitive and non-degenerate, \(L^G\oplus L_G\) has finite index in \(L\), and \(|G|L\subset L^G\oplus L_G\). If \(L\) is unimodular and \(|G|=p\) is prime, both \(L^G\) and \(L_G\) are \(p\)-elementary.
Not formalized. This bundle needs primitivity/nonsingularity of invariants and perpendicular coinvariants, an index bound and p-elementarity for arbitrary prime-order action. Involution-only or constructor-only data is insufficient.
Definition / construction / notation
1.7.C Overlattices. An overlattice of a non-degenerate symmetric lattice \(( N , b )\) is an integral lattice \(L\) containing \(N\) as a finite index sublattice. In particular \(b _ { \mathbb { Q } } | L\) is integer valued. If the latter form is even, we say that \(L\) is a quadratic overlattice.
Formalized. LeanCategories/Lattices/Valued/Gluing.lean::Overlattice; LeanCategories/Lattices/Valued/ScaleAndEvenness.lean::IsEven — For a nondegenerate integral lattice, Overlattice is an integral intermediate carrier between L and its metric dual; finite index follows from the finite discriminant setting. The source quadratic-overlattice refinement is exactly the IsEven condition on the restricted form.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Proposition 1.7.4
Proposition 1.7.4. 1. The overlattices \(L\) of a non-degenerate lattice \(( N , b )\) are in one-to-one correspondence with the isotropic subspaces \(\mathsf { H }\) of \(( \mathsf { d g } _ { N } , b _ { N } ^ { \# } )\) . The correspondence is given by \[ \begin{array} { r l } & { L \longmapsto \mathsf { H } _ { L } : = L / N } \\ & { \mathsf { H } \longmapsto \quad L _ { \mathsf { H } } : = \{ y \in N ^ { * } \mid y \bmod N \in \mathsf { H } \} . } \end{array} \] 2. The discriminant group of an overlattice \(L\) is \(( L / N ) ^ { \perp } / ( L / N )\) with discriminant form induced by the form \(b _ { N } ^ { \# }\) on \(N ^ { * } / N\) (observe that \(b _ { N } ^ { \# } | _ { L / N } = 0 .\) ). Unimodular overlattices \(L\) correspond to maximal isotropic subspaces of \(( \mathsf { d g } _ { N } , b _ { N } ^ { \# } )\) that is, overlattices \(L\) for which \(( L / N ) ^ { \perp } = L / N\) . 3. If ?? is even and \(\begin{array} { r } { q ( x ) = \frac { 1 } { 2 } b ( x , x ) } \end{array}\) , there is a one-to-one correspondence between subspaces isotropic with respect to the discriminant quadratic form on the one hand and even overlattices of \(N\) on the other hand.
Formalized. TauCeti/LinearAlgebra/IntegralLattice/Overlattice/Isotropic.lean::integralIntermediateCarrierOrderIsoIsotropicSubgroup, evenIntermediateCarrierOrderIsoIsotropicSubgroup; TauCeti/LinearAlgebra/IntegralLattice/Overlattice/OrthogonalQuotient/Bilinear.lean::IntermediateCarrier.discriminantBilinearOrthogonalQuotientIsometry; TauCeti/LinearAlgebra/IntegralLattice/Overlattice/OrthogonalQuotient/Quadratic.lean::IntermediateCarrier.discriminantOrthogonalQuotientIsometry; TauCeti/LinearAlgebra/IntegralLattice/Overlattice/Dual.lean::IntermediateCarrier.dual_eq_self_iff_isLagrangian — Full isotropic-subgroup correspondence as an order isomorphism, discriminant isometry A_M≃H-perp/H and unimodularity iff self-orthogonal subgroup. The quadratic version uses half norm in Q/Z and even subgroups/lattices. All statements assume the original lattice nondegenerate.
Searched: TauCeti@98a6bfc9f3cb4ab3a159d83858ce546d1e543c1b; Apache-2.0; Lean 4.34.0-rc2; Mathlib e21ec05048292b3de86d4cf1987e2208171a5642; source port required for project Lean 4.33.0
Example / comparison
We return to the lattice \(U ( 2 )\) in example 2 on page 34. The bilinear form is denoted \(^ { b }\) . Retaining the notation used there, \(U ( 2 ) = \mathbb { Z } ( e + f ) +\) \(\mathbb { Z } ( e - f )\) , where \(b ( e , e ) = 1\) , \(b ( f , f ) = - 1\) , and \(b ( e , f ) = 0\) . Now \(U ( 2 ) ^ { * } / U ( 2 ) =\) \(\scriptstyle { \frac { 1 } { 2 } } U ( 2 ) / U ( 2 )\) with the induced discriminant symmetric form \(b ^ { \# }\) has three isotropic subspaces (of order 2): \(\langle \overline { { e } } \rangle\) , \(\big \langle { \textstyle { \frac { 1 } { 2 } } } ( \overline { { e } } - \overline { { f } } ) \big \rangle\) , \(\big \langle { \textstyle { \frac { 1 } { 2 } } } ( \overline { { e } } + \overline { { f } } ) \big \rangle\) . These correspond to the three overlattices \(W = \mathbb { Z } e + \mathbb { Z } f\) , \(U ^ { \prime } = \mathbb { Z } ( e + f ) + \mathbb { Z } ( \textstyle \frac { 1 } { 2 } ( e - f ) )\) , and \(U ^ { \prime \prime } = \mathbb { Z } ( e - f ) + \mathbb { Z } ( \textstyle \frac { 1 } { 2 } ( e + f ) )\) , respectively. With respect to the discriminant quadratic form \(q ^ { \# }\) induced by the quadratic form \(\begin{array} { r } { q ( x ) = \frac { 1 } { 2 } b ( x , x ) } \end{array}\) on \(U ( 2 )\) , however, only \(\big \langle { \textstyle { \frac { 1 } { 2 } } } ( \overline { { e } } - \overline { { f } } ) \big \rangle\) and \(\big \langle { \textstyle { \frac { 1 } { 2 } } } ( \overline { { e } } + \overline { { f } } ) \big \rangle\) are isotropic (note that \(q ^ { \# } ( \overline { { e } } ) = \textstyle { \frac { 1 } { 2 } }\) (mod \(\mathbb { Z } )\) ). So the quadratic form ‘detects’ the even overlattices \(U ^ { \prime }\) and \(U ^ { \prime \prime }\) .
Not formalized. No complete enumeration of the three bilinear-isotropic lines of U(2), two quadratic-isotropic lines and the two specified even overlattices was identified.
Example / comparison
Consider the quadratic lattice \(N = \mathbb { Z } ^ { 8 } ( 2 )\) . In \(N ^ { * } / N\) take the span of the vectors \(\scriptstyle { \frac { 1 } { 2 } } ( 1 , 1 , 1 , 1 , 0 , 0 , 0 , 0 )\) , \(\scriptstyle { \frac { 1 } { 2 } } ( 1 , 1 , 0 , 0 , 1 , 1 , 0 , 0 )\) , \(\scriptstyle { \frac { 1 } { 2 } } ( 1 , 1 , 0 , 0 , 0 , 0 , 1 , 1 )\) , \(\scriptstyle { \frac { 1 } { 2 } } ( 1 , 0 , 0 , 1 , 1 , 0 , 0 , 1 )\) . This is an isotropic subspace of dimension 4. This leads to an even overlattice \(L\) in which \(N\) is a sublattice of index \(2 ^ { 4 }\) . By Lemma \(1 . 2 . 2 \ \operatorname { d i s c } ( L ) = 1\) and so \(L \simeq E _ { 8 }\) since up to isometry \(E _ { 8 }\) is the only positive definite quadratic lattice of rank 8 (see Section 1.12 for further background). Lemma 4.1.6 gives an alternative explanation of this embedding by looking at roots. Taking the span of \(\scriptstyle { \frac { 1 } { 2 } } ( 1 , 1 , 1 , 1 , 0 , 0 , 0 , 0 )\) , \(\scriptstyle { \frac { 1 } { 2 } } ( 0 , 0 , 0 , 0 , 1 , 1 , 1 , 1 )\) , \(\scriptstyle { \frac { 1 } { 2 } } ( 0 , 0 , 1 , 1 , 1 , 1 , 0 , 0 )\) in \(N ^ { * } / N\) we obtain in a similar way an even overlattice isometric to \(D _ { 8 }\) studied in Section 4.1.A. Indeed, a basis consisting of roots is given by the vectors in \(N ^ { * }\) (corresponding to the roots \(\alpha _ { 1 } , \ldots , \alpha _ { 8 }\) of the corresponding Dynkin diagram on page 81) \[ \begin{array} { l l } { \alpha _ { 1 } = ( 0 , 0 , 0 , 0 , - \frac { 1 } { 2 } , - \frac { 1 } { 2 } - \frac { 1 } { 2 } , - \frac { 1 } { 2 } ) , } & { \alpha _ { 2 } = ( 0 , 0 , 0 , 0 , \frac { 1 } { 2 } , \frac { 1 } { 2 } , \frac { 1 } { 2 } , - \frac { 1 } { 2 } ) , } \\ { \alpha _ { 3 } = ( 0 , 0 , 0 , 0 , - \frac { 1 } { 2 } , \ \frac { 1 } { 2 } , - \frac { 1 } { 2 } , \ \frac { 1 } { 2 } ) , } & { \alpha _ { 4 } = ( 0 , 0 , \frac { 1 } { 2 } , - \frac { 1 } { 2 } , \frac { 1 } { 2 } , - \frac { 1 } { 2 } , \ 0 , \ 0 ) , } \\ { \alpha _ { 5 } = ( - \frac { 1 } { 2 } , \frac { 1 } { 2 } , - \frac { 1 } { 2 } , \frac { 1 } { 2 } , 0 , 0 , 0 , 0 ) , } & { \alpha _ { 6 } = ( \frac { 1 } { 2 } , - \frac { 1 } { 2 } - \frac { 1 } { 2 } , - \frac { 1 } { 2 } , 0 , 0 , 0 , 0 ) , } \\ { \alpha _ { 7 } = ( - \frac { 1 } { 2 } , - \frac { 1 } { 2 } , \ \frac { 1 } { 2 } , \ \frac { 1 } { 2 } , 0 , 0 , 0 , 0 ) , } & { \alpha _ { 8 } = ( \frac { 1 } { 2 } , \ \frac { 1 } { 2 } , \ \frac { 1 } { 2 } , \frac { 1 } { 2 } , 0 , 0 , 0 , 0 ) . } \end{array} \] Proposition 1.7.4 also leads to the next result:
Not formalized. D8+≃E8 is a candidate, but the source bundle additionally uses the particular binary isotropic code in A_(Z8(2)) and a uniqueness assertion. The specific glue construction and uniqueness are not supplied by the isometry alone.
Lemma 1.7.6
Lemma 1.7.6. Let \(S\) be a non-degenerate primitive sublattice of a unimodular lattice \(L\) and \(T = S ^ { \perp }\) its orthogonal complement. Then there is a natural isometry \(\mathsf { d g } _ { S } \overset { \simeq } { \to } \mathsf { d g } _ { T } ( - 1 )\) of discriminant bilinear forms. If \(L\) is even it is an isometry of discriminant quadratic forms.
Not formalized. Anti-isometry structures and glue constructors assume the discriminant anti-isometry. They do not prove it from primitively embedded orthogonal complements in a unimodular lattice.
Proposition 1.7.7
Proposition 1.7.7 (Extending isometries). Let \(L\) , \(L ^ { \prime }\) be overlattices of non-degenerate symmetric (or quadratic) lattices \(N\) , \(N ^ { \prime }\) respectively. An isometry \(\lambda : N \overset { \sim } { \to } N ^ { \prime }\) extends to an isometry \(L \stackrel { \sim } { \to } L ^ { \prime }\) if and only if the isomorphism induced by \(\lambda\) on the discriminant groups sends \(L / N\) to \(L ^ { \prime } / N ^ { \prime }\) . In particular, \(\lambda \in { \mathsf { O } } ( N )\) extends to an isometry of \(L\) if and only if \(r _ { N , N ^ { \prime } } ( \lambda )\) preserves \(L / N\) .
Formalized. TauCeti/LinearAlgebra/IntegralLattice/Overlattice/Naturality.lean::Isometry.discriminantSubgroup_intermediateCarrierEquiv, Isometry.intermediateCarrierEquiv_intermediateCarrierOfDiscriminantSubgroup, Isometry.toIntegralLatticeIsometry — The order-isomorphism transport identifies the transported overlattice with the preimage of the transported discriminant subgroup, and constructs the restricting lattice isometry. Equality of the subgroup is equivalent to equality of its preimage by the established order isomorphism. This supplies both directions of the extension criterion.
Searched: TauCeti@98a6bfc9f3cb4ab3a159d83858ce546d1e543c1b; Apache-2.0; Lean 4.34.0-rc2; Mathlib e21ec05048292b3de86d4cf1987e2208171a5642; source port required for project Lean 4.33.0
Lemma 1.8.1
Lemma 1.8.1. Every even lattice \(( S , b )\) of rank \(s \leq a\) can be isometrically embedded in \[ \cal { L } = \underbrace { U \oplus \cdots \oplus U } _ { a c o p i e s } \] as a primitive sublattice such that \(S ^ { \perp } \simeq S ( - 1 ) \oplus \oplus ^ { ( a - s ) } U\) , where we view \(S\) as embedded in \(L\) .
Not formalized. No general primitive embedding S into U^a with perpendicular -S⊕U^(a-rank S) and all source rank/parity assumptions was identified.
Definition / construction / notation
To classify an integral lattice \(( L , b )\) , one traditionally passes to its localizations \(L _ { p }\) at primes \(p\) . By definition, \(L _ { p } = L \otimes _ { \mathbb { Z } } \mathbb { Z } _ { p }\) , where \(\mathbb { Z } _ { p }\) is the ring of \(p\) -adic integers.5 One extends the form \(^ { b }\) in a \(\mathbb { Z } _ { p }\) -linear fashion which results in a symmetric form \(b _ { p }\) on \(L _ { p }\) . Summarizing, we have \[ L _ { p } : = L \otimes _ { \mathbb { Z } } \mathbb { Z } _ { p } , \quad b _ { p } { \mathrm { ~ t h e ~ } } p { \mathrm { - a d i c ~ b i l i n e a r ~ e x t e n s i o n ~ o f ~ } } b . \]
Formalized. LeanCategories/Lattices/Valued/BaseChange.lean::baseChangeFiniteIntegral, baseChangeIntegral_pairing_tmul — Specializing finite integral scalar extension to Z -> Z_p gives L_p = L tensor Z_p and the displayed p-adic bilinear extension on pure tensors.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction / notation
For a \(p\)-adic lattice, the determinant of a Gram matrix defines the discriminant modulo squares of \(p\)-adic units.
Not formalized. The local lattice determinant retains its valuation and is taken modulo squares of units, whereas FieldSquareClass discards even valuation. The exact quotient/pair encoding for arbitrary nonzero determinant has not been identified.
Definition / construction / notation
As for forms on vector spaces and on free \(\mathbb { Z }\) -modules, we say that the lattice \(( L _ { p } , b _ { p } )\) is non-degenerate if \(\mathrm { d i s c } ( b _ { p } ) \neq 0\) and unimodular if \(\operatorname { d i s c } ( b _ { p } )\) is itself a unit up to squares, i.e., belongs to \(\mathsf { D } ( \mathbb { Z } _ { p } )\) .
Formalized. LeanCategories/Lattices/Valued/MetricDual.lean::IsFractionFieldNondegenerate, IsUnimodular — Specialize the integral pairing to Z_p; rational nondegeneracy and integral unimodularity remain distinct. Nonzero/unit Gram determinant criteria are the respective ones.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction / notation
The form \(b _ { p }\) induces a \(\mathbb { Q } _ { p } / \mathbb { Z } _ { p }\) -valued discriminant symmetric form ??# \(b _ { L _ { p } } ^ { \# }\) and \(( L _ { p } , q _ { p } )\) , using the polar form \(b _ { \mathbb { Q } _ { p } }\) to define \(L _ { p } ^ { * }\) , leads to a discriminant quadratic form \(q _ { L _ { p } } ^ { \# }\) on \(\mathrm { d g } _ { L _ { p } }\) : \[ \begin{array} { r l } { b _ { L _ { p } } ^ { \# } : \mathrm { d g } _ { L _ { p } } \times \mathrm { d g } _ { L _ { p } } } & { \longrightarrow \mathbb { Q } _ { p } / \mathbb { Z } _ { p } } \\ { q _ { L _ { p } } ^ { \# } : \quad \mathrm { d g } _ { L _ { p } } } & { \longrightarrow \mathbb { Q } _ { p } / \mathbb { Z } _ { p } . } \end{array} \]
Formalized. LeanCategories/Lattices/Valued/Discriminant.lean::discriminantGroup, FractionValueQuotient, discriminantBilinMap; LeanCategories/Lattices/Valued/DiscriminantQuadratic.lean::evenDiscriminantQuadraticMap, doubleValueEquiv — Specializing to the p-adic integer ring gives the bilinear discriminant form. For a quadratic lattice the project stores twice the source quadratic value in the double quotient; doubleValueEquiv is multiplication by two and identifies that convention with the source quotient-valued quadratic discriminant form.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction / notation
The set of all places of \(\mathbb { Q }\) is denoted by \(\mathcal { P }\) . This can be generalized to number fields where there are more places at infinity corresponding to embeddings of the field in the real or complex numbers. Except in Chapter 5.1 we won’t make use of this.
Not formalized. The source also introduces the places of a general number field, not merely the primes and real place of Q. Verify the unified finite/infinite place owner and notation before claiming this bundle.
Definition 1.9.1
Definition 1.9.1. The genus \({ \mathfrak { g } } ( L )\) of a lattice \(L\) is the set of isometry classes of lattices \(L ^ { \prime }\) such that \(L _ { v } ^ { \prime } \simeq L _ { v }\) for all places \(v \in \mathcal { S } ^ { }\) . We then say that the lattices \(L\) and \(L ^ { \prime }\) belong to the same genus, or, that they are genus-equivalent.
Formalized. LeanCategories/Lattices/Valued/LocalGlobal.lean::SameGenus — SameGenus quantifies integral isometry over all Z_p and real isometry, not just equality of rational forms over Q_p.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Construction / comparison
Lattices in the same genus can represent different integral isometry classes, but their rational quadratic spaces are isometric by the Hasse principle.
Not formalized. The local-global rational isometry consequence and the existence of distinct global integral classes in one genus are both required. Hanke LocalGlobalHassePrinciple is an empty imports/comments file; RatfuncWitt uses a different field. Neither supplies Hasse–Minkowski over Q.
Construction / comparison
Non-degeneracy, unimodularity, and discriminant commute with localization: for every place \(v\), \(\operatorname{disc}(L_v)\) is the image of \(\operatorname{disc}(L)\) in the local square-class group.
Not formalized. Need all local nondegeneracy/unimodularity tests and localization of discriminant. Global unimodularity is equivalent to unimodularity at every prime, not at one chosen prime. The individual base-change construction is insufficient.
Construction / comparison
The global discriminant is recovered from the local data by its real sign together with the \(p\)-primary orders of the discriminant group: \(\operatorname{disc}(L)=\operatorname{disc}(L_\infty)\prod_p p^{v(p)}\).
Not formalized. No complete signed-determinant reconstruction from the sign and the product of local discriminant orders was identified.
Proposition 1.9.2
Proposition 1.9.2. 1. The discriminant is a genus-invariant: all lattices of the same genus have the same discriminant. 2. The parity of a lattice is a genus-invariant: lattices of the same genus are either all even or all odd.
Not formalized. Signed determinant invariance exists. The entire source unit also includes parity invariance, which needs the integral two-adic test; do not count the determinant theorem as the pair of invariants.
Example / comparison
Example 1.9.3. Suppose that \(L\) has discriminant \(- 2 ^ { 2 } \cdot 3 ^ { 2 } \cdot 7 ^ { 4 }\) . Then the local discriminants at the places \(\infty , 2 , 3 , 7\) are \(- 1 , 7 \cdot 2 ^ { 2 } , 2 \cdot 3 ^ { 2 } , 6 \cdot 7 ^ { 4 }\) . This is clear for the place at \(\infty\) . For the prime 2 one observes that \(- 3 ^ { 2 } { \cdot } 7 ^ { 4 } \equiv 7\) mod 8 and Theorem A.2.1 tells us that the units in \(\mathbb { Z } _ { 2 }\) modulo squares of units are represented modulo 8 by one of the four numbers \(1 , 3 , 5 , 7\) . For the primes 3 and 7 we observe that \(- 2 ^ { 2 } \cdot 7 ^ { 4 } \equiv 2\) mod 3 respectively \(- 2 ^ { 2 } \cdot 3 ^ { 2 } \equiv 6\) mod 7. Conversely, given local discriminants \(- 1 , 7 \cdot 2 ^ { 2 } , 2 \cdot 3 ^ { 2 } , 6 \cdot 7 ^ { 4 }\) at the places \(\infty , 2 , 3 , 7\) and 1 elsewhere, we retrieve the global discriminant \(- 2 ^ { 2 } \cdot 3 ^ { 2 } \cdot 7 ^ { 4 }\) . Note that apart from the sign of \(L _ { \infty }\) , only the \(p\) -adic orders of the local discriminants are relevant in determining the global discriminant.
Not formalized. The specified determinant and local unit-square-class computations at 2,3,7 were not found as a verified Lean example.
Construction / comparison
Discriminant forms commute with localization: the restriction of \(b_L^\#\) to the \(p\)-primary discriminant group identifies, via \(\mathbf Q^{(p)}/\mathbf Z\simeq\mathbf Q_p/\mathbf Z_p\), with the discriminant form of \(L_p\); similarly for discriminant quadratic forms of even lattices.
Not formalized. Primary decomposition of an abstract finite form does not identify it with the discriminant of the p-adic base-changed lattice. That localization comparison for both b and q is the required claim.
Lemma 1.9.4
Lemma 1.9.4. Two integral symmetric forms of the same genus have isometric discriminant bilinear forms and two quadratic forms of the same genus have isometric discriminant quadratic forms.
Not formalized. Genus invariance of numerical determinant/signature is weaker than an isometry of the entire finite discriminant form; no complete globalization of all primary form isometries was identified.
Example / comparison
In our case \(L = \langle u \cdot p ^ { k } \rangle\) and then \(L ^ { * } = p ^ { - k } \mathbb { Z } _ { p }\) so that the discriminant group is \(L ^ { * } / L = p ^ { - k } \mathbb { Z } _ { p } / \mathbb { Z } _ { p } \simeq \mathbb { Z } / p ^ { k } \mathbb { Z }\) . The induced \(\mathbb { Q } ^ { ( \hat { p } ) } / \mathbb { Z }\) -valued form on \(L ^ { * } / L\) can then be identified with the symmetric form \(( x , y ) \mapsto u \cdot p ^ { - k } x y\) on \(\mathbb { Z } / p ^ { k } \mathbb { Z }\) , denoted \(\langle u \cdot p ^ { - k } \rangle\) . For a non-degenerate quadratic lattice \(( L , q )\) we define \(L ^ { * }\) using the form \(b _ { q }\) . Then in a similar way we identify the quadratic form on \(L ^ { * } / L\) with the quadratic form6 \(\langle u \cdot p ^ { - k } \rangle = [ { \textstyle { \frac { 1 } { 2 } } } u \cdot p ^ { - k } ]\) on \(\mathbb { Z } / 2 p ^ { k } \mathbb { Z }\) given by \(x \mapsto { \textstyle { \frac { 1 } { 2 } } } u p ^ { - k } x ^ { 2 }\) . The isometry class of the form depends on \(\bar { u } \in \mathsf { D } ( \mathbb { Z } _ { p } )\) . Hence we have two non-isometric forms, depending on \(u\) being a square or not.
Not formalized. The odd-p integral rank-one classification must include the two unit square classes and the resulting cyclic discriminant forms. A generic unit square-class quotient or a specified cyclic form is not the classification.
Definition / construction / notation
For a non-degenerate quadratic lattice \(( L , q )\) we define \(L ^ { * }\) using the form \(b _ { q }\) . Then in a similar way we identify the quadratic form on \(L ^ { * } / L\) with the quadratic form6 \(\langle u \cdot p ^ { - k } \rangle = [ { \textstyle { \frac { 1 } { 2 } } } u \cdot p ^ { - k } ]\) on \(\mathbb { Z } / 2 p ^ { k } \mathbb { Z }\) given by \(x \mapsto { \textstyle { \frac { 1 } { 2 } } } u p ^ { - k } x ^ { 2 }\) . The isometry class of the form depends on \(\bar { u } \in \mathsf { D } ( \mathbb { Z } _ { p } )\) . Hence we have two non-isometric forms, depending on \(u\) being a square or not.
Not formalized. The source compares p-adic rank-one quadratic isometry classes by unit square classes. TauCeti rankOne is an even Z-lattice calculation, not this local classification.
Definition / construction / notation
- Now let \(p = 2\) . Usually a 2-adic lattice is called a dyadic lattice and the underlying symmetric (quadratic) form a dyadic symmetric (quadratic) form. For a fixed \(k \geq 0\) we get four dyadic symmetric forms \(\langle u \cdot 2 ^ { k } \rangle\) given by \[ ( x , y ) \mapsto u \cdot 2 ^ { k } x y , \quad u \in \{ \pm 1 , \pm 3 \} . \]
Not formalized. The four unit square classes ±1,±3 over Z_2 and their completeness/distinctness need an exact theorem, not merely the quotient type.
Example / comparison
Now let \(p = 2\) . Usually a 2-adic lattice is called a dyadic lattice and the underlying symmetric (quadratic) form a dyadic symmetric (quadratic) form. For a fixed \(k \geq 0\) we get four dyadic symmetric forms \(\langle u \cdot 2 ^ { k } \rangle\) given by \[ ( x , y ) \mapsto u \cdot 2 ^ { k } x y , \quad u \in \{ \pm 1 , \pm 3 \} . \] Indeed, by Theorem A.2.1, the group \(\mathsf { D } ( \mathbb { Z } _ { 2 } )\) of units modulo squares of units in \(\mathbb { Z } _ { 2 }\) is represented by one of these numbers modulo 8. This gives the complete classification of rank one dyadic lattices. For the dyadic quadratic forms \(\langle u \cdot\) \(2 ^ { k } \rangle = [ u \cdot 2 ^ { k - 1 } ]\) given by \[ x \mapsto u \cdot 2 ^ { k - 1 } x ^ { 2 } , \quad k \geq 1 , \] the situation is similar.7 The corresponding discriminant forms are the \(\mathbb { Q } ^ { ( 2 ) } / \mathbb { Z }\) -valued symmetric forms on \(\mathbb { Z } / 2 ^ { k } \mathbb { Z }\) denoted \(\langle u \cdot 2 ^ { - k } \rangle\) . These give the polar forms of the quadratic forms \([ u \cdot 2 ^ { - k - 1 } ]\) on \(\mathbb { Z } / 2 ^ { k } \mathbb { Z }\) , \(u \in \{ \pm 1 , \pm 3 \}\) , \(k \geq 1\) , and are given by \[ ( x , y ) \mapsto u \cdot 2 ^ { - k } x y . \] In Section 6.1 we shall discuss the classification of these torsion forms. In contrast to the lattice case, for low values of \(k\) , units \(u , u ^ { \prime }\) that are different modulo squares might give rise to isometric symmetric or quadratic torsion forms.
Not formalized. The complete dyadic rank-one classification and special distinctions for small exponents k were not identified.
Definition / construction / notation
- The \(p\) -adic hyperbolic plane \(U = U _ { 0 }\) and \(U _ { k } = U ( p ^ { k } )\) , \(k \geq 1\) , give rank two symmetric \(p\) -adic lattices as follows, regardless whether \(p\) is an odd prime or \(p = 2\) . By definition, the Gram matrix of \(U _ { k }\) in the standard basis of \(\mathbb { Z } _ { p } ^ { 2 }\) is \[ U _ { k } = { \left( \begin{array} { l c } { 0 } & { p ^ { k } } \\ { p ^ { k } } & { 0 } \end{array} \right) } = { \left( \begin{array} { l c } { 0 } & { p ^ { k } } \\ { 0 } & { 0 } \end{array} \right) } + { \left( \begin{array} { l l } { 0 } & { 0 } \\ { p ^ { k } } & { 0 } \end{array} \right) } . \]
Formalized. LeanCategories/Lattices/Valued/Standard.lean::hyperbolicPlane, hyperbolicPlane_gramMatrix; LeanCategories/Lattices/Valued/BaseChange.lean::baseChangeIntegral, baseChangeIntegral_pairing_tmul; LeanCategories/Lattices/Valued/Constructions.lean::scaleLattice — Base-change the integral hyperbolic plane to the p-adic integers and scale its pairing by p^k; the standard-basis Gram matrix is then exactly the displayed U_k matrix.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Example / comparison
The \(p\) -adic hyperbolic plane \(U = U _ { 0 }\) and \(U _ { k } = U ( p ^ { k } )\) , \(k \geq 1\) , give rank two symmetric \(p\) -adic lattices as follows, regardless whether \(p\) is an odd prime or \(p = 2\) . By definition, the Gram matrix of \(U _ { k }\) in the standard basis of \(\mathbb { Z } _ { p } ^ { 2 }\) is \[ U _ { k } = { \left( \begin{array} { l c } { 0 } & { p ^ { k } } \\ { p ^ { k } } & { 0 } \end{array} \right) } = { \left( \begin{array} { l c } { 0 } & { p ^ { k } } \\ { 0 } & { 0 } \end{array} \right) } + { \left( \begin{array} { l l } { 0 } & { 0 } \\ { p ^ { k } } & { 0 } \end{array} \right) } . \] We have \(\mathrm { d i s c } ( U _ { k } ) = - p ^ { 2 k }\) . Observe that \(U _ { k }\) is the polar form of the quadratic form \[ ( x _ { 1 } , x _ { 2 } ) \mapsto p ^ { k } x _ { 1 } x _ { 2 } . \] We shall denote this form also by \(U _ { k }\) . Its discriminant group \(p ^ { - k } U _ { k } / U _ { k } \simeq\) \(\Phi ^ { 2 } ( \mathbb { Z } / p ^ { k } \mathbb { Z } )\) carries the quadratic form given by \[ ( { \bar { x } } _ { 1 } , { \bar { x } } _ { 2 } ) \mapsto p ^ { - k } { \bar { x } } _ { 1 } { \bar { x } } _ { 2 } \in \mathbb { Q } ^ { ( p ) } / \mathbb { Z } , \quad ( { \bar { x } } _ { 1 } , { \bar { x } } _ { 2 } ) \in \oplus ^ { 2 } ( \mathbb { Z } / p ^ { k } \mathbb { Z } ) . \] Its polar form has Gram matrix \[ u _ { k } = \left( \begin{array} { c c } { { 0 } } & { { p ^ { - k } } } \\ { { p ^ { - k } } } & { { 0 } } \end{array} \right) = \left( \begin{array} { c c } { { 0 } } & { { p ^ { - k } } } \\ { { 0 } } & { { 0 } } \end{array} \right) + \left( \begin{array} { c c } { { 0 } } & { { 0 } } \\ { { p ^ { - k } } } & { { 0 } } \end{array} \right) . \] The discriminant quadratic form of \(U _ { k }\) is also denoted \(u _ { k }\) .
Not formalized. Need the full U_k determinant, quadratic polar convention and explicit finite discriminant pairings at every exponent. Generic constructors do not prove the computation.
Definition / construction / notation
We shall denote this form also by \(U _ { k }\) . Its discriminant group \(p ^ { - k } U _ { k } / U _ { k } \simeq\) \(\Phi ^ { 2 } ( \mathbb { Z } / p ^ { k } \mathbb { Z } )\) carries the quadratic form given by \[ ( { \bar { x } } _ { 1 } , { \bar { x } } _ { 2 } ) \mapsto p ^ { - k } { \bar { x } } _ { 1 } { \bar { x } } _ { 2 } \in \mathbb { Q } ^ { ( p ) } / \mathbb { Z } , \quad ( { \bar { x } } _ { 1 } , { \bar { x } } _ { 2 } ) \in \oplus ^ { 2 } ( \mathbb { Z } / p ^ { k } \mathbb { Z } ) . \]
Not formalized. The source u_k family has exponent 2^k for arbitrary k; the Klein-four model only covers exponent two. No all-k canonical finite quadratic owner was identified.
Example / comparison
For \(p = 2\) the rank 2 bilinear dyadic lattice \(V _ { k }\) , \(k \geq 0\) , is given by the matrix \(2 ^ { k } V\) , where \[ V = { \binom { 2 } { 1 } } \quad { \binom { 1 } { 2 } } = { \binom { 1 } { 0 } } \quad { 1 } ) + { \binom { 1 } { 1 } } \quad { 0 } \atop 1 ) . \] So \(V _ { k }\) has discriminant \(3 \cdot 2 ^ { 2 k }\) . In particular, \(V _ { 0 } ~ = ~ V\) is unimodular. The decomposition of \(V\) indicates that \(V _ { k }\) is the polar form of the corresponding quadratic form (also denoted \(V _ { k }\) ) given by \[ ( x _ { 1 } , x _ { 2 } ) \mapsto 2 ^ { k } ( x _ { 1 } ^ { 2 } + x _ { 1 } x _ { 2 } + x _ { 2 } ^ { 2 } ) . \] The dyadic quadratic torsion form given by \[ ( \bar { x } _ { 1 } , \bar { x } _ { 2 } ) \mapsto 2 ^ { - k } ( \bar { x } _ { 1 } ^ { 2 } + \bar { x } _ { 1 } \bar { x } _ { 2 } + \bar { x } _ { 2 } ^ { 2 } ) , \quad ( \bar { x } _ { 1 } , \bar { x } _ { 2 } ) \in ( \mathbb { Z } / 2 ^ { k } \mathbb { Z } ) ^ { \oplus 2 } \] is isometric to the discriminant quadratic form of \(V _ { k }\) . To see this, note that the length of \(\mathsf { d g } _ { V _ { k } }\) equals the rank of \(V _ { k }\) and then the Gram matrix of the bilinear discriminant form with respect to the dual basis is given by \(( V _ { k } ) ^ { - 1 } \equiv 2 ^ { - 2 k } V _ { k } \equiv\) \(v _ { k }\) mod \(\mathbb { Z }\) . This is the Gram matrix of the polar form of (1.21) over \(\mathbb { Q } ^ { ( 2 ) } / \mathbb { Z }\) since \[ \begin{array}{c} v _ { k } = { \binom { 2 ^ { - k + 1 } } { 2 ^ { - k } } } \quad 2 ^ { - k } { } \\ { 2 ^ { - k + 1 } } \end{array} \quad \mathrm { ( } 2 ^ { - k } \quad 2 ^ { - k } ) + { \binom { 2 ^ { - k } \quad 2 ^ { - k } } { 2 ^ { - k } } } + { \binom { 2 ^ { - k } \quad 0 } { 2 ^ { - k } \quad 2 ^ { - k } } } . \] As in the case of \(u _ { k }\) , we shall denote the quadratic discriminant form of \(V _ { k }\) also by \(v _ { k }\) . Observe that while the quadratic forms \(u _ { 1 }\) and \(v _ { 1 }\) are not isometric (just consider their values on non-zero vectors), there is no difference between the symmetric torsion forms \(u _ { 1 }\) and \(v _ { 1 }\) since the Gram matrix of \(v _ { 1 }\) has the integer \(2 \cdot 2 ^ { - 1 } = 1\) on the diagonal which is zero in \(\mathbb { Q } ^ { ( 2 ) } / \mathbb { Z }\) as is the case for \(u _ { 1 }\) .
Not formalized. The all-k V_k matrix, determinant, discriminant refinement and u_1/v_1 bilinear-equal but quadratic-distinct comparison constitute one bundle, not a rank-two constructor.
Definition / construction / notation
As in the case of \(u _ { k }\) , we shall denote the quadratic discriminant form of \(V _ { k }\) also by \(v _ { k }\) .
Not formalized. A v_1 model is not the source arbitrary-exponent v_k finite quadratic family.
Theorem (Characterization of the genus, [171, Cor. 1.9.4])
Theorem (Characterization of the genus, [171, Cor. 1.9.4]). The genus of an even non-degenerate lattice \(L\) is determined by its signature and its discriminant quadratic form. In particular, an even unimodular lattice \(L\) belongs to a unique genus determined by its signature.
Not formalized. Nikulin genus classification by signature and the entire finite quadratic discriminant form is not implied by numerical genus invariants or the definition of SameGenus.
Definition / construction / notation
For a non-degenerate quadratic torsion group \((G,q^\#)\), the index modulo \(8\), denoted \(\tau_8(q^\#)\), is the index modulo \(8\) of an even lattice having \(q^\#\) as discriminant form.
Not formalized. The mod-eight signature invariant of a finite quadratic form requires existence of an even realization and independence from the realization, not simply reducing one lattice signature modulo eight.
Theorem (Existence of even lattices, [171, Th. 1.10.1])
Theorem (Existence of even lattices, [171, Th. 1.10.1]). Given a pair of non-negative integers \(( r _ { + } , r _ { - } )\) and a non-degenerate torsion quadratic group \(( G , q ^ { \# } )\) with \(\tau _ { 8 } ( q ^ { \# } ) \equiv r _ { + } - r _ { - }\) mod 8. Then there exists a non-degenerate even lattice \(L\) of rank \(r = r _ { + } + r _ { - }\) , signature \(( r _ { + } , r _ { - } )\) and with discriminant form \(( G , q ^ { \# } )\) if \(\ell ( G ) < r\) , where \(\ell\) is the minimal number of generators of \(G\) .
Not formalized. No full even-lattice realization theorem with the stated signature, mod-eight compatibility and strict rank/length inequality was found.
Example / comparison
Example 1.9.6. Consider the form \(q ^ { \# } = \langle - 3 \cdot 2 ^ { - 1 } \rangle = [ - 3 \cdot 2 ^ { - 2 } ]\) , i.e., the form on \(\mathbb { Z } / 2 \mathbb { Z }\) sending a generator to \(\frac { - 3 } { 4 } \in \mathbb { Q } / \mathbb { Z }\) We find \(\tau _ { 8 } ( q ^ { \# } ) = 1\) (cf. Proposition 12.3.3) and thus there exists a negative definite even lattice of rank 7 whose discriminant form equals \(q ^ { \# }\) . Indeed, \(E _ { 7 } ( - 1 )\) is such a lattice (cf. Table 4.1.1).
Not formalized. The E7 lattice and cyclic discriminant carrier exist, but the specified finite quadratic value -3/4 and its tau_8=1 realization comparison were not identified as a complete example.
Theorem 1.10.1
Theorem 1.10.1 (Eisenstein–Hermite). Fix positive integers \(n , d\) . There are only finitely many isometry classes of non-degenerate integral lattices \(L\) of rank \(n\) and \(| \operatorname { d i s c } ( L ) | \leq d\) .
Not formalized. The inspected finiteness results concern positive definite lattices. The source Eisenstein–Hermite theorem covers all nondegenerate integral lattices, including indefinite ones, of fixed rank and bounded absolute discriminant.
Definition / construction
For a non-degenerate integral lattice, \(m_L=\min_{0\ne y\in L}|b(y,y)|\); this minimum is \(0\) exactly when \(L\) contains a non-zero isotropic vector.
Not formalized. The source minimum uses the absolute norm of every nonzero vector and is zero for an isotropic vector. Positive-definite shortest-vector minima are not this definition on arbitrary nondegenerate lattices.
Proposition 1.10.2
Proposition 1.10.2. Let \(( L , b )\) be a non-degenerate integral lattice of rank \(n\) . Either \(m _ { L } = 0\) , which means that \(L\) contains an isotropic vector, or we have \[ 0 < m _ { L } \leq \left( \frac { 4 } { 3 } \right) ^ { \frac { n - 1 } { 2 } } \cdot d _ { L } ^ { \frac { 1 } { n } } , \quad d _ { L } = | \operatorname { d i s c } ( L ) | . \]
Not formalized. The existing positive-definite bound has coefficient n. The source bound is (4/3)^((n-1)/2), allows indefinite forms and its isotropic zero case. Neither the constant nor the hypotheses agree.
Remark 1.10.3
Remark 1.10.3. The absolute value of the discriminant \(d _ { L }\) of a lattice \(L\) can be related to the volume of a fundamental domain for \(L\) in \(V = L _ { \mathbb { R } }\) . To explain this, observe that there exists an orthogonal basis \(\pmb { B } = \{ b _ { 1 } , \ldots , b _ { n } \}\) of \(V\) with respect to \(b\) in which the Gram matrix for \(^ { b }\) reads \[ I _ { p , n - p } = \operatorname { d i a g } ( \underbrace { 1 , \ldots , 1 } _ { p } , \underbrace { - 1 , \ldots , - 1 } _ { n - p } ) . \] We put a euclidean structure on \(V\) by declaring \(\pmb { B }\) to be an orthonormal basis. The parallelepiped in \(V\) determined by the basis \(\pmb { { \cal E } }\) for \(L\) defined by \[ P _ { L } = \left\{ x _ { 1 } e _ { 1 } + \cdot \cdot \cdot + x _ { n } e _ { n } \ | \ 0 \leq x _ { j } \leq 1 , j = 1 , \ldots , n \right\} \] is a fundamental domain for \(L\) . Let the matrix \(E = ( e _ { i j } )\) relate the bases \(\pmb { B }\) and \(\pmb { { \cal E } }\) , that is \(\begin{array} { r } { e _ { i } = \sum _ { j } e _ { j i } b _ { j } } \end{array}\) . The volume of \(P _ { L }\) with respect to the euclidean metric in which \(\mathbf { B }\) is an orthonormal basis equals \(| \operatorname* { d e t } E |\) . Now we use the change of basis formula (1.2) to relate the Gram matrices \(B _ { E }\) for \(^ { b }\) with respect to \(\pmb { { \cal E } }\) and \(I _ { p , n - p }\) with respect to \(\pmb { B }\) . We find \[ \boldsymbol { B _ { E } } = \boldsymbol { E } ^ { \intercal } \boldsymbol { I _ { p , n - p } } \boldsymbol { E } \] and so, taking determinants, this gives \[ d _ { L } = ( \operatorname * { d e t } E ) ^ { 2 } = \mathrm { v o l } ^ { 2 } ( P _ { L } ) . \]
Not formalized. The source covolume-squared identity is taken in the Euclidean absolute-value metric associated with an indefinite form. A positive-definite or unformed Euclidean lattice formula needs this specific metric comparison.
Corollary 1.10.4
Corollary 1.10.4 (Finiteness of isometry classes in a genus). Every genus contains at most finitely many isometry classes of lattices.
Not formalized. The theorem in Mass assumes positive definiteness. The source genus-finiteness corollary includes indefinite nondegenerate genera; no such general statement was identified.
Definition 1.10.5
Definition 1.10.5. The class number of a genus is the number of isometry classes of that genus.
Formalized. LeanCategories/Lattices/Valued/Mass.lean::classNumber, GenusClass — The class number is the cardinality of the existing quotient class set of a genus, under its finiteness instance. This definition does not itself establish the preceding general finiteness theorem.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Example / comparison
Example 1.10.6. The genus of the odd ternary lattice with Gram matrix \(\operatorname{diag}(1,1,-3)\) has class number \(1\). The same argument also shows that every positive-definite even rank-two lattice of discriminant \(3\) is isometric to \(A_2\).
Not formalized. The two specified class-number-one examples require their integral genus classifications, not just constructors for the ternary lattice or A2.
Definition / construction
The restricted mass is the sum of reciprocal automorphism-group orders over the specified restricted collection of lattice classes.
Formalized. LeanCategories/Lattices/Valued/Mass.lean::mass — The explicit finite family mass is the sum of reciprocal cardinalities of its orthogonal groups. Use the positive-definite hypothesis to justify finiteness of those groups, not as a hidden generalization to indefinite mass.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction / notation
A Niemeier lattice is a positive-definite even unimodular lattice of rank \(24\).
Not formalized. The Niemeier type is the locus of positive definite even unimodular rank-24 lattices; no canonical owner for that locus was identified. Constructing a particular orthogonal sum does not define its classification class.
Theorem 1.12.1
Theorem 1.12.1 ([167],[44, Ch. 16]). The 24 isometry classes of Niemeier lattices are classified by their root sublattice, i.e., the sublattice spanned by the 2-roots. The latter is either 0 (no roots present) or of maximal rank 24.
Not formalized. No complete classification into exactly 24 rank-24 positive even unimodular isometry classes found; GitHub Niemeier query returned no Lean hits at the recorded date.
Example / comparison
Examples of Niemeier lattices include \(E_8^{\oplus3}\), \(\Gamma_{16}\oplus E_8\), and \(\Gamma_{24}\); the Leech lattice is the unique Niemeier lattice without roots.
Not formalized. The source includes several Niemeier examples and uniqueness of the rootless Leech lattice. Sphere-packing optimality or an E8 model is not the Niemeier/rootless uniqueness theorem.
Definition / construction
The mass of a genus is \(\operatorname{mass}(\mathfrak g(L))=\sum_{\Gamma\in\mathfrak g(L)}|O(\Gamma)|^{-1}\).
Formalized. LeanCategories/Lattices/Valued/Mass.lean::genusMass — For the positive definite context in which the finite orthogonal-group mass is defined, this is the finite sum over global isometry classes in the genus, with independence from chosen representatives.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction
The theta series of a positive-definite lattice is the generating series that counts vectors by their norm.
Formalized. LeanCategories/Lattices/Valued/Theta.lean::representationNumber, thetaSeries — The series counts vectors at each integral norm using the native pairing convention. Source q/b normalization must be stated explicitly when changing the exponent; finite coefficients require positive definiteness.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Theorem 1.12.2
Theorem 1.12.2. The two flat tori \(V / L _ { 1 }\) and \(V / L _ { 2 }\) , \(L _ { 1 } ~ = ~ \Gamma _ { 1 6 }\) , \(L _ { 2 } = E _ { 8 } \oplus E _ { 8 }\) , are not isomorphic as Riemannian manifolds but they are isospectral, that is, they have the same spectrum for the Laplace operator.
Not formalized. The unit requires nonisometric E8⊕E8 and Gamma16 to have equal theta series and the resulting flat-torus isospectral comparison. A general theta-series definition proves none of these.
Theorem 1.12.3
Theorem 1.12.3 ([66], Unique splitting of definite lattices). A definite lattice can be written in a natural (hence unique) way as an orthogonal sum of indecomposable lattices.
Not formalized. No uniqueness theorem for the decomposition of every definite integral lattice into orthogonally indecomposable summands was identified. Root-graph connectedness and a chosen complement are not that result.
Theorem: Theorem
Theorem. The isometry class of an indefinite unimodular lattice is uniquely determined by its parity, rank and index. Moreover, even unimodular lattices have index divisible by 8. Indefinite odd unimodular forms are diagonalizable over the integers (hence isometric to orthogonal direct sums of ⟨1⟩ and ⟨−1⟩ ). Indefinite even unimodular lattices of any rank exist as long as the index is divisible by 8.
Not formalized. The indefinite unimodular classification needs existence and uniqueness for all allowed ranks/signatures/parities and the mod-eight constraint, not just standard examples.
Example / comparison
Let \(L\) be a unimodular lattice of rank 7 and index \(^ { - 1 }\) . Then \(L\) must be odd and the form is diagonalizable, \(L \simeq \langle 1 \rangle ^ { \oplus 3 } \textcircled { \pm }\) \(\langle - 1 \rangle ^ { \{ \downarrow \} 4 }\) .
Not formalized. The source identification of every odd unimodular rank-seven index-minus-one lattice with the specified diagonal model depends on the full indefinite classification, which is not an identified owner.
Example / comparison
A unimodular even lattice of rank 22 and signature \(( 3 , 1 9 )\) is isometric to \[ \Lambda _ { \mathsf { K 3 } } : = U ^ { \oplus 3 } \oplus E _ { 8 } ( - 1 ) ^ { \oplus 2 } . \] This is the so-called \(\mathbf { \Delta } \mathbf { K } \mathbf { \mathcal { 3 } }\) lattice.
Not formalized. The constructed even unimodular lattice of signature (3,19) is available, but the source asserts uniqueness among all such lattices. The constructor does not cover that classification.
Example / comparison
An even unimodular lattice of rank 10 and signature \(( 1 , 9 )\) is isometric to the Enriques lattice \[ \Lambda _ { \mathsf { E n r } } : = U \oplus E _ { 8 } ( - 1 ) . \]
Not formalized. The Enriques-signature even unimodular model can be constructed as U⊕E8(-1), but the source uniqueness assertion is not supplied by that construction.
Example / comparison
(Rank 2 indefinite unimodular lattices.) Let \(L = \mathbb { Z } e _ { 1 } + \mathbb { Z } e _ { 2 }\) with Gram matrix \(\left( \begin{array} { c c } { { 0 } } & { { 1 } } \\ { { 1 } } & { { a } } \end{array} \right)\) We claim that if \(a\) is even then \(L \simeq U\) , and if \(a\) is odd, then \(L \simeq \langle 1 \rangle \oplus \langle - 1 \rangle\) . Indeed, if \(a\) is even, use the basis \(\{ e _ { 1 } , e _ { 2 } - \textstyle { \frac { 1 } { 2 } } a e _ { 1 } \}\) , while if \(a = 2 k + 1\) is odd, use the basis \(\{ e _ { 2 } - k e _ { 1 } , e _ { 2 } - ( k + 1 ) e _ { 1 } \}\) . This confirms the classification theorem in the case of unimodular rank 2 lattices of signature \(( 1 , 1 )\) . Indefinite but non-unimodular lattices also often have a unique isometry class in their genus. See Corollary 14.4.3 which states:
Not formalized. The binary indefinite unimodular classification and the parity-dependent basis changes for matrix [[0,1],[1,a]] are not an identified full result.
Theorem 1.13.2
Theorem 1.13.2 ([171, 1.13.3], [118]). Let \(L\) be an even non-degenerate indefinite lattice of rank \(r\) . Assume that the discriminant group of \(L\) can be generated by at most \(r - 2\) elements. Then the genus of \(L\) consists of one isometry class.
Not formalized. The rank≥length+2 singleton-genus theorem for even indefinite lattices is a classification theorem, not an implication of the glue construction or SameGenus predicate.
Example / comparison
Example 1.13.3. As soon as \(L\) is even, indefinite, and splits off an even unimodular lattice (this is always a lattice of rank \(\geq 2\) ) the assumption of the above theorem is satisfied. For example, using Example 1.6.8.2, the lattices \(U \oplus E _ { 8 } ( s )\) as well as \(\Gamma _ { 4 k } ( s ) \oplus U \oplus \cdot \cdot \cdot \oplus U\) , \(s \neq 0 , k , t \geq 1\) are is unique in their genus.
Not formalized. The examples require the singleton-genus conclusion, bounds for scaled E8/Gamma forms and unimodular summand arguments. Neither particular constructors nor the unproved general criterion closes the bundle.