Basic facts about the trace

Mathlib's LinearMap.trace R M is defined through a finite basis of M, and is 0 when M has none. This file names that case of the definition, so that proofs need not unfold LinearMap.trace. It also computes the trace of an endomorphism whose range lies in a free submodule with a given basis, as the trace of its matrix in that basis.

Main results

• TauCeti.LinearMap.trace_eq_zero_of_not_exists_basis: the trace vanishes on a module with no finite basis.
• TauCeti.LinearMap.trace_eq_zero_of_not_finite: the trace vanishes on a module that is not finite.
• LinearMap.eq_trace_smul_one_of_finrank_eq_one: on a free module of rank one, an endomorphism is its trace times the identity.
• LinearMap.trace_eq_sum_of_range_le_of_apply_single_eq: the trace of an endomorphism whose range lies in a free submodule ι → R is the trace of its matrix there.

theorem TauCeti.LinearMap.trace_eq_zero_of_not_exists_basis {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (h : ¬∃ (s : Finset M), Nonempty (Module.Basis (↥s) R M)) : LinearMap.trace R M = 0

The trace vanishes on a module with no finite basis. This is the endomorphism counterpart of Algebra.trace_eq_zero_of_not_exists_basis.

theorem TauCeti.LinearMap.trace_eq_zero_of_not_finite {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (h : ¬Module.Finite R M) : LinearMap.trace R M = 0

The trace vanishes on a module that is not finite.

theorem LinearMap.eq_trace_smul_one_of_finrank_eq_one {R : Type u_1} {V : Type u_2} [CommSemiring R] [AddCommMonoid V] [Module R V] [Module.Free R V] (h : Module.finrank R V = 1) (f : V →ₗ[R] V) : f = (trace R V) f • 1

On a free module of rank one, an endomorphism is its trace times the identity.

theorem LinearMap.trace_eq_sum_of_range_le_of_apply_single_eq {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [Fintype ι] [DecidableEq ι] {φ : (ι → R) →ₗ[R] M} (hφ : Function.Injective ⇑φ) {L : M →ₗ[R] M} (hL : L.range ≤ φ.range) {a : ι → ι → R} (hLa : ∀ (j : ι), L (φ (Pi.single j 1)) = φ (a j)) : (trace R M) L = ∑ j : ι, a j j

The trace of an endomorphism with range in a free submodule. Let φ be an injective linear map from ι → R to M, and let L be an endomorphism whose range lies in the range of φ and that sends the image under φ of the j-th standard basis vector of ι → R to φ (a j). Then the trace of L is the trace ∑ j, a j j of a.