Linear Functors

An additive functor between two R-linear categories is called linear if the induced map on hom types is a morphism of R-modules.

Implementation details

Functor.Linear is a Prop-valued class, defined by saying that for every two objects X and Y, the map F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y) is a morphism of R-modules.

class CategoryTheory.Functor.Linear (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) [F.Additive] : Prop

An additive functor F is R-linear provided F.map is an R-module morphism.

• map_smul : ∀ {X Y : C} (f : X ⟶ Y) (r : R), F.map (r • f) = r • F.map f

  the functor induces a linear map on morphisms

theorem CategoryTheory.Functor.Linear.map_smul {R : Type u_1} : ∀ {inst : Semiring R} {C : Type u_2} {D : Type u_3} {inst_1 : CategoryTheory.Category.{u_4, u_2} C} {inst_2 : CategoryTheory.Category.{u_5, u_3} D} {inst_3 : CategoryTheory.Preadditive C} {inst_4 : CategoryTheory.Preadditive D} {inst_5 : CategoryTheory.Linear R C} {inst_6 : CategoryTheory.Linear R D} {F : CategoryTheory.Functor C D} {inst_7 : F.Additive} [self : CategoryTheory.Functor.Linear R F] {X Y : C} (f : X ⟶ Y) (r : R), F.map (r • f) = r • F.map f

the functor induces a linear map on morphisms

@[simp]

theorem CategoryTheory.Functor.map_smul {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear R F] {X : C} {Y : C} (r : R) (f : X ⟶ Y) : F.map (r • f) = r • F.map f

@[simp]

theorem CategoryTheory.Functor.map_units_smul {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear R F] {X : C} {Y : C} (r : Rˣ) (f : X ⟶ Y) : F.map (r • f) = r • F.map f

instance CategoryTheory.Functor.instLinearId {R : Type u_1} [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R (CategoryTheory.Functor.id C)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instLinearComp {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_7, u_2} C] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear R F] {E : Type u_4} [CategoryTheory.Category.{u_5, u_4} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear R E] (G : CategoryTheory.Functor D E) [G.Additive] [CategoryTheory.Functor.Linear R G] : CategoryTheory.Functor.Linear R (F.comp G)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Functor.mapLinearMap_apply (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear R F] {X : C} {Y : C} : ∀ (a : X ⟶ Y), (CategoryTheory.Functor.mapLinearMap R F) a = (↑F.mapAddHom).toFun a

def CategoryTheory.Functor.mapLinearMap (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear R F] {X : C} {Y : C} : (X ⟶ Y) →ₗ[R] F.obj X ⟶ F.obj Y

F.mapLinearMap is an R-linear map whose underlying function is F.map.

Equations

• CategoryTheory.Functor.mapLinearMap R F = { toFun := (↑F.mapAddHom).toFun, map_add' := ⋯, map_smul' := ⋯ }

theorem CategoryTheory.Functor.coe_mapLinearMap (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear R F] {X : C} {Y : C} : ⇑(CategoryTheory.Functor.mapLinearMap R F) = F.map

instance CategoryTheory.Functor.inducedFunctorLinear (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] (F : C → D) : CategoryTheory.Functor.Linear R (CategoryTheory.inducedFunctor F)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.fullSubcategoryInclusionLinear (R : Type u_1) [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (Z : C → Prop) : CategoryTheory.Functor.Linear R (CategoryTheory.fullSubcategoryInclusion Z)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.natLinear {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.Functor.Linear ℕ F

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.intLinear {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.Functor.Linear ℤ F

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.ratLinear {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Linear ℚ C] [CategoryTheory.Linear ℚ D] : CategoryTheory.Functor.Linear ℚ F

Equations

• ⋯ = ⋯

instance CategoryTheory.Equivalence.inverseLinear (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear R e.functor] : CategoryTheory.Functor.Linear R e.inverse

Equations

• ⋯ = ⋯