feat(linear_algebra): use finsets to define det and trace (#7778)

This PR replaces `∃ (s : set M) (b : basis s R M), s.finite` with `∃ (s : finset M), nonempty (basis s R M)` in the definitions in `linear_map.det` and `linear_map.trace`. This should make it much easier to unfold those definitions without having to modify the instance cache or supply implicit params.

In particular, it should help a lot with #7667.

Author: Vierkantor

src/linear_algebra/basis.lean

@@ -333,6 +333,41 @@ end
   b.reindex_range.repr x ⟨b i, h⟩ = b.repr x i :=
 b.reindex_range_repr' _ rfl
 
+section fintype
+
+variables [fintype ι]
+
+/-- `b.reindex_finset_range` is a basis indexed by `finset.univ.image b`,
+the finite set of basis vectors themselves. -/
+def reindex_finset_range : basis (finset.univ.image b) R M :=
+b.reindex_range.reindex ((equiv.refl M).subtype_equiv (by simp))
+
+lemma reindex_finset_range_self (i : ι) (h := finset.mem_image_of_mem b (finset.mem_univ i)) :
+  b.reindex_finset_range ⟨b i, h⟩ = b i :=
+by { rw [reindex_finset_range, reindex_apply, reindex_range_apply], refl }
+
+@[simp] lemma reindex_finset_range_apply (x : finset.univ.image b) :
+  b.reindex_finset_range x = x :=
+by { rcases x with ⟨bi, hbi⟩, rcases finset.mem_image.mp hbi with ⟨i, -, rfl⟩,
+     exact b.reindex_finset_range_self i }
+
+lemma reindex_finset_range_repr_self (i : ι) :
+  b.reindex_finset_range.repr (b i) =
+    finsupp.single ⟨b i, finset.mem_image_of_mem b (finset.mem_univ i)⟩ 1 :=
+begin
+  ext ⟨bi, hbi⟩,
+  rw [reindex_finset_range, reindex_repr, reindex_range_repr_self],
+  convert finsupp.single_apply_left ((equiv.refl M).subtype_equiv _).symm.injective _ _ _,
+  refl
+end
+
+@[simp] lemma reindex_finset_range_repr (x : M) (i : ι)
+  (h := finset.mem_image_of_mem b (finset.mem_univ i)) :
+  b.reindex_finset_range.repr x ⟨b i, h⟩ = b.repr x i :=
+by simp [reindex_finset_range]
+
+end fintype
+
 end reindex
 
 protected lemma linear_independent : linear_independent R b :=

src/linear_algebra/determinant.lean

@@ -158,13 +158,13 @@ open_locale classical
 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)
+if H : ∃ (s : finset M), nonempty (basis s A M)
+then linear_map.det_aux (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)
+  if H : ∃ (s : finset M), nonempty (basis s A M)
+  then linear_map.det_aux (trunc.mk H.some_spec.some)
   else 1 :=
 by { ext, unfold linear_map.det,
      split_ifs,
@@ -178,18 +178,18 @@ 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) :
+lemma det_eq_det_to_matrix_of_finset [decidable_eq M]
+  {s : finset M} (b : basis s A M) (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⟩⟩,
+have ∃ (s : finset M), nonempty (basis s A M),
+from ⟨s, ⟨b⟩⟩,
 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] }
