feat(linear_algebra/trace): trace of projection maps (#14165)

This is proved under the `field` assumption instead of the finite free module assumptions generally used to talk about the trace because we need the submodules `p` and `f.ker` to also be free and finite.

- [x] depends on: #13872 


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

src/linear_algebra/contraction.lean

@@ -70,7 +70,7 @@ fst_apply, prod.smul_mk, zero_apply, smul_zero]}
   dual_tensor_hom R (M × N) (P × Q) ((g ∘ₗ snd R M N) ⊗ₜ inr R P Q q) :=
 by {ext; simp only [coe_comp, coe_inr, function.comp_app, prod_map_apply, dual_tensor_hom_apply,
   snd_apply, prod.smul_mk, zero_apply, smul_zero]}
-  
+
 lemma map_dual_tensor_hom (f : module.dual R M) (p : P) (g : module.dual R N) (q : Q) :
   tensor_product.map (dual_tensor_hom R M P (f ⊗ₜ[R] p)) (dual_tensor_hom R N Q (g ⊗ₜ[R] q)) =
   dual_tensor_hom R (M ⊗[R] N) (P ⊗[R] Q) (dual_distrib R M N (f ⊗ₜ g) ⊗ₜ[R] (p ⊗ₜ[R] q)) :=

src/linear_algebra/trace.lean

@@ -8,6 +8,7 @@ import linear_algebra.matrix.trace
 import linear_algebra.contraction
 import linear_algebra.tensor_product_basis
 import linear_algebra.free_module.strong_rank_condition
+import linear_algebra.projection
 
 /-!
 # Trace of a linear map
@@ -166,6 +167,10 @@ begin
   simp,
 end
 
+/-- The trace of the identity endomorphism is the dimension of the free module -/
+@[simp] theorem trace_id : trace R M id = (finrank R M : R) :=
+by rw [←one_eq_id, trace_one]
+
 theorem trace_prod_map :
   trace R (M × N) ∘ₗ prod_map_linear R M N M N R =
   (coprod id id : R × R →ₗ[R] R) ∘ₗ prod_map (trace R M) (trace R N) :=
@@ -251,6 +256,11 @@ end
 by rw [e.conj_apply, trace_comp_comm', ←comp_assoc, linear_equiv.comp_coe,
   linear_equiv.self_trans_symm, linear_equiv.refl_to_linear_map, id_comp]
 
+theorem is_proj.trace {p : submodule R M} {f : M →ₗ[R] M} (h : is_proj p f)
+  [module.free R p] [module.finite R p] [module.free R f.ker] [module.finite R f.ker] :
+  trace R M f = (finrank R p : R) :=
+by rw [h.eq_conj_prod_map, trace_conj', trace_prod_map', trace_id, map_zero, add_zero]
+
 end
 
 end linear_map