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 #
has_shift
: A typeclass asserting the existence of a shift functor.shift_equiv
: When the indexing monoid is a group, then the functor indexed byn
and-n
forms an self-equivalence ofC
.shift_comm
: When the indexing monoid is commutative, then shifts commute as well.
Implementation Notes #
Many of the definitions in this file are marked as an abbreviation
so that the simp lemmas in
category_theory/monoidal/End
can apply.
A monoidal functor from a group A
into C ⥤ C
induces
a self-equivalence of C
for each n : A
.
Equations
- shift : category_theory.monoidal_functor (category_theory.discrete A) (C ⥤ C)
A category has a shift indexed by an additive monoid A
if there is a monoidal functor from A
to C ⥤ C
.
Instances of this typeclass
Instances of other typeclasses for category_theory.has_shift
- category_theory.has_shift.has_sizeof_inst
- F : A → C ⥤ C
- ε : 𝟭 C ≅ self.F 0
- μ : Π (n m : A), self.F n ⋙ self.F m ≅ self.F (n + m)
- associativity : (∀ (m₁ m₂ m₃ : A) (X : C), (self.F m₃).map ((self.μ m₁ m₂).hom.app X) ≫ (self.μ (m₁ + m₂) m₃).hom.app X ≫ category_theory.eq_to_hom _ = (self.μ m₂ m₃).hom.app ((self.F m₁).obj X) ≫ (self.μ m₁ (m₂ + m₃)).hom.app X) . "obviously"
- left_unitality : (∀ (n : A) (X : C), (self.F n).map (self.ε.hom.app X) ≫ (self.μ 0 n).hom.app X = category_theory.eq_to_hom _) . "obviously"
- right_unitality : (∀ (n : A) (X : C), self.ε.hom.app ((self.F n).obj X) ≫ (self.μ n 0).hom.app X = category_theory.eq_to_hom _) . "obviously"
A helper structure to construct the shift functor (discrete A) ⥤ (C ⥤ C)
.
Instances for category_theory.shift_mk_core
- category_theory.shift_mk_core.has_sizeof_inst
Constructs a has_shift C A
instance from shift_mk_core
.
Equations
- category_theory.has_shift_mk C A h = {shift := {to_lax_monoidal_functor := {to_functor := {obj := (category_theory.discrete.functor h.F).obj, map := (category_theory.discrete.functor h.F).map, map_id' := _, map_comp' := _}, ε := h.ε.hom, μ := λ (m n : category_theory.discrete A), (h.μ m.as n.as).hom, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}}
The monoidal functor from A
to C ⥤ C
given a has_shift
instance.
The shift autoequivalence, moving objects and morphisms 'up'.
Shifting by i + j
is the same as shifting by i
and then shifting by j
.
Shifting by zero is the identity functor.
Shifting by i + j
is the same as shifting by i
and then shifting by j
.
Shifting by zero is the identity functor.
Shifting by i
is an equivalence.
Shifting by i
and then shifting by -i
is the identity.
Shifting by -i
and then shifting by i
is the identity.
Shifting by n
is a faithful functor.
Shifting by n
is a full functor.
Shifting by n
is an essentially surjective functor.
Shifting by i
and then shifting by -i
is the identity.
Shifting by -i
and then shifting by i
is the identity.
Shifting by n
and shifting by -n
forms an equivalence.
Equations
- category_theory.shift_equiv C n = {functor := category_theory.shift_functor C n, inverse := category_theory.shift_functor C (-n), unit_iso := (category_theory.add_neg_equiv (category_theory.shift_monoidal_functor C A) n).unit_iso, counit_iso := (category_theory.add_neg_equiv (category_theory.shift_monoidal_functor C A) n).counit_iso, functor_unit_iso_comp' := _}
When shifts are indexed by an additive commutative monoid, then shifts commute.
Equations
When shifts are indexed by an additive commutative monoid, then shifts commute.
Given a family of endomorphisms of C
which are interwined by a fully faithful F : C ⥤ D
with shift functors on D
, we can promote that family to shift functors on C
.
Equations
- category_theory.has_shift_of_fully_faithful F s i = category_theory.has_shift_mk C A {F := s, ε := category_theory.nat_iso_of_comp_fully_faithful F (((F.left_unitor ≪≫ F.right_unitor.symm) ≪≫ category_theory.iso_whisker_left F (category_theory.shift_functor_zero D A).symm) ≪≫ (i 0).symm), μ := λ (a b : A), category_theory.nat_iso_of_comp_fully_faithful F (((((((s a).associator (s b) F ≪≫ category_theory.iso_whisker_left (s a) (i b)) ≪≫ ((s a).associator F (category_theory.shift_functor D b)).symm) ≪≫ category_theory.iso_whisker_right (i a) (category_theory.shift_functor D b)) ≪≫ F.associator (category_theory.shift_functor D a) (category_theory.shift_functor D b)) ≪≫ category_theory.iso_whisker_left F (category_theory.shift_functor_add D a b).symm) ≪≫ (i (a + b)).symm), associativity := _, left_unitality := _, right_unitality := _}
When we construct shifts on a subcategory from shifts on the ambient category, the inclusion functor intertwines the shifts.
Equations
- category_theory.has_shift_of_fully_faithful_comm F s i m = i m