toCoalgHom — Mathlib

English

Any F with a CoalgHomClass structure yields a canonical coercion to a coalgebra hom from A to B.

Русский

Любой F с структурой CoalgHomClass порождает каноническое включение в коалгебраический гомоморфизм A → B.

LaTeX

$$$\\text{toCoalgHom}(f) : A \\to_{R}^{coalg} B$$$

Lean4

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

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