Trace of a linear map #

This file defines the trace of a linear map.

See also Mathlib/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 : Module.Basis ι R M) :

(M →ₗ[R] M) →ₗ[R] R

The trace of an endomorphism given a basis.

Equations

Instances For

source

📐 coverage

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

(traceAux R b) f = ((toMatrix b b) f).trace

source

📐 coverage

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 : Module.Basis ι R M) (c : Module.Basis κ R M) :

traceAux R b = traceAux R c

source

🔸 coverage

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

Instances For

source

📐 coverage

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 : Module.Basis (↥s) R M) (f : M →ₗ[R] M) :

(trace R M) f = ((toMatrix b b) f).trace

Auxiliary lemma for trace_eq_matrix_trace.

source

📐 coverage

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

(trace R M) f = ((toMatrix b b) f).trace

source

📐 coverage

@[simp]

theorem Matrix.trace_toLin_eq {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {ι : Type w} [DecidableEq ι] [Fintype ι] (A : Matrix ι ι R) (b : Module.Basis ι R M) :

(LinearMap.trace R M) ((toLin b b) A) = A.trace

source

📐 coverage

@[simp]

theorem Matrix.trace_toLin'_eq {R : Type u} [CommSemiring R] {ι : Type w} [DecidableEq ι] [Fintype ι] (A : Matrix ι ι R) :

(LinearMap.trace R (ι → R)) (toLin' A) = A.trace

source

📐 coverage

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

(trace R M) (f * g) = (trace R M) (g * f)

source

📐 coverage

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

(trace R M) (f * g * h) = (trace R M) (h * f * g)

source

📐 coverage

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

(trace R M) (f * (g * h)) = (trace R M) (h * (f * g))

source

📐 coverage

@[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)ˣ) :

(trace R M) (↑f * g * ↑f⁻¹) = (trace R M) g

The trace of an endomorphism is invariant under conjugation

source

📐 coverage

@[simp]

theorem LinearMap.trace_lie {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (f g : Module.End R M) :

(trace R M) ⁅f, g⁆ = 0

source

📐 coverage

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 : Module.Basis ι R M) :

trace R M ∘ₗ dualTensorHom R M M = contractLeft R M

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

source

📐 coverage

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 : Module.Basis ι R M) :

trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquivOfBasis b).symm

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

source

📐 coverage

@[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] :

trace R M ∘ₗ dualTensorHom R M M = contractLeft R M

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

source

📐 coverage

@[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) :

(trace R M) ((dualTensorHom R M M) x) = (contractLeft R M) x

source

📐 coverage

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] :

trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquiv R M M).symm

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

source

📐 coverage

@[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] :

(trace R M) 1 = ↑(Module.finrank R M)

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

source

📐 coverage

@[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] :

(trace R M) id = ↑(Module.finrank R M)

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

source

📐 coverage

@[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] :

trace R (Module.Dual R M) ∘ₗ Module.Dual.transpose = trace R M

source

📐 coverage

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] :

trace R (M × N) ∘ₗ prodMapLinear R M N M N R = id.coprod id ∘ₗ (trace R M).prodMap (trace R N)

source

📐 coverage

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) :

(trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g

source

📐 coverage

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] :

(TensorProduct.mapBilinear (RingHom.id R) M N M N).compr₂ (trace R (TensorProduct R M N)) = (lsmul R R).compl₁₂ (trace R M) (trace R N)

source

📐 coverage

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] :

(llcomp R M N M).compr₂ (trace R M) = (llcomp R N M N).flip.compr₂ (trace R N)

source

📐 coverage

@[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) :

(trace R (Module.Dual R M)) (Module.Dual.transpose f) = (trace R M) f

source

📐 coverage

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) :

(trace R (TensorProduct R M N)) (TensorProduct.map f g) = (trace R M) f * (trace R N) g

source

📐 coverage

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) :

(trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)

source

📐 coverage

@[simp]

theorem LinearMap.trace_smulRight {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] R) (x : M) :

(trace R M) (f.smulRight x) = f x

source

📐 coverage

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) :

(trace R P) (g ∘ₗ f ∘ₗ h) = (trace R N) (f ∘ₗ h ∘ₗ g)

source

📐 coverage

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) :

(trace R P) ((g ∘ₗ f) ∘ₗ h) = (trace R M) ((h ∘ₗ g) ∘ₗ f)

source

📐 coverage

@[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] (f : M →ₗ[R] M) (e : M ≃ₗ[R] N) :

(trace R N) (e.conj f) = (trace R M) f

source

📐 coverage

@[simp]

theorem LinearMap.trace_map {K : Type u_6} {V : Type u_7} {W : Type u_8} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] {F : Type u_9} [EquivLike F (Module.End K V) (Module.End K W)] [AlgEquivClass F K (Module.End K V) (Module.End K W)] (f : F) (x : Module.End K V) :

(trace K W) (f x) = (trace K V) x

source

📐 coverage

@[simp]

theorem Matrix.trace_map {K : Type u_6} {m : Type u_7} {n : Type u_8} [Field K] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] {F : Type u_9} [EquivLike F (Matrix m m K) (Matrix n n K)] [AlgEquivClass F K (Matrix m m K) (Matrix n n K)] (f : F) (x : Matrix m m K) :

(f x).trace = x.trace

source

📐 coverage

theorem LinearMap.IsProj.trace {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {p : Submodule R M} {f : M →ₗ[R] M} (h : IsProj p f) [Module.Free R ↥p] [Module.Finite R ↥p] [Module.Free R ↥f.ker] [Module.Finite R ↥f.ker] :

(LinearMap.trace R M) f = ↑(Module.finrank R ↥p)

source

📐 coverage

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

IsNilpotent ((trace R M) f)

source

📐 coverage

theorem LinearMap.trace_comp_eq_mul_of_commute_of_isNilpotent {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsReduced R] {f g : Module.End R M} (μ : R) (h_comm : Commute f g) (hg : IsNilpotent (g - (algebraMap R (Module.End R M)) μ)) :

(trace R M) (f ∘ₗ g) = μ * (trace R M) f

source

📐 coverage

@[simp]

theorem LinearMap.trace_baseChange {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) (A : Type u_6) [CommRing A] [Algebra R A] :

(trace A (TensorProduct R A M)) (baseChange A f) = (algebraMap R A) ((trace R M) f)

Documentation

Mathlib.LinearAlgebra.Trace

Trace of a linear map #

Tags #