rTensor_counit_comul — Mathlib

English

For any a in a coalgebra, applying the right tensor counit to the comultiplication yields 1 ⊗ a.

Русский

Для любого a в коалгебре применение правого тензорного counit к копуляции даёт 1 ⊗ a.

LaTeX

$$$\\mathrm{rTensor}_A(\\mathrm{counit})(\\mathrm{comul}(a)) = 1 \\otimes a.$$$

Lean4

@[simp]
theorem rTensor_counit_comul (a : A) : counit.rTensor A (comul a) = 1 ⊗ₜ[R] a :=
  LinearMap.congr_fun rTensor_counit_comp_comul a

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