instAdditivePullbackShiftShiftFunctorOfCoeAddMonoidHom

English

For every a in A, the shift functor on the pullback shift category PullbackShift C φ by a is an additive functor (i.e., preserves addition on hom-sets).

Русский

Для каждого a из A сдвиговый функтор над PullbackShift C φ по a является аддитивным функтором ( сохраняет сложение на множествах морфизмов).

LaTeX

$$$\forall a \in A: \ shiftFunctor (PullbackShift\; C \; \varphi)\ a \text{ is additive }$$$

Lean4

instance [Preadditive C] (a : A) [(shiftFunctor C (φ a)).Additive] : (shiftFunctor (PullbackShift C φ) a).Additive :=
  by
  change (shiftFunctor C (φ a)).Additive
  infer_instance

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