The Karoubi embedding is braided and linear

The canonical functor toKaroubi C is a braided monoidal functor (with respect to the in-tree monoidal and braided structures on the Karoubi envelope) and is ℂ-linear.

@[instance_reducible]

noncomputable instance RS.toKaroubiBraided {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.Idempotents.toKaroubi C).Braided

The Karoubi embedding is braided.

Equations

• RS.toKaroubiBraided = { toMonoidal := RS.toKaroubiMonoidal, braided := ⋯ }

instance RS.toKaroubiLinear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] : CategoryTheory.Functor.Linear ℂ (CategoryTheory.Idempotents.toKaroubi C)

The Karoubi embedding is ℂ-linear.