Theorems · Inductive type · category theory

CategoryTheory.HasShift

(C : Type u) → (A : Type u_2) → [CategoryTheory.Category.{v, u} C] → [AddMonoid A] → Type (max (max u u_2) v)

A category has a shift indexed by an additive monoid A if there is a monoidal functor from A to C ⥤ C.

Defined in

Mathlib.CategoryTheory.Shift.Basic

Cited by

1,527 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

CategoryTheory.CategoryAddMonoid