instLinearIntFunctorSingleFunctors

English

If R is a ring and the category C is R-linear, then the n-th single functor is R-linear (i.e., a linear functor).

Русский

Пусть R — кольцо и C — R--линейное. Тогда n-й одинарный функтор линейный над R.

LaTeX

$$$\\forall R\\, [\\text{Ring }R]\\, [\\text{Linear }R\, C],\\; (\\text{CochainComplex.singleFunctor } C).(n) \\text{ is linear over } R$$$

Lean4

instance (R : Type*) [Ring R] (n : ℤ) [Linear R C] : Functor.Linear R ((singleFunctors C).functor n) where
  map_smul f
    r := by
    dsimp [CochainComplex.singleFunctors, HomologicalComplex.single]
    aesop

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