shiftFunctor_map_apply — Mathlib

English

For a morphism f: X ⟶ Y in GradedObjectWithShift s C, the shift functor acts on maps by (shiftFunctor (GradedObjectWithShift s C) n).map f t = f (t + n • s).

Русский

Для морфизма f: X ⟶ Y в GradedObjectWithShift s C сдвиг-функтор действует на отображения так: (shiftFunctor (GradedObjectWithShift s C) n).map f t = f (t + n • s).

LaTeX

$$$ (shiftFunctor (GradedObjectWithShift\ s\ C)\ n).map f\ t = f\ (t + n \cdot s) $$$

Lean4

@[simp]
theorem shiftFunctor_map_apply {β : Type*} [AddCommGroup β] (s : β) {X Y : GradedObjectWithShift s C} (f : X ⟶ Y)
    (t : β) (n : ℤ) : (shiftFunctor (GradedObjectWithShift s C) n).map f t = f (t + n • s) :=
  rfl

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