feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basi…

…s-free characterization of the trace (#10372)




Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
Co-authored-by: Oliver Nash <github@olivernash.org>

src/data/finsupp/basic.lean

@@ -1297,6 +1297,14 @@ lift_add_hom.to_equiv.apply_eq_iff_eq_symm_apply.2 rfl
   f.sum single = f :=
 add_monoid_hom.congr_fun lift_add_hom_single_add_hom f
 
+@[simp] lemma sum_univ_single [add_comm_monoid M] [fintype α] (i : α) (m : M) :
+  ∑ (j : α), (single i m) j = m :=
+by simp [single]
+
+@[simp] lemma sum_univ_single' [add_comm_monoid M] [fintype α] (i : α) (m : M) :
+  ∑ (j : α), (single j m) i = m :=
+by simp [single]
+
 @[simp] lemma lift_add_hom_apply_single [add_comm_monoid M] [add_comm_monoid N]
   (f : α → M →+ N) (a : α) (b : M) :
   lift_add_hom f (single a b) = f a b :=
@@ -2325,6 +2333,15 @@ rfl
 
 end sum
 
+section
+variables [has_zero M] [monoid_with_zero R] [mul_action_with_zero R M]
+
+@[simp] lemma single_smul (a b : α) (f : α → M) (r : R) :
+  (single a r b) • (f a) = single a (r • f b) b :=
+by by_cases a = b; simp [h]
+
+end
+
 section
 variables [monoid G] [mul_action G α] [add_comm_monoid M]
 

src/data/matrix/basis.lean

@@ -124,6 +124,9 @@ variables (i j : n) (c : α) (i' j' : n)
 @[simp] lemma diag_zero (h : j ≠ i) : diag n α α (std_basis_matrix i j c) = 0 :=
 funext $ λ k, if_neg $ λ ⟨e₁, e₂⟩, h (e₂.trans e₁.symm)
 
+@[simp] lemma diag_same : diag n α α (std_basis_matrix i i c) = pi.single i c :=
+by { ext j, by_cases hij : i = j; try {rw hij}; simp [hij] }
+
 variable [fintype n]
 
 lemma trace_zero (h : j ≠ i) : trace n α α (std_basis_matrix i j c) = 0 := by simp [h]

src/linear_algebra/contraction.lean

@@ -1,9 +1,12 @@
 /-
 Copyright (c) 2020 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Oliver Nash
+Authors: Oliver Nash, Antoine Labelle
 -/
 import linear_algebra.dual
+import linear_algebra.matrix.to_lin
+import linear_algebra.tensor_product_basis
+import linear_algebra.free_module.finite.rank
 
 /-!
 # Contractions
@@ -17,15 +20,17 @@ some basic properties of these maps.
 contraction, dual module, tensor product
 -/
 
-universes u v
+section contraction
 
+open tensor_product linear_map matrix
+open_locale tensor_product big_operators
 
-section contraction
-open tensor_product
-open_locale tensor_product
+variables (R M N : Type*) [add_comm_group M] [add_comm_group N]
 
-variables (R : Type u) (M N : Type v)
-variables [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N]
+section comm_ring
+
+variables [comm_ring R] [module R M] [module R N]
+variables {ι : Type*} [decidable_eq ι] [fintype ι] (b : basis ι R M)
 
 /-- The natural left-handed pairing between a module and its dual. -/
 def contract_left : (module.dual R M) ⊗ M →ₗ[R] R := (uncurry _ _ _ _).to_fun linear_map.id
@@ -51,4 +56,57 @@ variables {R M N}
   dual_tensor_hom R M N (f ⊗ₜ n) m = (f m) • n :=
 by { dunfold dual_tensor_hom, rw uncurry_apply, refl, }
 
+/-- As a matrix, `dual_tensor_hom` evaluated on a basis element of `M* ⊗ N` is a matrix with a
+single one and zeros elsewhere -/
+theorem to_matrix_dual_tensor_hom
+  {m : Type*} {n : Type*} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n]
+  (bM : basis m R M) (bN : basis n R N) (j : m) (i : n) :
+    to_matrix bM bN (dual_tensor_hom R M N (bM.coord j ⊗ₜ bN i)) = std_basis_matrix i j 1 :=
+begin
+  ext i' j',
+  by_cases hij : (i = i' ∧ j = j');
+  simp [linear_map.to_matrix_apply, finsupp.single_eq_pi_single, hij],
+  rw [and_iff_not_or_not, not_not] at hij, cases hij; simp [hij],
+end
+
+local attribute [ext] tensor_product.ext
+
+/-- If `M` is free, the natural linear map $M^* ⊗ N → Hom(M, N)$ is an equivalence. This function
+provides this equivalence in return for a basis of `M`. -/
+@[simps]
+noncomputable def dual_tensor_hom_equiv_of_basis
+  {ι : Type*} [decidable_eq ι] [fintype ι] (b : basis ι R M) :
+  (module.dual R M) ⊗[R] N ≃ₗ[R] M →ₗ[R] N :=
+linear_equiv.of_linear
+  (dual_tensor_hom R M N)
+  (∑ i, (tensor_product.mk R _ N (b.dual_basis i)) ∘ₗ linear_map.applyₗ (b i))
+  (begin
+    ext f m,
+    simp only [applyₗ_apply_apply, coe_fn_sum, dual_tensor_hom_apply, mk_apply, id_coe, id.def,
+      fintype.sum_apply, function.comp_app, basis.coe_dual_basis, coe_comp,
+      basis.coord_apply, ← f.map_smul, (dual_tensor_hom R M N).map_sum, ← f.map_sum, b.sum_repr],
+  end)
+  (begin
+    ext f m,
+    simp only [applyₗ_apply_apply, coe_fn_sum, dual_tensor_hom_apply, mk_apply, id_coe, id.def,
+      fintype.sum_apply, function.comp_app, basis.coe_dual_basis, coe_comp,
+      compr₂_apply, tmul_smul, smul_tmul', ← sum_tmul, basis.sum_dual_apply_smul_coord],
+end)
+
+@[simp] lemma dual_tensor_hom_equiv_of_basis_to_linear_map :
+  (dual_tensor_hom_equiv_of_basis b : (module.dual R M) ⊗[R] N ≃ₗ[R] M →ₗ[R] N).to_linear_map =
+  dual_tensor_hom R M N :=
+rfl
+
+variables [module.free R M] [module.finite R M] [nontrivial R]
+
+open_locale classical
+
+/-- If `M` is finite free, the natural map $M^* ⊗ N → Hom(M, N)$ is an
+equivalence. -/
+@[simp] noncomputable def dual_tensor_hom_equiv : (module.dual R M) ⊗[R] N ≃ₗ[R] M →ₗ[R] N :=
+dual_tensor_hom_equiv_of_basis (module.free.choose_basis R M)
+
+end comm_ring
+
 end contraction

src/linear_algebra/dual.lean

@@ -98,6 +98,7 @@ namespace basis
 universes u v w
 
 open module module.dual submodule linear_map cardinal function
+open_locale big_operators
 
 variables {R M K V ι : Type*}
 
@@ -185,6 +186,20 @@ end
 
 end comm_semiring
 
+section
+
+variables [comm_semiring R] [add_comm_monoid M] [module R M] [fintype ι]
+variables (b : basis ι R M)
+
+@[simp] lemma sum_dual_apply_smul_coord (f : module.dual R M) : ∑ x, f (b x) • b.coord x = f :=
+begin
+  ext m,
+  simp_rw [linear_map.sum_apply, linear_map.smul_apply, smul_eq_mul, mul_comm (f _), ←smul_eq_mul,
+    ←f.map_smul, ←f.map_sum, basis.coord_apply, basis.sum_repr],
+end
+
+end
+
 section comm_ring
 
 variables [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι]

src/linear_algebra/tensor_product_basis.lean

@@ -28,6 +28,15 @@ finsupp.basis_single_one.map
     (finsupp_tensor_finsupp R _ _ _ _).trans $
     finsupp.lcongr (equiv.refl _) (tensor_product.lid R R)).symm
 
