shiftFunctor_obj_apply — Mathlib

English

The object component of the shift functor on GradedObjectWithShift s C shifts the grading by n • s: (shiftFunctor (GradedObjectWithShift s C) n).obj X t = X (t + n • s).

Русский

Компонента объекта сдвиг-функторa над GradedObjectWithShift s C смещает градацию на n • s: (shiftFunctor (GradedObjectWithShift s C) n).obj X t = X (t + n • s).

LaTeX

$$$ (shiftFunctor (GradedObjectWithShift\ s\ C)\ n).obj X\ t = X\ (t + n\,•\ s) $$$

Lean4

@[simp]
theorem shiftFunctor_obj_apply {β : Type*} [AddCommGroup β] (s : β) (X : β → C) (t : β) (n : ℤ) :
    (shiftFunctor (GradedObjectWithShift s C) n).obj X t = X (t + n • s) :=
  rfl

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