feat(linear_algebra/dual): transpose of linear maps (#4302)

This is filling an easy hole from the undergrad curriculum page: the transpose of a linear map. We don't prove much about it but at least we make contact with matrix transpose.

Co-authored-by: Anne Baanen t.baanen@vu.nl and Johan Commelin  johan@commelin.net



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

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/basic.lean

@@ -2046,6 +2046,13 @@ def arrow_congr {R M₁ M₂ M₂₁ M₂₂ : Sort*} [comm_ring R]
   arrow_congr e₁ e₂ f x = e₂ (f (e₁.symm x)) :=
 rfl
 
+@[simp] lemma arrow_congr_symm_apply {R M₁ M₂ M₂₁ M₂₂ : Sort*} [comm_ring R]
+  [add_comm_group M₁] [add_comm_group M₂] [add_comm_group M₂₁] [add_comm_group M₂₂]
+  [module R M₁] [module R M₂] [module R M₂₁] [module R M₂₂]
+  (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₂ →ₗ[R] M₂₂) (x : M₁) :
+  (arrow_congr e₁ e₂).symm f x = e₂.symm (f (e₁ x)) :=
+rfl
+
 lemma arrow_congr_comp {N N₂ N₃ : Sort*}
   [add_comm_group N] [add_comm_group N₂] [add_comm_group N₃] [module R N] [module R N₂] [module R N₃]
   (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃) (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :

src/linear_algebra/dual.lean

@@ -54,6 +54,20 @@ 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) :=
+(linear_map.llcomp R M M' R).flip
+
+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 +88,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 +138,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 +182,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
@@ -214,6 +215,9 @@ def linear_equiv_matrix' : ((n → R) →ₗ[R] (m → R)) ≃ₗ[R] matrix m n
 @[simp] lemma linear_equiv_matrix'_apply (f : (n → R) →ₗ[R] (m → R)) :
   linear_equiv_matrix' f = to_matrix f := rfl
 
+@[simp] lemma linear_equiv_matrix'_symm_apply (M : matrix m n R) :
+  linear_equiv_matrix'.symm M = M.to_lin := rfl
+
 variables {ι κ M₁ M₂ : Type*}
   [add_comm_group M₁] [module R M₁]
   [add_comm_group M₂] [module R M₂]
@@ -235,6 +239,11 @@ by simp only [linear_equiv_matrix, to_matrix, to_matrixₗ, ite_smul,
   linear_equiv.coe_coe, linear_equiv_matrix'_apply, finset.mem_univ, if_true,
   one_smul, zero_smul, finset.sum_ite_eq, hv₁.equiv_fun_symm_apply]
 
+lemma linear_equiv_matrix_symm_apply (m : matrix κ ι R) (x : M₁) :
+  (linear_equiv_matrix hv₁ hv₂).symm m x = hv₂.equiv_fun.symm (m.to_lin $ hv₁.equiv_fun x) :=
+by simp only [linear_equiv_matrix, linear_equiv.arrow_congr_symm_apply,
+    linear_equiv_matrix'_symm_apply, linear_equiv.symm_trans_apply]
+
 lemma linear_equiv_matrix_apply' (f : M₁ →ₗ[R] M₂) (i : κ) (j : ι) :
   linear_equiv_matrix hv₁ hv₂ f i j = hv₂.repr (f (v₁ j)) i :=
 linear_equiv_matrix_apply hv₁ hv₂ f i j
@@ -465,6 +474,40 @@ 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₂)
+
+@[simp] lemma linear_equiv_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
+
+lemma linear_equiv_matrix_symm_transpose (M : matrix ι₁ ι₂ K) :
+  (linear_equiv_matrix h₁.dual_basis_is_basis h₂.dual_basis_is_basis).symm Mᵀ =
+  module.dual.transpose ((linear_equiv_matrix h₂ h₁).symm M) :=
+begin
+  apply (linear_equiv_matrix h₁.dual_basis_is_basis h₂.dual_basis_is_basis).injective,
+  rw [linear_equiv.apply_symm_apply],
+  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, if_true,
+    linear_equiv_matrix_symm_apply, linear_equiv.map_smul, mul_boole, algebra.id.smul_eq_mul,
+    linear_equiv.map_sum, is_basis.equiv_fun_self, fintype.sum_apply, finset.sum_ite_eq',
+    finset.sum_ite_eq, is_basis.equiv_fun_symm_apply, pi.smul_apply, matrix.to_lin_apply,
+    matrix.mul_vec, matrix.dot_product, is_basis.equiv_fun_self, finset.mem_univ]
+end
+
+end transpose
 namespace matrix
 
 section trace