+     rw [det_eq_det_to_matrix_of_finset b.reindex_finset_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 :=

src/linear_algebra/finite_dimensional.lean

@@ -549,6 +549,10 @@ lemma finrank_eq_zero_of_not_exists_basis_finite
   (h : ¬ ∃ (s : set V) (b : basis.{v} (s : set V) K V), s.finite) : finrank K V = 0 :=
 finrank_eq_zero_of_basis_imp_not_finite (λ s b hs, h ⟨s, b, hs⟩)
 
+lemma finrank_eq_zero_of_not_exists_basis_finset
+  (h : ¬ ∃ (s : finset V), nonempty (basis s K V)) : finrank K V = 0 :=
+finrank_eq_zero_of_basis_imp_false (λ s b, h ⟨s, ⟨b⟩⟩)
+
 variables (K V)
 
 lemma finite_dimensional_bot : finite_dimensional K (⊥ : submodule K V) :=

src/linear_algebra/trace.lean

@@ -64,45 +64,36 @@ calc  matrix.trace ι R R (linear_map.to_matrix b b f)
 
 open_locale classical
 
-theorem trace_aux_reindex_range [nontrivial R] : trace_aux R b.reindex_range = trace_aux R b :=
-linear_map.ext $ λ f,
-begin
-  change ∑ i : set.range b, _ = ∑ i : ι, _, simp_rw [matrix.diag_apply], symmetry,
-  convert (equiv.of_injective _ b.injective).sum_comp _, ext i,
-  exact (linear_map.to_matrix_reindex_range b b f i i).symm
-end
-
 variables (R) (M)
 
 /-- Trace of an endomorphism independent of basis. -/
 def trace : (M →ₗ[R] M) →ₗ[R] R :=
-if H : ∃ (s : set M) (b : basis (s : set M) R M), s.finite
-then @trace_aux R _ _ _ _ _ _ (classical.choice H.some_spec.some_spec) H.some_spec.some
+if H : ∃ (s : finset M), nonempty (basis s R M)
+then trace_aux R H.some_spec.some
 else 0
 
 variables (R) {M}
 
 /-- Auxiliary lemma for `trace_eq_matrix_trace`. -/
-theorem trace_eq_matrix_trace_of_finite_set {s : set M} (b : basis s R M) (hs : fintype s)
+theorem trace_eq_matrix_trace_of_finset {s : finset M} (b : basis s R M)
   (f : M →ₗ[R] M) :
   trace R M f = matrix.trace s R R (linear_map.to_matrix b b f) :=
-have ∃ (s : set M) (b : basis (s : set M) R M), s.finite,
-from ⟨s, b, ⟨hs⟩⟩,
+have ∃ (s : finset M), nonempty (basis s R M),
+from ⟨s, ⟨b⟩⟩,
 by { rw [trace, dif_pos this, ← trace_aux_def], congr' 1, apply trace_aux_eq }
 
 theorem trace_eq_matrix_trace (f : M →ₗ[R] M) :
   trace R M f = matrix.trace ι R R (linear_map.to_matrix b b f) :=
 if hR : nontrivial R
 then by haveI := hR;
-        rw [trace_eq_matrix_trace_of_finite_set R b.reindex_range (set.fintype_range b),
-            ← trace_aux_def, ← trace_aux_def, trace_aux_reindex_range]
+        rw [trace_eq_matrix_trace_of_finset R b.reindex_finset_range,
+            ← trace_aux_def, ← trace_aux_def, trace_aux_eq R b]
 else @subsingleton.elim _ (not_nontrivial_iff_subsingleton.mp hR) _ _
 
 theorem trace_mul_comm (f g : M →ₗ[R] M) :
   trace R M (f * g) = trace R M (g * f) :=
-if H : ∃ (s : set M) (b : basis (s : set M) R M), s.finite then let ⟨s, b, hs⟩ := H in
-by { haveI := classical.choice hs,
-     simp_rw [trace_eq_matrix_trace R b, linear_map.to_matrix_mul], apply matrix.trace_mul_comm }
+if H : ∃ (s : finset M), nonempty (basis s R M) then let ⟨s, ⟨b⟩⟩ := H in
+by { simp_rw [trace_eq_matrix_trace R b, linear_map.to_matrix_mul], apply matrix.trace_mul_comm }
 else by rw [trace, dif_neg H, linear_map.zero_apply, linear_map.zero_apply]
 
 end linear_map

src/ring_theory/norm.lean

@@ -61,7 +61,7 @@ linear_map.det.comp (lmul R S).to_ring_hom.to_monoid_hom
 @[simp] lemma norm_apply (x : S) : norm R x = linear_map.det (lmul R S x) := rfl
 
 lemma norm_eq_one_of_not_exists_basis
-  (h : ¬ ∃ (s : set S) (b : basis s R S), s.finite) (x : S) : norm R x = 1 :=
+  (h : ¬ ∃ (s : finset S), nonempty (basis s R S)) (x : S) : norm R x = 1 :=
 by { rw [norm_apply, linear_map.det], split_ifs with h, refl }
 
 variables {R}
@@ -89,12 +89,11 @@ end
 @[simp]
 lemma norm_algebra_map (x : K) : norm K (algebra_map K L x) = x ^ finrank K L :=
 begin
-  by_cases H : ∃ (s : set L) (b : basis s K L), s.finite,
-  { haveI : fintype H.some := H.some_spec.some_spec.some,
-    rw [norm_algebra_map_of_basis H.some_spec.some, finrank_eq_card_basis H.some_spec.some] },
+  by_cases H : ∃ (s : finset L), nonempty (basis s K L),
+  { rw [norm_algebra_map_of_basis H.some_spec.some, finrank_eq_card_basis H.some_spec.some] },
   { rw [norm_eq_one_of_not_exists_basis K H, finrank_eq_zero_of_not_exists_basis, pow_zero],
     rintros ⟨s, ⟨b⟩⟩,
-    exact H ⟨↑s, b, s.finite_to_set⟩ },
+    exact H ⟨s, ⟨b⟩⟩ },
 end
 
 section eq_prod_roots

src/ring_theory/trace.lean

@@ -61,7 +61,7 @@ noncomputable def trace : S →ₗ[R] R :=
 variables {S}
 
 lemma trace_eq_zero_of_not_exists_basis
-  (h : ¬ ∃ (s : set S) (b : basis s R S), s.finite) : trace R S = 0 :=
+  (h : ¬ ∃ (s : finset S), nonempty (basis s R S)) : trace R S = 0 :=
 by { ext s, simp [linear_map.trace, h] }
 
 include b
@@ -92,10 +92,9 @@ omit b
 @[simp]
 lemma trace_algebra_map (x : K) : trace K L (algebra_map K L x) = finrank K L • x :=
 begin
-  by_cases H : ∃ (s : set L) (b : basis s K L), s.finite,
-  { haveI : fintype H.some := H.some_spec.some_spec.some,
-    rw [trace_algebra_map_of_basis H.some_spec.some, finrank_eq_card_basis H.some_spec.some] },
-  { simp [trace_eq_zero_of_not_exists_basis K H, finrank_eq_zero_of_not_exists_basis_finite H] }
+  by_cases H : ∃ (s : finset L), nonempty (basis s K L),
+  { rw [trace_algebra_map_of_basis H.some_spec.some, finrank_eq_card_basis H.some_spec.some] },
+  { simp [trace_eq_zero_of_not_exists_basis K H, finrank_eq_zero_of_not_exists_basis_finset H] }
 end
 
 section trace_form