Mathlib.LinearAlgebra.Determinant

equivOfPiLEquivPi definition

{R : Type*} [Finite m] [Finite n] [CommRing R] [Nontrivial R] (e : (m → R) ≃ₗ[R] n → R) : m ≃ n

Full source

/-- If `R^m` and `R^n` are linearly equivalent, then `m` and `n` are also equivalent. -/
def equivOfPiLEquivPi {R : Type*} [Finite m] [Finite n] [CommRing R] [Nontrivial R]
    (e : (m → R) ≃ₗ[R] n → R) : m ≃ n :=
  Basis.indexEquiv (Basis.ofEquivFun e.symm) (Pi.basisFun _ _)

Equivalence of index sets under linear equivalence of function spaces

Informal description

Given a commutative ring $R$ with at least two distinct elements, and finite types $m$ and $n$, if there exists a linear equivalence $e : (m \to R) \simeq_{\ell[R]} (n \to R)$ between the spaces of functions from $m$ to $R$ and from $n$ to $R$, then there exists a bijection between the index sets $m$ and $n$.

Matrix.indexEquivOfInv definition

 [Nontrivial A] [DecidableEq m] [DecidableEq n] {M : Matrix m n A} {M' : Matrix n m A} (hMM' : M * M' = 1)
  (hM'M : M' * M = 1) : m ≃ n

Full source

/-- If `M` and `M'` are each other's inverse matrices, they are square matrices up to
equivalence of types. -/
def indexEquivOfInv [Nontrivial A] [DecidableEq m] [DecidableEq n] {M : Matrix m n A}
    {M' : Matrix n m A} (hMM' : M * M' = 1) (hM'M : M' * M = 1) : m ≃ n :=
  equivOfPiLEquivPi (toLin'OfInv hMM' hM'M)

Bijection between index sets for inverse matrices

Informal description

Given a nontrivial commutative ring $A$ and finite types $m$ and $n$ with decidable equality, if $M$ is an $m \times n$ matrix and $M'$ is an $n \times m$ matrix over $A$ such that $M M' = I_m$ and $M' M = I_n$, then there exists a bijection between the index sets $m$ and $n$.

Matrix.det_comm theorem

[DecidableEq n] (M N : Matrix n n A) : det (M * N) = det (N * M)

Full source

theorem det_comm [DecidableEq n] (M N : Matrix n n A) : det (M * N) = det (N * M) := by
  rw [det_mul, det_mul, mul_comm]

Commutativity of Determinant for Matrix Products: $\det(MN) = \det(NM)$

Informal description

For any two square matrices $M$ and $N$ of size $n \times n$ over a commutative ring $A$ (where $n$ has decidable equality), the determinant of their product is commutative, i.e., \[ \det(MN) = \det(NM). \]

Matrix.det_comm' theorem

 [DecidableEq m] [DecidableEq n] {M : Matrix n m A} {N : Matrix m n A} {M' : Matrix m n A} (hMM' : M * M' = 1)
  (hM'M : M' * M = 1) : det (M * N) = det (N * M)

Full source

/-- If there exists a two-sided inverse `M'` for `M` (indexed differently),
then `det (N * M) = det (M * N)`. -/
theorem det_comm' [DecidableEq m] [DecidableEq n] {M : Matrix n m A} {N : Matrix m n A}
    {M' : Matrix m n A} (hMM' : M * M' = 1) (hM'M : M' * M = 1) : det (M * N) = det (N * M) := by
  nontriviality A
  -- Although `m` and `n` are different a priori, we will show they have the same cardinality.
  -- This turns the problem into one for square matrices, which is easy.
  let e := indexEquivOfInv hMM' hM'M
  rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm,
    submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]

Determinant Commutativity for Matrices with Two-Sided Inverses: $\det(MN) = \det(NM)$

Informal description

Let $A$ be a commutative ring, and let $m$ and $n$ be finite types with decidable equality. Given matrices $M \in \mathrm{Matrix}\, n\, m\, A$, $N \in \mathrm{Matrix}\, m\, n\, A$, and $M' \in \mathrm{Matrix}\, m\, n\, A$ such that $M M' = I_n$ and $M' M = I_m$, then the determinants of $M N$ and $N M$ are equal, i.e., \[ \det(M N) = \det(N M). \]

Matrix.det_conj_of_mul_eq_one theorem

 [DecidableEq m] [DecidableEq 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) : det (M * N * M') = det N

Full source

/-- 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. -/
theorem det_conj_of_mul_eq_one [DecidableEq m] [DecidableEq 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) :
    det (M * N * M') = det N := by
  rw [← det_comm' hM'M hMM', ← Matrix.mul_assoc, hM'M, Matrix.one_mul]

Determinant Invariance under Conjugation with Two-Sided Inverses: $\det(MNM') = \det(N)$

Informal description

Let $A$ be a commutative ring, and let $m$ and $n$ be finite types with decidable equality. Given matrices $M \in \mathrm{Matrix}\, m\, n\, A$, $M' \in \mathrm{Matrix}\, n\, m\, A$, and $N \in \mathrm{Matrix}\, n\, n\, A$ such that $M M' = I_m$ and $M' M = I_n$, then the determinant of $M N M'$ equals the determinant of $N$, i.e., \[ \det(M N M') = \det(N). \]

LinearMap.det_toMatrix_eq_det_toMatrix theorem

 [DecidableEq κ] (b : Basis ι A M) (c : Basis κ A M) (f : M →ₗ[A] M) :
  det (LinearMap.toMatrix b b f) = det (LinearMap.toMatrix c c f)

Full source

/-- The determinant of `LinearMap.toMatrix` does not depend on the choice of basis. -/
theorem det_toMatrix_eq_det_toMatrix [DecidableEq κ] (b : Basis ι A M) (c : Basis κ A M)
    (f : M →ₗ[A] M) : det (LinearMap.toMatrix b b f) = det (LinearMap.toMatrix c c f) := by
  rw [← linearMap_toMatrix_mul_basis_toMatrix c b c, ← basis_toMatrix_mul_linearMap_toMatrix b c b,
      Matrix.det_conj_of_mul_eq_one] <;>
    rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]

Basis Independence of Determinant for Linear Endomorphisms

Informal description

Let $M$ be a module over a commutative ring $A$ with two bases $b$ (indexed by $\iota$) and $c$ (indexed by $\kappa$, with decidable equality). For any linear endomorphism $f : M \to M$, the determinant of the matrix representation of $f$ with respect to basis $b$ is equal to the determinant of the matrix representation of $f$ with respect to basis $c$. In symbols: \[ \det(\text{toMatrix}_{b,b}(f)) = \det(\text{toMatrix}_{c,c}(f)) \] where $\text{toMatrix}_{x,y}(f)$ denotes the matrix representation of $f$ with respect to bases $x$ and $y$.

LinearMap.detAux definition

Full source

/-- 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`.
-/
irreducible_def detAux : Trunc (Basis ι A M) → (M →ₗ[A] M) →* A :=
  Trunc.lift
    (fun b : Basis ι A M => detMonoidHom.comp (toMatrixAlgEquiv b : (M →ₗ[A] M) →* Matrix ι ι A))
    fun b c => MonoidHom.ext <| det_toMatrix_eq_det_toMatrix b c

Determinant of an endomorphism (basis-dependent version)

Informal description

Given a commutative ring $ A $ and a finite-dimensional $ A $-module $ M $ with a basis indexed by $ \iota $, the determinant of an endomorphism $ f \colon M \to M $ is defined as the determinant of the matrix representation of $ f $ with respect to the basis. This definition is parametrized by a truncated basis (to allow for non-computable basis switching), and the result is independent of the choice of basis. If $ M $ does not have a finite basis, the determinant defaults to $ 1 $.

LinearMap.detAux_def theorem

: eta_helper Eq✝ @detAux.{} @(delta% @definition✝)

Full source

/-- 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`.
-/
irreducible_def detAux : Trunc (Basis ι A M) → (M →ₗ[A] M) →* A :=
  Trunc.lift
    (fun b : Basis ι A M => detMonoidHom.comp (toMatrixAlgEquiv b : (M →ₗ[A] M) →* Matrix ι ι A))
    fun b c => MonoidHom.ext <| det_toMatrix_eq_det_toMatrix b c

Definition of Determinant via Matrix Representation

Informal description

The definition of the determinant of an endomorphism $f \colon M \to M$ of a finite-dimensional module $M$ over a commutative ring $A$ is given by $\det(f) = \det(\text{toMatrix}_b(f))$, where $\text{toMatrix}_b(f)$ is the matrix representation of $f$ with respect to any basis $b$ of $M$.

LinearMap.detAux_def' theorem

(b : Basis ι A M) (f : M →ₗ[A] M) : LinearMap.detAux (Trunc.mk b) f = Matrix.det (LinearMap.toMatrix b b f)

Full source

/-- Unfold lemma for `detAux`.

See also `detAux_def''` which allows you to vary the basis.
-/
theorem detAux_def' (b : Basis ι A M) (f : M →ₗ[A] M) :
    LinearMap.detAux (Trunc.mk b) f = Matrix.det (LinearMap.toMatrix b b f) := by
  rw [detAux]
  rfl

Determinant of Linear Endomorphism via Matrix Representation

Informal description

Given a commutative ring $A$, a finite-dimensional $A$-module $M$ with a basis $b$ indexed by a finite type $\iota$, and an $A$-linear endomorphism $f \colon M \to M$, the determinant of $f$ (computed via the auxiliary function $\detAux$) equals the determinant of the matrix representation of $f$ with respect to the basis $b$. That is, \[ \det(f) = \det([f]_b^b) \] where $[f]_b^b$ denotes the matrix of $f$ in the basis $b$.

LinearMap.detAux_def'' theorem

 {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (tb : Trunc <| Basis ι A M) (b' : Basis ι' A M) (f : M →ₗ[A] M) :
  LinearMap.detAux tb f = Matrix.det (LinearMap.toMatrix b' b' f)

Full source

theorem detAux_def'' {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (tb : Trunc <| Basis ι A M)
    (b' : Basis ι' A M) (f : M →ₗ[A] M) :
    LinearMap.detAux tb f = Matrix.det (LinearMap.toMatrix b' b' f) := by
  induction tb using Trunc.induction_on with
  | h b => rw [detAux_def', det_toMatrix_eq_det_toMatrix b b']

Basis Independence of Determinant via Matrix Representation

Informal description

Let $A$ be a commutative ring and $M$ be a finite-dimensional $A$-module. For any finite type $\iota'$ with decidable equality, any truncated basis $tb$ of $M$ indexed by $\iota$, any basis $b'$ of $M$ indexed by $\iota'$, and any $A$-linear endomorphism $f \colon M \to M$, the determinant of $f$ (computed via the auxiliary function $\detAux$) equals the determinant of the matrix representation of $f$ with respect to the basis $b'$. That is, \[ \det(f) = \det([f]_{b'}^{b'}) \] where $[f]_{b'}^{b'}$ denotes the matrix of $f$ in the basis $b'$.

LinearMap.detAux_id theorem

(b : Trunc <| Basis ι A M) : LinearMap.detAux b LinearMap.id = 1

Full source

@[simp]
theorem detAux_id (b : Trunc <| Basis ι A M) : LinearMap.detAux b LinearMap.id = 1 :=
  (LinearMap.detAux b).map_one

Determinant of the Identity Endomorphism is One

Informal description

For any truncated basis $b$ of a finite-dimensional module $M$ over a commutative ring $A$, the determinant of the identity endomorphism $\text{id} \colon M \to M$ is equal to $1$.

LinearMap.detAux_comp theorem

 (b : Trunc <| Basis ι A M) (f g : M →ₗ[A] M) :
  LinearMap.detAux b (f.comp g) = LinearMap.detAux b f * LinearMap.detAux b g

Full source

@[simp]
theorem detAux_comp (b : Trunc <| Basis ι A M) (f g : M →ₗ[A] M) :
    LinearMap.detAux b (f.comp g) = LinearMap.detAux b f * LinearMap.detAux b g :=
  (LinearMap.detAux b).map_mul f g

Multiplicativity of Determinant under Composition: $\det(f \circ g) = \det(f) \det(g)$

Informal description

Let $A$ be a commutative ring and $M$ be a finite-dimensional $A$-module with a basis indexed by $\iota$. For any two endomorphisms $f, g \colon M \to M$, the determinant of the composition $f \circ g$ is equal to the product of the determinants of $f$ and $g$, i.e., \[ \det(f \circ g) = \det(f) \cdot \det(g). \]

LinearMap.det definition

Full source

/-- The determinant of an endomorphism independent of basis.

If there is no finite basis on `M`, the result is `1` instead.
-/
protected irreducible_def det : (M →ₗ[A] M) →* A :=
  if H : ∃ s : Finset M, Nonempty (Basis s A M) then LinearMap.detAux (Trunc.mk H.choose_spec.some)
  else 1

Determinant of a linear endomorphism

Informal description

The determinant of an endomorphism $ f \colon M \to M $ over a commutative ring $ A $, defined independently of the choice of basis. If $ M $ does not admit a finite basis, the determinant is defined to be $ 1 $.

LinearMap.det_def theorem

: eta_helper Eq✝ @det.{} @(delta% @definition✝)

Full source

/-- The determinant of an endomorphism independent of basis.

If there is no finite basis on `M`, the result is `1` instead.
-/
protected irreducible_def det : (M →ₗ[A] M) →* A :=
  if H : ∃ s : Finset M, Nonempty (Basis s A M) then LinearMap.detAux (Trunc.mk H.choose_spec.some)
  else 1

Implementation Detail of Linear Map Determinant Definition

Informal description

This appears to be an implementation detail about the definition of the determinant of a linear map, rather than a mathematical theorem. As such, it doesn't translate directly to an informal mathematical statement.

LinearMap.coe_det theorem

 [DecidableEq M] :
  ⇑(LinearMap.det : (M →ₗ[A] M) →* A) =
    if H : ∃ s : Finset M, Nonempty (Basis s A M) then LinearMap.detAux (Trunc.mk H.choose_spec.some) else 1

Full source

theorem coe_det [DecidableEq M] :
    ⇑(LinearMap.det : (M →ₗ[A] M) →* A) =
      if H : ∃ s : Finset M, Nonempty (Basis s A M) then
        LinearMap.detAux (Trunc.mk H.choose_spec.some)
      else 1 := by
  ext
  rw [LinearMap.det_def]
  split_ifs
  · congr -- use the correct `DecidableEq` instance
  rfl

Determinant of a Linear Endomorphism via Basis Construction

Informal description

For a commutative ring $A$ and an $A$-module $M$ with decidable equality, the determinant of a linear endomorphism $f \colon M \to M$ is given by the function: \[ \text{det}(f) = \begin{cases} \text{detAux}(\text{Trunc.mk } b) & \text{if there exists a finite set } s \subseteq M \text{ and a basis } b \text{ of } M \text{ indexed by } s, \\ 1 & \text{otherwise.} \end{cases} \] Here, $\text{detAux}$ computes the determinant using the given basis, and $\text{Trunc.mk } b$ represents the truncation of the basis $b$ to handle non-constructive aspects.

LinearMap.det_eq_det_toMatrix_of_finset theorem

 [DecidableEq M] {s : Finset M} (b : Basis s A M) (f : M →ₗ[A] M) :
  LinearMap.det f = Matrix.det (LinearMap.toMatrix b b f)

Full source

theorem det_eq_det_toMatrix_of_finset [DecidableEq M] {s : Finset M} (b : Basis s A M)
    (f : M →ₗ[A] M) : LinearMap.det f = Matrix.det (LinearMap.toMatrix b b f) := by
  have : ∃ s : Finset M, Nonempty (Basis s A M) := ⟨s, ⟨b⟩⟩
  rw [LinearMap.coe_det, dif_pos, detAux_def'' _ b] <;> assumption

Determinant of Linear Endomorphism Equals Determinant of Matrix Representation

Informal description

Let $A$ be a commutative ring and $M$ be an $A$-module with decidable equality. Given a finite subset $s \subseteq M$ and a basis $b$ of $M$ indexed by $s$, for any $A$-linear endomorphism $f \colon M \to M$, the determinant of $f$ is equal to the determinant of the matrix representation of $f$ with respect to the basis $b$. That is, \[ \det(f) = \det([f]_b^b) \] where $[f]_b^b$ denotes the matrix of $f$ in the basis $b$.

LinearMap.det_toMatrix theorem

(b : Basis ι A M) (f : M →ₗ[A] M) : Matrix.det (toMatrix b b f) = LinearMap.det f

Full source

@[simp]
theorem det_toMatrix (b : Basis ι A M) (f : M →ₗ[A] M) :
    Matrix.det (toMatrix b b f) = LinearMap.det f := by
  haveI := Classical.decEq M
  rw [det_eq_det_toMatrix_of_finset b.reindexFinsetRange,
    det_toMatrix_eq_det_toMatrix b b.reindexFinsetRange]

Determinant of Matrix Representation Equals Determinant of Linear Endomorphism

Informal description

Let $A$ be a commutative ring and $M$ be an $A$-module with a basis $b$ indexed by a finite type $\iota$. For any $A$-linear endomorphism $f \colon M \to M$, the determinant of the matrix representation of $f$ with respect to the basis $b$ is equal to the determinant of $f$ as a linear map. That is, \[ \det([f]_b^b) = \det(f) \] where $[f]_b^b$ denotes the matrix of $f$ in the basis $b$.

LinearMap.det_toMatrix' theorem

 {ι : Type*} [Fintype ι] [DecidableEq ι] (f : (ι → A) →ₗ[A] ι → A) :
  Matrix.det (LinearMap.toMatrix' f) = LinearMap.det f

Full source

@[simp]
theorem det_toMatrix' {ι : Type*} [Fintype ι] [DecidableEq ι] (f : (ι → A) →ₗ[A] ι → A) :
    Matrix.det (LinearMap.toMatrix' f) = LinearMap.det f := by simp [← toMatrix_eq_toMatrix']

Determinant of Matrix Representation Equals Determinant of Linear Endomorphism for Standard Basis

Informal description

Let $A$ be a commutative ring and $\iota$ be a finite type with decidable equality. For any $A$-linear endomorphism $f$ of the function space $\iota \to A$, the determinant of the matrix representation of $f$ (with respect to the standard basis) is equal to the determinant of $f$ as a linear map. That is, \[ \det([f]) = \det(f), \] where $[f]$ denotes the matrix of $f$ in the standard basis.

LinearMap.det_toLin theorem

(b : Basis ι R M) (f : Matrix ι ι R) : LinearMap.det (Matrix.toLin b b f) = f.det

Full source

@[simp]
theorem det_toLin (b : Basis ι R M) (f : Matrix ι ι R) :
    LinearMap.det (Matrix.toLin b b f) = f.det := by
  rw [← LinearMap.det_toMatrix b, LinearMap.toMatrix_toLin]

Determinant of Matrix-to-Linear-Map Transformation Equals Matrix Determinant

Informal description

Let $R$ be a commutative ring and $M$ be an $R$-module with a basis $b$ indexed by a finite type $\iota$. For any square matrix $f$ of size $\iota \times \iota$ with entries in $R$, the determinant of the linear endomorphism obtained by interpreting $f$ as a linear map (via the basis $b$) is equal to the determinant of the matrix $f$. That is, \[ \det(\text{Matrix.toLin } b b f) = \det(f). \]

LinearMap.det_toLin' theorem

(f : Matrix ι ι R) : LinearMap.det (Matrix.toLin' f) = Matrix.det f

Full source

@[simp]
theorem det_toLin' (f : Matrix ι ι R) : LinearMap.det (Matrix.toLin' f) = Matrix.det f := by
  simp only [← toLin_eq_toLin', det_toLin]

Determinant of Matrix-to-Linear-Map Transformation Equals Matrix Determinant (Standard Basis)

Informal description

For any square matrix $f$ of size $\iota \times \iota$ with entries in a commutative ring $R$, the determinant of the linear endomorphism obtained by interpreting $f$ as a linear map (via the standard basis) is equal to the determinant of the matrix $f$. That is, \[ \det(\text{Matrix.toLin}' f) = \det(f). \]

LinearMap.det_cases theorem

 [DecidableEq M] {P : A → Prop} (f : M →ₗ[A] M)
  (hb : ∀ (s : Finset M) (b : Basis s A M), P (Matrix.det (toMatrix b b f))) (h1 : P 1) : P (LinearMap.det f)

Full source

/-- To show `P (LinearMap.det f)` it suffices to consider `P (Matrix.det (toMatrix _ _ f))` and
`P 1`. -/
@[elab_as_elim]
theorem det_cases [DecidableEq M] {P : A → Prop} (f : M →ₗ[A] M)
    (hb : ∀ (s : Finset M) (b : Basis s A M), P (Matrix.det (toMatrix b b f))) (h1 : P 1) :
    P (LinearMap.det f) := by
  classical
  if H : ∃ s : Finset M, Nonempty (Basis s A M) then
    obtain ⟨s, ⟨b⟩⟩ := H
    rw [← det_toMatrix b]
    exact hb s b
  else
    rwa [LinearMap.det_def, dif_neg H]

Case Analysis Principle for Determinant of Linear Endomorphism

Informal description

Let $M$ be a module over a commutative ring $A$ with decidable equality, and let $P$ be a predicate on $A$. Given a linear endomorphism $f \colon M \to M$, to prove $P(\det(f))$ it suffices to: 1. Show $P(\det([f]_b^b))$ for every finite subset $s \subseteq M$ and every basis $b$ of $M$ indexed by $s$, where $[f]_b^b$ is the matrix representation of $f$ with respect to $b$. 2. Show $P(1)$ (which handles the case when $M$ has no finite basis).

LinearMap.det_comp theorem

(f g : M →ₗ[A] M) : LinearMap.det (f.comp g) = LinearMap.det f * LinearMap.det g

Full source

@[simp]
theorem det_comp (f g : M →ₗ[A] M) :
    LinearMap.det (f.comp g) = LinearMap.det f * LinearMap.det g :=
  LinearMap.det.map_mul f g

Multiplicativity of Determinant under Composition: $\det(f \circ g) = \det(f) \det(g)$

Informal description

For any two linear endomorphisms $f$ and $g$ of a module $M$ over a commutative ring $A$, the determinant of their composition satisfies $\det(f \circ g) = \det(f) \cdot \det(g)$.

LinearMap.det_id theorem

: LinearMap.det (LinearMap.id : M →ₗ[A] M) = 1

Full source

@[simp]
theorem det_id : LinearMap.det (LinearMap.id : M →ₗ[A] M) = 1 :=
  LinearMap.det.map_one

Determinant of the Identity Linear Map: $\det(\text{id}) = 1$

Informal description

The determinant of the identity linear map $\text{id} \colon M \to M$ over a commutative ring $A$ is equal to $1$.

LinearMap.det_smul theorem

[Module.Free A M] (c : A) (f : M →ₗ[A] M) : LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Full source

/-- Multiplying a map by a scalar `c` multiplies its determinant by `c ^ dim M`. -/
@[simp]
theorem det_smul [Module.Free A M] (c : A) (f : M →ₗ[A] M) :
    LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f := by
  nontriviality A
  by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)
  · have : Module.Finite A M := by
      rcases H with ⟨s, ⟨hs⟩⟩
      exact Module.Finite.of_basis hs
    simp only [← det_toMatrix (Module.finBasis A M), LinearEquiv.map_smul,
      Fintype.card_fin, Matrix.det_smul]
  · classical
      have : Module.finrank A M = 0 := finrank_eq_zero_of_not_exists_basis H
      simp [coe_det, H, this]

Determinant Scaling: $\det(c \cdot f) = c^{\dim M} \det(f)$

Informal description

Let $A$ be a commutative ring and $M$ be a free $A$-module of finite rank. For any scalar $c \in A$ and any linear endomorphism $f \colon M \to M$, the determinant of the scaled endomorphism $c \cdot f$ satisfies \[ \det(c \cdot f) = c^{\dim M} \cdot \det(f), \] where $\dim M$ denotes the rank of $M$ as an $A$-module.

LinearMap.det_zero' theorem

{ι : Type*} [Finite ι] [Nonempty ι] (b : Basis ι A M) : LinearMap.det (0 : M →ₗ[A] M) = 0

Full source

theorem det_zero' {ι : Type*} [Finite ι] [Nonempty ι] (b : Basis ι A M) :
    LinearMap.det (0 : M →ₗ[A] M) = 0 := by
  haveI := Classical.decEq ι
  cases nonempty_fintype ι
  rwa [← det_toMatrix b, LinearEquiv.map_zero, det_zero]

Determinant of Zero Endomorphism is Zero for Finite-Dimensional Modules

Informal description

Let $A$ be a commutative ring and $M$ be an $A$-module with a basis $b$ indexed by a finite nonempty type $\iota$. Then the determinant of the zero linear endomorphism $0 : M \to M$ is equal to $0$.

LinearMap.det_zero theorem

[Module.Free A M] : LinearMap.det (0 : M →ₗ[A] M) = (0 : A) ^ Module.finrank A M

Full source

/-- 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 det_zero [Module.Free A M] :
    LinearMap.det (0 : M →ₗ[A] M) = (0 : A) ^ Module.finrank A M := by
  simp only [← zero_smul A (1 : M →ₗ[A] M), det_smul, mul_one, MonoidHom.map_one]

Determinant of Zero Endomorphism: $\det(0) = 0^{\dim M}$

Informal description

Let $A$ be a commutative ring and $M$ be a free $A$-module of finite rank. The determinant of the zero endomorphism $0 : M \to M$ is equal to $0$ raised to the power of the rank of $M$ as an $A$-module, i.e., \[ \det(0) = 0^{\dim M}. \]

LinearMap.det_eq_one_of_not_module_finite theorem

(h : ¬Module.Finite R M) (f : M →ₗ[R] M) : f.det = 1

Full source

theorem det_eq_one_of_not_module_finite (h : ¬Module.Finite R M) (f : M →ₗ[R] M) : f.det = 1 := by
  rw [LinearMap.det, dif_neg, MonoidHom.one_apply]
  exact fun ⟨_, ⟨b⟩⟩ ↦ h (Module.Finite.of_basis b)

Determinant is One for Non-Finitely Generated Modules

Informal description

If an $R$-module $M$ is not finitely generated, then the determinant of any linear endomorphism $f \colon M \to M$ is equal to $1$.

LinearMap.det_eq_one_of_subsingleton theorem

[Subsingleton M] (f : M →ₗ[R] M) : LinearMap.det (f : M →ₗ[R] M) = 1

Full source

theorem det_eq_one_of_subsingleton [Subsingleton M] (f : M →ₗ[R] M) :
    LinearMap.det (f : M →ₗ[R] M) = 1 := by
  have b : Basis (Fin 0) R M := Basis.empty M
  rw [← f.det_toMatrix b]
  exact Matrix.det_isEmpty

Determinant is One for Subsingleton Modules

Informal description

For any $R$-module $M$ that is a subsingleton (i.e., has at most one element) and any linear endomorphism $f \colon M \to M$, the determinant of $f$ is equal to $1$.

LinearMap.det_eq_one_of_finrank_eq_zero theorem

 {𝕜 : Type*} [Field 𝕜] {M : Type*} [AddCommGroup M] [Module 𝕜 M] (h : Module.finrank 𝕜 M = 0) (f : M →ₗ[𝕜] M) :
  LinearMap.det (f : M →ₗ[𝕜] M) = 1

Full source

theorem det_eq_one_of_finrank_eq_zero {𝕜 : Type*} [Field 𝕜] {M : Type*} [AddCommGroup M]
    [Module 𝕜 M] (h : Module.finrank 𝕜 M = 0) (f : M →ₗ[𝕜] M) :
    LinearMap.det (f : M →ₗ[𝕜] M) = 1 := by
  classical
    refine @LinearMap.det_cases M _ 𝕜 _ _ _ (fun t => t = 1) f ?_ rfl
    intro s b
    have : IsEmpty s := by
      rw [← Fintype.card_eq_zero_iff]
      exact (Module.finrank_eq_card_basis b).symm.trans h
    exact Matrix.det_isEmpty

Determinant is One for Zero-Dimensional Vector Spaces

Informal description

Let $M$ be a vector space over a field $\mathbb{K}$ with finite rank zero. Then for any linear endomorphism $f \colon M \to M$, the determinant of $f$ is equal to $1$.

LinearMap.det_conj theorem

 {N : Type*} [AddCommGroup N] [Module A N] (f : M →ₗ[A] M) (e : M ≃ₗ[A] N) :
  LinearMap.det ((e : M →ₗ[A] N) ∘ₗ f ∘ₗ (e.symm : N →ₗ[A] M)) = LinearMap.det f

Full source

/-- Conjugating a linear map by a linear equiv does not change its determinant. -/
@[simp]
theorem det_conj {N : Type*} [AddCommGroup N] [Module A N] (f : M →ₗ[A] M) (e : M ≃ₗ[A] N) :
    LinearMap.det ((e : M →ₗ[A] N) ∘ₗ f ∘ₗ (e.symm : N →ₗ[A] M)) = LinearMap.det f := by
  classical
    by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)
    · rcases H with ⟨s, ⟨b⟩⟩
      rw [← det_toMatrix b f, ← det_toMatrix (b.map e), toMatrix_comp (b.map e) b (b.map e),
        toMatrix_comp (b.map e) b b, ← Matrix.mul_assoc, Matrix.det_conj_of_mul_eq_one]
      · rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
      · rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
    · have H' : ¬∃ t : Finset N, Nonempty (Basis t A N) := by
        contrapose! H
        rcases H with ⟨s, ⟨b⟩⟩
        exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩
      simp only [coe_det, H, H', MonoidHom.one_apply, dif_neg, not_false_eq_true]

Determinant Invariance under Linear Conjugation: $\det(e \circ f \circ e^{-1}) = \det(f)$

Informal description

Let $A$ be a commutative ring, and let $M$ and $N$ be $A$-modules. For any linear endomorphism $f \colon M \to M$ and any linear equivalence $e \colon M \simeq_A N$, the determinant of the conjugated endomorphism $e \circ f \circ e^{-1} \colon N \to N$ is equal to the determinant of $f$.

LinearMap.isUnit_det theorem

{A : Type*} [CommRing A] [Module A M] (f : M →ₗ[A] M) (hf : IsUnit f) : IsUnit (LinearMap.det f)

Full source

/-- If a linear map is invertible, so is its determinant. -/
theorem isUnit_det {A : Type*} [CommRing A] [Module A M] (f : M →ₗ[A] M) (hf : IsUnit f) :
    IsUnit (LinearMap.det f) := by
  obtain ⟨g, hg⟩ : ∃ g, f.comp g = 1 := hf.exists_right_inv
  have : LinearMap.det f * LinearMap.det g = 1 := by
    simp only [← LinearMap.det_comp, hg, MonoidHom.map_one]
  exact isUnit_of_mul_eq_one _ _ this

Invertibility of Determinant for Invertible Linear Maps

Informal description

Let $A$ be a commutative ring and $M$ an $A$-module. For any linear endomorphism $f \colon M \to M$, if $f$ is invertible (i.e., $f$ is a unit in the endomorphism ring), then its determinant $\det(f)$ is also a unit in $A$.

LinearMap.finiteDimensional_of_det_ne_one theorem

 {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] (f : M →ₗ[𝕜] M) (hf : LinearMap.det f ≠ 1) : FiniteDimensional 𝕜 M

Full source

/-- If a linear map has determinant different from `1`, then the space is finite-dimensional. -/
theorem finiteDimensional_of_det_ne_one {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] (f : M →ₗ[𝕜] M)
    (hf : LinearMap.detLinearMap.det f ≠ 1) : FiniteDimensional 𝕜 M := by
  by_cases H : ∃ s : Finset M, Nonempty (Basis s 𝕜 M)
  · rcases H with ⟨s, ⟨hs⟩⟩
    exact FiniteDimensional.of_fintype_basis hs
  · classical simp [LinearMap.coe_det, H] at hf

Finite-dimensionality from non-unity determinant of a linear endomorphism

Informal description

Let $M$ be a vector space over a field $\mathbb{K}$. If there exists a linear endomorphism $f \colon M \to M$ whose determinant is not equal to $1$, then $M$ is finite-dimensional over $\mathbb{K}$.

LinearMap.range_lt_top_of_det_eq_zero theorem

{𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] {f : M →ₗ[𝕜] M} (hf : LinearMap.det f = 0) : LinearMap.range f < ⊤

Full source

/-- If the determinant of a map vanishes, then the map is not onto. -/
theorem range_lt_top_of_det_eq_zero {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] {f : M →ₗ[𝕜] M}
    (hf : LinearMap.det f = 0) : LinearMap.range f < ⊤ := by
  have : FiniteDimensional 𝕜 M := by simp [f.finiteDimensional_of_det_ne_one, hf]
  contrapose hf
  simp only [lt_top_iff_ne_top, Classical.not_not, ← isUnit_iff_range_eq_top] at hf
  exact isUnit_iff_ne_zero.1 (f.isUnit_det hf)

Non-surjectivity of Linear Endomorphisms with Zero Determinant

Informal description

Let $\mathbb{K}$ be a field and $M$ a vector space over $\mathbb{K}$. For any linear endomorphism $f \colon M \to M$ with determinant $\det(f) = 0$, the range of $f$ is a proper subspace of $M$, i.e., $\text{range}(f) \subsetneq M$.

LinearMap.bot_lt_ker_of_det_eq_zero theorem

{𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] {f : M →ₗ[𝕜] M} (hf : LinearMap.det f = 0) : ⊥ < LinearMap.ker f

Full source

/-- If the determinant of a map vanishes, then the map is not injective. -/
theorem bot_lt_ker_of_det_eq_zero {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] {f : M →ₗ[𝕜] M}
    (hf : LinearMap.det f = 0) : ⊥ < LinearMap.ker f := by
  have : FiniteDimensional 𝕜 M := by simp [f.finiteDimensional_of_det_ne_one, hf]
  contrapose hf
  simp only [bot_lt_iff_ne_bot, Classical.not_not, ← isUnit_iff_ker_eq_bot] at hf
  exact isUnit_iff_ne_zero.1 (f.isUnit_det hf)

Nontrivial Kernel from Zero Determinant of a Linear Endomorphism

Informal description

Let $M$ be a vector space over a field $\mathbb{K}$ and $f \colon M \to M$ a linear endomorphism. If the determinant of $f$ is zero, then the kernel of $f$ is nontrivial, i.e., there exists a nonzero vector $v \in M$ such that $f(v) = 0$.

LinearMap.det_ring theorem

(f : R →ₗ[R] R) : f.det = f 1

Full source

/-- When the function is over the base ring, the determinant is the evaluation at `1`. -/
@[simp] lemma det_ring (f : R →ₗ[R] R) : f.det = f 1 := by
  simp [← det_toMatrix (Basis.singleton Unit R)]

Determinant of Linear Endomorphism over Base Ring Evaluates at Identity

Informal description

For any linear endomorphism $f \colon R \to R$ over a commutative ring $R$, the determinant of $f$ is equal to the evaluation of $f$ at the multiplicative identity $1 \in R$, i.e., $\det(f) = f(1)$.

LinearMap.det_mulLeft theorem

(a : R) : (mulLeft R a).det = a

Full source

lemma det_mulLeft (a : R) : (mulLeft R a).det = a := by simp

Determinant of Left Multiplication by $a$: $\det(x \mapsto a \cdot x) = a$

Informal description

For any element $a$ in a commutative ring $R$, the determinant of the left multiplication map $x \mapsto a \cdot x$ on $R$ is equal to $a$, i.e., $\det(\text{mulLeft}_R(a)) = a$.

LinearMap.det_mulRight theorem

(a : R) : (mulRight R a).det = a

Full source

lemma det_mulRight (a : R) : (mulRight R a).det = a := by simp

Determinant of Right Multiplication Map: $\det(\mathrm{mulRight}_R(a)) = a$

Informal description

For any element $a$ in a commutative ring $R$, the determinant of the right multiplication map $\mathrm{mulRight}_R(a) : R \to R$ (defined by $x \mapsto x \cdot a$) is equal to $a$, i.e., \[ \det(\mathrm{mulRight}_R(a)) = a. \]

LinearMap.det_prodMap theorem

 [Module.Free R M] [Module.Free R M'] [Module.Finite R M] [Module.Finite R M'] (f : Module.End R M)
  (f' : Module.End R M') : (prodMap f f').det = f.det * f'.det

Full source

theorem det_prodMap [Module.Free R M] [Module.Free R M'] [Module.Finite R M] [Module.Finite R M']
    (f : Module.End R M) (f' : Module.End R M') :
    (prodMap f f').det = f.det * f'.det := by
  let b := Module.Free.chooseBasis R M
  let b' := Module.Free.chooseBasis R M'
  rw [← det_toMatrix (b.prod b'), ← det_toMatrix b, ← det_toMatrix b', toMatrix_prodMap,
    det_fromBlocks_zero₂₁, det_toMatrix]

Determinant of Product Map: $\det(f \times f') = \det(f) \cdot \det(f')$

Informal description

Let $R$ be a commutative ring, and let $M$ and $M'$ be finitely generated free $R$-modules. For any $R$-linear endomorphisms $f \colon M \to M$ and $f' \colon M' \to M'$, the determinant of the product map $f \times f' \colon M \times M' \to M \times M'$ is equal to the product of the determinants of $f$ and $f'$, i.e., \[ \det(f \times f') = \det(f) \cdot \det(f'). \]

LinearMap.det_pi theorem

 [Module.Free R M] [Module.Finite R M] (f : ι → M →ₗ[R] M) :
  (LinearMap.pi (fun i ↦ (f i).comp (LinearMap.proj i))).det = ∏ i, (f i).det

Full source

theorem det_pi [Module.Free R M] [Module.Finite R M] (f : ι → M →ₗ[R] M) :
    (LinearMap.pi (fun i ↦ (f i).comp (LinearMap.proj i))).det = ∏ i, (f i).det := by
  classical
  let b := Module.Free.chooseBasis R M
  let B := (Pi.basis (fun _ : ι ↦ b)).reindex <|
    (Equiv.sigmaEquivProd _ _).trans (Equiv.prodComm _ _)
  simp_rw [← LinearMap.det_toMatrix B, ← LinearMap.det_toMatrix b]
  have : ((LinearMap.toMatrix B B) (LinearMap.pi fun i ↦ f i ∘ₗ LinearMap.proj i)) =
      Matrix.blockDiagonal (fun i ↦ LinearMap.toMatrix b b (f i)) := by
    ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
    unfold B
    simp_rw [LinearMap.toMatrix_apply', Matrix.blockDiagonal_apply, Basis.coe_reindex,
      Function.comp_apply, Basis.repr_reindex_apply, Equiv.symm_trans_apply, Equiv.prodComm_symm,
      Equiv.prodComm_apply, Equiv.sigmaEquivProd_symm_apply, Prod.swap_prod_mk, Pi.basis_apply,
      Pi.basis_repr, LinearMap.pi_apply, LinearMap.coe_comp, Function.comp_apply,
      LinearMap.toMatrix_apply', LinearMap.coe_proj, Function.eval, Pi.single_apply]
    split_ifs with h
    · rw [h]
    · simp only [map_zero, Finsupp.coe_zero, Pi.zero_apply]
  rw [this, Matrix.det_blockDiagonal]

Determinant of Product Map Equals Product of Determinants

Informal description

Let $R$ be a commutative ring and $M$ be a free and finitely generated $R$-module. Given a family of $R$-linear endomorphisms $f_i : M \to M$ for each $i$ in a finite index set $\iota$, the determinant of the linear map $\mathrm{pi}(f)$ (which maps $(x_i)_{i \in \iota}$ to $(f_i(x_i))_{i \in \iota}$) is equal to the product of the determinants of the individual $f_i$: \[ \det(\mathrm{pi}(f)) = \prod_{i \in \iota} \det(f_i). \]

LinearEquiv.det definition

: (M ≃ₗ[R] M) →* Rˣ

Full source

/-- On a `LinearEquiv`, the domain of `LinearMap.det` can be promoted to `Rˣ`. -/
protected def det : (M ≃ₗ[R] M) →* Rˣ :=
  (Units.map (LinearMap.det : (M →ₗ[R] M) →* R)).comp
    (LinearMap.GeneralLinearGroup.generalLinearEquiv R M).symm.toMonoidHom

Determinant of a linear automorphism as a multiplicative homomorphism

Informal description

The determinant of a linear isomorphism $ f \colon M \simeq_{R} M $ is a multiplicative homomorphism from the group of linear automorphisms of $ M $ to the group of units $ R^\times $ of the commutative ring $ R $. It is defined as the composition of the determinant homomorphism for linear endomorphisms with the inverse of the multiplicative equivalence between the general linear group and the group of linear automorphisms.

LinearEquiv.coe_det theorem

(f : M ≃ₗ[R] M) : ↑(LinearEquiv.det f) = LinearMap.det (f : M →ₗ[R] M)

Full source

@[simp]
theorem coe_det (f : M ≃ₗ[R] M) : ↑(LinearEquiv.det f) = LinearMap.det (f : M →ₗ[R] M) :=
  rfl

Determinant of a Linear Automorphism Equals Determinant as a Linear Map

Informal description

For any linear automorphism $ f \colon M \simeq_{R} M $ over a commutative ring $ R $, the image of the determinant of $ f $ under the canonical inclusion $ R^\times \hookrightarrow R $ is equal to the determinant of $ f $ viewed as a linear endomorphism $ M \to M $. In other words, $ \text{det}(f) = \text{det}(f \text{ as a linear map}) $.

LinearEquiv.coe_inv_det theorem

(f : M ≃ₗ[R] M) : ↑(LinearEquiv.det f)⁻¹ = LinearMap.det (f.symm : M →ₗ[R] M)

Full source

@[simp]
theorem coe_inv_det (f : M ≃ₗ[R] M) : ↑(LinearEquiv.det f)⁻¹ = LinearMap.det (f.symm : M →ₗ[R] M) :=
  rfl

Inverse Determinant of a Linear Automorphism Equals Determinant of its Inverse

Informal description

For any linear automorphism $f \colon M \simeq_{R} M$ over a commutative ring $R$, the inverse of the determinant of $f$ (as an element of the group of units $R^\times$) is equal to the determinant of the inverse automorphism $f^{-1} \colon M \to M$.

LinearEquiv.det_refl theorem

: LinearEquiv.det (LinearEquiv.refl R M) = 1

Full source

@[simp]
theorem det_refl : LinearEquiv.det (LinearEquiv.refl R M) = 1 :=
  Units.ext <| LinearMap.det_id

Determinant of the Identity Automorphism: $\det(\text{id}) = 1$

Informal description

The determinant of the identity linear automorphism $\text{refl}_R M \colon M \simeq_R M$ is equal to the multiplicative identity $1$ in the group of units $R^\times$ of the commutative ring $R$.

LinearEquiv.det_trans theorem

(f g : M ≃ₗ[R] M) : LinearEquiv.det (f.trans g) = LinearEquiv.det g * LinearEquiv.det f

Full source

@[simp]
theorem det_trans (f g : M ≃ₗ[R] M) :
    LinearEquiv.det (f.trans g) = LinearEquiv.det g * LinearEquiv.det f :=
  map_mul _ g f

Multiplicativity of Determinant for Linear Automorphisms: $\det(f \circ g) = \det(g) \det(f)$

Informal description

For any linear automorphisms $f, g \colon M \simeq_R M$ of an $R$-module $M$, the determinant of the composition $f \circ g$ satisfies \[ \det(f \circ g) = \det(g) \cdot \det(f). \]

LinearEquiv.det_symm theorem

(f : M ≃ₗ[R] M) : LinearEquiv.det f.symm = LinearEquiv.det f⁻¹

Full source

@[simp]
theorem det_symm (f : M ≃ₗ[R] M) : LinearEquiv.det f.symm = LinearEquiv.det f⁻¹ :=
  map_inv _ f

Determinant of Inverse Linear Automorphism: $\det(f^{-1}) = (\det f)^{-1}$

Informal description

For any linear automorphism $f \colon M \simeq_R M$ of an $R$-module $M$, the determinant of the inverse automorphism $f^{-1}$ is equal to the multiplicative inverse of the determinant of $f$, i.e., \[ \det(f^{-1}) = (\det f)^{-1}. \]

LinearEquiv.det_conj theorem

(f : M ≃ₗ[R] M) (e : M ≃ₗ[R] M') : LinearEquiv.det ((e.symm.trans f).trans e) = LinearEquiv.det f

Full source

/-- Conjugating a linear equiv by a linear equiv does not change its determinant. -/
@[simp]
theorem det_conj (f : M ≃ₗ[R] M) (e : M ≃ₗ[R] M') :
    LinearEquiv.det ((e.symm.trans f).trans e) = LinearEquiv.det f := by
  rw [← Units.eq_iff, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]

Invariance of Determinant under Linear Conjugation: $\det(e^{-1} \circ f \circ e) = \det(f)$

Informal description

Let $R$ be a commutative ring, and let $M$ and $M'$ be $R$-modules. For any linear automorphism $f \colon M \simeq_R M$ and any linear equivalence $e \colon M \simeq_R M'$, the determinant of the conjugated automorphism $e^{-1} \circ f \circ e \colon M' \simeq_R M'$ is equal to the determinant of $f$, i.e., \[ \det(e^{-1} \circ f \circ e) = \det(f). \]

LinearEquiv.det_mul_det_symm theorem

 {A : Type*} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) :
  LinearMap.det (f : M →ₗ[A] M) * LinearMap.det (f.symm : M →ₗ[A] M) = 1

Full source

/-- The determinants of a `LinearEquiv` and its inverse multiply to 1. -/
@[simp]
theorem LinearEquiv.det_mul_det_symm {A : Type*} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) :
    LinearMap.det (f : M →ₗ[A] M) * LinearMap.det (f.symm : M →ₗ[A] M) = 1 := by
  simp [← LinearMap.det_comp]

Product of Determinants of a Linear Isomorphism and Its Inverse is One

Informal description

Let $A$ be a commutative ring and $M$ an $A$-module. For any linear isomorphism $f \colon M \simeq_A M$, the product of the determinants of $f$ and its inverse $f^{-1}$ is equal to $1$, i.e., \[ \det(f) \cdot \det(f^{-1}) = 1. \]

LinearEquiv.det_symm_mul_det theorem

 {A : Type*} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) :
  LinearMap.det (f.symm : M →ₗ[A] M) * LinearMap.det (f : M →ₗ[A] M) = 1

Full source

/-- The determinants of a `LinearEquiv` and its inverse multiply to 1. -/
@[simp]
theorem LinearEquiv.det_symm_mul_det {A : Type*} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) :
    LinearMap.det (f.symm : M →ₗ[A] M) * LinearMap.det (f : M →ₗ[A] M) = 1 := by
  simp [← LinearMap.det_comp]

Product of Determinants of a Linear Isomorphism and Its Inverse is One

Informal description

For any linear isomorphism $ f \colon M \simeq_A M $ of modules over a commutative ring $ A $, the product of the determinants of $ f $ and its inverse $ f^{-1} $ is equal to $ 1 $, i.e., \[ \det(f^{-1}) \cdot \det(f) = 1. \]

LinearEquiv.isUnit_det theorem

(f : M ≃ₗ[R] M') (v : Basis ι R M) (v' : Basis ι R M') : IsUnit (LinearMap.toMatrix v v' f).det

Full source

theorem LinearEquiv.isUnit_det (f : M ≃ₗ[R] M') (v : Basis ι R M) (v' : Basis ι R M') :
    IsUnit (LinearMap.toMatrix v v' f).det := by
  apply isUnit_det_of_left_inverse
  simpa using (LinearMap.toMatrix_comp v v' v f.symm f).symm

Determinant of a Linear Isomorphism's Matrix is a Unit

Informal description

Let $R$ be a commutative ring, and let $M$ and $M'$ be $R$-modules with bases $v$ and $v'$ indexed by a finite type $\iota$, respectively. For any linear isomorphism $f \colon M \simeq_R M'$, the determinant of the matrix representation of $f$ with respect to the bases $v$ and $v'$ is a unit in $R$.

LinearEquiv.isUnit_det' theorem

{A : Type*} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) : IsUnit (LinearMap.det (f : M →ₗ[A] M))

Full source

/-- Specialization of `LinearEquiv.isUnit_det` -/
theorem LinearEquiv.isUnit_det' {A : Type*} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) :
    IsUnit (LinearMap.det (f : M →ₗ[A] M)) :=
  isUnit_of_mul_eq_one _ _ f.det_mul_det_symm

Determinant of a Linear Isomorphism is a Unit

Informal description

Let $A$ be a commutative ring and $M$ an $A$-module. For any linear isomorphism $f \colon M \simeq_A M$, the determinant of $f$ is a unit in $A$.

LinearEquiv.det_coe_symm theorem

 {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] (f : M ≃ₗ[𝕜] M) :
  LinearMap.det (f.symm : M →ₗ[𝕜] M) = (LinearMap.det (f : M →ₗ[𝕜] M))⁻¹

Full source

/-- The determinant of `f.symm` is the inverse of that of `f` when `f` is a linear equiv. -/
theorem LinearEquiv.det_coe_symm {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] (f : M ≃ₗ[𝕜] M) :
    LinearMap.det (f.symm : M →ₗ[𝕜] M) = (LinearMap.det (f : M →ₗ[𝕜] M))⁻¹ := by
  field_simp [IsUnit.ne_zero f.isUnit_det']

Inverse Determinant Formula for Linear Isomorphisms: $\det(f^{-1}) = (\det f)^{-1}$

Informal description

Let $\mathbb{K}$ be a field and $M$ a $\mathbb{K}$-module. For any linear isomorphism $f \colon M \simeq_{\mathbb{K}} M$, the determinant of its inverse $f^{-1}$ is equal to the multiplicative inverse of the determinant of $f$, i.e., \[ \det(f^{-1}) = (\det f)^{-1}. \]

LinearEquiv.ofIsUnitDet definition

 {f : M →ₗ[R] M'} {v : Basis ι R M} {v' : Basis ι R M'} (h : IsUnit (LinearMap.toMatrix v v' f).det) : M ≃ₗ[R] M'

Full source

/-- Builds a linear equivalence from a linear map whose determinant in some bases is a unit. -/
@[simps]
def LinearEquiv.ofIsUnitDet {f : M →ₗ[R] M'} {v : Basis ι R M} {v' : Basis ι R M'}
    (h : IsUnit (LinearMap.toMatrix v v' f).det) : M ≃ₗ[R] M' where
  toFun := f
  map_add' := f.map_add
  map_smul' := f.map_smul
  invFun := toLin v' v (toMatrix v v' f)⁻¹
  left_inv x :=
    calc toLintoLin v' v (toMatrix v v' f)⁻¹ (f x)
      _ = toLin v v ((toMatrix v v' f)⁻¹ * toMatrix v v' f) x := by
        rw [toLin_mul v v' v, toLin_toMatrix, LinearMap.comp_apply]
      _ = x := by simp [h]
  right_inv x :=
    calc f (toLin v' v (toMatrix v v' f)⁻¹ x)
      _ = toLin v' v' (toMatrix v v' f * (toMatrix v v' f)⁻¹) x := by
        rw [toLin_mul v' v v', LinearMap.comp_apply, toLin_toMatrix v v']
      _ = x := by simp [h]

Linear equivalence from linear map with unit determinant matrix

Informal description

Given a commutative ring $R$, $R$-modules $M$ and $M'$, bases $v$ and $v'$ for $M$ and $M'$ respectively indexed by a finite type $\iota$, and a linear map $f: M \to M'$ such that the determinant of its matrix representation with respect to $v$ and $v'$ is a unit in $R$, the function constructs a linear equivalence between $M$ and $M'$ whose underlying linear map is $f$.

LinearEquiv.coe_ofIsUnitDet theorem

 {f : M →ₗ[R] M'} {v : Basis ι R M} {v' : Basis ι R M'} (h : IsUnit (LinearMap.toMatrix v v' f).det) :
  (LinearEquiv.ofIsUnitDet h : M →ₗ[R] M') = f

Full source

@[simp]
theorem LinearEquiv.coe_ofIsUnitDet {f : M →ₗ[R] M'} {v : Basis ι R M} {v' : Basis ι R M'}
    (h : IsUnit (LinearMap.toMatrix v v' f).det) :
    (LinearEquiv.ofIsUnitDet h : M →ₗ[R] M') = f := by
  ext x
  rfl

Underlying linear map of $\text{LinearEquiv.ofIsUnitDet}$ equals original map

Informal description

Let $R$ be a commutative ring, $M$ and $M'$ be $R$-modules with bases $v$ and $v'$ respectively indexed by a finite type $\iota$, and $f: M \to M'$ be a linear map. If the determinant of the matrix representation of $f$ with respect to $v$ and $v'$ is a unit in $R$, then the underlying linear map of the linear equivalence $\text{LinearEquiv.ofIsUnitDet}\, h$ is equal to $f$.

LinearMap.equivOfDetNeZero abbrev

 {𝕜 : Type*} [Field 𝕜] {M : Type*} [AddCommGroup M] [Module 𝕜 M] [FiniteDimensional 𝕜 M] (f : M →ₗ[𝕜] M)
  (hf : LinearMap.det f ≠ 0) : M ≃ₗ[𝕜] M

Full source

/-- Builds a linear equivalence from a linear map on a finite-dimensional vector space whose
determinant is nonzero. -/
abbrev LinearMap.equivOfDetNeZero {𝕜 : Type*} [Field 𝕜] {M : Type*} [AddCommGroup M] [Module 𝕜 M]
    [FiniteDimensional 𝕜 M] (f : M →ₗ[𝕜] M) (hf : LinearMap.detLinearMap.det f ≠ 0) : M ≃ₗ[𝕜] M :=
  have : IsUnit (LinearMap.toMatrix (Module.finBasis 𝕜 M)
      (Module.finBasis 𝕜 M) f).det := by
    rw [LinearMap.det_toMatrix]
    exact isUnit_iff_ne_zero.2 hf
  LinearEquiv.ofIsUnitDet this

Linear isomorphism from endomorphism with nonzero determinant

Informal description

Let $\mathbb{K}$ be a field and $M$ be a finite-dimensional vector space over $\mathbb{K}$. For any linear endomorphism $f: M \to M$ with nonzero determinant, there exists a linear equivalence (isomorphism) between $M$ and itself whose underlying linear map is $f$.

LinearMap.associated_det_of_eq_comp theorem

 (e : M ≃ₗ[R] M) (f f' : M →ₗ[R] M) (h : ∀ x, f x = f' (e x)) : Associated (LinearMap.det f) (LinearMap.det f')

Full source

theorem LinearMap.associated_det_of_eq_comp (e : M ≃ₗ[R] M) (f f' : M →ₗ[R] M)
    (h : ∀ x, f x = f' (e x)) : Associated (LinearMap.det f) (LinearMap.det f') := by
  suffices Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f') by
    convert this using 2
    ext x
    exact h x
  rw [← mul_one (LinearMap.det f'), LinearMap.det_comp]
  exact Associated.mul_left _ (associated_one_iff_isUnit.mpr e.isUnit_det')

Determinants of Conjugate Endomorphisms are Associated

Informal description

Let $R$ be a commutative ring and $M$ an $R$-module. Given a linear isomorphism $e \colon M \simeq_R M$ and two linear endomorphisms $f, f' \colon M \to M$ such that $f(x) = f'(e(x))$ for all $x \in M$, the determinants of $f$ and $f'$ are associated elements in $R$ (i.e., they differ by multiplication by a unit).

LinearMap.associated_det_comp_equiv theorem

 {N : Type*} [AddCommGroup N] [Module R N] (f : N →ₗ[R] M) (e e' : M ≃ₗ[R] N) :
  Associated (LinearMap.det (f ∘ₗ ↑e)) (LinearMap.det (f ∘ₗ ↑e'))

Full source

theorem LinearMap.associated_det_comp_equiv {N : Type*} [AddCommGroup N] [Module R N]
    (f : N →ₗ[R] M) (e e' : M ≃ₗ[R] N) :
    Associated (LinearMap.det (f ∘ₗ ↑e)) (LinearMap.det (f ∘ₗ ↑e')) := by
  refine LinearMap.associated_det_of_eq_comp (e.trans e'.symm) _ _ ?_
  intro x
  simp only [LinearMap.comp_apply, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
    LinearEquiv.apply_symm_apply]

Determinants of Linear Maps Composed with Equivalent Isomorphisms are Associated

Informal description

Let $R$ be a commutative ring, and let $M$ and $N$ be $R$-modules with $N$ an additive commutative group. Given a linear map $f \colon N \to M$ and two linear isomorphisms $e, e' \colon M \simeq_R N$, the determinants of the compositions $f \circ e$ and $f \circ e'$ are associated elements in $R$ (i.e., they differ by multiplication by a unit).

Basis.det definition

: M [⋀^ι]→ₗ[R] R

Full source

/-- The determinant of a family of vectors with respect to some basis, as an alternating
multilinear map. -/
nonrec def Basis.det : M [⋀^ι]→ₗ[R] R where
  toMultilinearMap :=
    MultilinearMap.mk' (fun v ↦ det (e.toMatrix v))
      (fun v i x y ↦ by
        simp only [e.toMatrix_update, map_add, Finsupp.coe_add, det_updateCol_add])
      (fun u i c x ↦ by
        simp only [e.toMatrix_update, Algebra.id.smul_eq_mul, LinearEquiv.map_smul]
        apply det_updateCol_smul)
  map_eq_zero_of_eq' := by
    intro v i j h hij
    dsimp
    rw [← Function.update_eq_self i v, h, ← det_transpose, e.toMatrix_update, ← updateRow_transpose,
      ← e.toMatrix_transpose_apply]
    apply det_zero_of_row_eq hij
    rw [updateRow_ne hij.symm, updateRow_self]

Determinant of a family of vectors with respect to a basis

Informal description

Given a basis $ e $ of a module $ M $ over a commutative ring $ R $ indexed by a finite type $ \iota $, the determinant $ \text{Basis.det } e $ is an alternating multilinear map from $ \iota \to M $ to $ R $. For any family of vectors $ v : \iota \to M $, the determinant $ \text{Basis.det } e \ v $ is equal to the determinant of the matrix whose columns are the coordinates of the vectors $ v $ with respect to the basis $ e $.

Basis.det_apply theorem

(v : ι → M) : e.det v = Matrix.det (e.toMatrix v)

Full source

theorem Basis.det_apply (v : ι → M) : e.det v = Matrix.det (e.toMatrix v) :=
  rfl

Determinant of a Vector Family via Basis Coordinates

Informal description

Let $R$ be a commutative ring, $M$ be an $R$-module, and $\iota$ be a finite indexing type. Given a basis $e$ of $M$ indexed by $\iota$ and a family of vectors $v : \iota \to M$, the determinant of $v$ with respect to $e$ equals the determinant of the matrix whose columns are the coordinates of $v$ in the basis $e$. That is, \[ \det_e(v) = \det(e^{-1}v) \] where $e^{-1}v$ denotes the matrix representation of $v$ in the basis $e$.

Basis.det_self theorem

: e.det e = 1

Full source

theorem Basis.det_self : e.det e = 1 := by simp [e.det_apply]

Determinant of Basis Vectors with Respect to Themselves is One

Informal description

Given a basis $e$ of a finite-dimensional module $M$ over a commutative ring $R$, the determinant of the basis vectors with respect to themselves is equal to $1$, i.e., $\det(e) = 1$.

Basis.det_isEmpty theorem

[IsEmpty ι] : e.det = AlternatingMap.constOfIsEmpty R M ι 1

Full source

@[simp]
theorem Basis.det_isEmpty [IsEmpty ι] : e.det = AlternatingMap.constOfIsEmpty R M ι 1 := by
  ext v
  exact Matrix.det_isEmpty

Determinant of Basis with Empty Index Type is Constant One

Informal description

For any basis $e$ of a module $M$ over a commutative ring $R$ indexed by an empty type $\iota$, the determinant of $e$ is equal to the constant alternating map that sends every element of the empty function space $\iota \to M$ to $1 \in R$.

Basis.det_ne_zero theorem

[Nontrivial R] : e.det ≠ 0

Full source

/-- `Basis.det` is not the zero map. -/
theorem Basis.det_ne_zero [Nontrivial R] : e.det ≠ 0 := fun h => by simpa [h] using e.det_self

Nonvanishing of the Determinant Map for a Basis

Informal description

For a nontrivial commutative ring $R$ and a basis $e$ of a finite-dimensional module $M$ over $R$, the determinant map $\det(e)$ is not identically zero.

Basis.smul_det theorem

 {G} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) (v : ι → M) : (g • e).det v = e.det (g⁻¹ • v)

Full source

theorem Basis.smul_det {G} [Group G] [DistribMulAction G M] [SMulCommClass G R M]
    (g : G) (v : ι → M) :
    (g • e).det v = e.det (g⁻¹ • v) := by
  simp_rw [det_apply, toMatrix_smul_left]

Determinant Transformation under Basis Scaling by a Group Action

Informal description

Let $G$ be a group acting distributively on an $R$-module $M$ with scalar multiplication commuting with the $R$-action. For any basis $e$ of $M$ indexed by a finite type $\iota$, any group element $g \in G$, and any family of vectors $v \colon \iota \to M$, the determinant of the family $v$ with respect to the scaled basis $g \cdot e$ is equal to the determinant of the family $g^{-1} \cdot v$ with respect to the original basis $e$. In symbols: \[ \text{det}(g \cdot e)(v) = \text{det}(e)(g^{-1} \cdot v). \]

is_basis_iff_det theorem

{v : ι → M} : LinearIndependent R v ∧ span R (Set.range v) = ⊤ ↔ IsUnit (e.det v)

Full source

theorem is_basis_iff_det {v : ι → M} :
    LinearIndependentLinearIndependent R v ∧ span R (Set.range v) = ⊤LinearIndependent R v ∧ span R (Set.range v) = ⊤ ↔ IsUnit (e.det v) := by
  constructor
  · rintro ⟨hli, hspan⟩
    set v' := Basis.mk hli hspan.ge
    rw [e.det_apply]
    convert LinearEquiv.isUnit_det (LinearEquiv.refl R M) v' e using 2
    ext i j
    simp [v']
  · intro h
    rw [Basis.det_apply, Basis.toMatrix_eq_toMatrix_constr] at h
    set v' := Basis.map e (LinearEquiv.ofIsUnitDet h) with v'_def
    have : ⇑v' = v := by
      ext i
      rw [v'_def, Basis.map_apply, LinearEquiv.ofIsUnitDet_apply, e.constr_basis]
    rw [← this]
    exact ⟨v'.linearIndependent, v'.span_eq⟩

Basis Criterion via Determinant: $\text{span}(v) = M \text{ and } v \text{ linearly independent} \iff \det_e(v) \text{ is a unit}$

Informal description

Let $R$ be a commutative ring, $M$ be an $R$-module with a basis $e$ indexed by a finite type $\iota$, and $v : \iota \to M$ be a family of vectors. Then $v$ forms a basis of $M$ if and only if the determinant of $v$ with respect to $e$ is a unit in $R$. In other words: \[ \text{$v$ is linearly independent and spans $M$} \iff \det_e(v) \text{ is a unit in } R. \]

Basis.isUnit_det theorem

(e' : Basis ι R M) : IsUnit (e.det e')

Full source

theorem Basis.isUnit_det (e' : Basis ι R M) : IsUnit (e.det e') :=
  (is_basis_iff_det e).mp ⟨e'.linearIndependent, e'.span_eq⟩

Determinant of a Basis Change is a Unit

Informal description

Let $R$ be a commutative ring and $M$ be a finite-dimensional $R$-module with two bases $e$ and $e'$ indexed by a finite type $\iota$. Then the determinant of the basis $e'$ with respect to $e$ is a unit in $R$.

AlternatingMap.map_basis_eq_zero_iff theorem

{ι : Type*} [Finite ι] (e : Basis ι R M) (f : M [⋀^ι]→ₗ[R] R) : f e = 0 ↔ f = 0

Full source

@[simp]
theorem AlternatingMap.map_basis_eq_zero_iff {ι : Type*} [Finite ι] (e : Basis ι R M)
    (f : M [⋀^ι]→ₗ[R] R) : f e = 0 ↔ f = 0 :=
  ⟨fun h => by
    cases nonempty_fintype ι
    letI := Classical.decEq ι
    simpa [h] using f.eq_smul_basis_det e,
   fun h => h.symm ▸ AlternatingMap.zero_apply _⟩

Vanishing of Alternating Map on Basis Vectors Characterizes Zero Map

Informal description

Let $R$ be a commutative ring, $M$ a finite-dimensional $R$-module with basis $e$ indexed by a finite type $\iota$, and $f$ an $R$-linear alternating map from $\iota \to M$ to $R$. Then $f$ evaluated on the basis vectors $e$ is zero if and only if $f$ is the zero alternating map, i.e., $f(e) = 0 \leftrightarrow f = 0$.

AlternatingMap.map_basis_ne_zero_iff theorem

{ι : Type*} [Finite ι] (e : Basis ι R M) (f : M [⋀^ι]→ₗ[R] R) : f e ≠ 0 ↔ f ≠ 0

Full source

theorem AlternatingMap.map_basis_ne_zero_iff {ι : Type*} [Finite ι] (e : Basis ι R M)
    (f : M [⋀^ι]→ₗ[R] R) : f e ≠ 0f e ≠ 0 ↔ f ≠ 0 :=
  not_congr <| f.map_basis_eq_zero_iff e

Nonvanishing of Alternating Map on Basis Vectors Characterizes Nonzero Map

Informal description

Let $R$ be a commutative ring, $M$ a finite-dimensional $R$-module with basis $e$ indexed by a finite type $\iota$, and $f$ an $R$-linear alternating map from $\iota \to M$ to $R$. Then $f$ evaluated on the basis vectors $e$ is nonzero if and only if $f$ is not the zero alternating map, i.e., $f(e) \neq 0 \leftrightarrow f \neq 0$.

Basis.det_comp theorem

(e : Basis ι A M) (f : M →ₗ[A] M) (v : ι → M) : e.det (f ∘ v) = (LinearMap.det f) * e.det v

Full source

@[simp]
theorem Basis.det_comp (e : Basis ι A M) (f : M →ₗ[A] M) (v : ι → M) :
    e.det (f ∘ v) = (LinearMap.det f) * e.det v := by
  rw [Basis.det_apply, Basis.det_apply, ← f.det_toMatrix e, ← Matrix.det_mul,
    e.toMatrix_eq_toMatrix_constr (f ∘ v), e.toMatrix_eq_toMatrix_constr v, ← toMatrix_comp,
    e.constr_comp]

Determinant of Composition with Linear Endomorphism: $\det_e(f \circ v) = \det(f) \cdot \det_e(v)$

Informal description

Let $A$ be a commutative ring and $M$ be an $A$-module with a basis $e$ indexed by a finite type $\iota$. For any $A$-linear endomorphism $f \colon M \to M$ and any family of vectors $v \colon \iota \to M$, the determinant of the composed family $f \circ v$ with respect to the basis $e$ equals the product of the determinant of $f$ and the determinant of $v$ with respect to $e$. That is, \[ \det_e(f \circ v) = \det(f) \cdot \det_e(v). \]

Basis.det_comp_basis theorem

 [Module A M'] (b : Basis ι A M) (b' : Basis ι A M') (f : M →ₗ[A] M') :
  b'.det (f ∘ b) = LinearMap.det (f ∘ₗ (b'.equiv b (Equiv.refl ι) : M' →ₗ[A] M))

Full source

@[simp]
theorem Basis.det_comp_basis [Module A M'] (b : Basis ι A M) (b' : Basis ι A M') (f : M →ₗ[A] M') :
    b'.det (f ∘ b) = LinearMap.det (f ∘ₗ (b'.equiv b (Equiv.refl ι) : M' →ₗ[A] M)) := by
  rw [Basis.det_apply, ← LinearMap.det_toMatrix b', LinearMap.toMatrix_comp _ b, Matrix.det_mul,
    LinearMap.toMatrix_basis_equiv, Matrix.det_one, mul_one]
  congr 1; ext i j
  rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Function.comp_apply]

Determinant of Linear Map Composition with Basis Equivalence: $\det_{b'}(f \circ b) = \det(f \circ (b'.equiv\, b\, \text{id}_\iota))$

Informal description

Let $A$ be a commutative ring, and let $M$ and $M'$ be $A$-modules with bases $b : \iota \to M$ and $b' : \iota \to M'$ respectively. For any $A$-linear map $f : M \to M'$, the determinant of the family of vectors $(f \circ b) : \iota \to M'$ with respect to the basis $b'$ is equal to the determinant of the linear map $f \circ (b'.equiv\, b\, \text{id}_\iota) : M' \to M$, where $\text{id}_\iota$ is the identity equivalence on $\iota$. That is, \[ \det_{b'}(f \circ b) = \det(f \circ (b'.equiv\, b\, \text{id}_\iota)). \]

Basis.det_basis theorem

(b : Basis ι A M) (b' : Basis ι A M) : LinearMap.det (b'.equiv b (Equiv.refl ι)).toLinearMap = b'.det b

Full source

@[simp]
theorem Basis.det_basis (b : Basis ι A M) (b' : Basis ι A M) :
    LinearMap.det (b'.equiv b (Equiv.refl ι)).toLinearMap = b'.det b :=
  (b.det_comp_basis b' (LinearMap.id)).symm

Determinant of Basis Equivalence: $\det(b' \equiv b) = \det_{b'}(b)$

Informal description

Let $A$ be a commutative ring and $M$ be an $A$-module with two bases $b$ and $b'$ indexed by a finite type $\iota$. The determinant of the linear map induced by the basis equivalence $b' \equiv b$ (with respect to the identity equivalence on $\iota$) is equal to the determinant of the family of vectors $b$ with respect to the basis $b'$. That is, \[ \det\big((b'.equiv\, b\, \text{id}_\iota).toLinearMap\big) = \det_{b'}(b). \]

Basis.det_inv theorem

(b : Basis ι A M) (b' : Basis ι A M) : (b.isUnit_det b').unit⁻¹ = b'.det b

Full source

theorem Basis.det_inv (b : Basis ι A M) (b' : Basis ι A M) :
    (b.isUnit_det b').unit⁻¹ = b'.det b := by
  rw [← Units.mul_eq_one_iff_inv_eq, IsUnit.unit_spec, ← Basis.det_basis, ← Basis.det_basis]
  exact LinearEquiv.det_mul_det_symm _

Inverse of Unit Determinant Equals Determinant of Basis Change: $(b.\text{isUnit\_det}\, b').\text{unit}^{-1} = \det_{b'}(b)$

Informal description

Let $A$ be a commutative ring and $M$ be an $A$-module with two bases $b$ and $b'$ indexed by a finite type $\iota$. The inverse of the unit element corresponding to the determinant of $b'$ with respect to $b$ is equal to the determinant of $b$ with respect to $b'$. That is, \[ (b.\text{isUnit\_det}\, b').\text{unit}^{-1} = \det_{b'}(b). \]

Basis.det_reindex theorem

 {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M) (v : ι' → M) (e : ι ≃ ι') :
  (b.reindex e).det v = b.det (v ∘ e)

Full source

theorem Basis.det_reindex {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M) (v : ι' → M)
    (e : ι ≃ ι') : (b.reindex e).det v = b.det (v ∘ e) := by
  rw [Basis.det_apply, Basis.toMatrix_reindex', det_reindexAlgEquiv, Basis.det_apply]

Determinant Invariance under Basis Reindexing: $\det_{b \circ e^{-1}}(v) = \det_b(v \circ e)$

Informal description

Let $R$ be a commutative ring, $M$ be an $R$-module, and $\iota$, $\iota'$ be finite types with decidable equality. Given a basis $b$ of $M$ indexed by $\iota$, a family of vectors $v : \iota' \to M$, and an equivalence $e : \iota \simeq \iota'$ between the index types, the determinant of $v$ with respect to the reindexed basis $b.\text{reindex}\, e$ is equal to the determinant of $v \circ e$ with respect to the original basis $b$. That is, \[ \det_{b.\text{reindex}\, e}(v) = \det_b(v \circ e). \]

Basis.det_reindex' theorem

 {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M) (e : ι ≃ ι') : (b.reindex e).det = b.det.domDomCongr e

Full source

theorem Basis.det_reindex' {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M)
    (e : ι ≃ ι') : (b.reindex e).det = b.det.domDomCongr e :=
  AlternatingMap.ext fun _ => Basis.det_reindex _ _ _

Determinant of Reindexed Basis Equals Reindexed Determinant

Informal description

Let $R$ be a commutative ring, $M$ be an $R$-module, and $\iota$, $\iota'$ be finite types with decidable equality. Given a basis $b$ of $M$ indexed by $\iota$ and an equivalence $e : \iota \simeq \iota'$ between the index types, the determinant of the reindexed basis $b.\text{reindex}\, e$ is equal to the reindexed determinant $\text{Basis.det}\, b$ via the equivalence $e$. That is, \[ \det_{b.\text{reindex}\, e} = (\det_b).\text{domDomCongr}\, e. \]

Basis.det_reindex_symm theorem

 {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M) (v : ι → M) (e : ι' ≃ ι) :
  (b.reindex e.symm).det (v ∘ e) = b.det v

Full source

theorem Basis.det_reindex_symm {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M)
    (v : ι → M) (e : ι' ≃ ι) : (b.reindex e.symm).det (v ∘ e) = b.det v := by
  rw [Basis.det_reindex, Function.comp_assoc, e.self_comp_symm, Function.comp_id]

Determinant Invariance under Basis Reindexing with Symmetric Equivalence: $\det_{b \circ e}(v \circ e^{-1}) = \det_b(v)$

Informal description

Let $R$ be a commutative ring, $M$ be an $R$-module, and $\iota$, $\iota'$ be finite types with decidable equality. Given a basis $b$ of $M$ indexed by $\iota$, a family of vectors $v : \iota \to M$, and an equivalence $e : \iota' \simeq \iota$ between the index types, the determinant of $v \circ e$ with respect to the reindexed basis $b.\text{reindex}\, e^{-1}$ is equal to the determinant of $v$ with respect to the original basis $b$. That is, \[ \det_{b.\text{reindex}\, e^{-1}}(v \circ e) = \det_b(v). \]

Basis.det_map theorem

(b : Basis ι R M) (f : M ≃ₗ[R] M') (v : ι → M') : (b.map f).det v = b.det (f.symm ∘ v)

Full source

@[simp]
theorem Basis.det_map (b : Basis ι R M) (f : M ≃ₗ[R] M') (v : ι → M') :
    (b.map f).det v = b.det (f.symm ∘ v) := by
  rw [Basis.det_apply, Basis.toMatrix_map, Basis.det_apply]

Determinant Transformation under Basis Change via Linear Equivalence: $\det_{b \circ f}(v) = \det_b(f^{-1} \circ v)$

Informal description

Let $R$ be a commutative ring, $M$ and $M'$ be $R$-modules, and $\iota$ be a finite indexing type. Given a basis $b$ of $M$ indexed by $\iota$, a linear equivalence $f : M \simeq_R M'$, and a family of vectors $v : \iota \to M'$, the determinant of $v$ with respect to the transformed basis $b.map\ f$ equals the determinant of $f^{-1} \circ v$ with respect to the original basis $b$. That is, \[ \det_{b.map\ f}(v) = \det_b(f^{-1} \circ v). \]

Basis.det_map' theorem

(b : Basis ι R M) (f : M ≃ₗ[R] M') : (b.map f).det = b.det.compLinearMap f.symm

Full source

theorem Basis.det_map' (b : Basis ι R M) (f : M ≃ₗ[R] M') :
    (b.map f).det = b.det.compLinearMap f.symm :=
  AlternatingMap.ext <| b.det_map f

Determinant Transformation under Basis Change: $\det_{b \circ f} = \det_b \circ f^{-1}$

Informal description

Let $R$ be a commutative ring, $M$ and $M'$ be $R$-modules, and $\iota$ be a finite indexing type. Given a basis $b$ of $M$ indexed by $\iota$ and a linear equivalence $f : M \simeq_R M'$, the determinant map associated with the transformed basis $b \circ f$ is equal to the composition of the determinant map associated with $b$ and the linear map $f^{-1}$. That is, \[ \det_{b \circ f} = \det_b \circ f^{-1}. \]

Pi.basisFun_det theorem

: (Pi.basisFun R ι).det = Matrix.detRowAlternating

Full source

@[simp]
theorem Pi.basisFun_det : (Pi.basisFun R ι).det = Matrix.detRowAlternating := by
  ext M
  rw [Basis.det_apply, Basis.coePiBasisFun.toMatrix_eq_transpose, det_transpose]

Determinant of Standard Basis as Row Alternating Map

Informal description

For a finite index set $\iota$ and a commutative ring $R$, the determinant of the standard basis on the function space $\iota \to R$ is equal to the determinant viewed as an alternating multilinear map on the rows of a matrix with entries in $R$. That is, the determinant map $\det$ associated with the standard basis $\{e_i\}_{i \in \iota}$ (where $e_i(j) = \delta_{ij}$) coincides with the alternating multilinear map $\text{detRowAlternating}$ that computes the determinant of a matrix by treating its rows as vectors.

Pi.basisFun_det_apply theorem

(v : ι → ι → R) : (Pi.basisFun R ι).det v = (Matrix.of v).det

Full source

theorem Pi.basisFun_det_apply (v : ι → ι → R) :
    (Pi.basisFun R ι).det v = (Matrix.of v).det := by
  rw [Pi.basisFun_det]
  rfl

Determinant of Standard Basis Vectors Equals Matrix Determinant

Informal description

For any finite index set $\iota$ and commutative ring $R$, the determinant of a family of vectors $v : \iota \to \iota \to R$ with respect to the standard basis on $\iota \to R$ is equal to the determinant of the matrix formed by $v$. That is, if we view $v$ as a matrix (via the canonical equivalence `Matrix.of`), then $\det(v) = \det(\text{Matrix.of } v)$.

Basis.det_smul_mk_coord_eq_det_update theorem

 {v : ι → M} (hli : LinearIndependent R v) (hsp : ⊤ ≤ span R (range v)) (i : ι) :
  e.det v • (Basis.mk hli hsp).coord i = e.det.toMultilinearMap.toLinearMap v i

Full source

/-- 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`. -/
theorem Basis.det_smul_mk_coord_eq_det_update {v : ι → M} (hli : LinearIndependent R v)
    (hsp : ⊤ ≤ span R (range v)) (i : ι) :
    e.det v • (Basis.mk hli hsp).coord i = e.det.toMultilinearMap.toLinearMap v i := by
  apply (Basis.mk hli hsp).ext
  intro k
  rcases eq_or_ne k i with (rfl | hik) <;>
    simp only [Algebra.id.smul_eq_mul, Basis.coe_mk, LinearMap.smul_apply, LinearMap.coe_mk,
      MultilinearMap.toLinearMap_apply]
  · rw [Basis.mk_coord_apply_eq, mul_one, update_eq_self]
    congr
  · rw [Basis.mk_coord_apply_ne hik, mul_zero, eq_comm]
    exact e.det.map_eq_zero_of_eq _ (by simp [hik, Function.update_apply]) hik

Determinant Scaled by Coordinate Function Equals Linearized Determinant

Informal description

Let $M$ be a module over a commutative ring $R$ with a basis $e$ indexed by a finite type $\iota$. Given a linearly independent family of vectors $v : \iota \to M$ whose span is the entire module $M$, for any index $i \in \iota$, the determinant of $v$ with respect to $e$ scaled by the $i$-th coordinate function of the basis constructed from $v$ equals the linearization of the determinant map at $v$ in the $i$-th coordinate. More precisely, for any $i \in \iota$, we have: \[ \det_e(v) \cdot \text{coord}_i = \text{det}_e(v_1, \dots, v_{i-1}, \cdot, v_{i+1}, \dots, v_n), \] where $\text{coord}_i$ is the $i$-th coordinate function of the basis constructed from $v$, and the right-hand side is the linear map obtained by fixing all coordinates of $\text{det}_e$ except the $i$-th one to be those of $v$.

Basis.det_unitsSMul theorem

(e : Basis ι R M) (w : ι → Rˣ) : (e.unitsSMul w).det = (↑(∏ i, w i)⁻¹ : R) • e.det

Full source

/-- 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. -/
theorem Basis.det_unitsSMul (e : Basis ι R M) (w : ι → Rˣ) :
    (e.unitsSMul w).det = (↑(∏ i, w i)⁻¹ : R) • e.det := by
  ext f
  change
    (Matrix.det fun i j => (e.unitsSMul w).repr (f j) i) =
      (↑(∏ i, w i)⁻¹ : R) • Matrix.det fun i j => e.repr (f j) i
  simp only [e.repr_unitsSMul]
  convert Matrix.det_mul_column (fun i => (↑(w i)⁻¹ : R)) fun i j => e.repr (f j) i
  simp [← Finset.prod_inv_distrib]

Determinant of Basis Scaled by Units is Product of Inverses Times Original Determinant

Informal description

Let $M$ be a module over a commutative ring $R$ with a basis $e$ indexed by a finite type $\iota$, and let $w : \iota \to R^\times$ be a family of units in $R$. Then the determinant of the scaled basis $e.\text{unitsSMul}\, w$ is equal to the product of the inverses of the units $w_i$ multiplied by the determinant of the original basis $e$. That is, \[ \det(e.\text{unitsSMul}\, w) = \left(\prod_{i \in \iota} w_i^{-1}\right) \cdot \det(e). \]

Basis.det_unitsSMul_self theorem

(w : ι → Rˣ) : e.det (e.unitsSMul w) = ∏ i, (w i : R)

Full source

/-- The determinant of a basis constructed by `unitsSMul` is the product of the given units. -/
@[simp]
theorem Basis.det_unitsSMul_self (w : ι → Rˣ) : e.det (e.unitsSMul w) = ∏ i, (w i : R) := by
  simp [Basis.det_apply]

Determinant of Unit-Scaled Basis Vectors Equals Product of Units

Informal description

Let $M$ be a module over a commutative ring $R$ with a basis $e$ indexed by a finite type $\iota$, and let $w : \iota \to R^\times$ be a family of units in $R$. Then the determinant of the family of vectors obtained by scaling the basis $e$ with the units $w$ (i.e., the vectors $w_i \cdot e_i$ for each $i \in \iota$) with respect to the basis $e$ is equal to the product of the units $w_i$ considered as elements of $R$. In mathematical notation: \[ \det_e(e.\text{unitsSMul}\, w) = \prod_{i \in \iota} w_i. \]

Basis.det_isUnitSMul theorem

{w : ι → R} (hw : ∀ i, IsUnit (w i)) : e.det (e.isUnitSMul hw) = ∏ i, w i

Full source

/-- The determinant of a basis constructed by `isUnitSMul` is the product of the given units. -/
@[simp]
theorem Basis.det_isUnitSMul {w : ι → R} (hw : ∀ i, IsUnit (w i)) :
    e.det (e.isUnitSMul hw) = ∏ i, w i :=
  e.det_unitsSMul_self _

Determinant of Basis Scaled by Units Equals Product of Units

Informal description

Let $M$ be a module over a commutative ring $R$ with a basis $e$ indexed by a finite type $\iota$, and let $w : \iota \to R$ be a family of elements in $R$ such that each $w_i$ is a unit. Then the determinant of the family of vectors obtained by scaling the basis $e$ with the units $w$ (i.e., the vectors $w_i \cdot e_i$ for each $i \in \iota$) with respect to the basis $e$ is equal to the product of the units $w_i$. In mathematical notation: \[ \det_e(e.\text{isUnitSMul}\, w) = \prod_{i \in \iota} w_i. \]

Mathlib.LinearAlgebra.Determinant

Main definitions

Tags