mathlib3 documentation

category_theory.linear.linear_functor

Linear Functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
structure category_theory.functor.linear (R : Type u_1) [semiring R] {C : Type u_2} {D : Type u_3} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.linear R C] [category_theory.linear R D] (F : C ⥤ D) [F.additive] :
Prop

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

Instances of this typeclass
source
@[simp]
theorem category_theory.functor.map_smul {R : Type u_1} [semiring R] {C : Type u_2} {D : Type u_3} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.linear R C] [category_theory.linear R D] (F : C ⥤ D) [F.additive] [category_theory.functor.linear R F] {X Y : C} (r : R) (f : X ⟶ Y) :
F.map (r • f) = r • F.map f
source
@[protected, instance]
def category_theory.functor.id.linear {R : Type u_1} [semiring R] {C : Type u_2} [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] :
category_theory.functor.linear R (𝟭 C)
source
@[protected, instance]
def category_theory.functor.comp.linear {R : Type u_1} [semiring R] {C : Type u_2} {D : Type u_3} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.linear R C] [category_theory.linear R D] (F : C ⥤ D) [F.additive] [category_theory.functor.linear R F] {E : Type u_6} [category_theory.category E] [category_theory.preadditive E] [category_theory.linear R E] (G : D ⥤ E) [G.additive] [category_theory.functor.linear R G] :
category_theory.functor.linear R (F ⋙ G)
source
def category_theory.functor.map_linear_map (R : Type u_1) [semiring R] {C : Type u_2} {D : Type u_3} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.linear R C] [category_theory.linear R D] (F : C ⥤ D) [F.additive] [category_theory.functor.linear R F] {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
source
@[simp]
theorem category_theory.functor.map_linear_map_apply (R : Type u_1) [semiring R] {C : Type u_2} {D : Type u_3} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.linear R C] [category_theory.linear R D] (F : C ⥤ D) [F.additive] [category_theory.functor.linear R F] {X Y : C} (ᾰ : X ⟶ Y) :
⇑(category_theory.functor.map_linear_map R F) ᾰ = F.map_add_hom.to_fun ᾰ
source
theorem category_theory.functor.coe_map_linear_map (R : Type u_1) [semiring R] {C : Type u_2} {D : Type u_3} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.linear R C] [category_theory.linear R D] (F : C ⥤ D) [F.additive] [category_theory.functor.linear R F] {X Y : C} :
⇑(category_theory.functor.map_linear_map R F) = F.map
source
@[protected, instance]
def category_theory.functor.induced_functor_linear (R : Type u_1) [semiring R] {C : Type u_2} {D : Type u_3} [category_theory.category D] [category_theory.preadditive D] [category_theory.linear R D] (F : C → D) :
category_theory.functor.linear R (category_theory.induced_functor F)
source
@[protected, instance]
def category_theory.functor.full_subcategory_inclusion_linear (R : Type u_1) [semiring R] {C : Type u_2} [category_theory.category C] [category_theory.preadditive C] [category_theory.linear R C] (Z : C → Prop) :
category_theory.functor.linear R (category_theory.full_subcategory_inclusion Z)
source
@[protected, instance]
def category_theory.functor.nat_linear {C : Type u_2} {D : Type u_3} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C ⥤ D) [F.additive] :
category_theory.functor.linear ℕ F
source
@[protected, instance]
def category_theory.functor.int_linear {C : Type u_2} {D : Type u_3} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C ⥤ D) [F.additive] :
category_theory.functor.linear ℤ F
source
@[protected, instance]
def category_theory.functor.rat_linear {C : Type u_2} {D : Type u_3} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C ⥤ D) [F.additive] [category_theory.linear ℚ C] [category_theory.linear ℚ D] :
category_theory.functor.linear ℚ F
source
@[protected, instance]
def category_theory.equivalence.inverse_linear (R : Type u_1) [semiring R] {C : Type u_2} {D : Type u_3} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.linear R C] [category_theory.preadditive D] [category_theory.linear R D] (e : C ≌ D) [e.functor.additive] [category_theory.functor.linear R e.functor] :
category_theory.functor.linear R e.inverse