[Merged by Bors] - feat(linear_algebra/dual): transpose of linear maps

docs/undergrad.yaml

@@ -23,7 +23,7 @@ Linear algebra:
   Duality:
     dual vector space: 'module.dual'
     dual basis: 'is_basis.dual_basis'
-    transpose of a linear map: ''
+    transpose of a linear map: 'module.dual.transpose'
     orthogonality: ''
   Finite-dimensional vector spaces:
     finite-dimensionality : 'finite_dimensional'

src/linear_algebra/dual.lean

@@ -54,6 +54,30 @@ begin
   rw [linear_map.flip_apply, linear_map.id_apply]
 end
 
+variables {R M} {M' : Type*} [add_comm_group M'] [module R M']
+
+/-- The transposition of linear maps, as a linear map from `M →ₗ[R] M'` to
+`dual R M' →ₗ[R] dual R M`. -/
+def transpose : (M →ₗ[R] M') →ₗ[R] (dual R M' →ₗ[R] dual R M) :=
+{ to_fun := λ u, linear_map.lcomp R R u,
+  map_add' := begin
+    intros u v,
+    ext x,
+    simp only [linear_map.lcomp_apply, linear_map.add_apply, linear_map.map_add],
+  end,
+  map_smul' := begin
+    intros c u,
+    ext x,
+    simp only [linear_map.lcomp_apply, linear_map.smul_apply, map_smul_eq_smul_map],
+  end }
+
+lemma transpose_apply (u : M →ₗ[R] M') (l : dual R M') : transpose u l = l.comp u := rfl
+
+variables {M'' : Type*} [add_comm_group M''] [module R M'']
+
+lemma transpose_comp (u : M' →ₗ[R] M'') (v : M →ₗ[R] M') :
+  transpose (u.comp v) = (transpose v).comp (transpose u) := rfl
+
 end dual
 end module
 
@@ -74,8 +98,35 @@ def to_dual : V →ₗ[K] module.dual K V :=
 h.constr $ λ v, h.constr $ λ w, if w = v then 1 else 0
 
 lemma to_dual_apply (i j : ι) :
-  (h.to_dual (B i)) (B j) = if i = j then 1 else 0 :=
-  by erw [constr_basis h, constr_basis h]; ac_refl
+  h.to_dual (B i) (B j) = if i = j then 1 else 0 :=
+by { erw [constr_basis h, constr_basis h], ac_refl }
+
+@[simp] lemma to_dual_total_left (f : ι →₀ K) (i : ι) :
+  h.to_dual (finsupp.total ι V K B f) (B i) = f i :=
+begin
+  rw [finsupp.total_apply, finsupp.sum, linear_map.map_sum, linear_map.sum_apply],
+  simp_rw [linear_map.map_smul, linear_map.smul_apply, to_dual_apply, smul_eq_mul,
+           mul_boole, finset.sum_ite_eq'],
+  split_ifs with h,
+  { refl },
+  { rw finsupp.not_mem_support_iff.mp h }
+end
+
+@[simp] lemma to_dual_total_right (f : ι →₀ K) (i : ι) :
+  h.to_dual (B i) (finsupp.total ι V K B f) = f i :=
+begin
+  rw [finsupp.total_apply, finsupp.sum, linear_map.map_sum],
+  simp_rw [linear_map.map_smul, to_dual_apply, smul_eq_mul, mul_boole, finset.sum_ite_eq],
+  split_ifs with h,
+  { refl },
+  { rw finsupp.not_mem_support_iff.mp h }
+end
+
+lemma to_dual_apply_left (v : V) (i : ι) : h.to_dual v (B i) = h.repr v i :=
+by rw [← h.to_dual_total_left, h.total_repr]
+
+lemma to_dual_apply_right (i : ι) (v : V) : h.to_dual (B i) v = h.repr v i :=
+by rw [← h.to_dual_total_right, h.total_repr]
 
 def to_dual_flip (v : V) : (V →ₗ[K] K) := (linear_map.flip h.to_dual).to_fun v
 
@@ -97,18 +148,10 @@ include de
 lemma to_dual_swap_eq_to_dual (v w : V) : h.to_dual_flip v w = h.to_dual w v := rfl
 
 lemma to_dual_eq_repr (v : V) (i : ι) : (h.to_dual v) (B i) = h.repr v i :=
-begin
-  rw [←coord_fun_eq_repr, ←to_dual_swap_eq_to_dual],
-  apply congr_fun,
-  dsimp,
-  congr',
-  apply h.ext,
-  { intros,
-    rw [to_dual_swap_eq_to_dual, to_dual_apply],
-    { split_ifs with hx,
-      { rwa [hx, coord_fun_eq_repr, repr_eq_single, finsupp.single_apply, if_pos rfl] },
-      { rw [coord_fun_eq_repr, repr_eq_single, finsupp.single_apply], symmetry, convert if_neg hx } } }
-end
+h.to_dual_apply_left v i
+
+lemma to_dual_eq_equiv_fun [fintype ι] (v : V) (i : ι) : (h.to_dual v) (B i) = h.equiv_fun v i :=
+by rw [h.equiv_fun_apply, to_dual_eq_repr]
 
 lemma to_dual_inj (v : V) (a : h.to_dual v = 0) : v = 0 :=
 begin
@@ -149,13 +192,37 @@ begin
   exact disjoint_bot_right
 end
 
+@[simp] lemma dual_basis_apply_self (i j : ι) :
+  h.dual_basis i (B j) = if i = j then 1 else 0 :=
+h.to_dual_apply i j
+
 /-- A vector space is linearly equivalent to its dual space. -/
 def to_dual_equiv [fintype ι] : V ≃ₗ[K] (dual K V) :=
 linear_equiv.of_bijective h.to_dual h.to_dual_ker h.to_dual_range
 
 theorem dual_basis_is_basis [fintype ι] : is_basis K h.dual_basis :=
 h.to_dual_equiv.is_basis h
 
+@[simp] lemma total_dual_basis [fintype ι] (f : ι →₀ K) (i : ι) :
+  finsupp.total ι (dual K V) K h.dual_basis f (B i) = f i :=
+begin
+  rw [finsupp.total_apply, finsupp.sum_fintype, linear_map.sum_apply],
+  { simp_rw [smul_apply, smul_eq_mul, dual_basis_apply_self, mul_boole,
+             finset.sum_ite_eq', if_pos (finset.mem_univ i)] },
+  { intro, rw zero_smul },
+end
+
+lemma dual_basis_repr [fintype ι] (l : dual K V) (i : ι) :
+  h.dual_basis_is_basis.repr l i = l (B i) :=
+by rw [← total_dual_basis h, is_basis.total_repr h.dual_basis_is_basis l ]
+
+lemma dual_basis_equiv_fun [fintype ι] (l : dual K V) (i : ι) :
+  h.dual_basis_is_basis.equiv_fun l i = l (B i) :=
+by rw [is_basis.equiv_fun_apply, dual_basis_repr]
+
+lemma dual_basis_apply [fintype ι] (i : ι) (v : V) : h.dual_basis i v = h.equiv_fun v i :=
+h.to_dual_apply_right i v
+
 @[simp] lemma to_dual_to_dual [fintype ι] :
   (h.dual_basis_is_basis.to_dual).comp h.to_dual = eval K V :=
 begin

src/linear_algebra/matrix.lean

@@ -6,6 +6,7 @@ Author: Johannes Hölzl, Patrick Massot, Casper Putz
 import linear_algebra.finite_dimensional
 import linear_algebra.nonsingular_inverse
 import linear_algebra.multilinear
+import linear_algebra.dual
 
 /-!
 # Linear maps and matrices
@@ -465,6 +466,25 @@ end
 
 end det
 
+section transpose
+
+variables {K V₁ V₂ ι₁ ι₂ : Type*} [field K]
+          [add_comm_group V₁] [vector_space K V₁]
+          [add_comm_group V₂] [vector_space K V₂]
+          [fintype ι₁] [fintype ι₂] [decidable_eq ι₁] [decidable_eq ι₂]
+          {B₁ : ι₁ → V₁} (h₁ : is_basis K B₁)
+          {B₂ : ι₂ → V₂} (h₂ : is_basis K B₂)
+
+lemma matrix_transpose (u : V₁ →ₗ[K] V₂) :
+  linear_equiv_matrix h₂.dual_basis_is_basis h₁.dual_basis_is_basis (module.dual.transpose u) =
+  (linear_equiv_matrix h₁ h₂ u)ᵀ :=
+begin
+  ext i j,
+  simp only [linear_equiv_matrix_apply, module.dual.transpose_apply, h₁.dual_basis_equiv_fun,
+             h₂.dual_basis_apply, matrix.transpose_apply, linear_map.comp_apply]
+end
+
+end transpose
 namespace matrix
 
 section trace