Matrices associated with non-degenerate bilinear forms

Main definitions

• Matrix.Nondegenerate A: the proposition that when interpreted as a bilinear form, the matrix A is nondegenerate.

def Matrix.SeparatingRight {m : Type u_1} {n : Type u_2} {R : Type u_3} [NonUnitalNonAssocSemiring R] [Finite m] [Finite n] (M : Matrix m n R) : Prop

A matrix M is right-separating if for all w ≠ 0, there is a v with v * M * w ≠ 0.

Equations

• M.SeparatingRight = ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M.mulVec w = 0) → w = 0

def Matrix.SeparatingLeft {m : Type u_1} {n : Type u_2} {R : Type u_3} [NonUnitalNonAssocSemiring R] [Finite m] [Finite n] (M : Matrix m n R) : Prop

A matrix M is right-separating if for all v ≠ 0, there is a w with v * M * w ≠ 0.

Equations

• M.SeparatingLeft = ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M.mulVec w = 0) → v = 0

structure Matrix.Nondegenerate {m : Type u_1} {n : Type u_2} {R : Type u_3} [NonUnitalNonAssocSemiring R] [Finite m] [Finite n] (M : Matrix m n R) : Prop

A matrix M is nondegenerate if it is both left-separating and right-separating.

• separatingLeft : M.SeparatingLeft
• separatingRight : M.SeparatingRight

theorem Matrix.nondegenerate_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [NonUnitalNonAssocSemiring R] [Finite m] [Finite n] (M : Matrix m n R) : M.Nondegenerate ↔ M.SeparatingLeft ∧ M.SeparatingRight

theorem Matrix.separatingRight_def {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Fintype m] [Fintype n] : M.SeparatingRight ↔ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M.mulVec w = 0) → w = 0

theorem Matrix.separatingLeft_def {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Fintype m] [Fintype n] : M.SeparatingLeft ↔ ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M.mulVec w = 0) → v = 0

theorem Matrix.nondegenerate_def {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Fintype m] [Fintype n] : M.Nondegenerate ↔ (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M.mulVec w = 0) → v = 0) ∧ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M.mulVec w = 0) → w = 0

theorem Matrix.separatingLeft_iff_forall_vecMul_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Fintype m] [Finite n] : M.SeparatingLeft ↔ ∀ (v : m → R), vecMul v M = 0 → v = 0

theorem Matrix.separatingRight_iff_forall_mulVec_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Finite m] [Fintype n] : M.SeparatingRight ↔ ∀ (v : n → R), M.mulVec v = 0 → v = 0

theorem Matrix.SeparatingLeft.eq_zero_of_vecMul_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Fintype m] [Finite n] (hM : M.SeparatingLeft) {v : m → R} (hv : vecMul v M = 0) : v = 0

theorem Matrix.SeparatingRight.eq_zero_of_mulVec_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Finite m] [Fintype n] (hM : M.SeparatingRight) {v : n → R} (hv : M.mulVec v = 0) : v = 0

theorem Matrix.nondegenerate_iff_forall_vecMul_and_mulVec_eq_zero {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Fintype m] [Fintype n] : M.Nondegenerate ↔ (∀ (v : m → R), vecMul v M = 0 → v = 0) ∧ ∀ (v : n → R), M.mulVec v = 0 → v = 0

@[simp]

theorem Matrix.separatingLeft_transpose_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Finite m] [Finite n] : M.transpose.SeparatingLeft ↔ M.SeparatingRight

theorem Matrix.SeparatingRight.separatingLeft_transpose {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Finite m] [Finite n] : M.SeparatingRight → M.transpose.SeparatingLeft

Alias of the reverse direction of Matrix.separatingLeft_transpose_iff.

@[simp]

theorem Matrix.separatingRight_transpose_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Finite m] [Finite n] : M.transpose.SeparatingRight ↔ M.SeparatingLeft

theorem Matrix.SeparatingLeft.separatingRight_transpose {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Finite m] [Finite n] : M.SeparatingLeft → M.transpose.SeparatingRight

Alias of the reverse direction of Matrix.separatingRight_transpose_iff.

@[simp]

theorem Matrix.nondegenerate_transpose_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Finite m] [Finite n] : M.transpose.Nondegenerate ↔ M.Nondegenerate

theorem Matrix.Nondegenerate.transpose {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Finite m] [Finite n] : M.Nondegenerate → M.transpose.Nondegenerate

