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

source

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

Matrix.toLinearEquiv' P x = ↑(LinearMap.GeneralLinearGroup.generalLinearEquiv R (n → R)) (↑Matrix.GeneralLinearGroup.toLinear (unitOfInvertible P))

Instances For

source

@[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) :

↑(Matrix.toLinearEquiv' P h) = ↑Matrix.toLin' P

source

@[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) :

↑(LinearEquiv.symm (Matrix.toLinearEquiv' P h)) = ↑Matrix.toLin' ⅟P

source

@[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 : Basis n R M) [DecidableEq n] (A : Matrix n n R) (hA : IsUnit (Matrix.det A)) (a : M) :

↑(Matrix.toLinearEquiv b A hA) a = ↑(↑(Matrix.toLin b b) A) a

source

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 : Basis n R M) [DecidableEq n] (A : Matrix n n R) (hA : IsUnit (Matrix.det A)) :

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

One or more equations did not get rendered due to their size.

Instances For

source

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 : Basis n R M) [DecidableEq n] (A : Matrix n n R) (hA : IsUnit (Matrix.det A)) :

LinearMap.ker (↑(Matrix.toLin b b) A) = ⊥

source

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 : Basis n R M) [DecidableEq n] (A : Matrix n n R) (hA : IsUnit (Matrix.det A)) :

LinearMap.range (↑(Matrix.toLin b b) A) = ⊤

source

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 x, Matrix.mulVec M v = 0) ↔ Matrix.det M = 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.

source

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 x, Matrix.mulVec M v = 0) ↔ Matrix.det M = 0

source

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 x, Matrix.mulVec M v = 0) ↔ Matrix.det M = 0

source

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 x, Matrix.vecMul v M = 0) ↔ Matrix.det M = 0

source

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} :

Matrix.Nondegenerate M ↔ Matrix.det M ≠ 0

source

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} :

Matrix.Nondegenerate M → Matrix.det M ≠ 0

Alias of the forward direction of Matrix.nondegenerate_iff_det_ne_zero.

source

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} :

Matrix.det M ≠ 0 → Matrix.Nondegenerate M

Alias of the reverse direction of Matrix.nondegenerate_iff_det_ne_zero.

source

theorem Matrix.det_ne_zero_of_sum_col_pos {n : Type u_1} [Fintype n] [DecidableEq n] {S : Type u_2} [LinearOrderedCommRing S] {A : Matrix n n S} (h1 : ∀ (i j : n), i ≠ j → A i j < 0) (h2 : ∀ (j : n), 0 < Finset.sum Finset.univ fun i => A i j) :

Matrix.det A ≠ 0

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

source

theorem Matrix.det_ne_zero_of_sum_row_pos {n : Type u_1} [Fintype n] [DecidableEq n] {S : Type u_2} [LinearOrderedCommRing S] {A : Matrix n n S} (h1 : ∀ (i j : n), i ≠ j → A i j < 0) (h2 : ∀ (i : n), 0 < Finset.sum Finset.univ fun j => A i j) :

Matrix.det A ≠ 0

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