English
The canonical morphism R →+* CatCenter C for an R-linear category C is defined by mapping a ∈ R to the endomorphism a • id_X on each object X.
Русский
Каноническое отображение R в CatCenter C для R-линейной категории C задаётся отправлением a ∈ R на концевой эндоморфизм a • id_X на каждом объекте X.
LaTeX
$$$\text{toCatCenter}$ defines a ring homomorphism by $a \mapsto (X \mapsto a \cdot 1_X)$$$
Lean4
/-- The canonical morphism `R →+* CatCenter C` when `C` is a `R`-linear category. -/
@[simps]
def toCatCenter [Linear R C] : R →+* CatCenter C
where
toFun a := { app := fun X => a • 𝟙 X }
map_one' := by cat_disch
map_mul' a
b := by
rw [mul_comm]
ext X
dsimp only [CatCenter.mul_app']
rw [Linear.smul_comp, Linear.comp_smul, smul_smul]
simp
map_zero' := by cat_disch
map_add' a
b := by
ext X
dsimp
rw [NatTrans.app_add, add_smul]
