feat(linear_algebra/matrix): trace of an endomorphism independent of basis (#3125)

Author: kckennylau

src/data/equiv/basic.lean

@@ -1202,6 +1202,14 @@ noncomputable def of_bijective {α β} (f : α → β) (hf : bijective f) : α 
 @[simp] theorem coe_of_bijective {α β} {f : α → β} (hf : bijective f) :
   (of_bijective f hf : α → β) = f := rfl
 
+/-- If `f` is an injective function, then its domain is equivalent to its range. -/
+noncomputable def of_injective {α β} (f : α → β) (hf : injective f) : α ≃ _root_.set.range f :=
+of_bijective (λ x, ⟨f x, set.mem_range_self x⟩) ⟨λ x y hxy, hf $ by injections, λ ⟨_, x, rfl⟩, ⟨x, rfl⟩⟩
+
+@[simp] lemma of_injective_apply {α β} (f : α → β) (hf : injective f) (x : α) :
+  of_injective f hf x = ⟨f x, set.mem_range_self x⟩ :=
+rfl
+
 def subtype_quotient_equiv_quotient_subtype (p₁ : α → Prop) [s₁ : setoid α]
   [s₂ : setoid (subtype p₁)] (p₂ : quotient s₁ → Prop) (hp₂ :  ∀ a, p₁ a ↔ p₂ ⟦a⟧)
   (h : ∀ x y : subtype p₁, @setoid.r _ s₂ x y ↔ (x : α) ≈ y) :

src/linear_algebra/basic.lean

@@ -1607,6 +1607,7 @@ def to_add_equiv : M ≃+ M₂ := { .. e }
   (e₁.trans e₂) c = e₂ (e₁ c) := rfl
 @[simp] theorem apply_symm_apply (c : M₂) : e (e.symm c) = c := e.6 c
 @[simp] theorem symm_apply_apply (b : M) : e.symm (e b) = b := e.5 b
+@[simp] lemma symm_trans_apply (c : M₃) : (e₁.trans e₂).symm c = e₁.symm (e₂.symm c) := rfl
 
 @[simp] lemma trans_refl : e.trans (refl R M₂) = e := to_equiv_injective e.to_equiv.trans_refl
 @[simp] lemma refl_trans : (refl R M).trans e = e := to_equiv_injective e.to_equiv.refl_trans
@@ -1829,6 +1830,13 @@ lemma arrow_congr_comp {N N₂ N₃ : Sort*}
   arrow_congr e₁ e₃ (g.comp f) = (arrow_congr e₂ e₃ g).comp (arrow_congr e₁ e₂ f) :=
 by { ext, simp only [symm_apply_apply, arrow_congr_apply, linear_map.comp_apply], }
 
+lemma arrow_congr_trans {M₁ M₂ M₃ N₁ N₂ N₃ : Sort*}
+  [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] [add_comm_group M₃] [module R M₃]
+  [add_comm_group N₁] [module R N₁] [add_comm_group N₂] [module R N₂] [add_comm_group N₃] [module R N₃]
+  (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) :
+  (arrow_congr e₁ e₂).trans (arrow_congr e₃ e₄) = arrow_congr (e₁.trans e₃) (e₂.trans e₄) :=
+rfl
+
 /-- If `M₂` and `M₃` are linearly isomorphic then the two spaces of linear maps from `M` into `M₂`
 and `M` into `M₃` are linearly isomorphic. -/
 def congr_right (f : M₂ ≃ₗ[R] M₃) : (M →ₗ[R] M₂) ≃ₗ (M →ₗ M₃) := arrow_congr (linear_equiv.refl R M) f
@@ -2266,6 +2274,53 @@ end
 
 end pi
 
+section fun_left
+variables (R M) [semiring R] [add_comm_monoid M] [semimodule R M]
+variables {m n p : Type*}
+
+/-- Given an `R`-module `M` and a function `m → n` between arbitrary types,
+construct a linear map `(n → M) →ₗ[R] (m → M)` -/
+def fun_left (f : m → n) : (n → M) →ₗ[R] (m → M) :=
+mk (∘f) (λ _ _, rfl) (λ _ _, rfl)
+
+@[simp] theorem fun_left_apply (f : m → n) (g : n → M) (i : m) : fun_left R M f g i = g (f i) :=
+rfl
+
+@[simp] theorem fun_left_id (g : n → M) : fun_left R M _root_.id g = g :=
+rfl
+
+theorem fun_left_comp (f₁ : n → p) (f₂ : m → n) :
+  fun_left R M (f₁ ∘ f₂) = (fun_left R M f₂).comp (fun_left R M f₁) :=
+rfl
+
+/-- Given an `R`-module `M` and an equivalence `m ≃ n` between arbitrary types,
+construct a linear equivalence `(n → M) ≃ₗ[R] (m → M)` -/
+def fun_congr_left (e : m ≃ n) : (n → M) ≃ₗ[R] (m → M) :=
+linear_equiv.of_linear (fun_left R M e) (fun_left R M e.symm)
+  (ext $ λ x, funext $ λ i,
+    by rw [id_apply, ← fun_left_comp, equiv.symm_comp_self, fun_left_id])
+  (ext $ λ x, funext $ λ i,
+    by rw [id_apply, ← fun_left_comp, equiv.self_comp_symm, fun_left_id])
+
+@[simp] theorem fun_congr_left_apply (e : m ≃ n) (x : n → M) :
+  fun_congr_left R M e x = fun_left R M e x :=
+rfl
+
+@[simp] theorem fun_congr_left_id :
+  fun_congr_left R M (equiv.refl n) = linear_equiv.refl R (n → M) :=
+rfl
+
+@[simp] theorem fun_congr_left_comp (e₁ : m ≃ n) (e₂ : n ≃ p) :
+  fun_congr_left R M (equiv.trans e₁ e₂) =
+    linear_equiv.trans (fun_congr_left R M e₂) (fun_congr_left R M e₁) :=
+rfl
+
+@[simp] lemma fun_congr_left_symm (e : m ≃ n) :
+  (fun_congr_left R M e).symm = fun_congr_left R M e.symm :=
+rfl
+
+end fun_left
+
 universe i
 variables [semiring R] [add_comm_monoid M] [semimodule R M]
 

src/linear_algebra/basis.lean

@@ -735,6 +735,9 @@ end
 lemma is_basis.injective (hv : is_basis R v) (zero_ne_one : (0 : R) ≠ 1) : injective v :=
   λ x y h, linear_independent.injective zero_ne_one hv.1 h
 
+lemma is_basis.range (hv : is_basis R v) : is_basis R (λ x, x : range v → M) :=
+⟨hv.1.to_subtype_range, by { convert hv.2, ext i, exact ⟨λ ⟨p, hp⟩, hp ▸ p.2, λ hi, ⟨⟨i, hi⟩, rfl⟩⟩ }⟩
+
 /-- Given a basis, any vector can be written as a linear combination of the basis vectors. They are
 given by this linear map. This is one direction of `module_equiv_finsupp`. -/
 def is_basis.repr : M →ₗ (ι →₀ R) :=

src/linear_algebra/matrix.lean

@@ -69,6 +69,17 @@ end
 linear maps (n → R) →ₗ[R] (m → R). -/
 def to_lin : matrix m n R → (n → R) →ₗ[R] (m → R) := eval.to_fun
 
+theorem to_lin_of_equiv {p q : Type*} [fintype p] [fintype q] (e₁ : m ≃ p) (e₂ : n ≃ q)
+  (f : matrix p q R) : to_lin (λ i j, f (e₁ i) (e₂ j) : matrix m n R) =
+    linear_equiv.arrow_congr
+      (linear_map.fun_congr_left R R e₂)
+      (linear_map.fun_congr_left R R e₁)
+      (to_lin f) :=
+linear_map.ext $ λ v, funext $ λ i,
+calc  ∑ j : n, f (e₁ i) (e₂ j) * v j
+    = ∑ j : n, f (e₁ i) (e₂ j) * v (e₂.symm (e₂ j)) : by simp_rw e₂.symm_apply_apply
+... = ∑ k : q, f (e₁ i) k * v (e₂.symm k) : finset.sum_equiv e₂ (λ k, f (e₁ i) k * v (e₂.symm k))
+
 lemma to_lin_add (M N : matrix m n R) : (M + N).to_lin = M.to_lin + N.to_lin :=
 matrix.eval.map_add M N
 
@@ -113,6 +124,14 @@ def to_matrix [decidable_eq n] : ((n → R) →ₗ[R] (m → R)) → matrix m n
   (@linear_map.id _ (n → R) _ _ _).to_matrix = 1 :=
 by { ext, simp [to_matrix, to_matrixₗ, matrix.one_val, eq_comm] }
 
+theorem to_matrix_of_equiv {p q : Type*} [fintype p] [fintype q] [decidable_eq n] [decidable_eq q]
+  (e₁ : m ≃ p) (e₂ : n ≃ q) (f : (q → R) →ₗ[R] (p → R)) (i j) :
+  to_matrix f (e₁ i) (e₂ j) = to_matrix (linear_equiv.arrow_congr
+      (linear_map.fun_congr_left R R e₂)
+      (linear_map.fun_congr_left R R e₁) f) i j :=
+show f (λ k : q, ite (e₂ j = k) 1 0) (e₁ i) = f (λ k : q, ite (j = e₂.symm k) 1 0) (e₁ i),
+by { congr' 1, ext, congr' 1, rw equiv.eq_symm_apply }
+
 end linear_map
 
 section linear_equiv_matrix
@@ -169,6 +188,9 @@ def linear_equiv_matrix' : ((n → R) →ₗ[R] (m → R)) ≃ₗ[R] matrix m n
   map_add' := to_matrixₗ.map_add,
   map_smul' := to_matrixₗ.map_smul }
 
+@[simp] lemma linear_equiv_matrix'_apply (f : (n → R) →ₗ[R] (m → R)) :
+  linear_equiv_matrix' f = to_matrix f := rfl
+
 /-- Given a basis of two modules M₁ and M₂ over a commutative ring R, we get a linear equivalence
 between linear maps M₁ →ₗ M₂ and matrices over R indexed by the bases. -/
 def linear_equiv_matrix {ι κ M₁ M₂ : Type*}
@@ -179,6 +201,29 @@ def linear_equiv_matrix {ι κ M₁ M₂ : Type*}
   (M₁ →ₗ[R] M₂) ≃ₗ[R] matrix κ ι R :=
 linear_equiv.trans (linear_equiv.arrow_congr (equiv_fun_basis hv₁) (equiv_fun_basis hv₂)) linear_equiv_matrix'
 
+open_locale classical
+
+theorem linear_equiv_matrix_range {ι κ M₁ M₂ : Type*}
+  [add_comm_group M₁] [module R M₁]
+  [add_comm_group M₂] [module R M₂]
+  [fintype ι] [fintype κ]
+  {v₁ : ι → M₁} {v₂ : κ → M₂} (hv₁ : is_basis R v₁) (hv₂ : is_basis R v₂) (f : M₁ →ₗ[R] M₂) (k i) :
+  linear_equiv_matrix hv₁.range hv₂.range f ⟨v₂ k, mem_range_self k⟩ ⟨v₁ i, mem_range_self i⟩ =
+    linear_equiv_matrix hv₁ hv₂ f k i :=
+if H : (0 : R) = 1 then @subsingleton.elim _ (subsingleton_of_zero_eq_one R H) _ _ else
+begin
+  simp_rw [linear_equiv_matrix, linear_equiv.trans_apply, linear_equiv_matrix'_apply,
+    ← equiv.of_injective_apply _ (hv₁.injective H), ← equiv.of_injective_apply _ (hv₂.injective H),
+    to_matrix_of_equiv, ← linear_equiv.trans_apply, linear_equiv.arrow_congr_trans], congr' 3;
+  refine function.left_inverse.injective linear_equiv.symm_symm _; ext x;
+  simp_rw [linear_equiv.symm_trans_apply, equiv_fun_basis_symm_apply, fun_congr_left_symm,
+    fun_congr_left_apply, fun_left_apply],
+  convert (finset.sum_equiv (equiv.of_injective _ (hv₁.injective H)) _).symm,
+  simp_rw [equiv.symm_apply_apply, equiv.of_injective_apply, subtype.coe_mk],
+  convert (finset.sum_equiv (equiv.of_injective _ (hv₂.injective H)) _).symm,
+  simp_rw [equiv.symm_apply_apply, equiv.of_injective_apply, subtype.coe_mk]
+end
+
 end linear_equiv_matrix
 
 namespace matrix
@@ -190,6 +235,25 @@ lemma comp_to_matrix_mul {R : Type v} [comm_ring R] [decidable_eq l] [decidable_
 suffices (f.comp g) = (f.to_matrix ⬝ g.to_matrix).to_lin, by rw [this, to_lin_to_matrix],
 by rw [mul_to_lin, to_matrix_to_lin, to_matrix_to_lin]
 
+lemma linear_equiv_matrix_comp {R ι κ μ M₁ M₂ M₃ : Type*} [comm_ring R]
+  [add_comm_group M₁] [module R M₁]
+  [add_comm_group M₂] [module R M₂]
+  [add_comm_group M₃] [module R M₃]
+  [fintype ι] [decidable_eq ι] [fintype κ] [decidable_eq κ] [fintype μ]
+  {v₁ : ι → M₁} {v₂ : κ → M₂} {v₃ : μ → M₃}
+  (hv₁ : is_basis R v₁) (hv₂ : is_basis R v₂) (hv₃ : is_basis R v₃)
+  (f : M₂ →ₗ[R] M₃) (g : M₁ →ₗ[R] M₂) :
+  linear_equiv_matrix hv₁ hv₃ (f.comp g) =
+  linear_equiv_matrix hv₂ hv₃ f ⬝ linear_equiv_matrix hv₁ hv₂ g :=
+by simp_rw [linear_equiv_matrix, linear_equiv.trans_apply, linear_equiv_matrix'_apply,
+    linear_equiv.arrow_congr_comp _ (equiv_fun_basis hv₂), comp_to_matrix_mul]
+
+lemma linear_equiv_matrix_mul {R M ι : Type*} [comm_ring R]
+  [add_comm_group M] [module R M] [fintype ι] [decidable_eq ι]
+  {b : ι → M} (hb : is_basis R b) (f g : M →ₗ[R] M) :
+  linear_equiv_matrix hb hb (f * g) = linear_equiv_matrix hb hb f * linear_equiv_matrix hb hb g :=
+linear_equiv_matrix_comp hb hb hb f g
+
 section trace
 
 variables {R : Type v} {M : Type w} [ring R] [add_comm_group M] [module R M]
@@ -332,6 +396,87 @@ end finite_dimensional
 
 end matrix
 
+namespace linear_map
+
+open_locale matrix
+
+/-- The trace of an endomorphism given a basis. -/
+def trace_aux (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M]
+  {ι : Type w} [fintype ι] [decidable_eq ι] {b : ι → M} (hb : is_basis R b) :
+  (M →ₗ[R] M) →ₗ[R] R :=
+(matrix.trace ι R R).comp $ linear_equiv_matrix hb hb
+
+@[simp] lemma trace_aux_def (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M]
+  {ι : Type w} [fintype ι] [decidable_eq ι] {b : ι → M} (hb : is_basis R b) (f : M →ₗ[R] M) :
+  trace_aux R hb f = matrix.trace ι R R (linear_equiv_matrix hb hb f) :=
+rfl
+
+theorem trace_aux_eq' (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M]
+  {ι : Type w} [fintype ι] [decidable_eq ι] {b : ι → M} (hb : is_basis R b)
+  {κ : Type w} [fintype κ] [decidable_eq κ] {c : κ → M} (hc : is_basis R c) :
+  trace_aux R hb = trace_aux R hc :=
+linear_map.ext $ λ f,
+calc  matrix.trace ι R R (linear_equiv_matrix hb hb f)
+    = matrix.trace ι R R (linear_equiv_matrix hb hb ((linear_map.id.comp f).comp linear_map.id)) :
+  by rw [linear_map.id_comp, linear_map.comp_id]
+... = matrix.trace ι R R (linear_equiv_matrix hc hb linear_map.id ⬝
+        linear_equiv_matrix hc hc f ⬝
+        linear_equiv_matrix hb hc linear_map.id) :
+  by rw [matrix.linear_equiv_matrix_comp _ hc, matrix.linear_equiv_matrix_comp _ hc]
+... = matrix.trace κ R R (linear_equiv_matrix hc hc f ⬝
+        linear_equiv_matrix hb hc linear_map.id ⬝
+        linear_equiv_matrix hc hb linear_map.id) :
+  by rw [matrix.mul_assoc, matrix.trace_mul_comm]
+... = matrix.trace κ R R (linear_equiv_matrix hc hc ((f.comp linear_map.id).comp linear_map.id)) :
+  by rw [matrix.linear_equiv_matrix_comp _ hb, matrix.linear_equiv_matrix_comp _ hc]
+... = matrix.trace κ R R (linear_equiv_matrix hc hc f) :
+  by rw [linear_map.comp_id, linear_map.comp_id]
+
+open_locale classical
+
+theorem trace_aux_range (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M]
+  {ι : Type w} [fintype ι] {b : ι → M} (hb : is_basis R b) :
+  trace_aux R hb.range = trace_aux R hb :=
+linear_map.ext $ λ f, if H : 0 = 1 then @subsingleton.elim _ (subsingleton_of_zero_eq_one R H) _ _ else
+begin
+  change ∑ i : set.range b, _ = ∑ i : ι, _, simp_rw [matrix.diag_apply], symmetry,
+  convert finset.sum_equiv (equiv.of_injective _ $ hb.injective H) _, ext i,
+  exact (linear_equiv_matrix_range hb hb f i i).symm
+end
+
+/-- where `ι` and `κ` can reside in different universes -/
+theorem trace_aux_eq (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M]
+  {ι : Type*} [fintype ι] [decidable_eq ι] {b : ι → M} (hb : is_basis R b)
+  {κ : Type*} [fintype κ] [decidable_eq κ] {c : κ → M} (hc : is_basis R c) :
+  trace_aux R hb = trace_aux R hc :=
+calc  trace_aux R hb
+    = trace_aux R hb.range : by { rw trace_aux_range R hb, congr }
+... = trace_aux R hc.range : trace_aux_eq' _ _ _
+... = trace_aux R hc : by { rw trace_aux_range R hc, congr }
+
+/-- Trace of an endomorphism independent of basis. -/
+def trace (R : Type u) [comm_ring R] (M : Type v) [add_comm_group M] [module R M] :
+  (M →ₗ[R] M) →ₗ[R] R :=
+if H : ∃ s : finset M, is_basis R (λ x, x : (↑s : set M) → M)
+then trace_aux R (classical.some_spec H)
+else 0
+
+theorem trace_eq_matrix_trace (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M]
+  {ι : Type w} [fintype ι] {b : ι → M} (hb : is_basis R b) (f : M →ₗ[R] M) :
+  trace R M f = matrix.trace ι R R (linear_equiv_matrix hb hb f) :=
+have ∃ s : finset M, is_basis R (λ x, x : (↑s : set M) → M),
+from ⟨finset.univ.image b,
+  by { rw [finset.coe_image, finset.coe_univ, set.image_univ], exact hb.range }⟩,
+by { rw [trace, dif_pos this, ← trace_aux_def], congr' 1, apply trace_aux_eq }
+
+theorem trace_mul_comm (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M]
+  (f g : M →ₗ[R] M) : trace R M (f * g) = trace R M (g * f) :=
+if H : ∃ s : finset M, is_basis R (λ x, x : (↑s : set M) → M) then let ⟨s, hb⟩ := H in
+by { simp_rw [trace_eq_matrix_trace R hb, matrix.linear_equiv_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
+
 /-- The natural equivalence between linear endomorphisms of finite free modules and square matrices
 is compatible with the algebra structures. -/
 def alg_equiv_matrix' {R : Type v} [comm_ring R] [decidable_eq n] :