# The quotient category is linear #

If r : HomRel C is a congruence on a preadditive category C which satisfies certain compatibilities, we have already defined a preadditive structure on Quotient r in the file CategoryTheory.Quotient.Preadditive such that functor r : C ⥤ Quotient r is an additive functor. In this file, assuming moreover that C is a R-linear category and that the relation r is compatible with the scalar multiplication by any a : R, we show that Quotient r is a R-linear category and that functor r : C ⥤ Quotient r is a R-linear functor.

def CategoryTheory.Quotient.Linear.smul {R : Type u_1} {C : Type u_2} [] [] [] (r : ) (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X Y), r f₁ f₂r (a f₁) (a f₂)) (X : ) (Y : ) :
SMul R (X Y)

The scalar multiplications on morphisms in Quotient R.

Equations
• = { smul := fun (a : R) => Quot.lift (fun (g : X.as Y.as) => ) }
Instances For
@[simp]
theorem CategoryTheory.Quotient.Linear.smul_eq {R : Type u_1} {C : Type u_2} [] [] [] (r : ) (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X Y), r f₁ f₂r (a f₁) (a f₂)) (a : R) {X : C} {Y : C} (f : X Y) :
a .map f = .map (a f)
def CategoryTheory.Quotient.Linear.module' {R : Type u_1} {C : Type u_2} [] [] [] (r : ) (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X Y), r f₁ f₂r (a f₁) (a f₂)) [.Additive] (X : C) (Y : C) :
Module R (.obj X .obj Y)

Auxiliary definition for Quotient.Linear.module.

Equations
Instances For
def CategoryTheory.Quotient.Linear.module {R : Type u_1} {C : Type u_2} [] [] [] (r : ) (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X Y), r f₁ f₂r (a f₁) (a f₂)) [.Additive] (X : ) (Y : ) :
Module R (X Y)

Auxiliary definition for Quotient.linear.

Equations
Instances For
def CategoryTheory.Quotient.linear (R : Type u_1) {C : Type u_2} [] [] [] (r : ) (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X Y), r f₁ f₂r (a f₁) (a f₂)) [.Additive] :

Assuming Quotient r has already been endowed with a preadditive category structure such that functor r : C ⥤ Quotient r is additive, and that C has a R-linear category structure compatible with r, this is the induced R-linear category structure on Quotient r.

Equations
• = { homModule := inferInstance, smul_comp := , comp_smul := }
Instances For
instance CategoryTheory.Quotient.linear_functor (R : Type u_1) {C : Type u_2} [] [] [] (r : ) (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X Y), r f₁ f₂r (a f₁) (a f₂)) [.Additive] :
Equations
• =