Linear structure on a Karoubi completion

The underlying-morphism map transports the linear structure of the base category to its Karoubi completion.

def RS.karoubiHomAddHom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (P Q : CategoryTheory.Idempotents.Karoubi C) : (P ⟶ Q) →+ (P.X ⟶ Q.X)

The underlying-morphism map is additive.

Equations

• RS.karoubiHomAddHom P Q = { toFun := fun (g : P ⟶ Q) => g.f, map_zero' := ⋯, map_add' := ⋯ }

@[instance_reducible]

noncomputable instance RS.karoubiHomSMul {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] (P Q : CategoryTheory.Idempotents.Karoubi C) : SMul ℂ (P ⟶ Q)

Scaling a Karoubi morphism through its underlying morphism.

Equations

• RS.karoubiHomSMul P Q = { smul := fun (c : ℂ) (g : P ⟶ Q) => { f := c • g.f, comm := ⋯ } }

@[instance_reducible]

noncomputable instance RS.karoubiHomModule {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] (P Q : CategoryTheory.Idempotents.Karoubi C) : Module ℂ (P ⟶ Q)

Karoubi hom-sets inherit the complex module structure.

Equations

• RS.karoubiHomModule P Q = Function.Injective.module ℂ (RS.karoubiHomAddHom P Q) ⋯ ⋯

@[instance_reducible]

noncomputable instance RS.karoubiLinear {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] : CategoryTheory.Linear ℂ (CategoryTheory.Idempotents.Karoubi C)

The Karoubi completion of a complex linear category is linear.

Equations

• RS.karoubiLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

noncomputable def RS.karoubiHomLinearMap {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] (P Q : CategoryTheory.Idempotents.Karoubi C) : (P ⟶ Q) →ₗ[ℂ] P.X ⟶ Q.X

The underlying-morphism map is complex linear.

Equations

• RS.karoubiHomLinearMap P Q = { toFun := fun (g : P ⟶ Q) => g.f, map_add' := ⋯, map_smul' := ⋯ }