trace_eq_sum_trace_restrict' — Mathlib

English

The trace of a linear map equals the sum of traces on restricted components, with a refined internal decomposition.

Русский

След линейного отображения равен сумме следов на ограниченных компонентах при более точной внутренней декомпозиции.

LaTeX

$$trace_eq_sum_trace_restrict' …$$

Lean4

theorem trace_eq_sum_trace_restrict' (h : IsInternal N) (hN : {i | N i ≠ ⊥}.Finite) {f : M →ₗ[R] M}
    (hf : ∀ i, MapsTo f (N i) (N i)) : trace R M f = ∑ i ∈ hN.toFinset, trace R (N i) (f.restrict (hf i)) :=
  by
  let _ : Fintype { i // N i ≠ ⊥ } := hN.fintype
  let _ : Fintype {i | N i ≠ ⊥} := hN.fintype
  rw [← Finset.sum_coe_sort, trace_eq_sum_trace_restrict (isInternal_ne_bot_iff.mpr h) (hf ·)]
  exact Fintype.sum_equiv hN.subtypeEquivToFinset _ _ (fun i ↦ rfl)

Похожие утверждения