app_smul — Mathlib

English

The functor category is linear over R, with pointwise linear structure on morphisms and natural transformations.

Русский

Категория функторов линейна по отношению к R: отображения морфизмов и натуральных преобразований задано по точке.

LaTeX

$$$\\text{FunctorCategory Linear over }R: (F \\to G)\\text{ form an }R\\text{-module objectwise.}$$$

Lean4

@[simp]
theorem app_smul (X : C) (r : R) (α : F ⟶ G) : (r • α).app X = r • α.app X :=
  rfl

Похожие утверждения