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) :
The trace of an endomorphism given a basis.
Equations
- linear_map.trace_aux R b = (matrix.trace ι R R).comp ↑(linear_map.to_matrix b b)
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)
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] :
Trace of an endomorphism independent of basis.
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
.
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)
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)ˣ) :
⇑(linear_map.trace R M) (((↑f) * g) * ↑f⁻¹) = ⇑(linear_map.trace R M) g
The trace of an endomorphism is invariant under conjugation
@[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
@[simp]
theorem
linear_map.trace_one
(R : Type u)
[field R]
{M : Type v}
[add_comm_group M]
[module R M] :
⇑(linear_map.trace R M) 1 = ↑(finite_dimensional.finrank R M)
The trace of the identity endomorphism is the dimension of the vector space