counitBialgHom — Mathlib

English

The counit of a bialgebra yields a map A →ₐc[R] R which agrees with the coalgebra counit on A.

Русский

Кунаитер биалгебры образует отображение A →ₐc[R] R, согласующееся с counit на коалгебре.

LaTeX

$$counitBialgHom : A →ₐc[R] R; counitBialgHom x = Coalgebra.counit x$$

Lean4

/-- The counit of a bialgebra as a `BialgHom`. -/
noncomputable def counitBialgHom : A →ₐc[R] R :=
  { Coalgebra.counitCoalgHom R A, counitAlgHom R A with }

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