sum_counit_smul — Mathlib

English

For any f, the sum over repr of f applied to right parts with counit on left is equal to the mapped f(a) tensored with 1.

Русский

Сумма по представлениям f(правые) с counit слева равна f(a) ⊗ 1.

LaTeX

$$$\\sum_{i \\in \\mathrm{repr}.index} f(\\mathrm{repr.left}(i)) \\otimes_{R} \\operatorname{counit}(\\mathrm{repr.right}(i)) = f(a) \\otimes 1.$$$

Lean4

theorem sum_counit_smul (𝓡 : Repr R a) : ∑ x ∈ 𝓡.index, counit (R := R) (𝓡.left x) • 𝓡.right x = a := by
  simpa only [map_sum, TensorProduct.lift.tmul, LinearMap.lsmul_apply, one_smul] using
    congr(TensorProduct.lift (LinearMap.lsmul R A) $(sum_counit_tmul_eq (R := R) 𝓡))

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