# mathlibdocumentation

category_theory.linear.linear_functor

# 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]
structure category_theory.functor.linear (R : Type u_1) [semiring R] {C : Type u_2} {D : Type u_3} (F : C D) [F.additive] :
Prop
• map_smul' : (∀ {X Y : C} {f : X Y} {r : R}, F.map (r f) = r F.map f) . "obviously"

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

Instances of this typeclass
@[simp]
theorem category_theory.functor.map_smul {R : Type u_1} [semiring R] {C : Type u_2} {D : Type u_3} (F : C D) [F.additive] {X Y : C} (r : R) (f : X Y) :
F.map (r f) = r F.map f
@[protected, instance]
def category_theory.functor.id.linear {R : Type u_1} [semiring R] {C : Type u_2}  :
@[protected, instance]
def category_theory.functor.comp.linear {R : Type u_1} [semiring R] {C : Type u_2} {D : Type u_3} (F : C D) [F.additive] {E : Type u_6} (G : D E) [G.additive]  :
(F G)
def category_theory.functor.map_linear_map (R : Type u_1) [semiring R] {C : Type u_2} {D : Type u_3} (F : C D) [F.additive] {X Y : C} :
(X Y) →ₗ[R] F.obj X F.obj Y

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

Equations
@[simp]
theorem category_theory.functor.map_linear_map_apply (R : Type u_1) [semiring R] {C : Type u_2} {D : Type u_3} (F : C D) [F.additive] {X Y : C} (ᾰ : X Y) :
theorem category_theory.functor.coe_map_linear_map (R : Type u_1) [semiring R] {C : Type u_2} {D : Type u_3} (F : C D) [F.additive] {X Y : C} :
@[protected, instance]
def category_theory.functor.induced_functor_linear (R : Type u_1) [semiring R] {C : Type u_2} {D : Type u_3} (F : C → D) :
@[protected, instance]
def category_theory.functor.nat_linear {C : Type u_2} {D : Type u_3} (F : C D) [F.additive] :
@[protected, instance]
def category_theory.functor.int_linear {C : Type u_2} {D : Type u_3} (F : C D) [F.additive] :
@[protected, instance]
def category_theory.functor.rat_linear {C : Type u_2} {D : Type u_3} (F : C D) [F.additive]  :
@[protected, instance]
def category_theory.equivalence.inverse_linear (R : Type u_1) [semiring R] {C : Type u_2} {D : Type u_3} (e : C D) [e.functor.additive]  :