English
There is a canonical way to view an R-coalgebra X as an object of the category CoalgCat R: the object is obtained by equipping the underlying module X with the given coalgebra structure.
Русский
Существует канонический способ рассматривать R-коалгебру X как объект в категории CoalgCat R: объект получается путём надевания на базовую модульную структуру X данной структуры коалгебры.
LaTeX
$$$\\text{of} : (X , \\text{Coalgebra } R X) \\mapsto \\text{CoalgCat } R$$$
Lean4
/-- The object in the category of `R`-coalgebras associated to an `R`-coalgebra. -/
abbrev of (X : Type v) [AddCommGroup X] [Module R X] [Coalgebra R X] : CoalgCat R :=
{ ModuleCat.of R X with instCoalgebra := (inferInstance : Coalgebra R X) }
