mathlib documentation

linear_algebra.trace

Trace of a linear map #

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) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {ι : Type w} [decidable_eq ι] [fintype ι] (b : basis ι 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) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {ι : Type w} [decidable_eq ι] [fintype ι] (b : basis ι R M) (f : M →ₗ[R] M) :
theorem linear_map.trace_aux_eq (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {ι : Type w} [decidable_eq ι] [fintype ι] {κ : Type u_1} [decidable_eq κ] [fintype κ] (b : basis ι R M) (c : basis κ R M) :
noncomputable def linear_map.trace (R : Type u) [comm_ring R] (M : Type v) [add_comm_group M] [module R 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) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {s : finset M} (b : basis s R M) (f : M →ₗ[R] M) :

Auxiliary lemma for trace_eq_matrix_trace.

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

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} [add_comm_group M] [module R M] {ι : Type u_4} [fintype ι] (b : basis ι R 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} [add_comm_group M] [module R M] {ι : Type u_4} [fintype ι] [decidable_eq ι] (b : basis ι 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) [add_comm_group M] [module R M] [module.free R M] [module.finite R 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_eq_contract_apply (R : Type u_1) [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] [module.free R M] [module.finite R M] [nontrivial R] (x : tensor_product R (module.dual R 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_one (R : Type u_1) [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] [module.free R M] [module.finite R M] [nontrivial R] :

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

theorem linear_map.trace_comp_comm (R : Type u_1) [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] (N : Type u_3) [add_comm_group N] [module R N] [module.free R M] [module.finite R M] [module.free R N] [module.finite R N] [nontrivial R] :
theorem linear_map.trace_comp_comm' {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (N : Type u_3) [add_comm_group N] [module R N] [module.free R M] [module.finite R M] [module.free R N] [module.finite R N] [nontrivial R] (f : M →ₗ[R] N) (g : N →ₗ[R] M) :
@[simp]
theorem linear_map.trace_conj' {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (N : Type u_3) [add_comm_group N] [module R N] [module.free R M] [module.finite R M] [module.free R N] [module.finite R N] [nontrivial R] (f : M →ₗ[R] M) (e : M ≃ₗ[R] N) :