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

source
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
source
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) :
⇑(linear_map.trace_aux R b) f = ⇑(matrix.trace ι R R) (⇑(linear_map.to_matrix b b) f)
source
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) :
linear_map.trace_aux R b = linear_map.trace_aux R c
source
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
source
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) :
⇑(linear_map.trace R M) f = ⇑(matrix.trace ↥s R R) (⇑(linear_map.to_matrix b b) f)

Auxiliary lemma for trace_eq_matrix_trace.

source
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) :
⇑(linear_map.trace R M) f = ⇑(matrix.trace ι R R) (⇑(linear_map.to_matrix b b) f)
source
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)
source
@[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)ˣ) :
⇑(linear_map.trace R M) (((↑f) * g) * ↑f⁻¹) = ⇑(linear_map.trace R M) g

The trace of an endomorphism is invariant under conjugation

source
@[simp]
theorem linear_map.trace_conj' (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] (f g : M →ₗ[R] M) [invertible f] :
⇑(linear_map.trace R M) ((f * g) * ⅟ f) = ⇑(linear_map.trace R M) g

The trace of an endomorphism is invariant under conjugation

source
theorem linear_map.trace_eq_contract_of_basis (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {ι : Type w} [fintype ι] (b : basis ι R M) :
(linear_map.trace R M).comp (dual_tensor_hom R M M) = contract_left R M

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

source
theorem linear_map.trace_eq_contract_of_basis' (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {ι : Type w} [fintype ι] [decidable_eq ι] (b : basis ι R M) :
linear_map.trace R M = (contract_left R M).comp (dual_tensor_hom_equiv_of_basis b).symm.to_linear_map

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

source
@[simp]
theorem linear_map.trace_eq_contract (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] [module.free R M] [module.finite R M] [nontrivial R] :
(linear_map.trace R M).comp (dual_tensor_hom R M M) = contract_left 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

source
theorem linear_map.trace_eq_contract' (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] [module.free R M] [module.finite R M] [nontrivial R] :
linear_map.trace R M = (contract_left R M).comp dual_tensor_hom_equiv.symm.to_linear_map

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

source
@[simp]
theorem linear_map.trace_one (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] [module.free R M] [module.finite R M] [nontrivial R] :
⇑(linear_map.trace R M) 1 = ↑(finite_dimensional.finrank R M)

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