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 bynand-nforms 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.
@[simp]
theorem
category_theory.eq_to_hom_μ_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
(F : category_theory.monoidal_functor (category_theory.discrete A) (C ⥤ C))
{i j i' j' : A}
(h₁ : i = i')
(h₂ : j = j')
(X : C) :
category_theory.eq_to_hom _ ≫ (F.to_lax_monoidal_functor.μ {as := i'} {as := j'}).app X = (F.to_lax_monoidal_functor.μ {as := i} {as := j}).app X ≫ category_theory.eq_to_hom _
@[simp]
theorem
category_theory.eq_to_hom_μ_app_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
(F : category_theory.monoidal_functor (category_theory.discrete A) (C ⥤ C))
{i j i' j' : A}
(h₁ : i = i')
(h₂ : j = j')
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj ({as := i'} ⊗ {as := j'})).obj X ⟶ X') :
@[simp]
theorem
category_theory.μ_inv_app_eq_to_hom
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
(F : category_theory.monoidal_functor (category_theory.discrete A) (C ⥤ C))
{i j i' j' : A}
(h₁ : i = i')
(h₂ : j = j')
(X : C) :
category_theory.inv ((F.to_lax_monoidal_functor.μ {as := i} {as := j}).app X) ≫ category_theory.eq_to_hom _ = category_theory.eq_to_hom _ ≫ category_theory.inv ((F.to_lax_monoidal_functor.μ {as := i'} {as := j'}).app X)
@[simp]
theorem
category_theory.μ_inv_app_eq_to_hom_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
(F : category_theory.monoidal_functor (category_theory.discrete A) (C ⥤ C))
{i j i' j' : A}
(h₁ : i = i')
(h₂ : j = j')
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj {as := i'} ⊗ F.to_lax_monoidal_functor.to_functor.obj {as := j'}).obj X ⟶ X') :
category_theory.inv ((F.to_lax_monoidal_functor.μ {as := i} {as := j}).app X) ≫ category_theory.eq_to_hom _ ≫ f' = category_theory.eq_to_hom _ ≫ category_theory.inv ((F.to_lax_monoidal_functor.μ {as := i'} {as := j'}).app X) ≫ f'
noncomputable
def
category_theory.add_neg_equiv
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
(F : category_theory.monoidal_functor (category_theory.discrete A) (C ⥤ C))
(n : A) :
C ≌ C
A monoidal functor from a group A into C ⥤ C induces
a self-equivalence of C for each n : A.
Equations
@[simp]
theorem
category_theory.add_neg_equiv_functor
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
(F : category_theory.monoidal_functor (category_theory.discrete A) (C ⥤ C))
(n : A) :
(category_theory.add_neg_equiv F n).functor = F.to_lax_monoidal_functor.to_functor.obj {as := n}
@[simp]
theorem
category_theory.add_neg_equiv_unit_iso_hom
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
(F : category_theory.monoidal_functor (category_theory.discrete A) (C ⥤ C))
(n : A) :
(category_theory.add_neg_equiv F n).unit_iso.hom = (category_theory.unit_of_tensor_iso_unit F {as := n} {as := -n} (category_theory.discrete.eq_to_iso _)).inv
@[simp]
theorem
category_theory.add_neg_equiv_unit_iso_inv
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
(F : category_theory.monoidal_functor (category_theory.discrete A) (C ⥤ C))
(n : A) :
(category_theory.add_neg_equiv F n).unit_iso.inv = (category_theory.unit_of_tensor_iso_unit F {as := n} {as := -n} (category_theory.discrete.eq_to_iso _)).hom
@[simp]
theorem
category_theory.add_neg_equiv_counit_iso_hom
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
(F : category_theory.monoidal_functor (category_theory.discrete A) (C ⥤ C))
(n : A) :
(category_theory.add_neg_equiv F n).counit_iso.hom = F.to_lax_monoidal_functor.μ {as := -n} {as := n} ≫ F.to_lax_monoidal_functor.to_functor.map (category_theory.eq_to_hom _) ≫ F.ε_iso.inv
@[simp]
theorem
category_theory.add_neg_equiv_inverse
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
(F : category_theory.monoidal_functor (category_theory.discrete A) (C ⥤ C))
(n : A) :
(category_theory.add_neg_equiv F n).inverse = F.to_lax_monoidal_functor.to_functor.obj {as := -n}
@[simp]
theorem
category_theory.add_neg_equiv_counit_iso_inv
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
(F : category_theory.monoidal_functor (category_theory.discrete A) (C ⥤ C))
(n : A) :
(category_theory.add_neg_equiv F n).counit_iso.inv = F.to_lax_monoidal_functor.ε ≫ F.to_lax_monoidal_functor.to_functor.map (category_theory.eq_to_hom _) ≫ (F.μ_iso {as := -n} {as := n}).inv
@[class]
structure
category_theory.has_shift
(C : Type u)
(A : Type u_2)
[category_theory.category C]
[add_monoid A] :
Type (max u u_2 v)
- 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
@[nolint]
structure
category_theory.shift_mk_core
(C : Type u)
(A : Type u_1)
[category_theory.category C]
[add_monoid A] :
Type (max u u_1 v)
- 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
@[simp]
theorem
category_theory.has_shift_mk_shift_to_lax_monoidal_functor_to_functor
(C : Type u)
(A : Type u_1)
[category_theory.category C]
[add_monoid A]
(h : category_theory.shift_mk_core C A) :
@[simp]
theorem
category_theory.has_shift_mk_shift_to_lax_monoidal_functor_μ
(C : Type u)
(A : Type u_1)
[category_theory.category C]
[add_monoid A]
(h : category_theory.shift_mk_core C A)
(m n : category_theory.discrete A) :
category_theory.has_shift.shift.to_lax_monoidal_functor.μ m n = (h.μ m.as n.as).hom
def
category_theory.has_shift_mk
(C : Type u)
(A : Type u_1)
[category_theory.category C]
[add_monoid A]
(h : category_theory.shift_mk_core C A) :
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 := _}}
@[simp]
theorem
category_theory.has_shift_mk_shift_to_lax_monoidal_functor_ε
(C : Type u)
(A : Type u_1)
[category_theory.category C]
[add_monoid A]
(h : category_theory.shift_mk_core C A) :
def
category_theory.shift_monoidal_functor
(C : Type u)
(A : Type u_1)
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A] :
The monoidal functor from A to C ⥤ C given a has_shift instance.
@[reducible]
def
category_theory.shift_functor
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(i : A) :
C ⥤ C
The shift autoequivalence, moving objects and morphisms 'up'.
@[reducible]
noncomputable
def
category_theory.shift_functor_add
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(i j : A) :
Shifting by i + j is the same as shifting by i and then shifting by j.
@[reducible]
noncomputable
def
category_theory.shift_functor_zero
(C : Type u)
(A : Type u_1)
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A] :
category_theory.shift_functor C 0 ≅ 𝟭 C
Shifting by zero is the identity functor.
@[simp]
theorem
category_theory.has_shift.shift_obj_obj
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(n : A)
(X : C) :
@[reducible]
noncomputable
def
category_theory.shift_add
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i j : A) :
(category_theory.shift_functor C (i + j)).obj X ≅ (category_theory.shift_functor C j).obj ((category_theory.shift_functor C i).obj X)
Shifting by i + j is the same as shifting by i and then shifting by j.
theorem
category_theory.shift_add_hom_comp_eq_to_hom₁_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i i' j : A)
(h : i = i')
{X' : C}
(f' : (category_theory.shift_functor C j).obj ((category_theory.shift_functor C i').obj X) ⟶ X') :
(category_theory.shift_add X i j).hom ≫ category_theory.eq_to_hom _ ≫ f' = category_theory.eq_to_hom _ ≫ (category_theory.shift_add X i' j).hom ≫ f'
theorem
category_theory.shift_add_hom_comp_eq_to_hom₁
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i i' j : A)
(h : i = i') :
(category_theory.shift_add X i j).hom ≫ category_theory.eq_to_hom _ = category_theory.eq_to_hom _ ≫ (category_theory.shift_add X i' j).hom
theorem
category_theory.shift_add_hom_comp_eq_to_hom₂_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i j j' : A)
(h : j = j')
{X' : C}
(f' : (category_theory.shift_functor C j').obj ((category_theory.shift_functor C i).obj X) ⟶ X') :
(category_theory.shift_add X i j).hom ≫ category_theory.eq_to_hom _ ≫ f' = category_theory.eq_to_hom _ ≫ (category_theory.shift_add X i j').hom ≫ f'
theorem
category_theory.shift_add_hom_comp_eq_to_hom₂
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i j j' : A)
(h : j = j') :
(category_theory.shift_add X i j).hom ≫ category_theory.eq_to_hom _ = category_theory.eq_to_hom _ ≫ (category_theory.shift_add X i j').hom
theorem
category_theory.shift_add_hom_comp_eq_to_hom₁₂_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i j i' j' : A)
(h₁ : i = i')
(h₂ : j = j')
{X' : C}
(f' : (category_theory.shift_functor C j').obj ((category_theory.shift_functor C i').obj X) ⟶ X') :
(category_theory.shift_add X i j).hom ≫ category_theory.eq_to_hom _ ≫ f' = category_theory.eq_to_hom _ ≫ (category_theory.shift_add X i' j').hom ≫ f'
theorem
category_theory.shift_add_hom_comp_eq_to_hom₁₂
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i j i' j' : A)
(h₁ : i = i')
(h₂ : j = j') :
(category_theory.shift_add X i j).hom ≫ category_theory.eq_to_hom _ = category_theory.eq_to_hom _ ≫ (category_theory.shift_add X i' j').hom
theorem
category_theory.eq_to_hom_comp_shift_add_inv₁_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i i' j : A)
(h : i = i')
{X' : C}
(f' : (category_theory.shift_functor C (i' + j)).obj X ⟶ X') :
category_theory.eq_to_hom _ ≫ (category_theory.shift_add X i' j).inv ≫ f' = (category_theory.shift_add X i j).inv ≫ category_theory.eq_to_hom _ ≫ f'
theorem
category_theory.eq_to_hom_comp_shift_add_inv₁
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i i' j : A)
(h : i = i') :
category_theory.eq_to_hom _ ≫ (category_theory.shift_add X i' j).inv = (category_theory.shift_add X i j).inv ≫ category_theory.eq_to_hom _
theorem
category_theory.eq_to_hom_comp_shift_add_inv₂_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i j j' : A)
(h : j = j')
{X' : C}
(f' : (category_theory.shift_functor C (i + j')).obj X ⟶ X') :
category_theory.eq_to_hom _ ≫ (category_theory.shift_add X i j').inv ≫ f' = (category_theory.shift_add X i j).inv ≫ category_theory.eq_to_hom _ ≫ f'
theorem
category_theory.eq_to_hom_comp_shift_add_inv₂
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i j j' : A)
(h : j = j') :
category_theory.eq_to_hom _ ≫ (category_theory.shift_add X i j').inv = (category_theory.shift_add X i j).inv ≫ category_theory.eq_to_hom _
theorem
category_theory.eq_to_hom_comp_shift_add_inv₁₂
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i j i' j' : A)
(h₁ : i = i')
(h₂ : j = j') :
category_theory.eq_to_hom _ ≫ (category_theory.shift_add X i' j').inv = (category_theory.shift_add X i j).inv ≫ category_theory.eq_to_hom _
theorem
category_theory.eq_to_hom_comp_shift_add_inv₁₂_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C)
(i j i' j' : A)
(h₁ : i = i')
(h₂ : j = j')
{X' : C}
(f' : (category_theory.shift_functor C (i' + j')).obj X ⟶ X') :
category_theory.eq_to_hom _ ≫ (category_theory.shift_add X i' j').inv ≫ f' = (category_theory.shift_add X i j).inv ≫ category_theory.eq_to_hom _ ≫ f'
theorem
category_theory.shift_shift'
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X Y : C)
(f : X ⟶ Y)
(i j : A) :
(category_theory.shift_functor C j).map ((category_theory.shift_functor C i).map f) = (category_theory.shift_add X i j).inv ≫ (category_theory.shift_functor C (i + j)).map f ≫ (category_theory.shift_add Y i j).hom
@[reducible]
noncomputable
def
category_theory.shift_zero
{C : Type u}
(A : Type u_1)
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X : C) :
(category_theory.shift_functor C 0).obj X ≅ X
Shifting by zero is the identity functor.
theorem
category_theory.shift_zero'
{C : Type u}
(A : Type u_1)
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(X Y : C)
(f : X ⟶ Y) :
(category_theory.shift_functor C 0).map f = (category_theory.shift_zero A X).hom ≫ f ≫ (category_theory.shift_zero A Y).inv
@[protected, instance]
noncomputable
def
category_theory.shift_functor.is_equivalence
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(i : A) :
Shifting by i is an equivalence.
@[simp]
theorem
category_theory.shift_functor_inv
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(i : A) :
@[reducible]
noncomputable
def
category_theory.shift_functor_comp_shift_functor_neg
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(i : A) :
category_theory.shift_functor C i ⋙ category_theory.shift_functor C (-i) ≅ 𝟭 C
Shifting by i and then shifting by -i is the identity.
@[reducible]
noncomputable
def
category_theory.shift_functor_neg_comp_shift_functor
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(i : A) :
category_theory.shift_functor C (-i) ⋙ category_theory.shift_functor C i ≅ 𝟭 C
Shifting by -i and then shifting by i is the identity.
@[protected, instance]
def
category_theory.shift_functor_faithful
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(i : A) :
Shifting by n is a faithful functor.
@[protected, instance]
noncomputable
def
category_theory.shift_functor_full
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(i : A) :
Shifting by n is a full functor.
@[protected, instance]
def
category_theory.shift_functor_ess_surj
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(i : A) :
Shifting by n is an essentially surjective functor.
@[reducible]
noncomputable
def
category_theory.shift_shift_neg
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(X : C)
(i : A) :
(category_theory.shift_functor C (-i)).obj ((category_theory.shift_functor C i).obj X) ≅ X
Shifting by i and then shifting by -i is the identity.
@[reducible]
noncomputable
def
category_theory.shift_neg_shift
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(X : C)
(i : A) :
(category_theory.shift_functor C i).obj ((category_theory.shift_functor C (-i)).obj X) ≅ X
Shifting by -i and then shifting by i is the identity.
theorem
category_theory.shift_shift_neg'
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
{X Y : C}
(f : X ⟶ Y)
(i : A) :
(category_theory.shift_functor C (-i)).map ((category_theory.shift_functor C i).map f) = (category_theory.shift_shift_neg X i).hom ≫ f ≫ (category_theory.shift_shift_neg Y i).inv
theorem
category_theory.shift_neg_shift'
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
{X Y : C}
(f : X ⟶ Y)
(i : A) :
(category_theory.shift_functor C i).map ((category_theory.shift_functor C (-i)).map f) = (category_theory.shift_neg_shift X i).hom ≫ f ≫ (category_theory.shift_neg_shift Y i).inv
theorem
category_theory.shift_equiv_triangle
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(n : A)
(X : C) :
(category_theory.shift_functor C n).map (category_theory.shift_shift_neg X n).inv ≫ (category_theory.shift_neg_shift ((category_theory.shift_functor C n).obj X) n).hom = 𝟙 ((category_theory.shift_functor C n).obj X)
theorem
category_theory.shift_shift_neg_hom_shift
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(n : A)
(X : C) :
(category_theory.shift_functor C n).map (category_theory.shift_shift_neg X n).hom = (category_theory.shift_neg_shift ((category_theory.shift_functor C n).obj X) n).hom
theorem
category_theory.shift_shift_neg_inv_shift
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(n : A)
(X : C) :
(category_theory.shift_functor C n).map (category_theory.shift_shift_neg X n).inv = (category_theory.shift_neg_shift ((category_theory.shift_functor C n).obj X) n).inv
@[simp]
theorem
category_theory.shift_shift_neg_shift_eq
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(n : A)
(X : C) :
noncomputable
def
category_theory.shift_equiv
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(n : A) :
C ≌ C
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' := _}
@[simp]
theorem
category_theory.shift_equiv_inverse
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(n : A) :
@[simp]
theorem
category_theory.shift_equiv_functor
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(n : A) :
@[simp]
theorem
category_theory.shift_equiv_counit_iso
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(n : A) :
@[simp]
theorem
category_theory.shift_equiv_unit_iso
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(n : A) :
theorem
category_theory.shift_zero_eq_zero
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
(n : A) :
(category_theory.shift_functor C n).map 0 = 0
noncomputable
def
category_theory.shift_comm
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_comm_monoid A]
[category_theory.has_shift C A]
(X : C)
(i j : A) :
(category_theory.shift_functor C j).obj ((category_theory.shift_functor C i).obj X) ≅ (category_theory.shift_functor C i).obj ((category_theory.shift_functor C j).obj X)
When shifts are indexed by an additive commutative monoid, then shifts commute.
Equations
@[simp]
theorem
category_theory.shift_comm_symm
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_comm_monoid A]
[category_theory.has_shift C A]
(X : C)
(i j : A) :
(category_theory.shift_comm X i j).symm = category_theory.shift_comm X j i
theorem
category_theory.shift_comm'
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_comm_monoid A]
[category_theory.has_shift C A]
{X Y : C}
(f : X ⟶ Y)
(i j : A) :
(category_theory.shift_functor C j).map ((category_theory.shift_functor C i).map f) = (category_theory.shift_comm X i j).hom ≫ (category_theory.shift_functor C i).map ((category_theory.shift_functor C j).map f) ≫ (category_theory.shift_comm Y j i).hom
When shifts are indexed by an additive commutative monoid, then shifts commute.
theorem
category_theory.shift_comm_hom_comp_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_comm_monoid A]
[category_theory.has_shift C A]
{X Y : C}
(f : X ⟶ Y)
(i j : A)
{X' : C}
(f' : (category_theory.shift_functor C i).obj ((category_theory.shift_functor C j).obj Y) ⟶ X') :
(category_theory.shift_comm X i j).hom ≫ (category_theory.shift_functor C i).map ((category_theory.shift_functor C j).map f) ≫ f' = (category_theory.shift_functor C j).map ((category_theory.shift_functor C i).map f) ≫ (category_theory.shift_comm Y i j).hom ≫ f'
theorem
category_theory.shift_comm_hom_comp
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_comm_monoid A]
[category_theory.has_shift C A]
{X Y : C}
(f : X ⟶ Y)
(i j : A) :
(category_theory.shift_comm X i j).hom ≫ (category_theory.shift_functor C i).map ((category_theory.shift_functor C j).map f) = (category_theory.shift_functor C j).map ((category_theory.shift_functor C i).map f) ≫ (category_theory.shift_comm Y i j).hom
noncomputable
def
category_theory.has_shift_of_fully_faithful
{C : Type u}
{A : Type u_1}
[category_theory.category C]
{D : Type u_2}
[category_theory.category D]
[add_monoid A]
[category_theory.has_shift D A]
(F : C ⥤ D)
[category_theory.full F]
[category_theory.faithful F]
(s : A → C ⥤ C)
(i : Π (i : A), s i ⋙ F ≅ F ⋙ category_theory.shift_functor D i) :
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 := _}
@[nolint]
def
category_theory.has_shift_of_fully_faithful_comm
{C : Type u}
{A : Type u_1}
[category_theory.category C]
{D : Type u_2}
[category_theory.category D]
[add_monoid A]
[category_theory.has_shift D A]
(F : C ⥤ D)
[category_theory.full F]
[category_theory.faithful F]
(s : A → C ⥤ C)
(i : Π (i : A), s i ⋙ F ≅ F ⋙ category_theory.shift_functor D i)
(m : A) :
s m ⋙ F ≅ F ⋙ category_theory.shift_functor D m
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