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} [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

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

    source
    @[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
    source
    @[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
    source
    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
    • ⋯ = ⋯
    source
    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
    • ⋯ = ⋯
    source
    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
    Instances For
      source
      @[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
      source
      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
      source
      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
      • ⋯ = ⋯
      source
      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
      • ⋯ = ⋯
      source
      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
      • ⋯ = ⋯
      source
      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
      • ⋯ = ⋯
      source
      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
      • ⋯ = ⋯
      source
      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
      • ⋯ = ⋯