# Documentation

Mathlib.LinearAlgebra.Trace

# Trace of a linear map #

This file defines the trace of a linear map.

See also LinearAlgebra/Matrix/Trace.lean for the trace of a matrix.

## Tags #

linear_map, trace, diagonal

def LinearMap.traceAux (R : Type u) [] {M : Type v} [] [Module R M] {ι : Type w} [] [] (b : Basis ι R M) :
(M →ₗ[R] M) →ₗ[R] R

The trace of an endomorphism given a basis.

Instances For
theorem LinearMap.traceAux_def (R : Type u) [] {M : Type v} [] [Module R M] {ι : Type w} [] [] (b : Basis ι R M) (f : M →ₗ[R] M) :
↑() f = Matrix.trace (↑() f)
theorem LinearMap.traceAux_eq (R : Type u) [] {M : Type v} [] [Module R M] {ι : Type w} [] [] {κ : Type u_1} [] [] (b : Basis ι R M) (c : Basis κ R M) :
def LinearMap.trace (R : Type u) [] (M : Type v) [] [Module R M] :
(M →ₗ[R] M) →ₗ[R] R

Trace of an endomorphism independent of basis.

Instances For
theorem LinearMap.trace_eq_matrix_trace_of_finset (R : Type u) [] {M : Type v} [] [Module R M] {s : } (b : Basis { x // x s } R M) (f : M →ₗ[R] M) :
↑() f = Matrix.trace (↑() f)

Auxiliary lemma for trace_eq_matrix_trace.

theorem LinearMap.trace_eq_matrix_trace (R : Type u) [] {M : Type v} [] [Module R M] {ι : Type w} [] [] (b : Basis ι R M) (f : M →ₗ[R] M) :
↑() f = Matrix.trace (↑() f)
theorem LinearMap.trace_mul_comm (R : Type u) [] {M : Type v} [] [Module R M] (f : M →ₗ[R] M) (g : M →ₗ[R] M) :
↑() (f * g) = ↑() (g * f)
theorem LinearMap.trace_mul_cycle (R : Type u) [] {M : Type v} [] [Module R M] (f : M →ₗ[R] M) (g : M →ₗ[R] M) (h : M →ₗ[R] M) :
↑() (f * g * h) = ↑() (h * f * g)
theorem LinearMap.trace_mul_cycle' (R : Type u) [] {M : Type v} [] [Module R M] (f : M →ₗ[R] M) (g : M →ₗ[R] M) (h : M →ₗ[R] M) :
↑() (f * (g * h)) = ↑() (h * (f * g))
@[simp]
theorem LinearMap.trace_conj (R : Type u) [] {M : Type v} [] [Module R M] (g : M →ₗ[R] M) (f : (M →ₗ[R] M)ˣ) :
↑() (f * g * f⁻¹) = ↑() g

The trace of an endomorphism is invariant under conjugation

theorem LinearMap.trace_eq_contract_of_basis {R : Type u_1} [] {M : Type u_2} [] [Module R M] {ι : Type u_5} [] (b : Basis ι R M) :

The trace of a linear map correspond to the contraction pairing under the isomorphism End(M) ≃ M* ⊗ M

theorem LinearMap.trace_eq_contract_of_basis' {R : Type u_1} [] {M : Type u_2} [] [Module R M] {ι : Type u_5} [] [] (b : Basis ι R M) :

The trace of a linear map correspond to the contraction pairing under the isomorphism End(M) ≃ M* ⊗ M

@[simp]
theorem LinearMap.trace_eq_contract (R : Type u_1) [] (M : Type u_2) [] [Module R M] [] [] :

When M is finite free, the trace of a linear map correspond to the contraction pairing under the isomorphism End(M) ≃ M* ⊗ M

@[simp]
theorem LinearMap.trace_eq_contract_apply (R : Type u_1) [] (M : Type u_2) [] [Module R M] [] [] (x : TensorProduct R () M) :
↑() (↑() x) = ↑() x
theorem LinearMap.trace_eq_contract' (R : Type u_1) [] (M : Type u_2) [] [Module R M] [] [] :
= LinearMap.comp () ↑()

When M is finite free, the trace of a linear map correspond to the contraction pairing under the isomorphism End(M) ≃ M* ⊗ M

@[simp]
theorem LinearMap.trace_one (R : Type u_1) [] (M : Type u_2) [] [Module R M] [] [] :
↑() 1 = ↑()

The trace of the identity endomorphism is the dimension of the free module

@[simp]
theorem LinearMap.trace_id (R : Type u_1) [] (M : Type u_2) [] [Module R M] [] [] :
↑() LinearMap.id = ↑()

The trace of the identity endomorphism is the dimension of the free module

@[simp]
theorem LinearMap.trace_transpose (R : Type u_1) [] (M : Type u_2) [] [Module R M] [] [] :
LinearMap.comp (LinearMap.trace R ()) Module.Dual.transpose =
theorem LinearMap.trace_prodMap (R : Type u_1) [] (M : Type u_2) [] [Module R M] (N : Type u_3) [] [Module R N] [] [] [] [] :
theorem LinearMap.trace_prodMap' {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] [] [] [] [] (f : M →ₗ[R] M) (g : N →ₗ[R] N) :
↑(LinearMap.trace R (M × N)) () = ↑() f + ↑() g
theorem LinearMap.trace_tensorProduct (R : Type u_1) [] (M : Type u_2) [] [Module R M] (N : Type u_3) [] [Module R N] [] [] [] [] :
theorem LinearMap.trace_comp_comm (R : Type u_1) [] (M : Type u_2) [] [Module R M] (N : Type u_3) [] [Module R N] [] [] [] [] :
@[simp]
theorem LinearMap.trace_transpose' {R : Type u_1} [] {M : Type u_2} [] [Module R M] [] [] (f : M →ₗ[R] M) :
↑(LinearMap.trace R ()) (Module.Dual.transpose f) = ↑() f
theorem LinearMap.trace_tensorProduct' {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] [] [] [] [] (f : M →ₗ[R] M) (g : N →ₗ[R] N) :
↑(LinearMap.trace R ()) () = ↑() f * ↑() g
theorem LinearMap.trace_comp_comm' {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] [] [] [] [] (f : M →ₗ[R] N) (g : N →ₗ[R] M) :
↑() () = ↑() ()
theorem LinearMap.trace_comp_cycle {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} {P : Type u_4} [] [Module R N] [] [Module R P] [] [] [] [] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : P →ₗ[R] M) :
↑() (LinearMap.comp g ()) = ↑() (LinearMap.comp f ())
theorem LinearMap.trace_comp_cycle' {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} {P : Type u_4} [] [Module R N] [] [Module R P] [] [] [] [] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : P →ₗ[R] M) :
↑() (LinearMap.comp () h) = ↑() (LinearMap.comp () f)
@[simp]
theorem LinearMap.trace_conj' {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] [] [] [] [] (f : M →ₗ[R] M) (e : M ≃ₗ[R] N) :
↑() (↑() f) = ↑() f
theorem LinearMap.IsProj.trace {R : Type u_1} [] {M : Type u_2} [] [Module R M] [] [] {p : } {f : M →ₗ[R] M} (h : ) [Module.Free R { x // x p }] [Module.Finite R { x // x p }] [Module.Free R { x // }] [Module.Finite R { x // }] :
↑() f = ↑(FiniteDimensional.finrank R { x // x p })
theorem LinearMap.isNilpotent_trace_of_isNilpotent {R : Type u_1} [] {M : Type u_2} [] [Module R M] [] [] {f : M →ₗ[R] M} (hf : ) :
IsNilpotent (↑() f)