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.

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

    the functor induces a linear map on morphisms

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

    Equations
    Instances For