[Merged by Bors] - feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace

src/data/matrix/basis.lean

@@ -123,10 +123,15 @@ 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]
 
+lemma trace_same : trace n α α (std_basis_matrix i i c) = c := by simp
+
 @[simp] lemma mul_left_apply_same (b : n) (M : matrix n n α) :
   (std_basis_matrix i j c ⬝ M) i b = c * M j b :=
 by simp [mul_apply, std_basis_matrix]

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
@@ -21,8 +24,14 @@ universes u v
 
 
 section contraction
+
 open tensor_product
+open linear_map
+open matrix
 open_locale tensor_product
+open_locale big_operators
+
+section
 
 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]
@@ -51,4 +60,45 @@ 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 dual_tensor_hom_basis
+  {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
+
+end
+
+open finite_dimensional
+variables (R : Type u) (M N : Type v)
+variables [field R] [add_comm_group M] [add_comm_group N] [module R M] [module R N]
+variables [finite_dimensional R M]
+
+theorem dual_tensor_hom_surj : function.surjective (dual_tensor_hom R M N) :=
+begin
+  intro f,
+  have b := fin_basis R M,
+  use ∑ (i : fin (finrank R M)), (b.dual_basis i) ⊗ₜ f (b i),
+  ext m, simp,
+  nth_rewrite_rhs 0 ←basis.sum_repr b m, simp,
+end
+
+variables [finite_dimensional R N]
+
+theorem dual_tensor_hom_inj : function.injective (dual_tensor_hom R M N) :=
+  (injective_iff_surjective_of_finrank_eq_finrank (by simp)).2 (dual_tensor_hom_surj R M N)
+
+noncomputable def dual_tensor_hom_equiv : (module.dual R M) ⊗[R] N ≃ₗ[R] M →ₗ[R] N :=
+  linear_equiv.of_bijective (dual_tensor_hom R M N)
+    (dual_tensor_hom_inj R M N) (dual_tensor_hom_surj R M N)
+
+lemma dual_tensor_hom_equiv_to_lin (f : (module.dual R M) ⊗[R] N):
+  (dual_tensor_hom_equiv R M N) f = (dual_tensor_hom R M N) f := rfl
+
 end contraction

src/linear_algebra/tensor_product_basis.lean

@@ -27,6 +27,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 { dunfold basis.tensor_product, simp }
+
 end comm_ring
 
 section field

src/linear_algebra/trace.lean

@@ -1,11 +1,12 @@
 /-
 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
 
 /-!
 # Trace of a linear map
@@ -115,6 +116,28 @@ end
 section
 variables (R : Type u) [field R] {M : Type v} [add_comm_group M] [module R M]
 
+/-- The trace of a linear map correspond to the contraction pairing under the isomorphism
+ `M →ₗ M ≃ M* ⊗ M`-/
+lemma trace_eq_contract [finite_dimensional R M] :
+  (linear_map.trace R M) ∘ₗ ↑(dual_tensor_hom_equiv R M M) = contract_left R M :=
+begin
+  have b := fin_basis R M,
+  apply basis.ext (basis.tensor_product (b.dual_basis) b),
+  rintros ⟨i, j⟩,
+  simp [dual_tensor_hom_equiv_to_lin],
+  rw [trace_eq_matrix_trace R b, dual_tensor_hom_basis],
+  by_cases hij : i = j,
+  { rw [hij, matrix.std_basis_matrix.trace_same], 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
+ `M →ₗ M ≃ M* ⊗ M`-/
+lemma trace_eq_contract' [finite_dimensional R M] :
+  (linear_map.trace R M) = (contract_left R M) ∘ₗ ↑(dual_tensor_hom_equiv R M M).symm :=
+by { rw [←trace_eq_contract], ext f, simp }
+
 /-- 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) :=
 begin