Documentation

Mathlib.CategoryTheory.Linear.FunctorCategory

Linear structure on functor categories #

If C and D are categories and D is R-linear, then C ⥤ D is also R-linear.

Equations

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

Equations
Instances For
    @[simp]