Determinant of families of vectors #
This file defines the determinant of an endomorphism, and of a family of vectors
with respect to some basis. For the determinant of a matrix, see the file
linear_algebra.matrix.determinant.
Main definitions #
In the list below, and in all this file, R is a commutative ring (semiring
is sometimes enough), M and its variations are R-modules, ι, κ, n and m are finite
types used for indexing.
basis.det: the determinant of a family of vectors with respect to a basis, as a multilinear maplinear_map.det: the determinant of an endomorphismf : End R Mas a multiplicative homomorphism (ifMdoes not have a finiteR-basis, the result is1instead)linear_equiv.det: the determinant of an isomorphismf : M ≃ₗ[R] Mas a multiplicative homomorphism (ifMdoes not have a finiteR-basis, the result is1instead)
Tags #
basis, det, determinant
noncomputable
def
equiv_of_pi_lequiv_pi
{m : Type u_6}
{n : Type u_7}
[fintype m]
[fintype n]
{R : Type u_1}
[comm_ring R]
[nontrivial R]
(e : (m → R) ≃ₗ[R] n → R) :
m ≃ n
If R^m and R^n are linearly equivalent, then m and n are also equivalent.
Equations
- equiv_of_pi_lequiv_pi e = (basis.of_equiv_fun e.symm).index_equiv (pi.basis_fun R n)
noncomputable
def
matrix.index_equiv_of_inv
{A : Type u_5}
[comm_ring A]
{m : Type u_6}
{n : Type u_7}
[fintype m]
[fintype n]
[nontrivial A]
[decidable_eq m]
[decidable_eq n]
{M : matrix m n A}
{M' : matrix n m A}
(hMM' : M ⬝ M' = 1)
(hM'M : M' ⬝ M = 1) :
m ≃ n
If M and M' are each other's inverse matrices, they are square matrices up to
equivalence of types.
Equations
- matrix.index_equiv_of_inv hMM' hM'M = equiv_of_pi_lequiv_pi (matrix.to_lin'_of_inv hMM' hM'M)
theorem
matrix.det_comm'
{A : Type u_5}
[comm_ring A]
{m : Type u_6}
{n : Type u_7}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
{M : matrix n m A}
{N M' : matrix m n A}
(hMM' : M ⬝ M' = 1)
(hM'M : M' ⬝ M = 1) :
If there exists a two-sided inverse M' for M (indexed differently),
then det (N ⬝ M) = det (M ⬝ N).
theorem
matrix.det_conj_of_mul_eq_one
{A : Type u_5}
[comm_ring A]
{m : Type u_6}
{n : Type u_7}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
{M : matrix m n A}
{M' : matrix n m A}
{N : matrix n n A}
(hMM' : M ⬝ M' = 1)
(hM'M : M' ⬝ M = 1) :
If M' is a two-sided inverse for M (indexed differently), det (M ⬝ N ⬝ M') = det N.
See matrix.det_conj and matrix.det_conj' for the case when M' = M⁻¹ or vice versa.
Determinant of a linear map #
theorem
linear_map.det_to_matrix_eq_det_to_matrix
{M : Type u_2}
[add_comm_group M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{A : Type u_5}
[comm_ring A]
[module A M]
{κ : Type u_6}
[fintype κ]
[decidable_eq κ]
(b : basis ι A M)
(c : basis κ A M)
(f : M →ₗ[A] M) :
(⇑(linear_map.to_matrix b b) f).det = (⇑(linear_map.to_matrix c c) f).det
The determinant of linear_map.to_matrix does not depend on the choice of basis.
noncomputable
def
linear_map.det_aux
{M : Type u_2}
[add_comm_group M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{A : Type u_5}
[comm_ring A]
[module A M] :
The determinant of an endomorphism given a basis.
See linear_map.det for a version that populates the basis non-computably.
Although the trunc (basis ι A M) parameter makes it slightly more convenient to switch bases,
there is no good way to generalize over universe parameters, so we can't fully state in det_aux's
type that it does not depend on the choice of basis. Instead you can use the det_aux_def' lemma,
or avoid mentioning a basis at all using linear_map.det.
Equations
- linear_map.det_aux = trunc.lift (λ (b : basis ι A M), matrix.det_monoid_hom.comp ↑(linear_map.to_matrix_alg_equiv b)) linear_map.det_aux._proof_1
theorem
linear_map.det_aux_def
{M : Type u_2}
[add_comm_group M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{A : Type u_5}
[comm_ring A]
[module A M]
(b : basis ι A M)
(f : M →ₗ[A] M) :
⇑(linear_map.det_aux (trunc.mk b)) f = (⇑(linear_map.to_matrix b b) f).det
Unfold lemma for det_aux.
See also det_aux_def' which allows you to vary the basis.
theorem
linear_map.det_aux_def'
{M : Type u_2}
[add_comm_group M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{A : Type u_5}
[comm_ring A]
[module A M]
{ι' : Type u_1}
[fintype ι']
[decidable_eq ι']
(tb : trunc (basis ι A M))
(b' : basis ι' A M)
(f : M →ₗ[A] M) :
⇑(linear_map.det_aux tb) f = (⇑(linear_map.to_matrix b' b') f).det
@[simp]
theorem
linear_map.det_aux_id
{M : Type u_2}
[add_comm_group M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{A : Type u_5}
[comm_ring A]
[module A M]
(b : trunc (basis ι A M)) :
@[simp]
theorem
linear_map.det_aux_comp
{M : Type u_2}
[add_comm_group M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{A : Type u_5}
[comm_ring A]
[module A M]
(b : trunc (basis ι A M))
(f g : M →ₗ[A] M) :
⇑(linear_map.det_aux b) (f.comp g) = (⇑(linear_map.det_aux b) f) * ⇑(linear_map.det_aux b) g
@[protected]
noncomputable
def
linear_map.det
{M : Type u_2}
[add_comm_group M]
{A : Type u_5}
[comm_ring A]
[module A M] :
The determinant of an endomorphism independent of basis.
If there is no finite basis on M, the result is 1 instead.
theorem
linear_map.coe_det
{M : Type u_2}
[add_comm_group M]
{A : Type u_5}
[comm_ring A]
[module A M]
[decidable_eq M] :
theorem
linear_map.det_eq_det_to_matrix_of_finset
{M : Type u_2}
[add_comm_group M]
{A : Type u_5}
[comm_ring A]
[module A M]
[decidable_eq M]
{s : finset M}
(b : basis ↥s A M)
(f : M →ₗ[A] M) :
⇑linear_map.det f = (⇑(linear_map.to_matrix b b) f).det
@[simp]
theorem
linear_map.det_to_matrix
{M : Type u_2}
[add_comm_group M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{A : Type u_5}
[comm_ring A]
[module A M]
(b : basis ι A M)
(f : M →ₗ[A] M) :
(⇑(linear_map.to_matrix b b) f).det = ⇑linear_map.det f
@[simp]
theorem
linear_map.det_to_matrix'
{A : Type u_5}
[comm_ring A]
{ι : Type u_1}
[fintype ι]
[decidable_eq ι]
(f : (ι → A) →ₗ[A] ι → A) :
theorem
linear_map.det_cases
{M : Type u_2}
[add_comm_group M]
{A : Type u_5}
[comm_ring A]
[module A M]
[decidable_eq M]
{P : A → Prop}
(f : M →ₗ[A] M)
(hb : ∀ (s : finset M) (b : basis ↥s A M), P (⇑(linear_map.to_matrix b b) f).det)
(h1 : P 1) :
P (⇑linear_map.det f)
To show P f.det it suffices to consider P (to_matrix _ _ f).det and P 1.
@[simp]
theorem
linear_map.det_comp
{M : Type u_2}
[add_comm_group M]
{A : Type u_5}
[comm_ring A]
[module A M]
(f g : M →ₗ[A] M) :
⇑linear_map.det (f.comp g) = (⇑linear_map.det f) * ⇑linear_map.det g
@[simp]
theorem
linear_map.det_id
{M : Type u_2}
[add_comm_group M]
{A : Type u_5}
[comm_ring A]
[module A M] :
@[simp]
theorem
linear_map.det_smul
{𝕜 : Type u_1}
[field 𝕜]
{M : Type u_2}
[add_comm_group M]
[module 𝕜 M]
(c : 𝕜)
(f : M →ₗ[𝕜] M) :
⇑linear_map.det (c • f) = (c ^ finite_dimensional.finrank 𝕜 M) * ⇑linear_map.det f
Multiplying a map by a scalar c multiplies its determinant by c ^ dim M.
theorem
linear_map.det_zero'
{M : Type u_2}
[add_comm_group M]
{A : Type u_5}
[comm_ring A]
[module A M]
{ι : Type u_1}
[fintype ι]
[nonempty ι]
(b : basis ι A M) :
⇑linear_map.det 0 = 0
@[simp]
theorem
linear_map.det_zero
{𝕜 : Type u_1}
[field 𝕜]
{M : Type u_2}
[add_comm_group M]
[module 𝕜 M] :
⇑linear_map.det 0 = 0 ^ finite_dimensional.finrank 𝕜 M
In a finite-dimensional vector space, the zero map has determinant 1 in dimension 0,
and 0 otherwise. We give a formula that also works in infinite dimension, where we define
the determinant to be 1.
@[simp]
theorem
linear_map.det_conj
{M : Type u_2}
[add_comm_group M]
{A : Type u_5}
[comm_ring A]
[module A M]
{N : Type u_1}
[add_comm_group N]
[module A N]
(f : M →ₗ[A] M)
(e : M ≃ₗ[A] N) :
⇑linear_map.det (↑e.comp (f.comp ↑(e.symm))) = ⇑linear_map.det f
Conjugating a linear map by a linear equiv does not change its determinant.
theorem
linear_map.is_unit_det
{M : Type u_2}
[add_comm_group M]
{A : Type u_1}
[comm_ring A]
[module A M]
(f : M →ₗ[A] M)
(hf : is_unit f) :
If a linear map is invertible, so is its determinant.
theorem
linear_map.finite_dimensional_of_det_ne_one
{M : Type u_2}
[add_comm_group M]
{𝕜 : Type u_1}
[field 𝕜]
[module 𝕜 M]
(f : M →ₗ[𝕜] M)
(hf : ⇑linear_map.det f ≠ 1) :
If a linear map has determinant different from 1, then the space is finite-dimensional.
theorem
linear_map.range_lt_top_of_det_eq_zero
{M : Type u_2}
[add_comm_group M]
{𝕜 : Type u_1}
[field 𝕜]
[module 𝕜 M]
{f : M →ₗ[𝕜] M}
(hf : ⇑linear_map.det f = 0) :
If the determinant of a map vanishes, then the map is not onto.
theorem
linear_map.bot_lt_ker_of_det_eq_zero
{M : Type u_2}
[add_comm_group M]
{𝕜 : Type u_1}
[field 𝕜]
[module 𝕜 M]
{f : M →ₗ[𝕜] M}
(hf : ⇑linear_map.det f = 0) :
If the determinant of a map vanishes, then the map is not injective.
@[protected]
noncomputable
def
linear_equiv.det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M] :
On a linear_equiv, the domain of linear_map.det can be promoted to Rˣ.
@[simp]
theorem
linear_equiv.coe_det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(f : M ≃ₗ[R] M) :
@[simp]
theorem
linear_equiv.coe_inv_det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(f : M ≃ₗ[R] M) :
↑(⇑linear_equiv.det f)⁻¹ = ⇑linear_map.det ↑(f.symm)
@[simp]
theorem
linear_equiv.det_refl
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M] :
⇑linear_equiv.det (linear_equiv.refl R M) = 1
@[simp]
theorem
linear_equiv.det_trans
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(f g : M ≃ₗ[R] M) :
⇑linear_equiv.det (f.trans g) = (⇑linear_equiv.det g) * ⇑linear_equiv.det f
@[simp]
theorem
linear_equiv.det_symm
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(f : M ≃ₗ[R] M) :
@[simp]
theorem
linear_equiv.det_conj
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
(f : M ≃ₗ[R] M)
(e : M ≃ₗ[R] M') :
⇑linear_equiv.det ((e.symm.trans f).trans e) = ⇑linear_equiv.det f
Conjugating a linear equiv by a linear equiv does not change its determinant.
@[simp]
theorem
linear_equiv.det_mul_det_symm
{M : Type u_2}
[add_comm_group M]
{A : Type u_1}
[comm_ring A]
[module A M]
(f : M ≃ₗ[A] M) :
(⇑linear_map.det ↑f) * ⇑linear_map.det ↑(f.symm) = 1
The determinants of a linear_equiv and its inverse multiply to 1.
@[simp]
theorem
linear_equiv.det_symm_mul_det
{M : Type u_2}
[add_comm_group M]
{A : Type u_1}
[comm_ring A]
[module A M]
(f : M ≃ₗ[A] M) :
(⇑linear_map.det ↑(f.symm)) * ⇑linear_map.det ↑f = 1
The determinants of a linear_equiv and its inverse multiply to 1.
theorem
linear_equiv.is_unit_det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(f : M ≃ₗ[R] M')
(v : basis ι R M)
(v' : basis ι R M') :
is_unit (⇑(linear_map.to_matrix v v') ↑f).det
theorem
linear_equiv.is_unit_det'
{M : Type u_2}
[add_comm_group M]
{A : Type u_1}
[comm_ring A]
[module A M]
(f : M ≃ₗ[A] M) :
Specialization of linear_equiv.is_unit_det
theorem
linear_equiv.det_coe_symm
{M : Type u_2}
[add_comm_group M]
{𝕜 : Type u_1}
[field 𝕜]
[module 𝕜 M]
(f : M ≃ₗ[𝕜] M) :
⇑linear_map.det ↑(f.symm) = (⇑linear_map.det ↑f)⁻¹
The determinant of f.symm is the inverse of that of f when f is a linear equiv.
@[simp]
theorem
linear_equiv.of_is_unit_det_apply
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{f : M →ₗ[R] M'}
{v : basis ι R M}
{v' : basis ι R M'}
(h : is_unit (⇑(linear_map.to_matrix v v') f).det)
(ᾰ : M) :
⇑(linear_equiv.of_is_unit_det h) ᾰ = ⇑f ᾰ
@[simp]
theorem
linear_equiv.of_is_unit_det_symm_apply
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{f : M →ₗ[R] M'}
{v : basis ι R M}
{v' : basis ι R M'}
(h : is_unit (⇑(linear_map.to_matrix v v') f).det)
(ᾰ : M') :
⇑((linear_equiv.of_is_unit_det h).symm) ᾰ = ⇑(⇑(matrix.to_lin v' v) (⇑(linear_map.to_matrix v v') f)⁻¹) ᾰ
noncomputable
def
linear_equiv.of_is_unit_det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{f : M →ₗ[R] M'}
{v : basis ι R M}
{v' : basis ι R M'}
(h : is_unit (⇑(linear_map.to_matrix v v') f).det) :
Builds a linear equivalence from a linear map whose determinant in some bases is a unit.
@[simp]
theorem
linear_equiv.coe_of_is_unit_det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{f : M →ₗ[R] M'}
{v : basis ι R M}
{v' : basis ι R M'}
(h : is_unit (⇑(linear_map.to_matrix v v') f).det) :
noncomputable
def
linear_map.equiv_of_det_ne_zero
{𝕜 : Type u_1}
[field 𝕜]
{M : Type u_2}
[add_comm_group M]
[module 𝕜 M]
[finite_dimensional 𝕜 M]
(f : M →ₗ[𝕜] M)
(hf : ⇑linear_map.det f ≠ 0) :
Builds a linear equivalence from a linear map on a finite-dimensional vector space whose determinant is nonzero.
Equations
- f.equiv_of_det_ne_zero hf = have this : is_unit (⇑(linear_map.to_matrix (finite_dimensional.fin_basis 𝕜 M) (finite_dimensional.fin_basis 𝕜 M)) f).det, from _, linear_equiv.of_is_unit_det this
noncomputable
def
basis.det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M) :
alternating_map R M R ι
The determinant of a family of vectors with respect to some basis, as an alternating multilinear map.
theorem
basis.det_apply
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M)
(v : ι → M) :
theorem
basis.det_self
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M) :
theorem
basis.det_ne_zero
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M)
[nontrivial R] :
basis.det is not the zero map.
theorem
is_basis_iff_det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M)
{v : ι → M} :
linear_independent R v ∧ submodule.span R (set.range v) = ⊤ ↔ is_unit (⇑(e.det) v)
theorem
basis.is_unit_det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e e' : basis ι R M) :
theorem
alternating_map.eq_smul_basis_det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M)
(f : alternating_map R M R ι) :
Any alternating map to R where ι has the cardinality of a basis equals the determinant
map with respect to that basis, multiplied by the value of that alternating map on that basis.
@[simp]
theorem
alternating_map.map_basis_eq_zero_iff
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M)
(f : alternating_map R M R ι) :
theorem
alternating_map.map_basis_ne_zero_iff
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M)
(f : alternating_map R M R ι) :
@[simp]
theorem
basis.det_comp
{M : Type u_2}
[add_comm_group M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{A : Type u_5}
[comm_ring A]
[module A M]
(e : basis ι A M)
(f : M →ₗ[A] M)
(v : ι → M) :
theorem
basis.det_reindex
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{ι' : Type u_3}
[fintype ι']
[decidable_eq ι']
(b : basis ι R M)
(v : ι' → M)
(e : ι ≃ ι') :
theorem
basis.det_reindex_symm
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{ι' : Type u_3}
[fintype ι']
[decidable_eq ι']
(b : basis ι R M)
(v : ι → M)
(e : ι' ≃ ι) :
@[simp]
theorem
basis.det_map
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(b : basis ι R M)
(f : M ≃ₗ[R] M')
(v : ι → M') :
theorem
basis.det_map'
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(b : basis ι R M)
(f : M ≃ₗ[R] M') :
@[simp]
theorem
basis.det_smul_mk_coord_eq_det_update
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M)
{v : ι → M}
(hli : linear_independent R v)
(hsp : submodule.span R (set.range v) = ⊤)
(i : ι) :
⇑(e.det) v • (basis.mk hli hsp).coord i = e.det.to_multilinear_map.to_linear_map v i
If we fix a background basis e, then for any other basis v, we can characterise the
coordinates provided by v in terms of determinants relative to e.
@[simp]
theorem
basis.det_units_smul
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M)
(w : ι → Rˣ) :
The determinant of a basis constructed by units_smul is the product of the given units.
@[simp]
theorem
basis.det_is_unit_smul
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M)
{w : ι → R}
(hw : ∀ (i : ι), is_unit (w i)) :
⇑(e.det) ⇑(e.is_unit_smul hw) = ∏ (i : ι), w i
The determinant of a basis constructed by is_unit_smul is the product of the given units.