GradedObjectWithShift — Mathlib

English

For φ between graded objects, the right unitor is natural with respect to φ, i.e., map preserves the morphism φ up to the unitor isomorphisms.

Русский

Для φ между градуированными объектами правый унитор натурален по отношению к φ, т. е. отображение сохраняет морфизм φ с учётом изоморфий унитора.

LaTeX

$$$ φ ≫ (mapBifunctorRightUnitor F Y e p hp X').hom = (mapBifunctorRightUnitor F Y e p hp X).hom ≫ φ $$$

Lean4

/-- A type synonym for `β → C`, used for `β`-graded objects in a category `C`
with a shift functor given by translation by `s`.
-/
@[nolint unusedArguments]
abbrev GradedObjectWithShift {β : Type w} [AddCommGroup β] (_ : β) (C : Type u) : Type max w u :=
  GradedObject β C

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