Orthogonal complements of bilinear forms

This file records facts about the orthogonal complement LinearMap.BilinForm.orthogonal that Mathlib lacks. A vector lies in the orthogonal complement of the span of one or two vectors exactly when it is orthogonal to each of them. Adjoining a vector x whose self-pairing is a non-zero-divisor dividing all its pairings (over a field: a non-isotropic vector) to an orthogonal basis of the orthogonal complement of x gives an orthogonal basis of the whole module, for a reflexive form; this is the inductive step of every diagonalization argument, over a field as over a valuation ring. Adjoining an orthogonal vector whose self-pairing is a right non-zero-divisor to a left-separating subspace of a reflexive bilinear space produces a nondegenerate restriction; this is the structural step used when a Cartan--Dieudonne argument enlarges a fixed subspace.

Main results

• LinearMap.BilinForm.mem_orthogonal_span_singleton_iff, LinearMap.BilinForm.mem_orthogonal_span_pair_iff: membership in the orthogonal complement of the span of one or two vectors.
• LinearMap.BilinForm.IsRefl.exists_orthogonal_basis_of_orthogonal_span_singleton: an orthogonal basis of x^⊥ extends by x to an orthogonal basis of the whole space.
• TauCeti.BilinForm.restrict_nondegenerate_sup_span_singleton: adjoining an orthogonal vector to a left-separating subspace produces a nondegenerate restriction.
• LinearMap.BilinForm.isCompl_orthogonal_of_flip_restrict_bijective: a perfect flipped restriction splits a bilinear module over a commutative ring.
• LinearMap.BilinForm.isCompl_orthogonal_of_restrict_bijective: a perfect symmetric restriction splits a bilinear module over a commutative ring.
• LinearMap.BilinForm.restrict_span_singleton_bijective_of_isUnit: unit self-pairing makes the cyclic restriction perfect.
• LinearMap.BilinForm.isCompl_span_singleton_orthogonal_of_dvd: a vector whose self-pairing is a non-zero-divisor dividing all its pairings splits off.
• LinearMap.BilinForm.isCompl_span_singleton_orthogonal_of_isUnit: a vector with unit self-pairing splits off.

theorem LinearMap.BilinForm.mem_orthogonal_span_singleton_iff {K : Type u_1} {V : Type u_2} [CommSemiring K] [AddCommMonoid V] [Module K V] (B : LinearMap.BilinForm K V) {x y : V} : y ∈ B.orthogonal (K ∙ x) ↔ (B x) y = 0

A vector is orthogonal to the span of a vector x exactly when it is orthogonal to x.

theorem LinearMap.BilinForm.mem_orthogonal_span_pair_iff {K : Type u_1} {V : Type u_2} [CommSemiring K] [AddCommMonoid V] [Module K V] (B : LinearMap.BilinForm K V) {x y z : V} : z ∈ B.orthogonal (Submodule.span K {x, y}) ↔ (B x) z = 0 ∧ (B y) z = 0

A vector is orthogonal to the span of two vectors exactly when it is orthogonal to both.

theorem TauCeti.BilinForm.restrict_nondegenerate_sup_span_singleton {K : Type u_1} {V : Type u_2} [CommSemiring K] [AddCommMonoid V] [Module K V] (B : LinearMap.BilinForm K V) (hB : B.IsRefl) (W : Submodule K V) (hW : LinearMap.SeparatingLeft (B.restrict W)) (x : V) (hxx : (B x) x ∈ nonZeroDivisorsRight K) (hx : x ∈ B.orthogonal W) : (B.restrict (W ⊔ K ∙ x)).Nondegenerate

Adjoining a vector whose self-pairing is a right non-zero-divisor from the orthogonal complement of a left-separating subspace preserves nondegeneracy.

theorem LinearMap.BilinForm.isCompl_orthogonal_of_flip_restrict_bijective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (S : Submodule R M) (h : Function.Bijective ⇑(B.flip.restrict S)) : IsCompl S (B.orthogonal S)

A submodule with perfect flipped restricted pairing is complementary to its right orthogonal complement.

theorem LinearMap.BilinForm.isCompl_orthogonal_of_restrict_bijective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (S : Submodule R M) (hB : (B.restrict S).IsSymm) (h : Function.Bijective ⇑(B.restrict S)) : IsCompl S (B.orthogonal S)

A submodule with perfect symmetric restricted pairing is complementary to its orthogonal complement.

theorem LinearMap.BilinForm.restrict_span_singleton_bijective_of_isUnit {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (x : M) (hx : IsUnit ((B x) x)) : Function.Bijective ⇑(B.restrict (R ∙ x))

Unit self-pairing makes the restricted pairing on the cyclic span perfect.

theorem LinearMap.BilinForm.isCompl_span_singleton_orthogonal_of_dvd {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) {x : M} (hx : (B x) x ∈ nonZeroDivisors R) (hdvd : ∀ (y : M), (B x) x ∣ (B x) y) : IsCompl (R ∙ x) (B.orthogonal (R ∙ x))

A vector x whose self-pairing B x x is a non-zero-divisor dividing every pairing B x y spans an orthogonal direct summand. Over a field this is the condition B x x ≠ 0; over a valuation ring it says that B x x has minimal valuation among the pairings of x.

theorem LinearMap.BilinForm.IsRefl.exists_orthogonal_basis_of_orthogonal_span_singleton {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsRefl) {x : M} (hx : (B x) x ∈ nonZeroDivisors R) (hdvd : ∀ (y : M), (B x) x ∣ (B x) y) {d : ℕ} {v : Module.Basis (Fin d) R ↥(B.orthogonal (R ∙ x))} (hv : (B.restrict (B.orthogonal (R ∙ x))).iIsOrtho ⇑v) : ∃ (b : Module.Basis (Fin (d + 1)) R M), B.iIsOrtho ⇑b

Adjoining a vector x to an orthogonal basis of the orthogonal complement of x gives an orthogonal basis of the whole module, for a reflexive form, provided the self-pairing B x x is a non-zero-divisor dividing every pairing B x y. Over a field this says B x x ≠ 0.

theorem LinearMap.BilinForm.isCompl_span_singleton_orthogonal_of_isUnit {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (x : M) (hx : IsUnit ((B x) x)) : IsCompl (R ∙ x) (B.orthogonal (R ∙ x))

A vector with unit self-pairing spans an orthogonal direct summand.