Theorems · Definition · category theory

CategoryTheory.NatTrans.appLinearMap

{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) →ₗ[R] F.obj X ⟶ G.obj X

Application of a natural transformation at a fixed object, as group homomorphism

Defined in

Mathlib.CategoryTheory.Linear.FunctorCategory

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Linear