mathlib documentation

linear_algebra.matrix.to_linear_equiv

Matrices and linear equivalences #

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

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

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
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) :
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) :
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.

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

Alias of nondegenerate_iff_det_ne_zero.

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

Alias of nondegenerate_iff_det_ne_zero.