Modular bilinear forms

A bilinear form B is a-modular when it is a times a perfect pairing (LinearMap.BilinForm.IsModular). For a lattice over a discrete valuation ring with uniformizer π, a π^i-modular form is one of scale π^i whose dual lattice is π^{-i} times the lattice; 1-modular forms are the unimodular ones. The modular forms are the constituents of a Jordan splitting.

This file proves the facts about modular forms that hold over every commutative ring:

• when a is a non-zero-divisor, a-modularity is characterized by divisibility of all values by a, left separation, and the representability of a f for each linear functional f (LinearMap.BilinForm.isModular_iff);
• on a nonzero free module, the scale ideal is generated by a (LinearMap.BilinForm.IsModular.scaleIdeal_eq_span), so parity can be measured relative to the actual scale rather than the coefficient ring;
• when a is a non-zero-divisor, every form C with a • C = B for an a-modular B is a perfect pairing (LinearMap.BilinForm.IsModular.isPerfPair_of_smul_eq), and it is symmetric when B is (LinearMap.BilinForm.IsSymm.of_smul);
• a vector x with a r ∣ B x y for all y, where B is a-modular and a and r are non-zero-divisors, is divisible by r (LinearMap.BilinForm.IsModular.exists_eq_smul_of_forall_dvd);
• the block-diagonal product of two a-modular forms is a-modular (LinearMap.BilinForm.IsModular.prod), and so is the restriction of a product form to a product of a-modular submodules (LinearMap.BilinForm.IsModular.restrict_prod);
• the orthogonal sum of two a-modular submodules is a-modular (LinearMap.BilinForm.IsModular.restrict_sup);
• an a-modular submodule splits off orthogonally when a divides every value of the form (LinearMap.BilinForm.IsModular.isCompl_orthogonal).

A form whose Gram matrix in a basis is a times a matrix of unit determinant is a-modular (Module.Basis.isModular_of_isUnit_det), so a family with such a Gram matrix spans an a-modular submodule (LinearMap.BilinForm.isModular_restrict_span_range). Over a local ring, a pairing B u w which is a non-zero-divisor dividing every value of a symmetric form therefore gives a B u w-modular orthogonal summand inside the span of u and w (LinearMap.BilinForm.IsSymm.exists_isModular_restrict_isCompl_orthogonal): either B u u or B w w is B u w times a unit, or u and w span a binary summand whose Gram matrix is B u w times a matrix of unit determinant. No inverse of 2 is needed; this is the splitting step of the Jordan decomposition at a dyadic prime, where rank-two constituents such as the hyperbolic plane cannot be diagonalized.

Over a local domain, a form on a finite free module which is the orthogonal internal sum of finitely many π ^ e i-modular submodules with e i ≤ j has a Gram matrix G and a symmetric matrix H with G * H = π ^ j • 1, namely the block diagonal matrix of the rescaled inverses of the Gram matrices of the summands; when 2 ∣ π and the summands with e i = j are even at their own scale, H has even diagonal (LinearMap.BilinForm.exists_basis_toMatrix_mul_eq_of_isInternal).

Main definitions

• LinearMap.BilinForm.IsModular: B is a times a perfect pairing.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §82E and 91C.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 8, Lemma 4.1.

theorem LinearMap.BilinForm.exists_smul_eq_of_forall_dvd {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} (ha : a ∈ nonZeroDivisors R) (h : ∀ (x y : M), a ∣ (B x) y) : ∃ (C : LinearMap.BilinForm R M), a • C = B

If a is a non-zero-divisor dividing every value of B, then B is a times a bilinear form.

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

A bilinear form B is a-modular when it is a times a perfect pairing: B = a • C for a form C identifying M with its dual on both sides. Over a discrete valuation ring with uniformizer π, a π ^ i-modular lattice is one of scale π ^ i whose dual lattice is π ^ (-i) times the lattice, and the 1-modular forms are the unimodular ones.

