Shift #
A Shift
on a category C
indexed by a monoid A
is nothing more than a monoidal functor
from A
to C ⥤ C
. A typical example to keep in mind might be the category of
complexes ⋯ → C_{n-1} → C_n → C_{n+1} → ⋯
. It has a shift indexed by ℤ
, where we assign to
each n : ℤ
the functor C ⥤ C
that re-indexes the terms, so the degree i
term of Shift n C
would be the degree i+n
-th term of C
.
Main definitions #
HasShift
: A typeclass asserting the existence of a shift functor.shiftEquiv
: When the indexing monoid is a group, then the functor indexed byn
and-n
forms a self-equivalence ofC
.shiftComm
: When the indexing monoid is commutative, then shifts commute as well.
Implementation Notes #
[HasShift C A]
is implemented using MonoidalFunctor (Discrete A) (C ⥤ C)
.
However, the API of monoidal functors is used only internally: one should use the API of
shifts functors which includes shiftFunctor C a : C ⥤ C
for a : A
,
shiftFunctorZero C A : shiftFunctor C (0 : A) ≅ 𝟭 C
and
shiftFunctorAdd C i j : shiftFunctor C (i + j) ≅ shiftFunctor C i ⋙ shiftFunctor C j
(and its variant shiftFunctorAdd'
). These isomorphisms satisfy some coherence properties
which are stated in lemmas like shiftFunctorAdd'_assoc
, shiftFunctorAdd'_zero_add
and
shiftFunctorAdd'_add_zero
.
- shift : CategoryTheory.MonoidalFunctor (CategoryTheory.Discrete A) (CategoryTheory.Functor C C)
a shift is a monoidal functor from
A
toC ⥤ C
A category has a shift indexed by an additive monoid A
if there is a monoidal functor from A
to C ⥤ C
.
Instances
- F : A → CategoryTheory.Functor C C
the family of shift functors
- zero : CategoryTheory.ShiftMkCore.F s 0 ≅ CategoryTheory.Functor.id C
the shift by 0 identifies to the identity functor
- add : (n m : A) → CategoryTheory.ShiftMkCore.F s (n + m) ≅ CategoryTheory.Functor.comp (CategoryTheory.ShiftMkCore.F s n) (CategoryTheory.ShiftMkCore.F s m)
the composition of shift functors identifies to the shift by the sum
- assoc_hom_app : ∀ (m₁ m₂ m₃ : A) (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.ShiftMkCore.add s (m₁ + m₂) m₃).hom.app X) ((CategoryTheory.ShiftMkCore.F s m₃).map ((CategoryTheory.ShiftMkCore.add s m₁ m₂).hom.app X)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (CategoryTheory.ShiftMkCore.F s (m₁ + m₂ + m₃)).obj X = (CategoryTheory.ShiftMkCore.F s (m₁ + (m₂ + m₃))).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ShiftMkCore.add s m₁ (m₂ + m₃)).hom.app X) ((CategoryTheory.ShiftMkCore.add s m₂ m₃).hom.app ((CategoryTheory.ShiftMkCore.F s m₁).obj X)))
compatibility with the associativity
- zero_add_hom_app : ∀ (n : A) (X : C), (CategoryTheory.ShiftMkCore.add s 0 n).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (CategoryTheory.ShiftMkCore.F s (0 + n)).obj X = (CategoryTheory.ShiftMkCore.F s n).obj ((CategoryTheory.Functor.id C).obj X))) ((CategoryTheory.ShiftMkCore.F s n).map (s.zero.inv.app X))
compatibility with the left addition with 0
- add_zero_hom_app : ∀ (n : A) (X : C), (CategoryTheory.ShiftMkCore.add s n 0).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (CategoryTheory.ShiftMkCore.F s (n + 0)).obj X = (CategoryTheory.Functor.id C).obj ((CategoryTheory.ShiftMkCore.F s n).obj X))) (s.zero.inv.app ((CategoryTheory.ShiftMkCore.F s n).obj X))
compatibility with the right addition with 0
A helper structure to construct the shift functor (Discrete A) ⥤ (C ⥤ C)
.
Instances For
Constructs a HasShift C A
instance from ShiftMkCore
.
Instances For
The monoidal functor from A
to C ⥤ C
given a HasShift
instance.
Instances For
The shift autoequivalence, moving objects and morphisms 'up'.
Instances For
Shifting by i + j
is the same as shifting by i
and then shifting by j
.
Instances For
When k = i + j
, shifting by k
is the same as shifting by i
and then shifting by j
.
Instances For
Shifting by zero is the identity functor.
Instances For
shifting an object X
by n
is obtained by the notation X⟦n⟧
Instances For
shifting a morphism f
by n
is obtained by the notation f⟦n⟧'
Instances For
Shifting by i + j
is the same as shifting by i
and then shifting by j
.
Instances For
Shifting by zero is the identity functor.
Instances For
When i + j = 0
, shifting by i
and by j
gives the identity functor
Instances For
Shifting by i
and shifting by j
forms an equivalence when i + j = 0
.
Instances For
Shifting by n
and shifting by -n
forms an equivalence.
Instances For
Shifting by i
is an equivalence.
Shifting by n
is an essentially surjective functor.
Shifting by i
and then shifting by -i
is the identity.
Instances For
Shifting by -i
and then shifting by i
is the identity.
Instances For
When shifts are indexed by an additive commutative monoid, then shifts commute.
Instances For
When shifts are indexed by an additive commutative monoid, then shifts commute.
Instances For
When shifts are indexed by an additive commutative monoid, then shifts commute.
auxiliary definition for hasShiftOfFullyFaithful
Instances For
auxiliary definition for hasShiftOfFullyFaithful
Instances For
Given a family of endomorphisms of C
which are intertwined by a fully faithful F : C ⥤ D
with shift functors on D
, we can promote that family to shift functors on C
.