Multiplication by an integer in a preadditive category

In a preadditive category, multiplication by an integer n on an object X is the morphism n • 𝟙 X, which is also the image of n in the endomorphism ring End X (CategoryTheory.End.intCast_asHom, CategoryTheory.End.natCast_asHom). It commutes with every morphism (CategoryTheory.End.intCast_asHom_comp, CategoryTheory.End.natCast_asHom_comp).

The inverse of a scalar multiple r • 𝟙 and its preservation by linear functors are in TauCeti.CategoryTheory.Linear.Endomorphism.

theorem CategoryTheory.End.intCast_asHom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (X : C) (n : ℤ) : (↑n).asHom = n • CategoryStruct.id X

The integer n in the endomorphism ring of X is multiplication by n, the morphism n • 𝟙 X.

theorem CategoryTheory.End.natCast_asHom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (X : C) (n : ℕ) : (↑n).asHom = n • CategoryStruct.id X

The natural number n in the endomorphism ring of X is multiplication by n, the morphism n • 𝟙 X.

theorem CategoryTheory.End.intCast_asHom_comp {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} (f : X ⟶ Y) (n : ℤ) : CategoryStruct.comp (↑n).asHom f = CategoryStruct.comp f (↑n).asHom

Multiplication by an integer n commutes with every morphism.

theorem CategoryTheory.End.intCast_asHom_comp_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} (f : X ⟶ Y) (n : ℤ) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (↑n).asHom (CategoryStruct.comp f h) = CategoryStruct.comp f (CategoryStruct.comp (↑n).asHom h)

Multiplication by an integer n commutes with every morphism.

theorem CategoryTheory.End.natCast_asHom_comp {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} (f : X ⟶ Y) (n : ℕ) : CategoryStruct.comp (↑n).asHom f = CategoryStruct.comp f (↑n).asHom

Multiplication by a natural number n commutes with every morphism.

theorem CategoryTheory.End.natCast_asHom_comp_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X Y : C} (f : X ⟶ Y) (n : ℕ) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (↑n).asHom (CategoryStruct.comp f h) = CategoryStruct.comp f (CategoryStruct.comp (↑n).asHom h)

Multiplication by a natural number n commutes with every morphism.