theorem LinearMap.BilinForm.isModular_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} : B.IsModular a ↔ ∃ (C : LinearMap.BilinForm R M), a • C = B ∧ IsPerfPair C

Modularity is equivalent to a scaled perfect-pairing witness. This characteristic lemma allows importing modules to construct and extract the witness without unfolding the definition.

@[simp]

theorem LinearMap.BilinForm.isModular_one_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} : B.IsModular 1 ↔ IsPerfPair B

A form is 1-modular exactly when it is a perfect pairing.

theorem LinearMap.BilinForm.IsModular.dvd {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} (h : B.IsModular a) (x y : M) : a ∣ (B x) y

Every value of an a-modular form is divisible by a.

theorem LinearMap.BilinForm.IsModular.smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} (h : B.IsModular a) (r : R) : (r • B).IsModular (r * a)

Multiplying an a-modular form by r multiplies its modularity factor by r.

theorem LinearMap.BilinForm.IsModular.of_associated {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} (h : B.IsModular a) {b : R} (hab : Associated a b) : B.IsModular b

Modularity only depends on a up to a unit.

theorem LinearMap.BilinForm.IsModular.nondegenerate {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} (h : B.IsModular a) (ha : a ∈ nonZeroDivisors R) : B.Nondegenerate

An a-modular form with a a non-zero-divisor is nondegenerate.

theorem LinearMap.BilinForm.isModular_of_subsingleton {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} [Subsingleton M] : B.IsModular a

A form on a subsingleton module is a-modular for every a.

theorem LinearMap.BilinForm.IsModular.congr {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (h : B.IsModular a) (e : M ≃ₗ[R] M') : ((BilinForm.congr e) B).IsModular a

Modularity is transported along a linear equivalence of the underlying modules.

@[simp]

theorem LinearMap.BilinForm.isModular_congr_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (e : M ≃ₗ[R] M') : ((congr e) B).IsModular a ↔ B.IsModular a

Modularity is invariant under a linear equivalence of the underlying modules.

theorem LinearMap.BilinForm.IsModular.prod {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} {M' : Type u_3} [AddCommMonoid M'] [Module R M'] {C : LinearMap.BilinForm R M'} (hB : B.IsModular a) (hC : C.IsModular a) : (B.prod C).IsModular a

The block-diagonal product of two a-modular forms is a-modular.

theorem LinearMap.BilinForm.IsModular.restrict_prod {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} {M' : Type u_3} [AddCommMonoid M'] [Module R M'] {C : LinearMap.BilinForm R M'} {P : Submodule R M} {Q : Submodule R M'} (hB : (B.restrict P).IsModular a) (hC : (C.restrict Q).IsModular a) : ((B.prod C).restrict (P.prod Q)).IsModular a

The restriction of a block-diagonal product form to a product of submodules is a-modular when the restrictions of the factors are.

@[simp]

theorem LinearMap.BilinForm.isModular_restrict_map_subtype_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} {P : Submodule R M} {K : Submodule R ↥P} : (B.restrict (Submodule.map P.subtype K)).IsModular a ↔ ((B.restrict P).restrict K).IsModular a

Modularity of a restriction to a submodule of a submodule is modularity of the restriction to its image in the ambient module.

theorem LinearMap.BilinForm.IsModular.scaleIdeal_eq_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} [Module.Free R M] [Nontrivial M] (h : B.IsModular a) : B.scaleIdeal = Ideal.span {a}

A modular form on a nonzero free module has scale generated by its modularity factor.

theorem LinearMap.BilinForm.IsModular.normIdeal_le_mul_scaleIdeal_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} [Module.Free R M] (h : B.IsModular a) (r : R) : B.normIdeal ≤ Ideal.span {r} * B.scaleIdeal ↔ B.normIdeal ≤ Ideal.span {r * a}

For a modular form on a free module, norm containment relative to its actual scale is equivalent to containment in the product of the modularity factor and the given factor. This includes the zero module, whose scale and norm ideals are both zero.

theorem LinearMap.BilinForm.isModular_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} (hB : B.IsSymm) (ha : a ∈ nonZeroDivisors R) : B.IsModular a ↔ (∀ (x y : M), a ∣ (B x) y) ∧ (∀ (x : M), (∀ (y : M), (B x) y = 0) → x = 0) ∧ ∀ (f : Module.Dual R M), ∃ (x : M), ∀ (y : M), (B x) y = a * f y

