English
If V is R-linear and X,Y are objects of Action V G, then Action V G carries a natural structure of a linear category over R; in particular, each Hom-set is an R-module and composition is bilinear with respect to the R-action.
Русский
Если V линейна над R, и X,Y — объекты Action V G, то Action V G естественно является линейной категорией над R; в частности, каждая пара Hom-наборов образует модуль над R, а композиция линейна по отношению к действию R.
LaTeX
$$$\text{Action}(V,G)$ is a linear category over $R$; each $\mathrm{Hom}_{\mathrm{Action}(V,G)}(X,Y)$ is an $R$-module and composition is $R$-bilinear.$$
Lean4
instance : Linear R (Action V G)
where
homModule X
Y :=
{ smul := fun r f => ⟨r • f.hom, by simp [f.comm]⟩
one_smul := by intros; ext; exact one_smul _ _
smul_zero := by intros; ext; exact smul_zero _
zero_smul := by intros; ext; exact zero_smul _ _
add_smul := by intros; ext; exact add_smul _ _ _
smul_add := by intros; ext; exact smul_add _ _ _
mul_smul := by intros; ext; exact mul_smul _ _ _ }
smul_comp := by intros; ext; exact Linear.smul_comp _ _ _ _ _ _
comp_smul := by intros; ext; exact Linear.comp_smul _ _ _ _ _ _
