instLinearIntUpSingleFunctor — Mathlib

English

In the up-shift setting, the n-th single functor is linear over R.

Русский

В направлении верхнего сдвига n-й одинарный функтор линейный над кольцом R.

LaTeX

$$$\forall R\, [\text{Ring } R] \; [\text{Linear } R\; C],\; (\text{HomotopyCategory.singleFunctor } C n).Linear_R$$$

Lean4

instance (R : Type*) [Ring R] [Linear R C] (n : ℤ) : Functor.Linear R (HomotopyCategory.singleFunctor C n) :=
  inferInstanceAs (Functor.Linear R (CochainComplex.singleFunctor C n ⋙ HomotopyCategory.quotient _ _))

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