functorCategoryLinear — Mathlib

English

For a natural transformation α: F ⇒ G, its evaluation at X is an R-linear map α_X: F.obj X → G.obj X.

Русский

Для натурального преобразования α: F ⇒ G его значение на X задаёт линейный по R гомоморфизм α_X: F.obj X → G.obj X.

LaTeX

$$$\\alpha_X: F.obj X \\to G.obj X$ is R-linear in α.$$

Lean4

instance functorCategoryLinear : Linear R (C ⥤ D)
    where
  homModule F
    G :=
    { smul := fun r α =>
        { app := fun X => r • α.app X
          naturality := by
            intros
            rw [comp_smul, smul_comp, α.naturality] }
      one_smul := by
        intros
        ext
        apply one_smul
      zero_smul := by
        intros
        ext
        apply zero_smul
      smul_zero := by
        intros
        ext
        apply smul_zero
      add_smul := by
        intros
        ext
        apply add_smul
      smul_add := by
        intros
        ext
        apply smul_add
      mul_smul := by
        intros
        ext
        apply mul_smul }
  smul_comp := by
    intros
    ext
    apply smul_comp
  comp_smul := by
    intros
    ext
    apply comp_smul

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