Shift #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
[has_shift C A] is implemented using monoidal_functor (discrete A) (C ⥤ C).
However, the API of monodial functors is used only internally: one should use the API of
shifts functors which includes shift_functor C a : C ⥤ C for a : A,
shift_functor_zero C A : shift_functor C (0 : A) ≅ 𝟭 C and
shift_functor_add C i j : shift_functor C (i + j) ≅ shift_functor C i ⋙ shift_functor C j
(and its variant shift_functor_add'). These isomorphisms satisfy some coherence properties
which are stated in lemmas like shift_functor_add'_assoc, shift_functor_add'_zero_add and
shift_functor_add'_add_zero.
@[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
- zero : self.F 0 ≅ 𝟭 C
- add : Π (n m : A), self.F (n + m) ≅ self.F n ⋙ self.F m
- assoc_hom_app : ∀ (m₁ m₂ m₃ : A) (X : C), (self.add (m₁ + m₂) m₃).hom.app X ≫ (self.F m₃).map ((self.add m₁ m₂).hom.app X) = category_theory.eq_to_hom _ ≫ (self.add m₁ (m₂ + m₃)).hom.app X ≫ (self.add m₂ m₃).hom.app ((self.F m₁).obj X)
- zero_add_hom_app : ∀ (n : A) (X : C), (self.add 0 n).hom.app X = category_theory.eq_to_hom _ ≫ (self.F n).map (self.zero.inv.app X)
- add_zero_hom_app : ∀ (n : A) (X : C), (self.add n 0).hom.app X = category_theory.eq_to_hom _ ≫ self.zero.inv.app ((self.F n).obj X)
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
theorem
category_theory.shift_mk_core.assoc_hom_app_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
(self : category_theory.shift_mk_core C A)
(m₁ m₂ m₃ : A)
(X : C)
{X' : C}
(f' : (self.F m₃).obj ((self.F m₁ ⋙ self.F m₂).obj X) ⟶ X') :
theorem
category_theory.shift_mk_core.assoc_inv_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
(h : category_theory.shift_mk_core C A)
(m₁ m₂ m₃ : A)
(X : C) :
theorem
category_theory.shift_mk_core.assoc_inv_app_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
(h : category_theory.shift_mk_core C A)
(m₁ m₂ m₃ : A)
(X : C)
{X' : C}
(f' : (h.F (m₁ + m₂ + m₃)).obj X ⟶ X') :
theorem
category_theory.shift_mk_core.zero_add_inv_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
(h : category_theory.shift_mk_core C A)
(n : A)
(X : C) :
theorem
category_theory.shift_mk_core.add_zero_inv_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
(h : category_theory.shift_mk_core C A)
(n : A)
(X : C) :
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.zero.inv, μ := λ (m n : category_theory.discrete A), (h.add m.as n.as).inv, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}}
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.
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'.
Equations
Instances for category_theory.shift_functor
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.
Equations
- category_theory.shift_functor_add C i j = ((category_theory.shift_monoidal_functor C A).μ_iso {as := i} {as := j}).symm
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 k : A)
(h : i + j = k) :
When k = i + j, shifting by k is the same as shifting by i and then shifting by j.
Equations
theorem
category_theory.shift_functor_add'_eq_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) :
category_theory.shift_functor_add' C i j (i + j) rfl = category_theory.shift_functor_add C i j
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.
Equations
theorem
category_theory.shift_mk_core.shift_functor_eq
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
(h : category_theory.shift_mk_core C A)
(a : A) :
category_theory.shift_functor C a = h.F a
theorem
category_theory.shift_mk_core.shift_functor_zero_eq
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
(h : category_theory.shift_mk_core C A) :
theorem
category_theory.shift_mk_core.shift_functor_add_eq
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
(h : category_theory.shift_mk_core C A)
(a b : A) :
category_theory.shift_functor_add C a b = h.add a b
theorem
category_theory.shift_functor_add'_zero_add
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a : A) :
theorem
category_theory.shift_functor_add'_add_zero
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a : A) :
theorem
category_theory.shift_functor_add'_assoc
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A)
(h₁₂ : a₁ + a₂ = a₁₂)
(h₂₃ : a₂ + a₃ = a₂₃)
(h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) :
category_theory.shift_functor_add' C a₁₂ a₃ a₁₂₃ _ ≪≫ category_theory.iso_whisker_right (category_theory.shift_functor_add' C a₁ a₂ a₁₂ h₁₂) (category_theory.shift_functor C a₃) ≪≫ (category_theory.shift_functor C a₁).associator (category_theory.shift_functor C a₂) (category_theory.shift_functor C a₃) = category_theory.shift_functor_add' C a₁ a₂₃ a₁₂₃ _ ≪≫ category_theory.iso_whisker_left (category_theory.shift_functor C a₁) (category_theory.shift_functor_add' C a₂ a₃ a₂₃ h₂₃)
theorem
category_theory.shift_functor_add_assoc
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a₁ a₂ a₃ : A) :
category_theory.shift_functor_add C (a₁ + a₂) a₃ ≪≫ category_theory.iso_whisker_right (category_theory.shift_functor_add C a₁ a₂) (category_theory.shift_functor C a₃) ≪≫ (category_theory.shift_functor C a₁).associator (category_theory.shift_functor C a₂) (category_theory.shift_functor C a₃) = category_theory.shift_functor_add' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) _ ≪≫ category_theory.iso_whisker_left (category_theory.shift_functor C a₁) (category_theory.shift_functor_add C a₂ a₃)
theorem
category_theory.shift_functor_add'_zero_add_hom_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a : A)
(X : C) :
(category_theory.shift_functor_add' C 0 a a _).hom.app X = (category_theory.shift_functor C a).map ((category_theory.shift_functor_zero C A).inv.app X)
theorem
category_theory.shift_functor_add_zero_add_hom_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a : A)
(X : C) :
(category_theory.shift_functor_add C 0 a).hom.app X = category_theory.eq_to_hom _ ≫ (category_theory.shift_functor C a).map ((category_theory.shift_functor_zero C A).inv.app X)
theorem
category_theory.shift_functor_add'_zero_add_inv_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a : A)
(X : C) :
(category_theory.shift_functor_add' C 0 a a _).inv.app X = (category_theory.shift_functor C a).map ((category_theory.shift_functor_zero C A).hom.app X)
theorem
category_theory.shift_functor_add_zero_add_inv_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a : A)
(X : C) :
(category_theory.shift_functor_add C 0 a).inv.app X = (category_theory.shift_functor C a).map ((category_theory.shift_functor_zero C A).hom.app X) ≫ category_theory.eq_to_hom _
theorem
category_theory.shift_functor_add'_add_zero_hom_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a : A)
(X : C) :
(category_theory.shift_functor_add' C a 0 a _).hom.app X = (category_theory.shift_functor_zero C A).inv.app ((category_theory.shift_functor C a).obj X)
theorem
category_theory.shift_functor_add_add_zero_hom_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a : A)
(X : C) :
(category_theory.shift_functor_add C a 0).hom.app X = category_theory.eq_to_hom _ ≫ (category_theory.shift_functor_zero C A).inv.app ((category_theory.shift_functor C a).obj X)
theorem
category_theory.shift_functor_add'_add_zero_inv_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a : A)
(X : C) :
(category_theory.shift_functor_add' C a 0 a _).inv.app X = (category_theory.shift_functor_zero C A).hom.app ((category_theory.shift_functor C a).obj X)
theorem
category_theory.shift_functor_add_add_zero_inv_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a : A)
(X : C) :
(category_theory.shift_functor_add C a 0).inv.app X = (category_theory.shift_functor_zero C A).hom.app ((category_theory.shift_functor C a).obj X) ≫ category_theory.eq_to_hom _
theorem
category_theory.shift_functor_add'_assoc_hom_app_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A)
(h₁₂ : a₁ + a₂ = a₁₂)
(h₂₃ : a₂ + a₃ = a₂₃)
(h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃)
(X : C)
{X' : C}
(f' : (category_theory.shift_functor C a₃).obj ((category_theory.shift_functor C a₁ ⋙ category_theory.shift_functor C a₂).obj X) ⟶ X') :
(category_theory.shift_functor_add' C a₁₂ a₃ a₁₂₃ _).hom.app X ≫ (category_theory.shift_functor C a₃).map ((category_theory.shift_functor_add' C a₁ a₂ a₁₂ h₁₂).hom.app X) ≫ f' = (category_theory.shift_functor_add' C a₁ a₂₃ a₁₂₃ _).hom.app X ≫ (category_theory.shift_functor_add' C a₂ a₃ a₂₃ h₂₃).hom.app ((category_theory.shift_functor C a₁).obj X) ≫ f'
theorem
category_theory.shift_functor_add'_assoc_hom_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A)
(h₁₂ : a₁ + a₂ = a₁₂)
(h₂₃ : a₂ + a₃ = a₂₃)
(h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃)
(X : C) :
(category_theory.shift_functor_add' C a₁₂ a₃ a₁₂₃ _).hom.app X ≫ (category_theory.shift_functor C a₃).map ((category_theory.shift_functor_add' C a₁ a₂ a₁₂ h₁₂).hom.app X) = (category_theory.shift_functor_add' C a₁ a₂₃ a₁₂₃ _).hom.app X ≫ (category_theory.shift_functor_add' C a₂ a₃ a₂₃ h₂₃).hom.app ((category_theory.shift_functor C a₁).obj X)
theorem
category_theory.shift_functor_add'_assoc_inv_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A)
(h₁₂ : a₁ + a₂ = a₁₂)
(h₂₃ : a₂ + a₃ = a₂₃)
(h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃)
(X : C) :
(category_theory.shift_functor C a₃).map ((category_theory.shift_functor_add' C a₁ a₂ a₁₂ h₁₂).inv.app X) ≫ (category_theory.shift_functor_add' C a₁₂ a₃ a₁₂₃ _).inv.app X = (category_theory.shift_functor_add' C a₂ a₃ a₂₃ h₂₃).inv.app ((category_theory.shift_functor C a₁).obj X) ≫ (category_theory.shift_functor_add' C a₁ a₂₃ a₁₂₃ _).inv.app X
theorem
category_theory.shift_functor_add'_assoc_inv_app_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A)
(h₁₂ : a₁ + a₂ = a₁₂)
(h₂₃ : a₂ + a₃ = a₂₃)
(h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃)
(X : C)
{X' : C}
(f' : (category_theory.shift_functor C a₁₂₃).obj X ⟶ X') :
(category_theory.shift_functor C a₃).map ((category_theory.shift_functor_add' C a₁ a₂ a₁₂ h₁₂).inv.app X) ≫ (category_theory.shift_functor_add' C a₁₂ a₃ a₁₂₃ _).inv.app X ≫ f' = (category_theory.shift_functor_add' C a₂ a₃ a₂₃ h₂₃).inv.app ((category_theory.shift_functor C a₁).obj X) ≫ (category_theory.shift_functor_add' C a₁ a₂₃ a₁₂₃ _).inv.app X ≫ f'
theorem
category_theory.shift_functor_add_assoc_hom_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a₁ a₂ a₃ : A)
(X : C) :
(category_theory.shift_functor_add C (a₁ + a₂) a₃).hom.app X ≫ (category_theory.shift_functor C a₃).map ((category_theory.shift_functor_add C a₁ a₂).hom.app X) = (category_theory.shift_functor_add' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) _).hom.app X ≫ (category_theory.shift_functor_add C a₂ a₃).hom.app ((category_theory.shift_functor C a₁).obj X)
theorem
category_theory.shift_functor_add_assoc_hom_app_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a₁ a₂ a₃ : A)
(X : C)
{X' : C}
(f' : (category_theory.shift_functor C a₃).obj ((category_theory.shift_functor C a₁ ⋙ category_theory.shift_functor C a₂).obj X) ⟶ X') :
(category_theory.shift_functor_add C (a₁ + a₂) a₃).hom.app X ≫ (category_theory.shift_functor C a₃).map ((category_theory.shift_functor_add C a₁ a₂).hom.app X) ≫ f' = (category_theory.shift_functor_add' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) _).hom.app X ≫ (category_theory.shift_functor_add C a₂ a₃).hom.app ((category_theory.shift_functor C a₁).obj X) ≫ f'
theorem
category_theory.shift_functor_add_assoc_inv_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a₁ a₂ a₃ : A)
(X : C) :
(category_theory.shift_functor C a₃).map ((category_theory.shift_functor_add C a₁ a₂).inv.app X) ≫ (category_theory.shift_functor_add C (a₁ + a₂) a₃).inv.app X = (category_theory.shift_functor_add C a₂ a₃).inv.app ((category_theory.shift_functor C a₁).obj X) ≫ (category_theory.shift_functor_add' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) _).inv.app X
theorem
category_theory.shift_functor_add_assoc_inv_app_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(a₁ a₂ a₃ : A)
(X : C)
{X' : C}
(f' : (category_theory.shift_functor C (a₁ + a₂ + a₃)).obj X ⟶ X') :
(category_theory.shift_functor C a₃).map ((category_theory.shift_functor_add C a₁ a₂).inv.app X) ≫ (category_theory.shift_functor_add C (a₁ + a₂) a₃).inv.app X ≫ f' = (category_theory.shift_functor_add C a₂ a₃).inv.app ((category_theory.shift_functor C a₁).obj X) ≫ (category_theory.shift_functor_add' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) _).inv.app X ≫ f'
@[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_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
noncomputable
def
category_theory.shift_functor_comp_iso_id
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_monoid A]
[category_theory.has_shift C A]
(i j : A)
(h : i + j = 0) :
When i + j = 0, shifting by i and by j gives the identity functor
Equations
- category_theory.shift_functor_comp_iso_id C i j h = (category_theory.shift_functor_add' C i j 0 h).symm ≪≫ category_theory.shift_functor_zero C A
@[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]
(i j : A)
(h : i + j = 0) :
(category_theory.shift_equiv' C i j h).inverse = category_theory.shift_functor C j
@[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]
(i j : A)
(h : i + j = 0) :
(category_theory.shift_equiv' C i j h).unit_iso = (category_theory.shift_functor_comp_iso_id C i j h).symm
@[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]
(i j : A)
(h : i + j = 0) :
(category_theory.shift_equiv' C i j h).counit_iso = category_theory.shift_functor_comp_iso_id C j i _
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]
(i j : A)
(h : i + j = 0) :
C ≌ C
shifting by i and shifting by j forms an equivalence when i + j = 0.
Equations
- category_theory.shift_equiv' C i j h = {functor := category_theory.shift_functor C i, inverse := category_theory.shift_functor C j, unit_iso := (category_theory.shift_functor_comp_iso_id C i j h).symm, counit_iso := category_theory.shift_functor_comp_iso_id C j i _, functor_unit_iso_comp' := _}
@[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]
(i j : A)
(h : i + j = 0) :
(category_theory.shift_equiv' C i j h).functor = category_theory.shift_functor C i
@[reducible]
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]
(i : A) :
C ≌ C
shifting by n and shifting by -n forms an equivalence.
@[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) :
@[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_functor_comp_iso_id C i (-i) _).hom.app X ≫ f ≫ (category_theory.shift_functor_comp_iso_id C i (-i) _).inv.app Y
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_functor_comp_iso_id C (-i) i _).hom.app X ≫ f ≫ (category_theory.shift_functor_comp_iso_id C (-i) i _).inv.app Y
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_functor_comp_iso_id_hom_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(n m : A)
(h : n + m = 0)
(X : C) :
(category_theory.shift_functor C n).map ((category_theory.shift_functor_comp_iso_id C n m h).hom.app X) = (category_theory.shift_functor_comp_iso_id C m n _).hom.app ((category_theory.shift_functor C n).obj X)
theorem
category_theory.shift_shift_functor_comp_iso_id_inv_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_group A]
[category_theory.has_shift C A]
(n m : A)
(h : n + m = 0)
(X : C) :
(category_theory.shift_functor C n).map ((category_theory.shift_functor_comp_iso_id C n m h).inv.app X) = (category_theory.shift_functor_comp_iso_id C m n _).inv.app ((category_theory.shift_functor C n).obj X)
theorem
category_theory.shift_shift_functor_comp_iso_id_add_neg_self_hom_app
{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_functor_comp_iso_id C n (-n) _).hom.app X) = (category_theory.shift_functor_comp_iso_id C (-n) n _).hom.app ((category_theory.shift_functor C n).obj X)
theorem
category_theory.shift_shift_functor_comp_iso_id_add_neg_self_inv_app
{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_functor_comp_iso_id C n (-n) _).inv.app X) = (category_theory.shift_functor_comp_iso_id C (-n) n _).inv.app ((category_theory.shift_functor C n).obj X)
theorem
category_theory.shift_shift_functor_comp_iso_id_neg_add_self_hom_app
{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_functor_comp_iso_id C (-n) n _).hom.app X) = (category_theory.shift_functor_comp_iso_id C n (-n) _).hom.app ((category_theory.shift_functor C (-n)).obj X)
theorem
category_theory.shift_shift_functor_comp_iso_id_neg_add_self_inv_app
{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_functor_comp_iso_id C (-n) n _).inv.app X) = (category_theory.shift_functor_comp_iso_id C n (-n) _).inv.app ((category_theory.shift_functor C (-n)).obj X)
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_functor_comm
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_comm_monoid A]
[category_theory.has_shift C A]
(i j : A) :
When shifts are indexed by an additive commutative monoid, then shifts commute.
Equations
- category_theory.shift_functor_comm C i j = (category_theory.shift_functor_add C i j).symm ≪≫ category_theory.shift_functor_add' C j i (i + j) _
theorem
category_theory.shift_functor_comm_eq
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_comm_monoid A]
[category_theory.has_shift C A]
(i j k : A)
(h : i + j = k) :
category_theory.shift_functor_comm C i j = (category_theory.shift_functor_add' C i j k h).symm ≪≫ category_theory.shift_functor_add' C j i k _
theorem
category_theory.shift_functor_comm_symm
(C : Type u)
{A : Type u_1}
[category_theory.category C]
[add_comm_monoid A]
[category_theory.has_shift C A]
(i j : A) :
@[reducible]
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.
@[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
theorem
category_theory.shift_functor_zero_hom_app_shift
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_comm_monoid A]
[category_theory.has_shift C A]
{X : C}
(n : A) :
(category_theory.shift_functor_zero C A).hom.app ((category_theory.shift_functor C n).obj X) = (category_theory.shift_functor_comm C n 0).hom.app X ≫ (category_theory.shift_functor C n).map ((category_theory.shift_functor_zero C A).hom.app X)
theorem
category_theory.shift_functor_zero_inv_app_shift
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_comm_monoid A]
[category_theory.has_shift C A]
{X : C}
(n : A) :
(category_theory.shift_functor_zero C A).inv.app ((category_theory.shift_functor C n).obj X) = (category_theory.shift_functor C n).map ((category_theory.shift_functor_zero C A).inv.app X) ≫ (category_theory.shift_functor_comm C n 0).inv.app X
theorem
category_theory.shift_functor_comm_hom_app_comp_shift_shift_functor_add_hom_app_assoc
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_comm_monoid A]
[category_theory.has_shift C A]
(m₁ m₂ m₃ : A)
(X : C)
{X' : C}
(f' : (category_theory.shift_functor C m₁).obj ((category_theory.shift_functor C m₂ ⋙ category_theory.shift_functor C m₃).obj X) ⟶ X') :
(category_theory.shift_functor_comm C m₁ (m₂ + m₃)).hom.app X ≫ (category_theory.shift_functor C m₁).map ((category_theory.shift_functor_add C m₂ m₃).hom.app X) ≫ f' = (category_theory.shift_functor_add C m₂ m₃).hom.app ((category_theory.shift_functor C m₁).obj X) ≫ (category_theory.shift_functor C m₃).map ((category_theory.shift_functor_comm C m₁ m₂).hom.app X) ≫ (category_theory.shift_functor_comm C m₁ m₃).hom.app ((category_theory.shift_functor C m₂).obj X) ≫ f'
theorem
category_theory.shift_functor_comm_hom_app_comp_shift_shift_functor_add_hom_app
{C : Type u}
{A : Type u_1}
[category_theory.category C]
[add_comm_monoid A]
[category_theory.has_shift C A]
(m₁ m₂ m₃ : A)
(X : C) :
(category_theory.shift_functor_comm C m₁ (m₂ + m₃)).hom.app X ≫ (category_theory.shift_functor C m₁).map ((category_theory.shift_functor_add C m₂ m₃).hom.app X) = (category_theory.shift_functor_add C m₂ m₃).hom.app ((category_theory.shift_functor C m₁).obj X) ≫ (category_theory.shift_functor C m₃).map ((category_theory.shift_functor_comm C m₁ m₂).hom.app X) ≫ (category_theory.shift_functor_comm C m₁ m₃).hom.app ((category_theory.shift_functor C m₂).obj X)
noncomputable
def
category_theory.has_shift_of_fully_faithful_zero
{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) :
auxiliary definition for has_shift_of_fully_faithful
@[simp]
theorem
category_theory.map_has_shift_of_fully_faithful_zero_hom_app
{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)
(X : C) :
@[simp]
theorem
category_theory.map_has_shift_of_fully_faithful_zero_inv_app
{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)
(X : C) :
noncomputable
def
category_theory.has_shift_of_fully_faithful_add
{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)
(a b : A) :
auxiliary definition for has_shift_of_fully_faithful
Equations
- category_theory.has_shift_of_fully_faithful_add F s i a b = category_theory.nat_iso_of_comp_fully_faithful F (i (a + b) ≪≫ category_theory.iso_whisker_left F (category_theory.shift_functor_add D a b) ≪≫ (F.associator (category_theory.shift_functor D a) (category_theory.shift_functor D b)).symm ≪≫ category_theory.iso_whisker_right (i a).symm (category_theory.shift_functor D b) ≪≫ (s a).associator F (category_theory.shift_functor D b) ≪≫ category_theory.iso_whisker_left (s a) (i b).symm ≪≫ ((s a).associator (s b) F).symm)
@[simp]
theorem
category_theory.map_has_shift_of_fully_faithful_add_hom_app
{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)
(a b : A)
(X : C) :
@[simp]
theorem
category_theory.map_has_shift_of_fully_faithful_add_inv_app
{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)
(a b : A)
(X : C) :
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, zero := category_theory.has_shift_of_fully_faithful_zero F s i, add := category_theory.has_shift_of_fully_faithful_add F s i, assoc_hom_app := _, zero_add_hom_app := _, add_zero_hom_app := _}