The trace as a closed loop of coevaluation and contraction #
For a finite-dimensional vector space V over a field K, Mathlib's coevaluation K V sends
1 to the canonical tensor ∑ i, bᵢ ⊗ bᵢ* of V ⊗ V*, and contractLeft K V contracts
V* ⊗ V to K. Inserting an endomorphism f on the V factor, swapping the two factors and
contracting gives ∑ i, bᵢ* (f bᵢ), which is the trace of f.
This is the linear-algebra content of the statement that in the rigid symmetric category of
finite-dimensional vector spaces the categorical trace of f is its linear trace.
Main results #
LinearMap.trace_eq_contractLeft_comm_rTensor_coevaluation: the trace offis the contraction of the swapped image of the coevaluation underf ⊗ id.
theorem
LinearMap.trace_eq_contractLeft_comm_rTensor_coevaluation
(K : Type u_1)
[Field K]
{V : Type u_2}
[AddCommGroup V]
[Module K V]
[FiniteDimensional K V]
(f : V →ₗ[K] V)
:
(trace K V) f = (contractLeft K V) ((TensorProduct.comm K V (Module.Dual K V)) ((rTensor (Module.Dual K V) f) ((coevaluation K V) 1)))
The trace of an endomorphism f of a finite-dimensional vector space is the contraction of
the canonical tensor coevaluation K V 1 after applying f to its V factor and swapping the
two factors.