Trace of a linear map

This file defines the trace of a linear map.

See also LinearAlgebra/Matrix/Trace.lean for the trace of a matrix.

Tags

linear_map, trace, diagonal

def LinearMap.traceAux (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {ι : Type w} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) : (M →ₗ[R] M) →ₗ[R] R

The trace of an endomorphism given a basis.

Equations

• LinearMap.traceAux R b = LinearMap.comp (Matrix.traceLinearMap ι R R) ↑(LinearMap.toMatrix b b)

theorem LinearMap.traceAux_def (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {ι : Type w} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (f : M →ₗ[R] M) : ↑(LinearMap.traceAux R b) f = Matrix.trace (↑(LinearMap.toMatrix b b) f)

theorem LinearMap.traceAux_eq (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {ι : Type w} [DecidableEq ι] [Fintype ι] {κ : Type u_1} [DecidableEq κ] [Fintype κ] (b : Basis ι R M) (c : Basis κ R M) : LinearMap.traceAux R b = LinearMap.traceAux R c

def LinearMap.trace (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : (M →ₗ[R] M) →ₗ[R] R

Trace of an endomorphism independent of basis.

Equations

• LinearMap.trace R M = if H : ∃ s, Nonempty (Basis { x // x ∈ s } R M) then LinearMap.traceAux R (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose H } R M))) else 0

theorem LinearMap.trace_eq_matrix_trace_of_finset (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {s : Finset M} (b : Basis { x // x ∈ s } R M) (f : M →ₗ[R] M) : ↑(LinearMap.trace R M) f = Matrix.trace (↑(LinearMap.toMatrix b b) f)

Auxiliary lemma for trace_eq_matrix_trace.

theorem LinearMap.trace_eq_matrix_trace (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {ι : Type w} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (f : M →ₗ[R] M) : ↑(LinearMap.trace R M) f = Matrix.trace (↑(LinearMap.toMatrix b b) f)

theorem LinearMap.trace_mul_comm (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) (g : M →ₗ[R] M) : ↑(LinearMap.trace R M) (f * g) = ↑(LinearMap.trace R M) (g * f)

theorem LinearMap.trace_mul_cycle (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) (g : M →ₗ[R] M) (h : M →ₗ[R] M) : ↑(LinearMap.trace R M) (f * g * h) = ↑(LinearMap.trace R M) (h * f * g)

theorem LinearMap.trace_mul_cycle' (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) (g : M →ₗ[R] M) (h : M →ₗ[R] M) : ↑(LinearMap.trace R M) (f * (g * h)) = ↑(LinearMap.trace R M) (h * (f * g))

@[simp]

theorem LinearMap.trace_conj (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (g : M →ₗ[R] M) (f : (M →ₗ[R] M)ˣ) : ↑(LinearMap.trace R M) (↑f * g * ↑f⁻¹) = ↑(LinearMap.trace R M) g

The trace of an endomorphism is invariant under conjugation

theorem LinearMap.trace_eq_contract_of_basis {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_5} [Finite ι] (b : Basis ι R M) : LinearMap.comp (LinearMap.trace R M) (dualTensorHom R M M) = contractLeft R M

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

theorem LinearMap.trace_eq_contract_of_basis' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (b : Basis ι R M) : LinearMap.trace R M = LinearMap.comp (contractLeft R M) ↑(LinearEquiv.symm (dualTensorHomEquivOfBasis b))

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

@[simp]

theorem LinearMap.trace_eq_contract (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] : LinearMap.comp (LinearMap.trace R M) (dualTensorHom R M M) = contractLeft 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 LinearMap.trace_eq_contract_apply (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (x : TensorProduct R (Module.Dual R M) M) : ↑(LinearMap.trace R M) (↑(dualTensorHom R M M) x) = ↑(contractLeft R M) x

theorem LinearMap.trace_eq_contract' (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] : LinearMap.trace R M = LinearMap.comp (contractLeft R M) ↑(LinearEquiv.symm (dualTensorHomEquiv 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 LinearMap.trace_one (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] : ↑(LinearMap.trace R M) 1 = ↑(FiniteDimensional.finrank R M)

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

@[simp]

theorem LinearMap.trace_id (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] : ↑(LinearMap.trace R M) LinearMap.id = ↑(FiniteDimensional.finrank R M)

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

@[simp]

theorem LinearMap.trace_transpose (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] : LinearMap.comp (LinearMap.trace R (Module.Dual R M)) Module.Dual.transpose = LinearMap.trace R M

theorem LinearMap.trace_prodMap (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (N : Type u_3) [AddCommGroup N] [Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] : LinearMap.comp (LinearMap.trace R (M × N)) (LinearMap.prodMapLinear R M N M N R) = LinearMap.comp (LinearMap.coprod LinearMap.id LinearMap.id) (LinearMap.prodMap (LinearMap.trace R M) (LinearMap.trace R N))

theorem LinearMap.trace_prodMap' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] (f : M →ₗ[R] M) (g : N →ₗ[R] N) : ↑(LinearMap.trace R (M × N)) (LinearMap.prodMap f g) = ↑(LinearMap.trace R M) f + ↑(LinearMap.trace R N) g

theorem LinearMap.trace_tensorProduct (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (N : Type u_3) [AddCommGroup N] [Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] : LinearMap.compr₂ (TensorProduct.mapBilinear R M N M N) (LinearMap.trace R (TensorProduct R M N)) = LinearMap.compl₁₂ (LinearMap.lsmul R R) (LinearMap.trace R M) (LinearMap.trace R N)

theorem LinearMap.trace_comp_comm (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (N : Type u_3) [AddCommGroup N] [Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] : LinearMap.compr₂ (LinearMap.llcomp R M N M) (LinearMap.trace R M) = LinearMap.compr₂ (LinearMap.flip (LinearMap.llcomp R N M N)) (LinearMap.trace R N)

@[simp]

theorem LinearMap.trace_transpose' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) : ↑(LinearMap.trace R (Module.Dual R M)) (↑Module.Dual.transpose f) = ↑(LinearMap.trace R M) f

theorem LinearMap.trace_tensorProduct' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] (f : M →ₗ[R] M) (g : N →ₗ[R] N) : ↑(LinearMap.trace R (TensorProduct R M N)) (TensorProduct.map f g) = ↑(LinearMap.trace R M) f * ↑(LinearMap.trace R N) g

theorem LinearMap.trace_comp_comm' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] (f : M →ₗ[R] N) (g : N →ₗ[R] M) : ↑(LinearMap.trace R M) (LinearMap.comp g f) = ↑(LinearMap.trace R N) (LinearMap.comp f g)

theorem LinearMap.trace_comp_cycle {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} {P : Type u_4} [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] [Module.Free R N] [Module.Finite R N] [Module.Free R P] [Module.Finite R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : P →ₗ[R] M) : ↑(LinearMap.trace R P) (LinearMap.comp g (LinearMap.comp f h)) = ↑(LinearMap.trace R N) (LinearMap.comp f (LinearMap.comp h g))

theorem LinearMap.trace_comp_cycle' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} {P : Type u_4} [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] [Module.Free R M] [Module.Finite R M] [Module.Free R P] [Module.Finite R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : P →ₗ[R] M) : ↑(LinearMap.trace R P) (LinearMap.comp (LinearMap.comp g f) h) = ↑(LinearMap.trace R M) (LinearMap.comp (LinearMap.comp h g) f)

@[simp]

theorem LinearMap.trace_conj' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] (f : M →ₗ[R] M) (e : M ≃ₗ[R] N) : ↑(LinearMap.trace R N) (↑(LinearEquiv.conj e) f) = ↑(LinearMap.trace R M) f

theorem LinearMap.IsProj.trace {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {p : Submodule R M} {f : M →ₗ[R] M} (h : LinearMap.IsProj p f) [Module.Free R { x // x ∈ p }] [Module.Finite R { x // x ∈ p }] [Module.Free R { x // x ∈ LinearMap.ker f }] [Module.Finite R { x // x ∈ LinearMap.ker f }] : ↑(LinearMap.trace R M) f = ↑(FiniteDimensional.finrank R { x // x ∈ p })

theorem LinearMap.isNilpotent_trace_of_isNilpotent {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {f : M →ₗ[R] M} (hf : IsNilpotent f) : IsNilpotent (↑(LinearMap.trace R M) f)