English
For any representation of a coalgebra, the sum of left counit times mapped right equals 1 ⊗ f(a).
Русский
Для представления коалгебры сумма по индексу левой части counit, умноженная на отображённое правое, равна 1 ⊗ f(a).
LaTeX
$$$\\sum_{i \\in \\mathrm{repr}.index} \\operatorname{counit}(\\mathrm{repr.left}(i)) \\otimes f(\\mathrm{repr.right}(i)) = 1 \\otimes f(a).$$$
Lean4
@[simp]
theorem sum_counit_tmul_map_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, counit (R := R) (repr.left i) ⊗ₜ f (repr.right i) = 1 ⊗ₜ[R] f a :=
by
have := sum_counit_tmul_eq repr
apply_fun LinearMap.lTensor R (f : A →ₗ[R] B) at this
simp_all only [map_sum, LinearMap.lTensor_tmul, LinearMap.coe_coe]
