Theorems · Theorem · category theory

CategoryTheory.NatTrans.appLinearMap_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 D]
  [inst_4 : CategoryTheory.Linear R D] {F G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G),
  (CategoryTheory.NatTrans.appLinearMap X) α = α.app X

Defined in

Mathlib.CategoryTheory.Linear.FunctorCategory

Cited by

0 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Linear