toBialgHom — Mathlib

English

For any F in BialgHomClass, the counit composed with f equals the counit on A.

Русский

Для любого F в BialgHomClass композиция counit с f равна counit на A.

LaTeX

$$$ (counitAlgHom\\, R B) \\circ (f : A \\to_{R} B) = counitAlgHom\\, R A $$$

Lean4

/-- Turn an element of a type `F` satisfying `BialgHomClass F R A B` into an actual
`BialgHom`. This is declared as the default coercion from `F` to `A →ₐc[R] B`. -/
@[coe]
def toBialgHom (f : F) : A →ₐc[R] B :=
  { CoalgHomClass.toCoalgHom f, AlgHomClass.toAlgHom f with toFun := f }

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