Functors which commute with shifts #
Let C and D be two categories equipped with shifts by an additive monoid A. In this file,
we define the notion of functor F : C ⥤ D which "commutes" with these shifts. The associated
type class is [F.CommShift A]. The data consists of commutation isomorphisms
F.commShiftIso a : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a for all a : A
which satisfy a compatibility with the addition and the zero. After this was formalised in Lean,
it was found that this definition is exactly the definition which appears in Jean-Louis
Verdier's thesis (I 1.2.3/1.2.4), although the language is different. (In Verdier's thesis,
the shift is not given by a monoidal functor Discrete A ⥤ C ⥤ C, but by a fibred
category C ⥤ BA, where BA is the category with one object, the endomorphisms of which
identify to A. The choice of a cleavage for this fibered category gives the individual
shift functors.)
References #
- [Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes][verdier1996]
@[simp]
theorem
CategoryTheory.Functor.CommShift.isoZero_hom_app
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
(F : CategoryTheory.Functor C D)
(A : Type u_4)
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
(X : C)
:
(CategoryTheory.Functor.CommShift.isoZero F A).hom.app X = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
((CategoryTheory.shiftFunctorZero D A).inv.app (F.toPrefunctor.obj X))
@[simp]
theorem
CategoryTheory.Functor.CommShift.isoZero_inv_app
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
(F : CategoryTheory.Functor C D)
(A : Type u_4)
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
(X : C)
:
(CategoryTheory.Functor.CommShift.isoZero F A).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero D A).hom.app (F.toPrefunctor.obj X))
(F.toPrefunctor.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))
noncomputable def
CategoryTheory.Functor.CommShift.isoZero
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
(F : CategoryTheory.Functor C D)
(A : Type u_4)
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
:
For any functor F : C ⥤ D, this is the obvious isomorphism
shiftFunctor C (0 : A) ⋙ F ≅ F ⋙ shiftFunctor D (0 : A) deduced from the
isomorphisms shiftFunctorZero on both categories C and D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.CommShift.isoAdd'_hom_app
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
{F : CategoryTheory.Functor C D}
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
{a : A}
{b : A}
{c : A}
(h : a + b = c)
(e₁ : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D a))
(e₂ : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C b) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D b))
(X : C)
:
(CategoryTheory.Functor.CommShift.isoAdd' h e₁ e₂).hom.app X = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.shiftFunctorAdd' C a b c h).hom.app X))
(CategoryTheory.CategoryStruct.comp (e₂.hom.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).toPrefunctor.map (e₁.hom.app X))
((CategoryTheory.shiftFunctorAdd' D a b c h).inv.app (F.toPrefunctor.obj X))))
@[simp]
theorem
CategoryTheory.Functor.CommShift.isoAdd'_inv_app
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
{F : CategoryTheory.Functor C D}
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
{a : A}
{b : A}
{c : A}
(h : a + b = c)
(e₁ : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D a))
(e₂ : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C b) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D b))
(X : C)
:
(CategoryTheory.Functor.CommShift.isoAdd' h e₁ e₂).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' D a b c h).hom.app (F.toPrefunctor.obj X))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).toPrefunctor.map (e₁.inv.app X))
(CategoryTheory.CategoryStruct.comp (e₂.inv.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X))
(F.toPrefunctor.map ((CategoryTheory.shiftFunctorAdd' C a b c h).inv.app X))))
noncomputable def
CategoryTheory.Functor.CommShift.isoAdd'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
{F : CategoryTheory.Functor C D}
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
{a : A}
{b : A}
{c : A}
(h : a + b = c)
(e₁ : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D a))
(e₂ : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C b) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D b))
:
If a functor F : C ⥤ D is equipped with "commutation isomorphisms" with the
shifts by a and b, then there is a commutation isomorphism with the shift by c when
a + b = c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Functor.CommShift.isoAdd
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
{F : CategoryTheory.Functor C D}
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
{a : A}
{b : A}
(e₁ : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D a))
(e₂ : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C b) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D b))
:
CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C (a + b)) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D (a + b))
If a functor F : C ⥤ D is equipped with "commutation isomorphisms" with the
shifts by a and b, then there is a commutation isomorphism with the shift by a + b.
Equations
- CategoryTheory.Functor.CommShift.isoAdd e₁ e₂ = CategoryTheory.Functor.CommShift.isoAdd' (_ : a + b = a + b) e₁ e₂
Instances For
@[simp]
theorem
CategoryTheory.Functor.CommShift.isoAdd_hom_app
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_7, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
{F : CategoryTheory.Functor C D}
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
{a : A}
{b : A}
(e₁ : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D a))
(e₂ : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C b) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D b))
(X : C)
:
(CategoryTheory.Functor.CommShift.isoAdd e₁ e₂).hom.app X = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X))
(CategoryTheory.CategoryStruct.comp (e₂.hom.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).toPrefunctor.map (e₁.hom.app X))
((CategoryTheory.shiftFunctorAdd D a b).inv.app (F.toPrefunctor.obj X))))
@[simp]
theorem
CategoryTheory.Functor.CommShift.isoAdd_inv_app
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_7, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
{F : CategoryTheory.Functor C D}
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
{a : A}
{b : A}
(e₁ : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D a))
(e₂ : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C b) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D b))
(X : C)
:
(CategoryTheory.Functor.CommShift.isoAdd e₁ e₂).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).hom.app (F.toPrefunctor.obj X))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).toPrefunctor.map (e₁.inv.app X))
(CategoryTheory.CategoryStruct.comp (e₂.inv.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X))
(F.toPrefunctor.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X))))
class
CategoryTheory.Functor.CommShift
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
(F : CategoryTheory.Functor C D)
(A : Type u_4)
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
:
Type (max (max u_1 u_4) u_7)
A functor F commutes with the shift by a monoid A if it is equipped with
commutation isomorphisms with the shifts by all a : A, and these isomorphisms
satisfy coherence properties with respect to 0 : A and the addition in A.
- iso : (a : A) → CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor C a) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.shiftFunctor D a)
- add : ∀ (a b : A), CategoryTheory.Functor.CommShift.iso (a + b) = CategoryTheory.Functor.CommShift.isoAdd (CategoryTheory.Functor.CommShift.iso a) (CategoryTheory.Functor.CommShift.iso b)
Instances
def
CategoryTheory.Functor.commShiftIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
(F : CategoryTheory.Functor C D)
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
[CategoryTheory.Functor.CommShift F A]
(a : A)
:
If a functor F commutes with the shift by A (i.e. [F.CommShift A]), then
F.commShiftIso a is the given isomorphism shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a.
Instances For
@[simp]
theorem
CategoryTheory.Functor.commShiftIso_hom_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
(F : CategoryTheory.Functor C D)
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
[CategoryTheory.Functor.CommShift F A]
{X : C}
{Y : C}
(f : X ⟶ Y)
(a : A)
{Z : D}
(h : (CategoryTheory.shiftFunctor D a).toPrefunctor.obj (F.toPrefunctor.obj Y) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.shiftFunctor C a).toPrefunctor.map f))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).hom.app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).hom.app X)
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).toPrefunctor.map (F.toPrefunctor.map f)) h)
@[simp]
theorem
CategoryTheory.Functor.commShiftIso_hom_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
(F : CategoryTheory.Functor C D)
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
[CategoryTheory.Functor.CommShift F A]
{X : C}
{Y : C}
(f : X ⟶ Y)
(a : A)
:
CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.shiftFunctor C a).toPrefunctor.map f))
((CategoryTheory.Functor.commShiftIso F a).hom.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).hom.app X)
((CategoryTheory.shiftFunctor D a).toPrefunctor.map (F.toPrefunctor.map f))
@[simp]
theorem
CategoryTheory.Functor.commShiftIso_inv_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
(F : CategoryTheory.Functor C D)
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
[CategoryTheory.Functor.CommShift F A]
{X : C}
{Y : C}
(f : X ⟶ Y)
(a : A)
{Z : D}
(h : F.toPrefunctor.obj ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj Y) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).toPrefunctor.map (F.toPrefunctor.map f))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app X)
(CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.shiftFunctor C a).toPrefunctor.map f)) h)
@[simp]
theorem
CategoryTheory.Functor.commShiftIso_inv_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
(F : CategoryTheory.Functor C D)
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
[CategoryTheory.Functor.CommShift F A]
{X : C}
{Y : C}
(f : X ⟶ Y)
(a : A)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).toPrefunctor.map (F.toPrefunctor.map f))
((CategoryTheory.Functor.commShiftIso F a).inv.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app X)
(F.toPrefunctor.map ((CategoryTheory.shiftFunctor C a).toPrefunctor.map f))
theorem
CategoryTheory.Functor.commShiftIso_zero
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_7, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
(F : CategoryTheory.Functor C D)
(A : Type u_4)
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
[CategoryTheory.Functor.CommShift F A]
:
theorem
CategoryTheory.Functor.commShiftIso_add
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_7, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
(F : CategoryTheory.Functor C D)
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
[CategoryTheory.Functor.CommShift F A]
(a : A)
(b : A)
:
theorem
CategoryTheory.Functor.commShiftIso_add'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_7, u_1} C]
[CategoryTheory.Category.{u_6, u_2} D]
(F : CategoryTheory.Functor C D)
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
[CategoryTheory.HasShift D A]
[CategoryTheory.Functor.CommShift F A]
{a : A}
{b : A}
{c : A}
(h : a + b = c)
:
instance
CategoryTheory.Functor.CommShift.id
(C : Type u_1)
[CategoryTheory.Category.{u_6, u_1} C]
{A : Type u_4}
[AddMonoid A]
[CategoryTheory.HasShift C A]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Functor.map_shiftFunctorComm_hom_app
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_7, u_2} D]
{B : Type u_5}
[AddCommMonoid B]
[CategoryTheory.HasShift C B]
[CategoryTheory.HasShift D B]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.CommShift F B]
(X : C)
(a : B)
(b : B)
:
F.toPrefunctor.map ((CategoryTheory.shiftFunctorComm C a b).hom.app X) = CategoryTheory.CategoryStruct.comp
((CategoryTheory.Functor.commShiftIso F b).hom.app ((CategoryTheory.shiftFunctor C a).toPrefunctor.obj X))
(CategoryTheory.CategoryStruct.comp
((CategoryTheory.shiftFunctor D b).toPrefunctor.map ((CategoryTheory.Functor.commShiftIso F a).hom.app X))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm D a b).hom.app (F.toPrefunctor.obj X))
(CategoryTheory.CategoryStruct.comp
((CategoryTheory.shiftFunctor D a).toPrefunctor.map ((CategoryTheory.Functor.commShiftIso F b).inv.app X))
((CategoryTheory.Functor.commShiftIso F a).inv.app ((CategoryTheory.shiftFunctor C b).toPrefunctor.obj X)))))