English
For a type X with an additive group structure and an R-module structure, there is a canonical object of ModuleCat(R) corresponding to X.
Русский
Для типа X с аддитивной структурой и модульной структурой L над R существует канонический объект в ModuleCat(R), соответствующий X.
LaTeX
$$$ X \\text{ with } (X,+)\\text{ and } R\\text{-module structure} \\;\Rightarrow\\; \\mathrm{of}(R,X) \\in \\mathrm{ModuleCat}(R).$$$
Lean4
/-- The object in the category of R-algebras associated to a type equipped with the appropriate
typeclasses. This is the preferred way to construct a term of `ModuleCat R`. -/
abbrev of (X : Type v) [AddCommGroup X] [Module R X] : ModuleCat.{v} R :=
⟨X⟩
