English
Summing counit-weighted right components with scalar action recovers the original element a.
Русский
Суммирование counit, умножаемое на правые компоненты с действием скаляра восстанавливает исходный элемент a.
LaTeX
$$$\\sum_{x \\in 𝓡.index} \\operatorname{counit}(𝓡.left x) \\cdot 𝓡.right x = a.$$$
Lean4
@[simp]
theorem sum_map_tmul_counit_eq {B : Type*} [AddCommMonoid B] [Module R B] {F : Type*} [FunLike F A B]
[LinearMapClass F R A B] (f : F) (a : A) {repr : Repr R a} :
∑ i ∈ repr.index, f (repr.left i) ⊗ₜ counit (R := R) (repr.right i) = f a ⊗ₜ[R] 1 :=
by
have := sum_tmul_counit_eq repr
apply_fun LinearMap.rTensor R (f : A →ₗ[R] B) at this
simp_all only [map_sum, LinearMap.rTensor_tmul, LinearMap.coe_coe]
-- Cannot be @[simp] because `a₁` cannot be inferred by `simp`.
