Bilinear forms over local rings

This file records consequences of a unit Gram determinant or a perfect pairing over a local ring. A nonunit diagonal entry forces a unit off-diagonal entry in the same row. A symmetric perfect pairing with nonunit diagonal values splits off a binary perfect summand whenever a dual vector takes the value one. For an even symmetric form when 2 is a nonunit, such an entry determines a perfect binary summand and an orthogonal decomposition.

Main results

• LinearMap.BilinForm.exists_index_ne_zero_isUnit_apply_of_not_isUnit_diag_of_isUnit_det finds a unit off-diagonal entry from a nonunit diagonal entry.
• LinearMap.BilinForm.IsSymm.exists_mem_maximalIdeal_of_mem_span_pair: a vector of the span of a pair with unit mutual pairing and self-pairings in 𝔪, pairing into 𝔪 with the pair, has coordinates in 𝔪.
• LinearMap.BilinForm.IsSymm.exists_binary_isPerfPair_isCompl_orthogonal_of_dual_apply_eq_one splits a binary perfect summand from a perfect pairing with nonunit diagonal values.
• LinearMap.BilinForm.IsSymm.exists_binary_isPerfPair_isCompl_orthogonal splits a perfect binary summand from an even unimodular form.
• LinearMap.BilinForm.IsSymm.exists_basis_orthogonal splits off the span of a family with unit Gram determinant, with a basis of the complement and the resulting factorization of the Gram determinant.
• LinearMap.BilinForm.IsSymm.exists_basis_orthogonal_span_singleton_isUnit_det: in particular, the orthogonal complement of a vector with unit self-pairing in a unimodular form is unimodular.
• LinearMap.BilinForm.IsSymm.equivalent_of_equivalent_restrict_orthogonal recombines two such splittings with the same Gram matrix into an isometry.

theorem LinearMap.BilinForm.IsSymm.equivalent_of_equivalent_restrict_orthogonal {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R N} {ι : Type u_4} [Fintype ι] [DecidableEq ι] (hB : B.IsSymm) (hC : C.IsSymm) {v : ι → M} {v' : ι → N} {G : Matrix ι ι R} (hG : ∀ (i j : ι), (B (v i)) (v j) = G i j) (hG' : ∀ (i j : ι), (C (v' i)) (v' j) = G i j) (hdet : IsUnit G.det) (hc : IsCompl (Submodule.span R (Set.range v)) (B.orthogonal (Submodule.span R (Set.range v)))) (hc' : IsCompl (Submodule.span R (Set.range v')) (C.orthogonal (Submodule.span R (Set.range v')))) (h : (B.restrict (B.orthogonal (Submodule.span R (Set.range v)))).Equivalent (C.restrict (C.orthogonal (Submodule.span R (Set.range v'))))) : B.Equivalent C

Recombining blocks. If families v in M and v' in N have the same Gram matrix G of unit determinant, and the restrictions of B and C to the orthogonal complements of their spans are isometric, then B and C are isometric.

theorem LinearMap.BilinForm.IsSymm.exists_basis_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) {m k : ℕ} (b : Module.Basis (Fin (m + k)) R M) {v : Fin k → M} {G : Matrix (Fin k) (Fin k) R} (hG : ∀ (i j : Fin k), (B (v i)) (v j) = G i j) (hdet : IsUnit G.det) : IsCompl (Submodule.span R (Set.range v)) (B.orthogonal (Submodule.span R (Set.range v))) ∧ ∃ (t : Module.Basis (Fin m) R ↥(B.orthogonal (Submodule.span R (Set.range v)))) (w : R), IsUnit w ∧ ((toMatrix b) B).det = w ^ 2 * (G.det * ((toMatrix t) (B.restrict (B.orthogonal (Submodule.span R (Set.range v))))).det)

Splitting off a block. If the Gram matrix G of a family v of k vectors has unit determinant, the span S of v is complementary to its orthogonal complement T. If M has a basis of size m + k, then T has a basis t of size m, and the Gram determinant of B is w ^ 2 * det G * det (B|_T) for a unit w.

