Theorems · Theorem · category theory

CategoryTheory.Functor.mapLinearMap_apply

∀ (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) [inst_7 : CategoryTheory.Functor.Linear R F] [inst_8 : F.Additive] {X Y : C}
  (a : X ⟶ Y), (CategoryTheory.Functor.mapLinearMap R F) a = (↑F.mapAddHom).toFun a

Defined in

Mathlib.CategoryTheory.Linear.LinearFunctor

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext

Assumes

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