appLinearMap — Mathlib

English

There is an R-linear map appLinearMap that sends a natural transformation to its X-component.

Русский

Существует $R$-линейное отображение appLinearMap, отправляющее натуральное преобразование в его компоненту в X.

LaTeX

$$$\\text{appLinearMap}(X): (F ⟶ G) \\to_{R} F.obj X \\to G.obj X$ is linear.$$

Lean4

/-- Application of a natural transformation at a fixed object,
as group homomorphism -/
@[simps]
def appLinearMap (X : C) : (F ⟶ G) →ₗ[R] F.obj X ⟶ G.obj X
    where
  toFun α := α.app X
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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