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} [Semiring R] [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] (r : HomRel C) [Congruence r] (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)) (X Y : Quotient r) : SMul R (X ⟶ Y)

The scalar multiplications on morphisms in Quotient R.

Equations

• CategoryTheory.Quotient.Linear.smul r hr X Y = { smul := fun (a : R) => Quot.lift (fun (g : X.as ⟶ Y.as) => Quot.mk (CategoryTheory.Quotient.CompClosure r) (a • g)) ⋯ }

@[simp]

theorem CategoryTheory.Quotient.Linear.smul_eq {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] (r : HomRel C) [Congruence r] (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)) (a : R) {X Y : C} (f : X ⟶ Y) : a • (functor r).map f = (functor r).map (a • f)

def CategoryTheory.Quotient.Linear.module' {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] (r : HomRel C) [Congruence r] (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)) [Preadditive (Quotient r)] [(functor r).Additive] (X Y : C) : Module R ((functor r).obj X ⟶ (functor r).obj Y)

Auxiliary definition for Quotient.Linear.module.

Equations

• CategoryTheory.Quotient.Linear.module' r hr X Y = Module.mk ⋯ ⋯

def CategoryTheory.Quotient.Linear.module {R : Type u_1} {C : Type u_2} [Semiring R] [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] (r : HomRel C) [Congruence r] (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)) [Preadditive (Quotient r)] [(functor r).Additive] (X Y : Quotient r) : Module R (X ⟶ Y)

Auxiliary definition for Quotient.linear.

Equations

• CategoryTheory.Quotient.Linear.module r hr X Y = CategoryTheory.Quotient.Linear.module' r hr X.as Y.as

def CategoryTheory.Quotient.linear (R : Type u_1) {C : Type u_2} [Semiring R] [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] (r : HomRel C) [Congruence r] (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)) [Preadditive (Quotient r)] [(functor r).Additive] : Linear R (Quotient r)

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

• CategoryTheory.Quotient.linear R r hr = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

instance CategoryTheory.Quotient.linear_functor (R : Type u_1) {C : Type u_2} [Semiring R] [Category.{u_3, u_2} C] [Preadditive C] [Linear R C] (r : HomRel C) [Congruence r] (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)) [Preadditive (Quotient r)] [(functor r).Additive] : Functor.Linear R (functor r)