Characterization of modular symmetric forms. For a non-zero-divisor a, a symmetric form is a-modular exactly when a divides all of its values, it is left-separating, and a f is represented by a vector for every linear functional f.

theorem LinearMap.BilinForm.IsModular.isPerfPair_of_smul_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} (h : B.IsModular a) (ha : a ∈ nonZeroDivisors R) {C : LinearMap.BilinForm R M} (hC : a • C = B) : IsPerfPair C

The unimodular rescaling of a modular form. If B is a-modular with a a non-zero-divisor, then every form C with a • C = B is a perfect pairing: the perfect pairing of which B is a times is unique.

theorem LinearMap.BilinForm.IsModular.exists_eq_smul_of_forall_dvd {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} (h : B.IsModular a) (ha : a ∈ nonZeroDivisors R) {r : R} (hr : r ∈ nonZeroDivisors R) {x : M} (hx : ∀ (y : M), a * r ∣ (B x) y) : ∃ (z : M), x = r • z

Divisibility in a modular form. If B is a-modular, with a and r non-zero-divisors, and a * r divides B x y for every y, then x is r times a vector.

theorem LinearMap.BilinForm.IsModular.restrict_sup {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} (hB : B.IsSymm) (ha : a ∈ nonZeroDivisors R) {S T : Submodule R M} (hS : (B.restrict S).IsModular a) (hT : (B.restrict T).IsModular a) (hST : ∀ x ∈ S, ∀ y ∈ T, (B x) y = 0) : (B.restrict (S ⊔ T)).IsModular a

Orthogonal sums of modular forms are modular. If two orthogonal submodules carry a-modular restrictions of a symmetric form, with a a non-zero-divisor, so does their sum.

theorem LinearMap.BilinForm.IsModular.isCompl_orthogonal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} (hB : B.IsSymm) (ha : a ∈ nonZeroDivisors R) (hdvd : ∀ (x y : M), a ∣ (B x) y) {S : Submodule R M} (h : (B.restrict S).IsModular a) : IsCompl S (B.orthogonal S)

A modular submodule splits off. If a non-zero-divisor a divides every value of a symmetric form B and the restriction of B to S is a-modular, then S is complementary to its orthogonal complement.

theorem Module.Basis.isModular_of_isUnit_det {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Basis ι R M) {G : Matrix ι ι R} (ha : a ∈ nonZeroDivisors R) (hG : ∀ (i j : ι), (B (b i)) (b j) = a * G i j) (hdet : IsUnit G.det) : B.IsModular a

A Gram matrix a times a matrix of unit determinant gives a modular form. If the Gram matrix of B in a finite basis is a times a matrix of unit determinant, with a a non-zero-divisor, then B is a-modular.

theorem LinearMap.BilinForm.isModular_restrict_span_range {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} {ι : Type u_3} [Fintype ι] [DecidableEq ι] {v : ι → M} {G : Matrix ι ι R} (ha : a ∈ nonZeroDivisors R) (hG : ∀ (i j : ι), (B (v i)) (v j) = a * G i j) (hdet : IsUnit G.det) : (B.restrict (Submodule.span R (Set.range v))).IsModular a

A Gram block of unit determinant spans a modular submodule. If the Gram matrix of a finite family v is a times a matrix of unit determinant, with a a non-zero-divisor, then the restriction of B to the span of v is a-modular.

