Additive and linear structure on morphisms of a full subcategory

A full subcategory of a preadditive (resp. R-linear) category inherits a preadditive (resp. R-linear) structure. This file records that the underlying morphism of a sum, a negation, a difference or a scalar multiple of morphisms in the full subcategory is the corresponding operation applied to the underlying morphisms in the ambient category. The zero morphism is Mathlib's CategoryTheory.ObjectProperty.zero_hom.

Main results

• CategoryTheory.ObjectProperty.add_hom, CategoryTheory.ObjectProperty.neg_hom, CategoryTheory.ObjectProperty.sub_hom: the underlying morphism of a morphism built from the preadditive structure.
• CategoryTheory.ObjectProperty.smul_hom: the underlying morphism of a scalar multiple.

@[simp]

theorem CategoryTheory.ObjectProperty.add_hom {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} [Preadditive C] {X Y : P.FullSubcategory} (f g : X ⟶ Y) : (f + g).hom = f.hom + g.hom

The underlying morphism of a sum in a full subcategory is the sum of the underlying morphisms.

@[simp]

theorem CategoryTheory.ObjectProperty.neg_hom {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} [Preadditive C] {X Y : P.FullSubcategory} (f : X ⟶ Y) : (-f).hom = -f.hom

The underlying morphism of a negation in a full subcategory is the negation of the underlying morphism.

@[simp]

theorem CategoryTheory.ObjectProperty.sub_hom {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} [Preadditive C] {X Y : P.FullSubcategory} (f g : X ⟶ Y) : (f - g).hom = f.hom - g.hom

The underlying morphism of a difference in a full subcategory is the difference of the underlying morphisms.

@[simp]

theorem CategoryTheory.ObjectProperty.smul_hom {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {R : Type w} [Semiring R] [Preadditive C] [Linear R C] {X Y : P.FullSubcategory} (r : R) (f : X ⟶ Y) : (r • f).hom = r • f.hom

The underlying morphism of a scalar multiple in a full subcategory of a linear category is the scalar multiple of the underlying morphism.