Theorems · Definition · category theory

CategoryTheory.Functor.mapLinearMap

(R : Type u_1) →
  [inst : Semiring R] →
    {C : Type u_2} →
      {D : Type u_3} →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
          [inst_2 : CategoryTheory.Category.{v_2, 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) →
                      [CategoryTheory.Functor.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.

Defined in

Mathlib.CategoryTheory.Linear.LinearFunctor

Cited by

2 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

SemiringCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.PreadditiveCategoryTheory.LinearCategoryTheory.LinearCategoryTheory.Functor.LinearCategoryTheory.Functor.Additive