Separating vectors by a left- or right-separating form

For a left-separating matrix M over a field (for example a nondegenerate one), the linear forms w ↦ v ⬝ᵥ M *ᵥ w determine v. This file records the two-vector form of that statement: if x is not a multiple of u, then some w is orthogonal to u but not to x. Otherwise the form of x would vanish on the kernel of the form of u, making it a multiple of that form by Mathlib's mem_span_of_iInf_ker_le_ker, and left separation would make x the same multiple of u. This complements Mathlib's Matrix.Nondegenerate.exists_not_ortho_of_ne_zero, the case u = 0, and is the basic tool for moving vectors by transvections in the classical groups.

For a right-separating matrix M over any commutative semiring (for example a nondegenerate one, over the field with two elements as well), two nonzero vectors x and y have a common vector z pairing nontrivially with both M *ᵥ x and M *ᵥ y.

Main results

• Matrix.SeparatingLeft.exists_ortho_and_not_ortho_of_notMem_span: a vector orthogonal to u but not to x, when x is not a multiple of u.
• Matrix.SeparatingRight.exists_not_ortho_and_not_ortho_of_ne_zero_of_ne_zero: a vector z with z ⬝ᵥ M *ᵥ x ≠ 0 and z ⬝ᵥ M *ᵥ y ≠ 0, for nonzero x and y.

theorem Matrix.SeparatingLeft.exists_ortho_and_not_ortho_of_notMem_span {m : Type u_1} {n : Type u_2} {K : Type u_3} [Fintype m] [Fintype n] [Field K] {M : Matrix m n K} (hM : M.SeparatingLeft) {u x : m → K} (hx : x ∉ K ∙ u) : ∃ (w : n → K), u ⬝ᵥ M.mulVec w = 0 ∧ x ⬝ᵥ M.mulVec w ≠ 0

A vector orthogonal to u but not to x, for a left-separating matrix M, when x is not a multiple of u.

theorem Matrix.SeparatingRight.exists_not_ortho_and_not_ortho_of_ne_zero_of_ne_zero {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommSemiring R] {M : Matrix m n R} (hM : M.SeparatingRight) {x y : n → R} (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (z : m → R), z ⬝ᵥ M.mulVec x ≠ 0 ∧ z ⬝ᵥ M.mulVec y ≠ 0

If M is right-separating (for example nondegenerate) and x, y are nonzero, then some z pairs nontrivially with both: z ⬝ᵥ M *ᵥ x ≠ 0 and z ⬝ᵥ M *ᵥ y ≠ 0. This holds over any commutative semiring, in particular over the field with two elements.