# mathlib3documentation

linear_algebra.trace

# Trace of a linear map #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the trace of a linear map.

See also linear_algebra/matrix/trace.lean for the trace of a matrix.

## Tags #

linear_map, trace, diagonal

noncomputable def linear_map.trace_aux (R : Type u) {M : Type v} [ M] {ι : Type w} [decidable_eq ι] [fintype ι] (b : R M) :
(M →ₗ[R] M) →ₗ[R] R

The trace of an endomorphism given a basis.

Equations
theorem linear_map.trace_aux_def (R : Type u) {M : Type v} [ M] {ι : Type w} [decidable_eq ι] [fintype ι] (b : R M) (f : M →ₗ[R] M) :
b) f = ( b) f).trace
theorem linear_map.trace_aux_eq (R : Type u) {M : Type v} [ M] {ι : Type w} [decidable_eq ι] [fintype ι] {κ : Type u_1} [decidable_eq κ] [fintype κ] (b : R M) (c : R M) :
noncomputable def linear_map.trace (R : Type u) (M : Type v) [ M] :
(M →ₗ[R] M) →ₗ[R] R

Trace of an endomorphism independent of basis.

Equations
theorem linear_map.trace_eq_matrix_trace_of_finset (R : Type u) {M : Type v} [ M] {s : finset M} (b : R M) (f : M →ₗ[R] M) :
M) f = ( b) f).trace

Auxiliary lemma for trace_eq_matrix_trace.

theorem linear_map.trace_eq_matrix_trace (R : Type u) {M : Type v} [ M] {ι : Type w} [decidable_eq ι] [fintype ι] (b : R M) (f : M →ₗ[R] M) :
M) f = ( b) f).trace
theorem linear_map.trace_mul_comm (R : Type u) {M : Type v} [ M] (f g : M →ₗ[R] M) :
M) (f * g) = M) (g * f)
@[simp]
theorem linear_map.trace_conj (R : Type u) {M : Type v} [ M] (g : M →ₗ[R] M) (f : (M →ₗ[R] M)ˣ) :
M) (f * g * f⁻¹) = M) g

The trace of an endomorphism is invariant under conjugation

theorem linear_map.trace_eq_contract_of_basis {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {ι : Type u_4} [finite ι] (b : R M) :
M).comp M M) =

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

theorem linear_map.trace_eq_contract_of_basis' {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {ι : Type u_4} [fintype ι] [decidable_eq ι] (b : R M) :

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

@[simp]
theorem linear_map.trace_eq_contract (R : Type u_1) [comm_ring R] (M : Type u_2) [ M] [ M] [ M] [nontrivial R] :
M).comp M 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 linear_map.trace_eq_contract_apply (R : Type u_1) [comm_ring R] (M : Type u_2) [ M] [ M] [ M] [nontrivial R] (x : M) M) :
M) ( M M) x) = M) x
theorem linear_map.trace_eq_contract' (R : Type u_1) [comm_ring R] (M : Type u_2) [ M] [ M] [ M] [nontrivial R] :

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 linear_map.trace_one (R : Type u_1) [comm_ring R] (M : Type u_2) [ M] [ M] [ M] [nontrivial R] :
M) 1 =

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

@[simp]
theorem linear_map.trace_id (R : Type u_1) [comm_ring R] (M : Type u_2) [ M] [ M] [ M] [nontrivial R] :

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

@[simp]
theorem linear_map.trace_transpose (R : Type u_1) [comm_ring R] (M : Type u_2) [ M] [ M] [ M] [nontrivial R] :
theorem linear_map.trace_prod_map (R : Type u_1) [comm_ring R] (M : Type u_2) [ M] (N : Type u_3) [ N] [ M] [ M] [ N] [ N] [nontrivial R] :
(M × N)).comp M N R) = M).prod_map N))
theorem linear_map.trace_prod_map' {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {N : Type u_3} [ N] [ M] [ M] [ N] [ N] [nontrivial R] (f : M →ₗ[R] M) (g : N →ₗ[R] N) :
(M × N)) (f.prod_map g) = M) f + N) g
theorem linear_map.trace_tensor_product (R : Type u_1) [comm_ring R] (M : Type u_2) [ M] (N : Type u_3) [ N] [ M] [ M] [ N] [ N] [nontrivial R] :
M N).compr₂ M N)) = R).compl₁₂ M) N)
theorem linear_map.trace_comp_comm (R : Type u_1) [comm_ring R] (M : Type u_2) [ M] (N : Type u_3) [ N] [ M] [ M] [ N] [ N] [nontrivial R] :
N M).compr₂ M) = M N).flip.compr₂ N)
@[simp]
theorem linear_map.trace_transpose' {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] [ M] [ M] [nontrivial R] (f : M →ₗ[R] M) :
M)) = M) f
theorem linear_map.trace_tensor_product' {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {N : Type u_3} [ N] [ M] [ M] [ N] [ N] [nontrivial R] (f : M →ₗ[R] M) (g : N →ₗ[R] N) :
M N)) g) = M) f * N) g
theorem linear_map.trace_comp_comm' {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {N : Type u_3} [ N] [ M] [ M] [ N] [ N] [nontrivial R] (f : M →ₗ[R] N) (g : N →ₗ[R] M) :
M) (g.comp f) = N) (f.comp g)
@[simp]
theorem linear_map.trace_conj' {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {N : Type u_3} [ N] [ M] [ M] [ N] [ N] [nontrivial R] (f : M →ₗ[R] M) (e : M ≃ₗ[R] N) :
N) ((e.conj) f) = M) f
theorem linear_map.is_proj.trace {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] [ M] [ M] [nontrivial R] {p : M} {f : M →ₗ[R] M} (h : f) [ p] [ p] [ ] [ ] :
M) f =