English
An alternate formulation of trace vanishing in presence of internal direct sum and mapsTo conditions.
Русский
Алтернативная формулировка исчезновения следа при наличии условий отображения.
LaTeX
$$trace_eq_zero_of_mapsTo_ne_alt$$
Lean4
/-- The trace of an endomorphism of a direct sum is the sum of the traces on each component.
See also `LinearMap.trace_restrict_eq_sum_trace_restrict`. -/
theorem trace_eq_sum_trace_restrict (h : IsInternal N) [Fintype ι] {f : M →ₗ[R] M} (hf : ∀ i, MapsTo f (N i) (N i)) :
trace R M f = ∑ i, trace R (N i) (f.restrict (hf i)) :=
by
let b : (i : ι) → Basis _ R (N i) := fun i ↦ Module.Free.chooseBasis R (N i)
simp_rw [trace_eq_matrix_trace R (h.collectedBasis b), toMatrix_directSum_collectedBasis_eq_blockDiagonal' h h b b hf,
Matrix.trace_blockDiagonal', ← trace_eq_matrix_trace]
