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
LinearAlgebra.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 mapLinearMap.det
: the determinant of an endomorphismf : End R M
as a multiplicative homomorphism (ifM
does not have a finiteR
-basis, the result is1
instead)LinearEquiv.det
: the determinant of an isomorphismf : M ≃ₗ[R] M
as a multiplicative homomorphism (ifM
does not have a finiteR
-basis, the result is1
instead)
Tags #
basis, det, determinant
If R^m
and R^n
are linearly equivalent, then m
and n
are also equivalent.
Equations
- equivOfPiLEquivPi e = (Basis.ofEquivFun e.symm).indexEquiv (Pi.basisFun R n)
Instances For
If M
and M'
are each other's inverse matrices, they are square matrices up to
equivalence of types.
Equations
- Matrix.indexEquivOfInv hMM' hM'M = equivOfPiLEquivPi (Matrix.toLin'OfInv hMM' hM'M)
Instances For
If there exists a two-sided inverse M'
for M
(indexed differently),
then det (N * M) = det (M * N)
.
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 #
The determinant of LinearMap.toMatrix
does not depend on the choice of basis.
The determinant of an endomorphism given a basis.
See LinearMap.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 detAux
's
type that it does not depend on the choice of basis. Instead you can use the detAux_def''
lemma,
or avoid mentioning a basis at all using LinearMap.det
.
Equations
Instances For
Unfold lemma for detAux
.
See also detAux_def''
which allows you to vary the basis.
The determinant of an endomorphism independent of basis.
If there is no finite basis on M
, the result is 1
instead.
Equations
Instances For
To show P (LinearMap.det f)
it suffices to consider P (Matrix.det (toMatrix _ _ f))
and
P 1
.
Multiplying a map by a scalar c
multiplies its determinant by c ^ dim 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
.
Conjugating a linear map by a linear equiv does not change its determinant.
If a linear map has determinant different from 1
, then the space is finite-dimensional.
If the determinant of a map vanishes, then the map is not onto.
If the determinant of a map vanishes, then the map is not injective.
On a LinearEquiv
, the domain of LinearMap.det
can be promoted to Rˣ
.
Equations
- LinearEquiv.det = (Units.map LinearMap.det).comp (LinearMap.GeneralLinearGroup.generalLinearEquiv R M).symm.toMonoidHom
Instances For
Conjugating a linear equiv by a linear equiv does not change its determinant.
The determinants of a LinearEquiv
and its inverse multiply to 1.
The determinants of a LinearEquiv
and its inverse multiply to 1.
Specialization of LinearEquiv.isUnit_det
Builds a linear equivalence from a linear map whose determinant in some bases is a unit.
Equations
- LinearEquiv.ofIsUnitDet h = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑((Matrix.toLin v' v) ((LinearMap.toMatrix v v') f)⁻¹), left_inv := ⋯, right_inv := ⋯ }
Instances For
Builds a linear equivalence from a linear map on a finite-dimensional vector space whose determinant is nonzero.
Equations
- f.equivOfDetNeZero hf = let_fun this := ⋯; LinearEquiv.ofIsUnitDet this
Instances For
The determinant of a family of vectors with respect to some basis, as an alternating multilinear map.
Equations
- e.det = { toFun := fun (v : ι → M) => (e.toMatrix v).det, map_add' := ⋯, map_smul' := ⋯, map_eq_zero_of_eq' := ⋯ }
Instances For
Basis.det
is not the zero map.
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.
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
.
If a basis is multiplied columnwise by scalars w : ι → Rˣ
, then the determinant with respect
to this basis is multiplied by the product of the inverse of these scalars.
The determinant of a basis constructed by unitsSMul
is the product of the given units.
The determinant of a basis constructed by isUnitSMul
is the product of the given units.