Sequences of functors from a category equipped with a shift
Let F : C ⥤ A
be a functor from a category C
that is equipped with a
shift by an additive monoid M
. In this file, we define a typeclass
F.ShiftSequence M
which includes the data of a sequence of functors
F.shift a : C ⥤ A
for all a : A
. For each a : A
, we have
an isomorphism F.isoShift a : shiftFunctor C a ⋙ F ≅ F.shift a
which
satisfies some coherence relations. This allows to state results
(e.g. the long exact sequence of an homology functor (TODO)) using
functors F.shift a
rather than shiftFunctor C a ⋙ F
. The reason
for this design is that we can often choose functors F.shift a
that
have better definitional properties than shiftFunctor C a ⋙ F
.
For example, if C
is the derived category (TODO) of an abelian
category A
and F
is the homology functor in degree 0
, then
for any n : ℤ
, we may choose F.shift n
to be the homology functor
in degree n
.
A shift sequence for a functor F : C ⥤ A
when C
is equipped with a shift
by a monoid M
involves a sequence of functor sequence n : C ⥤ A
for all n : M
which behave like shiftFunctor C n ⋙ F
.
- sequence : M → CategoryTheory.Functor C A
a sequence of functors
- isoZero : CategoryTheory.Functor.ShiftSequence.sequence F 0 ≅ F
sequence 0
identifies to the given functor - shiftIso : (n a a' : M) → n + a = a' → (CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C n) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≅ CategoryTheory.Functor.ShiftSequence.sequence F a')
compatibility isomorphism with the shift
- shiftIso_zero : ∀ (a : M), CategoryTheory.Functor.ShiftSequence.shiftIso 0 a a (_ : 0 + a = a) = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ CategoryTheory.Functor.leftUnitor (CategoryTheory.Functor.ShiftSequence.sequence F a)
- shiftIso_add : ∀ (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a''), CategoryTheory.Functor.ShiftSequence.shiftIso (m + n) a a'' (_ : m + n + a = a'') = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ CategoryTheory.Functor.associator (CategoryTheory.shiftFunctor C m) (CategoryTheory.shiftFunctor C n) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C m) (CategoryTheory.Functor.ShiftSequence.shiftIso n a a' ha') ≪≫ CategoryTheory.Functor.ShiftSequence.shiftIso m a' a'' ha''
Instances
The tautological shift sequence on a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The shifted functors given by the shift sequence.
Equations
Instances For
Compatibility isomorphism shiftFunctor C n ⋙ F.shift a ≅ F.shift a'
when n + a = a'
.
Equations
- CategoryTheory.Functor.shiftIso F n a a' ha' = CategoryTheory.Functor.ShiftSequence.shiftIso n a a' ha'
Instances For
The canonical isomorphism F.shift 0 ≅ F
.
Equations
- CategoryTheory.Functor.isoShiftZero F M = CategoryTheory.Functor.ShiftSequence.isoZero
Instances For
The canonical isomorphism shiftFunctor C n ⋙ F ≅ F.shift n
.
Equations
- One or more equations did not get rendered due to their size.