Alias of the reverse direction of Matrix.nondegenerate_transpose_iff.

theorem Matrix.Nondegenerate.eq_zero_of_ortho {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Fintype m] [Fintype n] (hM : M.Nondegenerate) {v : m → R} (hv : ∀ (w : n → R), v ⬝ᵥ M.mulVec w = 0) : v = 0

If M is nondegenerate and w * M * v = 0 for all w, then v = 0.

theorem Matrix.Nondegenerate.exists_not_ortho_of_ne_zero {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Fintype m] [Fintype n] (hM : M.Nondegenerate) {v : m → R} (hv : v ≠ 0) : ∃ (w : n → R), v ⬝ᵥ M.mulVec w ≠ 0

If M is nondegenerate and v ≠ 0, then there is some w such that w * M * v ≠ 0.

theorem Matrix.Nondegenerate.eq_zero_of_ortho' {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Fintype m] [Fintype n] (hM : M.Nondegenerate) {w : n → R} (hw : ∀ (v : m → R), v ⬝ᵥ M.mulVec w = 0) : w = 0

If M is nondegenerate and w * M * v = 0 for all v, then w = 0.

theorem Matrix.Nondegenerate.exists_not_ortho_of_ne_zero' {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {M : Matrix m n R} [Fintype m] [Fintype n] (hM : M.Nondegenerate) {w : n → R} (hw : w ≠ 0) : ∃ (v : m → R), v ⬝ᵥ M.mulVec w ≠ 0

If M is nondegenerate and w ≠ 0, then there is some v such that v * M * w ≠ 0.

theorem Matrix.Nondegenerate.of_det_mem_nonZeroDivisors {m : Type u_1} {R : Type u_3} [CommRing R] [Fintype m] [DecidableEq m] {M : Matrix m m R} (hM : M.det ∈ nonZeroDivisors R) : M.Nondegenerate

theorem Matrix.nondegenerate_of_det_ne_zero {m : Type u_1} {R : Type u_3} [CommRing R] [Fintype m] [DecidableEq m] {M : Matrix m m R} [NoZeroDivisors R] (hM : M.det ≠ 0) : M.Nondegenerate

If M is square and has nonzero determinant, then M as a bilinear form on n → R is nondegenerate. The "iff" implication, nondegenerate_iff_det_ne_zero, is proved in a later file.

See also BilinForm.nondegenerateOfDetNeZero' and BilinForm.nondegenerateOfDetNeZero.

theorem Matrix.eq_zero_of_det_mem_nonZeroDivisors_of_vecMul_eq_zero {m : Type u_1} {R : Type u_3} [CommRing R] [Fintype m] [DecidableEq m] {M : Matrix m m R} (hM : M.det ∈ nonZeroDivisors R) {v : m → R} (hv : vecMul v M = 0) : v = 0

theorem Matrix.eq_zero_of_vecMul_eq_zero {m : Type u_1} {R : Type u_3} [CommRing R] [Fintype m] [DecidableEq m] {M : Matrix m m R} [NoZeroDivisors R] (hM : M.det ≠ 0) {v : m → R} (hv : vecMul v M = 0) : v = 0

theorem Matrix.eq_zero_of_det_mem_nonZeroDivisors_of_mulVec_eq_zero {m : Type u_1} {R : Type u_3} [CommRing R] [Fintype m] [DecidableEq m] {M : Matrix m m R} (hM : M.det ∈ nonZeroDivisors R) {v : m → R} (hv : M.mulVec v = 0) : v = 0

theorem Matrix.eq_zero_of_mulVec_eq_zero {m : Type u_1} {R : Type u_3} [CommRing R] [Fintype m] [DecidableEq m] {M : Matrix m m R} [NoZeroDivisors R] (hM : M.det ≠ 0) {v : m → R} (hv : M.mulVec v = 0) : v = 0

theorem LinearIndependent.sum_smul_of_nondegenerate {ι : Type u_1} {κ : Type u_2} {R : Type u_3} {M : Type u_4} [Fintype ι] [Finite κ] [CommRing R] [AddCommGroup M] [Module R M] {v : ι → M} (hv : LinearIndependent R v) {A : Matrix κ ι R} (hA : A.Nondegenerate) : LinearIndependent R fun (i : κ) => ∑ j : ι, A i j • v j