Matrices and linear equivalences

This file gives the map Matrix.toLinearEquiv from matrices with invertible determinant, to linear equivs.

Main definitions

• Matrix.toLinearEquiv: a matrix with an invertible determinant forms a linear equiv

Main results

• Matrix.exists_mulVec_eq_zero_iff: M maps some v ≠ 0 to zero iff det M = 0

Tags

matrix, linear_equiv, determinant, inverse

def Matrix.toLinearEquiv' {n : Type u_1} [Fintype n] {R : Type u_2} [CommRing R] [DecidableEq n] (P : Matrix n n R) : Invertible P → (n → R) ≃ₗ[R] n → R

An invertible matrix yields a linear equivalence from the free module to itself.

See Matrix.toLinearEquiv for the same map on arbitrary modules.

Equations

• P.toLinearEquiv' x✝ = (LinearMap.GeneralLinearGroup.generalLinearEquiv R (n → R)) (Matrix.GeneralLinearGroup.toLin (unitOfInvertible P))

@[simp]

theorem Matrix.toLinearEquiv'_apply {n : Type u_1} [Fintype n] {R : Type u_2} [CommRing R] [DecidableEq n] (P : Matrix n n R) (h : Invertible P) : ↑(P.toLinearEquiv' h) = toLin' P

@[simp]

theorem Matrix.toLinearEquiv'_symm_apply {n : Type u_1} [Fintype n] {R : Type u_2} [CommRing R] [DecidableEq n] (P : Matrix n n R) (h : Invertible P) : ↑(P.toLinearEquiv' h).symm = toLin' ⅟P

noncomputable def Matrix.toLinearEquiv {n : Type u_1} [Fintype n] {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis n R M) [DecidableEq n] (A : Matrix n n R) (hA : IsUnit A.det) : M ≃ₗ[R] M

Given hA : IsUnit A.det and b : Basis R b, A.toLinearEquiv b hA is the LinearEquiv arising from toLin b b A.

See Matrix.toLinearEquiv' for this result on n → R.

Equations

• Matrix.toLinearEquiv b A hA = { toFun := ⇑((Matrix.toLin b b) A), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑((Matrix.toLin b b) A⁻¹), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Matrix.toLinearEquiv_apply {n : Type u_1} [Fintype n] {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis n R M) [DecidableEq n] (A : Matrix n n R) (hA : IsUnit A.det) (a : M) : (toLinearEquiv b A hA) a = ((toLin b b) A) a

theorem Matrix.ker_toLin_eq_bot {n : Type u_1} [Fintype n] {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis n R M) [DecidableEq n] (A : Matrix n n R) (hA : IsUnit A.det) : LinearMap.ker ((toLin b b) A) = ⊥

theorem Matrix.range_toLin_eq_top {n : Type u_1} [Fintype n] {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis n R M) [DecidableEq n] (A : Matrix n n R) (hA : IsUnit A.det) : LinearMap.range ((toLin b b) A) = ⊤

theorem Matrix.exists_mulVec_eq_zero_iff_aux {n : Type u_1} [Fintype n] {K : Type u_4} [DecidableEq n] [Field K] {M : Matrix n n K} : (∃ (v : n → K), v ≠ 0 ∧ M.mulVec v = 0) ↔ M.det = 0

This holds for all integral domains (see Matrix.exists_mulVec_eq_zero_iff), not just fields, but it's easier to prove it for the field of fractions first.

theorem Matrix.exists_mulVec_eq_zero_iff' {n : Type u_1} [Fintype n] {A : Type u_4} (K : Type u_5) [DecidableEq n] [CommRing A] [Nontrivial A] [Field K] [Algebra A K] [IsFractionRing A K] {M : Matrix n n A} : (∃ (v : n → A), v ≠ 0 ∧ M.mulVec v = 0) ↔ M.det = 0

theorem Matrix.exists_mulVec_eq_zero_iff {n : Type u_1} [Fintype n] {A : Type u_4} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} : (∃ (v : n → A), v ≠ 0 ∧ M.mulVec v = 0) ↔ M.det = 0

theorem Matrix.exists_vecMul_eq_zero_iff {n : Type u_1} [Fintype n] {A : Type u_4} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} : (∃ (v : n → A), v ≠ 0 ∧ vecMul v M = 0) ↔ M.det = 0

theorem Matrix.nondegenerate_iff_det_ne_zero {n : Type u_1} [Fintype n] {A : Type u_4} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} : M.Nondegenerate ↔ M.det ≠ 0

theorem Matrix.Nondegenerate.mul_iff_right {n : Type u_1} [Fintype n] {A : Type u_4} [CommRing A] [IsDomain A] {M N : Matrix n n A} (h : N.Nondegenerate) : (M * N).Nondegenerate ↔ M.Nondegenerate

theorem Matrix.Nondegenerate.mul_iff_left {n : Type u_1} [Fintype n] {A : Type u_4} [CommRing A] [IsDomain A] {M N : Matrix n n A} (h : M.Nondegenerate) : (M * N).Nondegenerate ↔ N.Nondegenerate

theorem Matrix.Nondegenerate.smul_iff {n : Type u_1} [Finite n] {A : Type u_4} [CommRing A] [IsDomain A] {M : Matrix n n A} {t : A} (h : t ≠ 0) : (t • M).Nondegenerate ↔ M.Nondegenerate

theorem Matrix.Nondegenerate.det_ne_zero {n : Type u_1} [Fintype n] {A : Type u_4} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} : M.Nondegenerate → M.det ≠ 0

Alias of the forward direction of Matrix.nondegenerate_iff_det_ne_zero.

theorem Matrix.Nondegenerate.of_det_ne_zero {n : Type u_1} [Fintype n] {A : Type u_4} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} : M.det ≠ 0 → M.Nondegenerate

Alias of the reverse direction of Matrix.nondegenerate_iff_det_ne_zero.

theorem Matrix.det_ne_zero_of_sum_col_pos {n : Type u_1} [Fintype n] [DecidableEq n] {S : Type u_2} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) => A i j < 0) (h2 : ∀ (j : n), 0 < ∑ i : n, A i j) : A.det ≠ 0

A matrix whose nondiagonal entries are negative with the sum of the entries of each column positive has nonzero determinant.

theorem Matrix.det_ne_zero_of_sum_row_pos {n : Type u_1} [Fintype n] [DecidableEq n] {S : Type u_2} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) => A i j < 0) (h2 : ∀ (i : n), 0 < ∑ j : n, A i j) : A.det ≠ 0

A matrix whose nondiagonal entries are negative with the sum of the entries of each row positive has nonzero determinant.