counit_def — Mathlib

English

The counit on the tensor product of two coalgebras over S is the composition of the rid map with the map on counits; i.e., counit_{A⊗B} = rid ∘ map counit counit.

Русский

counit на тензорном произведении коалгебр задаётся как композиция rid с отображением counit на-слоях; то есть counit_{A⊗B} = rid ∘ map counit counit.

LaTeX

$$$\operatorname{counit}_{A \otimes_R B} = \mathrm{AlgebraTensorModule.rid\; } R S S \; \circ_\ell \; \mathrm{AlgebraTensorModule.map}\;\big(\operatorname{counit}, \operatorname{counit}\big).$$$

Lean4

theorem counit_def :
    Coalgebra.counit (R := S) (A := A ⊗[R] B) =
      AlgebraTensorModule.rid R S S ∘ₗ AlgebraTensorModule.map counit counit :=
  rfl

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