English
There is an R-linear structure on the category C, provided by φ: R →+* CatCenter C, such that composition respects the scalar action on both sides: (a • f) ≫ g = a • (f ≫ g) and f ≫ (a • g) = a • (f ≫ g).
Русский
Существует структура линейности над R на категории C, задаваемая φ; умножение-морфизмов распределяется по композиции слева и справа: (a • f) ≫ g = a • (f ≫ g) и f ≫ (a • g) = a • (f ≫ g).
LaTeX
$$$a \cdot (f \circ g) = (a \cdot f) \circ g \quad\text{and}\quad (f \circ a \cdot g) = a \cdot (f \circ g)$$$
Lean4
/-- The `R`-linear structure on a preadditive category `C` equipped with
a ring morphism `R →+* CatCenter C`. -/
def ofRingMorphism : Linear R C := by
letI := homModuleOfRingMorphism φ
exact
{ smul_comp := fun X Y Z r f g => by simp only [smulOfRingMorphism_smul_eq, assoc]
comp_smul := fun X Y Z f r g => by simp only [smulOfRingMorphism_smul_eq', assoc] }
