Linear combinations of intertwining endomorphisms #
An intertwining relation is preserved by addition and scalar multiplication in a linear category.
theorem
RS.intertwine_add
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
[CategoryTheory.Preadditive A]
{P Q : A}
{a b : P ⟶ P}
{a' b' : Q ⟶ Q}
{T : P ⟶ Q}
(ha : CategoryTheory.CategoryStruct.comp a T = CategoryTheory.CategoryStruct.comp T a')
(hb : CategoryTheory.CategoryStruct.comp b T = CategoryTheory.CategoryStruct.comp T b')
:
Intertwining endomorphisms are closed under addition.
theorem
RS.intertwine_smul
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
[CategoryTheory.Preadditive A]
[CategoryTheory.Linear ℂ A]
{P Q : A}
{a : P ⟶ P}
{a' : Q ⟶ Q}
{T : P ⟶ Q}
(r : ℂ)
(h : CategoryTheory.CategoryStruct.comp a T = CategoryTheory.CategoryStruct.comp T a')
:
Intertwining endomorphisms are closed under scalar multiplication.