Traces of coordinate-reindexing maps

This file computes the trace of an endomorphism of a finite product that selects an input coordinate for each output coordinate and applies a linear endomorphism there. Only fixed coordinates contribute to the trace.

The results are linear-algebra inputs for character formulas of induced representations and finite direct sums of representations.

Main results

• LinearMap.trace_pi_of_apply_eq: the trace formula for a coordinate-reindexing map on a constant finite product.
• LinearMap.trace_piMap: the trace of a coordinatewise endomorphism LinearMap.piMap f of a finite dependent product is the sum of the traces of its components.

theorem LinearMap.trace_pi_of_apply_eq {k : Type u} {ι : Type v} {M : Type w} [CommRing k] [Fintype ι] [AddCommGroup M] [Module k M] [Module.Free k M] [Module.Finite k M] (T : (ι → M) →ₗ[k] ι → M) (σ : ι → ι) (f : ι → M →ₗ[k] M) (hT : ∀ (x : ι → M) (i : ι), T x i = (f i) (x (σ i))) : (trace k (ι → M)) T = ∑ i : ι, if σ i = i then (trace k M) (f i) else 0

The trace of a coordinate-reindexing endomorphism of a finite product is the sum of the traces on its fixed coordinates.

@[simp]

theorem LinearMap.trace_piMap {k : Type u} {ι : Type v} [CommRing k] [Fintype ι] {M : ι → Type u_1} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module k (M i)] [∀ (i : ι), Module.Free k (M i)] [∀ (i : ι), Module.Finite k (M i)] (f : (i : ι) → M i →ₗ[k] M i) : (trace k ((i : ι) → M i)) (piMap f) = ∑ i : ι, (trace k (M i)) (f i)

The trace of the coordinatewise endomorphism LinearMap.piMap f of a finite dependent product of finite free modules is the sum of the traces of the f i.