mathlib3 documentation

linear_algebra.matrix.to_linear_equiv

Matrices and linear equivalences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file gives the map matrix.to_linear_equiv from matrices with invertible determinant, to linear equivs.

Main definitions #

Main results #

Tags #

matrix, linear_equiv, determinant, inverse

source
def matrix.to_linear_equiv' {R : Type u_1} [comm_ring R] {n : Type u_3} [fintype n] [decidable_eq n] (P : matrix n n R) (h : invertible P) :
(n → R) ≃ₗ[R] n → R

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

See matrix.to_linear_equiv for the same map on arbitrary modules.

Equations
source
@[simp]
theorem matrix.to_linear_equiv'_apply {R : Type u_1} [comm_ring R] {n : Type u_3} [fintype n] [decidable_eq n] (P : matrix n n R) (h : invertible P) :
↑(P.to_linear_equiv' h) = ⇑matrix.to_lin' P
source
@[simp]
theorem matrix.to_linear_equiv'_symm_apply {R : Type u_1} [comm_ring R] {n : Type u_3} [fintype n] [decidable_eq n] (P : matrix n n R) (h : invertible P) :
↑((P.to_linear_equiv' h).symm) = ⇑matrix.to_lin' (⅟ P)
source
@[simp]
theorem matrix.to_linear_equiv_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {n : Type u_3} [fintype n] (b : basis n R M) [decidable_eq n] (A : matrix n n R) (hA : is_unit A.det) (ᾰ : M) :
⇑(matrix.to_linear_equiv b A hA) ᾰ = ⇑(⇑(matrix.to_lin b b) A) ᾰ
source
noncomputable def matrix.to_linear_equiv {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {n : Type u_3} [fintype n] (b : basis n R M) [decidable_eq n] (A : matrix n n R) (hA : is_unit A.det) :
M ≃ₗ[R] M

Given hA : is_unit A.det and b : basis R b, A.to_linear_equiv b hA is the linear_equiv arising from to_lin b b A.

See matrix.to_linear_equiv' for this result on n → R.

Equations
source
theorem matrix.ker_to_lin_eq_bot {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {n : Type u_3} [fintype n] (b : basis n R M) [decidable_eq n] (A : matrix n n R) (hA : is_unit A.det) :
linear_map.ker (⇑(matrix.to_lin b b) A) = ⊥
source
theorem matrix.range_to_lin_eq_top {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {n : Type u_3} [fintype n] (b : basis n R M) [decidable_eq n] (A : matrix n n R) (hA : is_unit A.det) :
linear_map.range (⇑(matrix.to_lin b b) A) = ⊤
source
theorem matrix.exists_mul_vec_eq_zero_iff_aux {n : Type u_3} [fintype n] {K : Type u_1} [decidable_eq n] [field K] {M : matrix n n K} :
(∃ (v : n → K) (H : v ≠ 0), M.mul_vec v = 0) ↔ M.det = 0

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

source
theorem matrix.exists_mul_vec_eq_zero_iff' {n : Type u_3} [fintype n] {A : Type u_1} (K : Type u_2) [decidable_eq n] [comm_ring A] [nontrivial A] [field K] [algebra A K] [is_fraction_ring A K] {M : matrix n n A} :
(∃ (v : n → A) (H : v ≠ 0), M.mul_vec v = 0) ↔ M.det = 0
source
theorem matrix.exists_mul_vec_eq_zero_iff {n : Type u_3} [fintype n] {A : Type u_1} [decidable_eq n] [comm_ring A] [is_domain A] {M : matrix n n A} :
(∃ (v : n → A) (H : v ≠ 0), M.mul_vec v = 0) ↔ M.det = 0
source
theorem matrix.exists_vec_mul_eq_zero_iff {n : Type u_3} [fintype n] {A : Type u_1} [decidable_eq n] [comm_ring A] [is_domain A] {M : matrix n n A} :
(∃ (v : n → A) (H : v ≠ 0), matrix.vec_mul v M = 0) ↔ M.det = 0
source
theorem matrix.nondegenerate_iff_det_ne_zero {n : Type u_3} [fintype n] {A : Type u_1} [decidable_eq n] [comm_ring A] [is_domain A] {M : matrix n n A} :
M.nondegenerate ↔ M.det ≠ 0
source
theorem matrix.nondegenerate.det_ne_zero {n : Type u_3} [fintype n] {A : Type u_1} [decidable_eq n] [comm_ring A] [is_domain A] {M : matrix n n A} :
M.nondegenerate → M.det ≠ 0

Alias of the forward direction of matrix.nondegenerate_iff_det_ne_zero.

source
theorem matrix.nondegenerate.of_det_ne_zero {n : Type u_3} [fintype n] {A : Type u_1} [decidable_eq n] [comm_ring A] [is_domain A] {M : matrix n n A} :
M.det ≠ 0 → M.nondegenerate

Alias of the reverse direction of matrix.nondegenerate_iff_det_ne_zero.