+@[simp]
+lemma basis.tensor_product_apply (b : basis ι R M) (c : basis κ R N) (i : ι) (j : κ) :
+  basis.tensor_product b c (i, j) = b i ⊗ₜ c j :=
+by simp [basis.tensor_product]
+
+lemma basis.tensor_product_apply' (b : basis ι R M) (c : basis κ R N) (i : ι × κ) :
+  basis.tensor_product b c i = b i.1 ⊗ₜ c i.2 :=
+by simp [basis.tensor_product]
+
 end comm_ring
 
 section field

src/linear_algebra/trace.lean

@@ -1,11 +1,13 @@
 /-
 Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
+Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen, Antoine Labelle
 -/
 import linear_algebra.matrix.to_lin
 import linear_algebra.matrix.trace
-
+import linear_algebra.contraction
+import linear_algebra.tensor_product_basis
+import linear_algebra.free_module.strong_rank_condition
 
 /-!
 # Trace of a linear map
@@ -110,18 +112,56 @@ by { rw trace_mul_comm, simp }
 end
 
 section
-variables (R : Type u) [field R] {M : Type v} [add_comm_group M] [module R M]
 
-/-- The trace of the identity endomorphism is the dimension of the vector space -/
-@[simp] theorem trace_one : trace R M 1 = (finrank R M : R) :=
+variables (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M]
+variables {ι : Type w} [fintype ι]
+
+/-- The trace of a linear map correspond to the contraction pairing under the isomorphism
+ `End(M) ≃ M* ⊗ M`-/
+lemma trace_eq_contract_of_basis (b : basis ι R M) :
+  (linear_map.trace R M) ∘ₗ (dual_tensor_hom R M M) = contract_left R M :=
 begin
   classical,
