English
Let k be a field. The category ModuleCat A is a k-linear category: for all M,N, the hom-sets Hom(M,N) are k-vector spaces and composition is bilinear; i.e., (f+g)∘h = f∘h + g∘h and h∘(r f) = r (h∘f) for all f,g: M→N, h: N→O, r ∈ k.
Русский
Пусть k — поле. Категория ModuleCat A является k-линейной категорией: для любых M,N множества гомоморфизмов Hom(M,N) образуют векторные пространства над k, и композиция линейна по каждому аргументу; то есть (f+g)∘h = f∘h + g∘h и h∘(r f) = r (h∘f) для любых f,g: M→N, h: N→O, r ∈ k.
LaTeX
$$$ \\forall M,N,O:\\; \\mathrm{Hom}(M,N) \\text{ is a } k\\text{-module},\\;\\text{and } (f+g)\\circ h = f\\circ h + g\\circ h,\\; h\\circ (r f) = r (h\\circ f).$$$
Lean4
instance linearOverField : Linear k (ModuleCat.{v} A) where homModule _ _ := inferInstance
