Documentation

Mathlib.CategoryTheory.Quotient.Linear

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

The scalar multiplications on morphisms in Quotient R.

Equations
Instances For
    @[simp]
    theorem CategoryTheory.Quotient.Linear.smul_eq {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (r : HomRel C) [CategoryTheory.Congruence 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) :
    def CategoryTheory.Quotient.Linear.module' {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (r : HomRel C) [CategoryTheory.Congruence r] (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X Y), r f₁ f₂r (a f₁) (a f₂)) [CategoryTheory.Preadditive (CategoryTheory.Quotient r)] [(CategoryTheory.Quotient.functor r).Additive] (X : C) (Y : C) :

    Auxiliary definition for Quotient.Linear.module.

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

      Auxiliary definition for Quotient.linear.

      Equations
      Instances For

        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
        Instances For