# Documentation

Mathlib.Algebra.DirectSum.LinearMap

# Linear maps between direct sums #

This file contains results about linear maps which respect direct sum decompositions of their domain and codomain.

theorem LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal' {ι : Type u_1} [] {R : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [] [] [Module R M₁] {N₁ : ιSubmodule R M₁} (h₁ : ) [] [Module R M₂] {N₂ : ιSubmodule R M₂} (h₂ : ) {κ₁ : ιType u_7} {κ₂ : ιType u_8} [(i : ι) → Fintype (κ₁ i)] [(i : ι) → Fintype (κ₂ i)] [(i : ι) → DecidableEq (κ₁ i)] [] (b₁ : (i : ι) → Basis (κ₁ i) R (N₁ i)) (b₂ : (i : ι) → Basis (κ₂ i) R (N₂ i)) {f : M₁ →ₗ[R] M₂} (hf : ∀ (i : ι), Set.MapsTo f (N₁ i) (N₂ i)) :
= Matrix.blockDiagonal' fun (i : ι) => (LinearMap.toMatrix (b₁ i) (b₂ i)) (LinearMap.restrict f (_ : Set.MapsTo f (N₁ i) (N₂ i)))

If a linear map f : M₁ → M₂ respects direct sum decompositions of M₁ and M₂, then it has a block diagonal matrix with respect to bases compatible with the direct sum decompositions.

theorem LinearMap.trace_eq_sum_trace_restrict {ι : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [Module R M] {N : ι} [] (h : ) [∀ (i : ι), Module.Finite R (N i)] [∀ (i : ι), Module.Free R (N i)] [] {f : M →ₗ[R] M} (hf : ∀ (i : ι), Set.MapsTo f (N i) (N i)) :
() f = Finset.sum Finset.univ fun (i : ι) => (LinearMap.trace R (N i)) (LinearMap.restrict f (_ : Set.MapsTo f (N i) (N i)))
theorem LinearMap.trace_eq_sum_trace_restrict' {ι : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [Module R M] {N : ι} [] (h : ) [∀ (i : ι), Module.Finite R (N i)] [∀ (i : ι), Module.Free R (N i)] (hN : Set.Finite {i : ι | N i }) {f : M →ₗ[R] M} (hf : ∀ (i : ι), Set.MapsTo f (N i) (N i)) :
() f = Finset.sum () fun (i : ι) => (LinearMap.trace R (N i)) (LinearMap.restrict f (_ : Set.MapsTo f (N i) (N i)))
theorem LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero {R : Type u_2} {M : Type u_3} [] [] [Module R M] [] [] [] {f : } {g : } (h_comm : Commute f g) (hf : ⨆ (μ : R), ⨆ (k : ), = ) (hg : ∀ (μ : R), (LinearMap.trace R (⨆ (k : ), )) (LinearMap.restrict g (_ : Set.MapsTo g (⨆ (k : ), ) (⨆ (k : ), ))) = 0) :
() () = 0

If f and g are commuting endomorphisms of a finite, free R-module M, such that f is triangularizable, then to prove that the trace of g ∘ f vanishes, it is sufficient to prove that the trace of g vanishes on each generalized eigenspace of f.