-  by_cases H : ∃ (s : finset M), nonempty (basis s R M),
-  { obtain ⟨s, ⟨b⟩⟩ := H,
-    rw [trace_eq_matrix_trace R b, to_matrix_one, finrank_eq_card_finset_basis b],
-    simp, },
-  { suffices : (finrank R M : R) = 0, { simp [this, trace, H], },
-    simp [finrank_eq_zero_of_not_exists_basis H], },
+  apply basis.ext (basis.tensor_product (basis.dual_basis b) b),
+  rintros ⟨i, j⟩,
+  simp only [function.comp_app, basis.tensor_product_apply, basis.coe_dual_basis, coe_comp],
+  rw [trace_eq_matrix_trace R b, to_matrix_dual_tensor_hom],
+  by_cases hij : i = j,
+  { rw [hij], simp},
+  rw matrix.std_basis_matrix.trace_zero j i (1:R) hij,
+  simp [finsupp.single_eq_pi_single, hij],
+end
+
+/-- The trace of a linear map correspond to the contraction pairing under the isomorphism
+ `End(M) ≃ M* ⊗ M`-/
+lemma trace_eq_contract_of_basis' [decidable_eq ι] (b : basis ι R M) :
+  (linear_map.trace R M) =
+  (contract_left R M) ∘ₗ (dual_tensor_hom_equiv_of_basis b).symm.to_linear_map :=
+by simp [linear_equiv.eq_comp_to_linear_map_symm, trace_eq_contract_of_basis R b]
+
+variables [module.free R M] [module.finite R M] [nontrivial R]
+
+/-- When `M` is finite free, the trace of a linear map correspond to the contraction pairing under
+the isomorphism `End(M) ≃ M* ⊗ M`-/
+@[simp] theorem trace_eq_contract :
+  (linear_map.trace R M) ∘ₗ (dual_tensor_hom R M M) = contract_left R M :=
+trace_eq_contract_of_basis R (module.free.choose_basis R M)
+
+open_locale classical
+
+/-- When `M` is finite free, the trace of a linear map correspond to the contraction pairing under
+the isomorphism `End(M) ≃ M* ⊗ M`-/
+theorem trace_eq_contract' :
+  (linear_map.trace R M) =
+  (contract_left R M) ∘ₗ (dual_tensor_hom_equiv).symm.to_linear_map :=
+trace_eq_contract_of_basis' R (module.free.choose_basis R M)
+
+/-- The trace of the identity endomorphism is the dimension of the free module -/
+@[simp] theorem trace_one : trace R M 1 = (finrank R M : R) :=
+begin
+  have b := module.free.choose_basis R M,
+  rw [trace_eq_matrix_trace R b, to_matrix_one, module.free.finrank_eq_card_choose_basis_index],
+  simp,
 end
 
 end

src/representation_theory/basic.lean

@@ -100,7 +100,8 @@ noncomputable def character (g : G) : k :=
 linear_map.trace k V (as_group_hom k G V g)
 
 /-- The evaluation of the character at the identity is the dimension of the representation. -/
-theorem char_one : character k G V 1 = finite_dimensional.finrank k V := by simp
+theorem char_one [finite_dimensional k V] : character k G V 1 = finite_dimensional.finrank k V :=
+by simp
 
 /-- The character of a representation is constant on conjugacy classes. -/
 theorem char_conj (g : G) (h : G) : (character k G V) (h * g * h⁻¹) = (character k G V) g := by simp