theorem LinearMap.BilinForm.IsSymm.exists_basis_orthogonal_span_singleton_isUnit_det {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) {n : ℕ} (b : Module.Basis (Fin (n + 1)) R M) (hdet : IsUnit ((toMatrix b) B).det) {x : M} (hx : IsUnit ((B x) x)) : ∃ (t : Module.Basis (Fin n) R ↥(B.orthogonal (R ∙ x))), IsUnit ((toMatrix t) (B.restrict (B.orthogonal (R ∙ x)))).det

The orthogonal complement of a vector x with unit self-pairing, for a symmetric form whose Gram determinant in a basis of size n + 1 is a unit, has a basis of size n in which the Gram determinant of the restricted form is a unit.

theorem LinearMap.BilinForm.exists_index_ne_zero_isUnit_apply_of_not_isUnit_diag_of_isUnit_det {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) {n : ℕ} (b : Module.Basis (Fin (n + 1)) R M) (hdiag : ¬IsUnit ((B (b 0)) (b 0))) (hdet : IsUnit ((toMatrix b) B).det) : ∃ (i : Fin (n + 1)), ↑i ≠ 0 ∧ IsUnit ((B (b 0)) (b i))

In a positive-rank unimodular form over a local ring, if the first basis vector has nonunit self-pairing, it pairs to a unit with a different basis vector.

theorem LinearMap.BilinForm.IsSymm.isUnit_pairGramDet_of_dvd_apply_self {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (hB : B.IsSymm) {x y : M} (hxx2 : 2 ∣ (B x) x) (h2 : ¬IsUnit 2) (hxy : IsUnit ((B x) y)) : IsUnit !![(B x) x, (B x) y; (B y) x, (B y) y].det

In a symmetric form over a local ring where 2 is not a unit, two vectors have a unit Gram determinant if their mutual pairing is a unit and one self-pairing is divisible by 2.

theorem LinearMap.BilinForm.IsSymm.exists_mem_maximalIdeal_of_mem_span_pair {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsSymm) {e f : M} (h₁ : IsUnit ((B e) f)) (he : (B e) e ∈ IsLocalRing.maximalIdeal R) (hf : (B f) f ∈ IsLocalRing.maximalIdeal R) {s : M} (hs : s ∈ Submodule.span R {e, f}) (hse : (B s) e ∈ IsLocalRing.maximalIdeal R) (hsf : (B s) f ∈ IsLocalRing.maximalIdeal R) : ∃ α ∈ IsLocalRing.maximalIdeal R, ∃ β ∈ IsLocalRing.maximalIdeal R, s = α • e + β • f

In a symmetric form over a local ring, let e, f have self-pairings in the maximal ideal and unit mutual pairing. A vector s of their span pairing into the maximal ideal with both e and f has both coordinates in the maximal ideal.

theorem LinearMap.BilinForm.IsSymm.exists_binary_isPerfPair_isCompl_orthogonal_of_dual_apply_eq_one {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) [IsPerfPair B] (hB : B.IsSymm) (hdiag : ∀ (x : M), ¬IsUnit ((B x) x)) (x : M) (f : Module.Dual R M) (hfx : f x = 1) : ∃ (S : Submodule R M), Nonempty (Module.Basis (Fin 2) R ↥S) ∧ IsPerfPair (B.restrict S) ∧ IsCompl S (B.orthogonal S)

A symmetric perfect pairing with nonunit diagonal values splits off a binary perfect pairing if some linear functional takes the value one. The summand is supplied with a basis and is complementary to its orthogonal complement.

theorem LinearMap.BilinForm.IsSymm.exists_binary_isPerfPair_isCompl_orthogonal {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (hB : B.IsSymm) {n : ℕ} (b : Module.Basis (Fin (n + 2)) R M) (heven : ∀ (x : M), 2 ∣ (B x) x) (h2 : ¬IsUnit 2) (hdet : IsUnit ((toMatrix b) B).det) : ∃ (S : Submodule R M), Module.finrank R ↥S = 2 ∧ IsPerfPair (B.restrict S) ∧ IsCompl S (B.orthogonal S)

Even unimodular forms split off a perfect binary summand. In rank at least two, an even symmetric form with unit Gram determinant has two basis vectors whose span has rank two, carries a perfect restriction of the form, and is complementary to its orthogonal complement.