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)
[comm_semiring R]
{M : Type v}
[add_comm_monoid 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_linear_map ι R R).comp ↑(linear_map.to_matrix b b)
theorem
linear_map.trace_aux_def
(R : Type u)
[comm_semiring R]
{M : Type v}
[add_comm_monoid M]
[module R M]
{ι : Type w}
[decidable_eq ι]
[fintype ι]
(b : basis ι R M)
(f : M →ₗ[R] M) :
⇑(linear_map.trace_aux R b) f = (⇑(linear_map.to_matrix b b) f).trace
theorem
linear_map.trace_aux_eq
(R : Type u)
[comm_semiring R]
{M : Type v}
[add_comm_monoid 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_semiring R]
(M : Type v)
[add_comm_monoid M]
[module R M] :
Trace of an endomorphism independent of basis.
theorem
linear_map.trace_eq_matrix_trace_of_finset
(R : Type u)
[comm_semiring R]
{M : Type v}
[add_comm_monoid M]
[module R M]
{s : finset M}
(b : basis ↥s R M)
(f : M →ₗ[R] M) :
⇑(linear_map.trace R M) f = (⇑(linear_map.to_matrix b b) f).trace
Auxiliary lemma for trace_eq_matrix_trace.
theorem
linear_map.trace_eq_matrix_trace
(R : Type u)
[comm_semiring R]
{M : Type v}
[add_comm_monoid M]
[module R M]
{ι : Type w}
[decidable_eq ι]
[fintype ι]
(b : basis ι R M)
(f : M →ₗ[R] M) :
⇑(linear_map.trace R M) f = (⇑(linear_map.to_matrix b b) f).trace
theorem
linear_map.trace_mul_comm
(R : Type u)
[comm_semiring R]
{M : Type v}
[add_comm_monoid 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_semiring R]
{M : Type v}
[add_comm_monoid 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
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}
[finite ι]
(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
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] :
(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
@[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) :
⇑(linear_map.trace R M) (⇑(dual_tensor_hom R M M) x) = ⇑(contract_left R M) x
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] :
linear_map.trace R M = (contract_left R M).comp (dual_tensor_hom_equiv R M M).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
@[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] :
⇑(linear_map.trace R M) 1 = ↑(finite_dimensional.finrank R M)
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)
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M]
[nontrivial R] :
⇑(linear_map.trace R M) linear_map.id = ↑(finite_dimensional.finrank R M)
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)
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M]
[nontrivial R] :
(linear_map.trace R (module.dual R M)).comp module.dual.transpose = linear_map.trace R M
theorem
linear_map.trace_prod_map
(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] :
(linear_map.trace R (M × N)).comp (linear_map.prod_map_linear R M N M N R) = (linear_map.id.coprod linear_map.id).comp ((linear_map.trace R M).prod_map (linear_map.trace R N))
theorem
linear_map.trace_prod_map'
{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)
(g : N →ₗ[R] N) :
⇑(linear_map.trace R (M × N)) (f.prod_map g) = ⇑(linear_map.trace R M) f + ⇑(linear_map.trace R N) g
theorem
linear_map.trace_tensor_product
(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] :
(tensor_product.map_bilinear R M N M N).compr₂ (linear_map.trace R (tensor_product R M N)) = (linear_map.lsmul R R).compl₁₂ (linear_map.trace R M) (linear_map.trace R N)
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] :
(linear_map.llcomp R M N M).compr₂ (linear_map.trace R M) = (linear_map.llcomp R N M N).flip.compr₂ (linear_map.trace R N)
@[simp]
theorem
linear_map.trace_transpose'
{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]
(f : M →ₗ[R] M) :
⇑(linear_map.trace R (module.dual R M)) (⇑module.dual.transpose f) = ⇑(linear_map.trace R M) f
theorem
linear_map.trace_tensor_product'
{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)
(g : N →ₗ[R] N) :
⇑(linear_map.trace R (tensor_product R M N)) (tensor_product.map f g) = ⇑(linear_map.trace R M) f * ⇑(linear_map.trace R N) g
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) :
⇑(linear_map.trace R M) (g.comp f) = ⇑(linear_map.trace R N) (f.comp g)
@[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) :
⇑(linear_map.trace R N) (⇑(e.conj) f) = ⇑(linear_map.trace R M) f
theorem
linear_map.is_proj.trace
{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]
{p : submodule R M}
{f : M →ₗ[R] M}
(h : linear_map.is_proj p f)
[module.free R ↥p]
[module.finite R ↥p]
[module.free R ↥(linear_map.ker f)]
[module.finite R ↥(linear_map.ker f)] :
⇑(linear_map.trace R M) f = ↑(finite_dimensional.finrank R ↥p)