feat(linear_algebra): the determinant of an endomorphism (#7635)

 `linear_map.det` is the determinant of an endomorphism, which is defined independent of a basis. If there is no finite basis, the determinant is defined to be equal to `1`.

This approach is inspired by `linear_map.trace`.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

docs/undergrad.yaml

@@ -35,7 +35,7 @@ Linear algebra:
   Multilinearity:
     multilinear map: 'multilinear_map'
     determinant of vectors: 'basis.det'
-    determinant of endomorphisms: ''
+    determinant of endomorphisms: 'linear_map.det'
     special linear group: ''
     orientation of a $\R$-valued vector space: ''
   Matrices:

src/linear_algebra/determinant.lean

@@ -16,12 +16,10 @@ import ring_theory.matrix_algebra
 /-!
 # Determinant of families of vectors
 
-This file defines the determinant of a family of vectors with respect to
-some basis. For the determinant of a matrix, see the file
+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`.
 
-It also contains some results on the determinant of linear maps and linear equivs.
-
 ## Main definitions
 
 In the list below, and in all this file, `R` is a commutative ring (semiring
@@ -30,6 +28,9 @@ types used for indexing.
 
  * `basis.det`: the determinant of a family of vectors with respect to a basis,
    as a multilinear map
+ * `linear_map.det`: the determinant of an endomorphism `f : End R M` as a
+   multiplicative homomorphism (if `M` does not have a finite `R`-basis, the
+   result is `1` instead)
 
 ## Tags
 
@@ -59,7 +60,6 @@ section conjugate
 variables {A : Type*} [integral_domain A]
 variables {m n : Type*} [fintype m] [fintype n]
 
-
 /-- If `R^m` and `R^n` are linearly equivalent, then `m` and `n` are also equivalent. -/
 def equiv_of_pi_lequiv_pi {R : Type*} [integral_domain R]
   (e : (m → R) ≃ₗ[R] (n → R)) : m ≃ n :=
@@ -95,6 +95,119 @@ end
 
 end conjugate
 
+namespace linear_map
+
+/-! ### Determinant of a linear map -/
+
+variables {A : Type*} [integral_domain A] [module A M]
+variables {κ : Type*} [fintype κ]
+
+/-- The determinant of `linear_map.to_matrix` does not depend on the choice of basis. -/
+lemma det_to_matrix_eq_det_to_matrix [decidable_eq κ]
+  (b : basis ι A M) (c : basis κ A M) (f : M →ₗ[A] M) :
+  det (linear_map.to_matrix b b f) = det (linear_map.to_matrix c c f) :=
+by rw [← linear_map_to_matrix_mul_basis_to_matrix c b c,
+       ← basis_to_matrix_mul_linear_map_to_matrix b c b,
+       matrix.det_conj]; rw [basis.to_matrix_mul_to_matrix, basis.to_matrix_self]
+
+/-- 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`.
+-/
+def det_aux : trunc (basis ι A M) → (M →ₗ[A] M) →* A :=
+trunc.lift
+  (λ b : basis ι A M,
+    (monoid_hom.of (matrix.det)).comp (to_matrix_alg_equiv b : (M →ₗ[A] M) →* matrix ι ι A))
+  (λ b c, monoid_hom.ext $ det_to_matrix_eq_det_to_matrix b c)
+
+/-- Unfold lemma for `det_aux`.
+
+See also `det_aux_def'` which allows you to vary the basis.
+-/
+lemma det_aux_def (b : basis ι A M) (f : M →ₗ[A] M) :
+  linear_map.det_aux (trunc.mk b) f = matrix.det (linear_map.to_matrix b b f) :=
+rfl
+
+-- Discourage the elaborator from unfolding `det_aux` and producing a huge term.
+attribute [irreducible] linear_map.det_aux
+
+lemma det_aux_def' {ι' : Type*} [fintype ι'] [decidable_eq ι']
+  (tb : trunc $ basis ι A M) (b' : basis ι' A M) (f : M →ₗ[A] M) :
+  linear_map.det_aux tb f = matrix.det (linear_map.to_matrix b' b' f) :=
+by { apply trunc.induction_on tb, intro b, rw [det_aux_def, det_to_matrix_eq_det_to_matrix b b'] }
+
+@[simp]
+lemma det_aux_id (b : trunc $ basis ι A M) : linear_map.det_aux b (linear_map.id) = 1 :=
+(linear_map.det_aux b).map_one
+
+@[simp]
+lemma det_aux_comp (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 :=
+(linear_map.det_aux b).map_mul f g
+
+section
+open_locale classical
+
+/-- The determinant of an endomorphism independent of basis.
+
+If there is no finite basis on `M`, the result is `1` instead.
+-/
+protected def det : (M →ₗ[A] M) →* A :=
+if H : ∃ (s : set M) (b : basis s A M), s.finite
+then @linear_map.det_aux _ _ _ _ H.some_spec.some_spec.some _ _ _ (trunc.mk H.some_spec.some)
+else 1
+
+lemma coe_det [decidable_eq M] : ⇑(linear_map.det : (M →ₗ[A] M) →* A) =
+  if H : ∃ (s : set M) (b : basis s A M), s.finite
+  then @linear_map.det_aux _ _ _ _ H.some_spec.some_spec.some _ _ _ (trunc.mk H.some_spec.some)
+  else 1 :=
+by { ext, unfold linear_map.det,
+     split_ifs,
+     { congr }, -- use the correct `decidable_eq` instance
+     refl }
+
+end
+
+-- Discourage the elaborator from unfolding `det` and producing a huge term.
+attribute [irreducible] linear_map.det
+
+-- Auxiliary lemma, the `simp` normal form goes in the other direction
+-- (using `linear_map.det_to_matrix`)
+lemma det_eq_det_to_matrix_of_finite_set [decidable_eq M]
+  {s : set M} (b : basis s A M) [hs : fintype s] (f : M →ₗ[A] M) :
+  f.det = matrix.det (linear_map.to_matrix b b f) :=
+have ∃ (s : set M) (b : basis s A M), s.finite,
+from ⟨s, b, ⟨hs⟩⟩,
+by rw [linear_map.coe_det, dif_pos, det_aux_def' _ b]; assumption
+
+@[simp] lemma det_to_matrix
+  (b : basis ι A M) (f : M →ₗ[A] M) :
+  matrix.det (to_matrix b b f) = f.det :=
+by { haveI := classical.dec_eq M,
+     rw [det_eq_det_to_matrix_of_finite_set b.reindex_range, det_to_matrix_eq_det_to_matrix b] }
+
+@[simp]
+lemma det_comp (f g : M →ₗ[A] M) : (f.comp g).det = f.det * g.det :=
+linear_map.det.map_mul f g
+
+@[simp]
+lemma det_id : (linear_map.id : M →ₗ[A] M).det = 1 :=
+linear_map.det.map_one
+
+lemma det_zero {ι : Type*} [fintype ι] [nonempty ι] (b : basis ι A M) :
+  linear_map.det (0 : M →ₗ[A] M) = 0 :=
+by { haveI := classical.dec_eq ι,
+     rw [← det_to_matrix b, linear_equiv.map_zero, det_zero],
+     assumption }
+
+end linear_map
+
+-- Cannot be stated using `linear_map.det` because `f` is not an endomorphism.
 lemma linear_equiv.is_unit_det (f : M ≃ₗ[R] M') (v : basis ι R M) (v' : basis ι R M') :
   is_unit (linear_map.to_matrix v v' f).det :=
 begin