English
For objects X, Y in a preadditive category C with a ring morphism φ: R →+* CatCenter C, the set Hom_C(X, Y) carries a natural structure of an R-module given by the action described above.
Русский
Для объектов X, Y в преддобавительной категории C с кольцевым отображением φ: R →+* CatCenter C множество Hom_C(X, Y) естественно является модулем над R.
LaTeX
$$$\mathrm{Hom}_C(X,Y)$ is an $R$-module with action given by $a \cdot f := ((\smulOfRingMorphism(\varphi) \, X \, Y)\, a)(f)$$$
Lean4
/-- The `R`-module structure on the type `X ⟶ Y` of morphisms in
a category `C` equipped with a ring morphism `R →+* CatCenter C`. -/
def homModuleOfRingMorphism : Module R (X ⟶ Y) :=
by
letI := smulOfRingMorphism φ X Y
exact
{ one_smul := fun a => by
simp only [smulOfRingMorphism_smul_eq, Functor.id_obj, map_one, End.one_def, NatTrans.id_app, id_comp]
mul_smul := fun a b f => by
simp only [smulOfRingMorphism_smul_eq', Functor.id_obj, map_mul, End.mul_def, NatTrans.comp_app, assoc]
smul_zero := fun a => by simp only [smulOfRingMorphism_smul_eq, Functor.id_obj, comp_zero]
zero_smul := fun a => by simp only [smulOfRingMorphism_smul_eq, Functor.id_obj, map_zero, zero_app, zero_comp]
smul_add := fun a b => by simp [smulOfRingMorphism_smul_eq]
add_smul := fun a b f => by
simp only [smulOfRingMorphism_smul_eq]
rw [map_add, NatTrans.app_add, Preadditive.add_comp] }
