Documentation

Mathlib.CategoryTheory.Linear.LinearFunctor

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.

source
class CategoryTheory.Functor.Linear (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] [Preadditive C] [Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : Functor C D) :
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

Instances
    source
    @[simp]
    theorem CategoryTheory.Functor.map_smul {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] [Preadditive C] [Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : Functor C D) [Linear R F] {X Y : C} (r : R) (f : X ⟶ Y) :
    F.map (r • f) = r • F.map f
    source
    @[simp]
    theorem CategoryTheory.Functor.map_units_smul {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] [Preadditive C] [Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : Functor C D) [Linear R F] {X Y : C} (r : Rˣ) (f : X ⟶ Y) :
    F.map (r • f) = r • F.map f
    source
    instance CategoryTheory.Functor.instLinearId {R : Type u_1} [Semiring R] {C : Type u_2} [Category.{u_4, u_2} C] [Preadditive C] [CategoryTheory.Linear R C] :
    Linear R (Functor.id C)
    source
    instance CategoryTheory.Functor.instLinearComp {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{u_7, u_2} C] [Category.{u_6, u_3} D] [Preadditive C] [Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : Functor C D) [Linear R F] {E : Type u_4} [Category.{u_5, u_4} E] [Preadditive E] [CategoryTheory.Linear R E] (G : Functor D E) [Linear R G] :
    Linear R (F.comp G)
    source
    def CategoryTheory.Functor.mapLinearMap (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] [Preadditive C] [Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : Functor C D) [Linear R F] [F.Additive] {X 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
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Functor.mapLinearMap_apply (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] [Preadditive C] [Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : Functor C D) [Linear R F] [F.Additive] {X Y : C} (a✝ : X ⟶ Y) :
      (mapLinearMap R F) a✝ = (↑F.mapAddHom).toFun a✝
      source
      theorem CategoryTheory.Functor.coe_mapLinearMap (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] [Preadditive C] [Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : Functor C D) [Linear R F] [F.Additive] {X Y : C} :
      ⇑(mapLinearMap R F) = F.map
      source
      instance CategoryTheory.Functor.inducedFunctorLinear (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{u_4, u_3} D] [Preadditive D] [CategoryTheory.Linear R D] (F : C → D) :
      Linear R (inducedFunctor F)
      source
      instance CategoryTheory.Functor.fullSubcategoryInclusionLinear (R : Type u_1) [Semiring R] {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [CategoryTheory.Linear R C] (Z : C → Prop) :
      Linear R (fullSubcategoryInclusion Z)
      source
      instance CategoryTheory.Functor.natLinear {C : Type u_2} {D : Type u_3} [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] :
      Linear ℕ F
      source
      instance CategoryTheory.Functor.intLinear {C : Type u_2} {D : Type u_3} [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] :
      Linear ℤ F
      source
      instance CategoryTheory.Functor.ratLinear {C : Type u_2} {D : Type u_3} [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] [CategoryTheory.Linear ℚ C] [CategoryTheory.Linear ℚ D] :
      Linear ℚ F
      source
      instance CategoryTheory.Equivalence.inverseLinear (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] [Preadditive C] [Linear R C] [Preadditive D] [Linear R D] (e : C ≌ D) [Functor.Linear R e.functor] :
      Functor.Linear R e.inverse