Induced shift sequences #
When G : C ⥤ A
is a functor from a category equipped with a shift by a
monoid M
, we have defined in the file CategoryTheory.Shift.ShiftSequence
a type class G.ShiftSequence M
which provides functors G.shift a : C ⥤ A
for all a : M
,
isomorphisms shiftFunctor C n ⋙ G.shift a ≅ G.shift a'
when n + a = a'
,
and isomorphisms G.isoShift a : shiftFunctor C a ⋙ G ≅ G.shift a
for all a
, all of
which satisfy good coherence properties. The idea is that it allows to use functors
G.shift a
which may have better definitional properties than shiftFunctor C a ⋙ G
.
The typical example shall be [(homologyFunctor C (ComplexShape.up ℤ) 0).ShiftSequence ℤ]
for any abelian category C
(TODO).
Similarly as a shift on a category may induce a shift on a quotient or a localized
category (see the file CategoryTheory.Shift.Induced
), this file shows that
under certain assumptions, there is an induced "shift sequence". The main application
will be the construction of a shift sequence for the homology functor on the
homotopy category of cochain complexes (TODO), and also on the derived category (TODO).
The isoZero
field of the induced shift sequence.
Equations
Instances For
The shiftIso
field of the induced shift sequence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given an isomorphism of functors e : L ⋙ F ≅ G
relating functors L : C ⥤ D
,
F : D ⥤ A
and G : C ⥤ A
, an additive monoid M
, a family of functors F' : M → D ⥤ A
equipped with isomorphisms e' : ∀ m, L ⋙ F' m ≅ G.shift m
, this is the shift sequence
induced on F
induced by a shift sequence for the functor G
, provided that
the functor (whiskeringLeft C D A).obj L
of precomposition by L
is fully faithful.
Equations
- One or more equations did not get rendered due to their size.