counit_eq_algHom_toLinearMap — Mathlib

English

The counit on the tensor product A ⊗[R] B equals the linear map obtained by composing the rid map with the map that applies counit on each factor.

Русский

Куниt на тензорном произведении A ⊗_R B равен линейному отображению, получаемому из rid и map, применяющего counit к каждому фактору.

LaTeX

$$Coalgebra.counit (R := S) (A := A ⊗[R] B) = ((Algebra.TensorProduct.rid _ _ _).toAlgHom.comp (Algebra.TensorProduct.map (Bialgebra.counitAlgHom S A) (Bialgebra.counitAlgHom R B))).toLinearMap$$

Lean4

theorem counit_eq_algHom_toLinearMap :
    Coalgebra.counit (R := S) (A := A ⊗[R] B) =
      ((Algebra.TensorProduct.rid _ _ _).toAlgHom.comp
          (Algebra.TensorProduct.map (Bialgebra.counitAlgHom S A) (Bialgebra.counitAlgHom R B))).toLinearMap :=
  rfl

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