theorem LinearMap.BilinForm.IsSymm.linearIndependent_and_isModular_restrict_span_pair {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {a : R} [IsLocalRing R] (hB : B.IsSymm) {u w : M} {s t : R} (ha : a ∈ nonZeroDivisors R) (huw : (B u) w = a) (hu : (B u) u = a * s) (hw : (B w) w = a * t) (hst : ¬IsUnit (s * t)) : LinearIndependent R ![u, w] ∧ (B.restrict (Submodule.span R (Set.range ![u, w]))).IsModular a

A symmetric binary Gram block scaled by a non-zero-divisor is linearly independent and spans a modular submodule when the product of its normalized diagonal entries is a nonunit. This is the binary case of the local orthogonal splitting construction.

theorem LinearMap.BilinForm.IsSymm.exists_isModular_restrict_isCompl_orthogonal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} [IsLocalRing R] (hB : B.IsSymm) {u w : M} (hd : (B u) w ∈ nonZeroDivisors R) (hdvd : ∀ (x y : M), (B u) w ∣ (B x) y) : ∃ (S : Submodule R M), S ≠ ⊥ ∧ S ≤ Submodule.span R {u, w} ∧ (B.restrict S).IsModular ((B u) w) ∧ IsCompl S (B.orthogonal S)

The splitting step of the Jordan decomposition. Over a local ring, let B u w be a non-zero-divisor dividing every value of a symmetric form B. Then some nonzero submodule of the span of u and w is B u w-modular and complementary to its orthogonal complement. No inverse of 2 is needed: when neither B u u nor B w w is B u w times a unit, the summand is the binary one spanned by u and w.

theorem LinearMap.BilinForm.IsSymm.exists_ne_bot_isModular_pow_isCompl_orthogonal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} [IsDomain R] [IsDiscreteValuationRing R] [Module.Free R M] [Module.Finite R M] (hB : B.IsSymm) (hB0 : B ≠ 0) {π : R} (hπ : Irreducible π) : ∃ (S : Submodule R M) (k : ℕ), S ≠ ⊥ ∧ IsCompl S (B.orthogonal S) ∧ (B.restrict S).IsModular (π ^ k)

Over a discrete valuation ring with uniformizer π, a nonzero symmetric bilinear form on a finite free module has a nonzero direct summand S, complementary to its orthogonal B.orthogonal S, on which the form is π ^ k-modular for some k.

Gram matrices of orthogonal sums of modular forms

theorem LinearMap.BilinForm.exists_basis_toMatrix_mul_eq_of_isInternal {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {π : R} [IsDomain R] [IsLocalRing R] [Module.Free R M] [Module.Finite R M] (hB : B.IsSymm) (hπ : π ≠ 0) {o : Type} [Finite o] [DecidableEq o] {P : o → Submodule R M} (hP : DirectSum.IsInternal P) (horth : ∀ (i i' : o), i ≠ i' → ∀ x ∈ P i, ∀ y ∈ P i', (B x) y = 0) {e : o → ℕ} (hmod : ∀ (i : o), (B.restrict (P i)).IsModular (π ^ e i)) {j : ℕ} (hle : ∀ (i : o), e i ≤ j) : ∃ (ι : Type) (x : Fintype ι) (x_1 : DecidableEq ι) (b : Module.Basis ι R M) (H : Matrix ι ι R), (toMatrix b) B * H = π ^ j • 1 ∧ H.IsSymm ∧ (2 ∣ π → (∀ (i : o), e i = j → ∀ w ∈ P i, 2 * π ^ j ∣ (B w) w) → ∀ (i : ι), 2 ∣ H i i)

A form on a finite free module which is the orthogonal internal direct sum of finitely many submodules P i, each π ^ e i-modular with e i ≤ j, has a Gram matrix G and a symmetric matrix H such that G * H = π ^ j • 1. When 2 ∣ π and the summands with e i = j are even at their own scale, H has even diagonal.