Matrices and linear equivalences #
This file gives the map matrix.to_linear_equiv
from matrices with invertible determinant,
to linear equivs.
Main definitions #
matrix.to_linear_equiv
: a matrix with an invertible determinant forms a linear equiv
Main results #
matrix.exists_mul_vec_eq_zero_iff
:M
maps somev ≠ 0
to zero iffdet M = 0
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) :
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.
@[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
@[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⁻¹
@[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) ᾰ
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
.
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) :
(⇑(matrix.to_lin b b) A).ker = ⊥
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) :
(⇑(matrix.to_lin b b) A).range = ⊤
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} :
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} :
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} :
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
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 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} :
M.det ≠ 0 → M.nondegenerate
Alias of nondegenerate_iff_det_ne_zero
.