mathlib documentation

linear_algebra.determinant

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.

Tags #

basis, det, determinant

def equiv_of_pi_lequiv_pi {m : Type u_6} {n : Type u_7} [fintype m] [fintype n] {R : Type u_1} [integral_domain 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
def matrix.index_equiv_of_inv {A : Type u_5} [integral_domain 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} (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
theorem matrix.det_comm {A : Type u_5} [integral_domain A] {n : Type u_7} [fintype n] [decidable_eq n] (M N : matrix n n A) :
(M N).det = (N M).det
theorem matrix.det_comm' {A : Type u_5} [integral_domain 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) :
(M N).det = (N M).det

If there exists a two-sided inverse M' for M (indexed differently), then det (N ⬝ M) = det (M ⬝ N).

theorem matrix.det_conj {A : Type u_5} [integral_domain 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) :
(M N M').det = N.det

If M' is a two-sided inverse for M (indexed differently), det (M ⬝ N ⬝ M') = det N.

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} [integral_domain A] [module A M] {κ : Type u_6} [fintype κ] [decidable_eq κ] (b : basis ι A M) (c : basis κ A M) (f : M →ₗ[A] M) :

The determinant of linear_map.to_matrix does not depend on the choice of basis.

def linear_map.det_aux {M : Type u_2} [add_comm_group M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {A : Type u_5} [integral_domain A] [module A M] :
trunc (basis ι A M)(M →ₗ[A] M) →* A

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
theorem linear_map.det_aux_def {M : Type u_2} [add_comm_group M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {A : Type u_5} [integral_domain A] [module A M] (b : basis ι A M) (f : M →ₗ[A] M) :

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} [integral_domain A] [module A M] {ι' : Type u_1} [fintype ι'] [decidable_eq ι'] (tb : trunc (basis ι A M)) (b' : basis ι' A M) (f : M →ₗ[A] M) :
@[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} [integral_domain 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} [integral_domain A] [module A M] (b : trunc (basis ι A M)) (f g : M →ₗ[A] M) :
def linear_map.det {M : Type u_2} [add_comm_group M] {A : Type u_5} [integral_domain A] [module A M] :
(M →ₗ[A] M) →* A

The determinant of an endomorphism independent of basis.

If there is no finite basis on M, the result is 1 instead.

Equations
theorem linear_map.coe_det {M : Type u_2} [add_comm_group M] {A : Type u_5} [integral_domain A] [module A M] [decidable_eq M] :
linear_map.det = dite (∃ (s : finset M), nonempty (basis s A M)) (λ (H : ∃ (s : finset M), nonempty (basis s A M)), (linear_map.det_aux (trunc.mk (nonempty.some _)))) (λ (H : ¬∃ (s : finset M), nonempty (basis s A M)), 1)
theorem linear_map.det_eq_det_to_matrix_of_finset {M : Type u_2} [add_comm_group M] {A : Type u_5} [integral_domain A] [module A M] [decidable_eq M] {s : finset M} (b : basis s A M) (f : M →ₗ[A] M) :
@[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} [integral_domain A] [module A M] (b : basis ι A M) (f : M →ₗ[A] M) :
@[simp]
theorem linear_map.det_to_matrix' {A : Type u_5} [integral_domain 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} [integral_domain 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) :

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} [integral_domain A] [module A M] (f g : M →ₗ[A] M) :
@[simp]
theorem linear_map.det_id {M : Type u_2} [add_comm_group M] {A : Type u_5} [integral_domain 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) :

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} [integral_domain A] [module A M] {ι : Type u_1} [fintype ι] [nonempty ι] (b : basis ι A M) :
@[simp]
theorem linear_map.det_zero {𝕜 : Type u_1} [field 𝕜] {M : Type u_2} [add_comm_group M] [module 𝕜 M] :

In a finite-dimensional vector space, the zero map has determinant 1 in dimension 0, and 0 otherwise.

@[simp]
theorem linear_map.det_conj {M : Type u_2} [add_comm_group M] {A : Type u_5} [integral_domain A] [module A M] {N : Type u_1} [add_comm_group N] [module A N] (f : M →ₗ[A] M) (e : M ≃ₗ[A] N) :

Conjugating a linear map by a linear equiv does not change its determinant.

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') :
theorem linear_equiv.is_unit_det' {M : Type u_2} [add_comm_group M] {A : Type u_1} [integral_domain A] [module A M] (f : M ≃ₗ[A] M) :

Specialization of linear_equiv.is_unit_det

@[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) :
@[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') :
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) :
M ≃ₗ[R] M'

Builds a linear equivalence from a linear map whose determinant in some bases is a unit.

Equations
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) :
M ≃ₗ[𝕜] M

Builds a linear equivalence from a linear map on a finite-dimensional vector space whose determinant is nonzero.

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

The determinant of a family of vectors with respect to some basis, as an alternating multilinear map.

Equations
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) :
(e.det) v = (e.to_matrix v).det
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) :
(e.det) e = 1
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} :
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) :
@[simp]
theorem basis.det_comp {M : Type u_2} [add_comm_group M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {A : Type u_5} [integral_domain A] [module A M] (e : basis ι A M) (f : M →ₗ[A] M) (v : ι → M) :
(e.det) (f v) = (linear_map.det f) * (e.det) v
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 : ι ι') :
((b.reindex e).det) v = (b.det) (v 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 : ι' ι) :
((b.reindex e.symm).det) (v e) = (b.det) v
@[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') :
((b.map f).det) v = (b.det) ((f.symm) v)