sum_antipode_mul_eq_smul — Mathlib

English

For a representation repr of a comodule, the sum over indices of antipode(left i) times right i equals counit(a) times 1.

Русский

Для представления repr ко-модуля сумма по индексу i от antipode(left i) умноженного на right i равна counit(a) умноженное на 1.

LaTeX

$$$\sum_{i \in \text{repr.index}} \bigl( antipode\,R\,(\text{repr.left } i) \bigr) \cdot \bigl( \text{repr.right } i \bigr) = \mathrm{counit}\,(R\,a) \cdot 1$$$

Lean4

theorem sum_antipode_mul_eq_smul (repr : Repr R a) :
    ∑ i ∈ repr.index, antipode R (repr.left i) * repr.right i = counit (R := R) a • 1 := by
  rw [sum_antipode_mul_eq_algebraMap_counit, Algebra.smul_def, mul_one]

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