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.{v_1, u_2} C] [Category.{v_2, 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
    theorem CategoryTheory.Functor.linear_iff (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{v_1, u_2} C] [Category.{v_2, u_3} D] [Preadditive C] [Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : Functor C D) :
    Linear R F ↔ ∀ (X : C) (r : R), F.map (r • CategoryStruct.id X) = r • CategoryStruct.id (F.obj X)
    source
    @[simp]
    theorem CategoryTheory.Functor.map_smul {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{v_1, u_2} C] [Category.{v_2, 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.{v_1, u_2} C] [Category.{v_2, 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.{v_1, 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.{v_1, u_2} C] [Category.{v_2, 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.{v_3, u_4} E] [Preadditive E] [CategoryTheory.Linear R E] (G : Functor D E) [Linear R G] :
    Linear R (F.comp G)
    source
    theorem CategoryTheory.Functor.linear_of_full_essSurj_comp {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{v_1, u_2} C] [Category.{v_2, 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.{v_3, u_4} E] [Preadditive E] [CategoryTheory.Linear R E] (G : Functor D E) [F.Full] [F.EssSurj] [Linear R (F.comp G)] :
    Linear R G
    source
    theorem CategoryTheory.Functor.linear_comp_iff_of_full_of_essSurj {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{v_1, u_2} C] [Category.{v_2, 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.{v_3, u_4} E] [Preadditive E] [CategoryTheory.Linear R E] (G : Functor D E) [F.Full] [F.EssSurj] :
    Linear R (F.comp G) ↔ Linear R G
    source
    def CategoryTheory.Functor.mapLinearMap (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{v_1, u_2} C] [Category.{v_2, 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.{v_1, u_2} C] [Category.{v_2, 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.{v_1, u_2} C] [Category.{v_2, 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
      theorem CategoryTheory.Functor.linear_of_iso (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{v_1, u_2} C] [Category.{v_2, u_3} D] [Preadditive C] [Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] {F G : Functor C D} (e : F ≅ G) [Linear R F] :
      Linear R G
      source
      instance CategoryTheory.Functor.inducedFunctorLinear (R : Type u_1) [Semiring R] {C : Type u_2} {D : Type u_3} [Category.{v_2, 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_4} [Category.{v_3, u_4} C] [Preadditive C] [CategoryTheory.Linear R C] (Z : ObjectProperty C) :
      Linear R Z.ι
      source
      instance CategoryTheory.Functor.natLinear {C : Type u_2} {D : Type u_3} [Category.{v_1, u_2} C] [Category.{v_2, 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.{v_1, u_2} C] [Category.{v_2, 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.{v_1, u_2} C] [Category.{v_2, 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.{v_1, u_2} C] [Category.{v_2, u_3} D] [Preadditive C] [Preadditive D] [Linear R C] [Linear R D] (e : C ≌ D) [Functor.Linear R e.functor] :
      Functor.Linear R e.inverse