Functors intertwining autoequivalences

An isomorphism e.functor ⋙ F ≅ F ⋙ e'.functor says that a functor intertwines two autoequivalences. When these autoequivalences generate shifts by ℤ, the isomorphism extends coherently to every integral shift. This file constructs the resulting Functor.CommShift ℤ structure.

The construction uses the strict models of autoequivalence-generated shifts from CategoryTheory.Equivalence.IntSequence. Applying F degreewise sends an e-sequence to an e'-sequence, and this functor commutes strictly with reindexing. The compatibility is then transported back along evaluation in degree zero.

Main definitions

• CategoryTheory.Equivalence.IntSequence.mapFunctor: apply an intertwining functor degreewise to an integer sequence.
• CategoryTheory.Functor.commShiftOfIntertwining: the coherent compatibility with the integral shifts generated by two intertwined autoequivalences.

def CategoryTheory.Equivalence.IntSequence.mapFunctor {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {e : C ≌ C} {e' : D ≌ D} {F : Functor C D} (α : e.functor.comp F ≅ F.comp e'.functor) : Functor e.IntSequence e'.IntSequence

Applying a functor degreewise to integer sequences, using an isomorphism saying that the functor intertwines the generating autoequivalences.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.mapFunctor_map_f {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {e : C ≌ C} {e' : D ≌ D} {F : Functor C D} (α : e.functor.comp F ≅ F.comp e'.functor) {X Y : e.IntSequence} (φ : X ⟶ Y) (n : ℤ) : ((mapFunctor α).map φ).f n = F.map (φ.f n)

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.mapFunctor_obj_X {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {e : C ≌ C} {e' : D ≌ D} {F : Functor C D} (α : e.functor.comp F ≅ F.comp e'.functor) (X : e.IntSequence) (n : ℤ) : ((mapFunctor α).obj X).X n = F.obj (X.X n)

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.mapFunctor_obj_iso_hom {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {e : C ≌ C} {e' : D ≌ D} {F : Functor C D} (α : e.functor.comp F ≅ F.comp e'.functor) (X : e.IntSequence) (n m : ℤ) (h : n + 1 = m) : (((mapFunctor α).obj X).iso n m h).hom = CategoryStruct.comp (α.inv.app (X.X n)) (F.map (X.iso n m h).hom)

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.mapFunctor_obj_iso_inv {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {e : C ≌ C} {e' : D ≌ D} {F : Functor C D} (α : e.functor.comp F ≅ F.comp e'.functor) (X : e.IntSequence) (n m : ℤ) (h : n + 1 = m) : (((mapFunctor α).obj X).iso n m h).inv = CategoryStruct.comp (F.map (X.iso n m h).inv) (α.hom.app (X.X n))

def CategoryTheory.Equivalence.IntSequence.mapFunctorCompEvalIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {e : C ≌ C} {e' : D ≌ D} {F : Functor C D} (α : e.functor.comp F ≅ F.comp e'.functor) : (mapFunctor α).comp eval ≅ eval.comp F

Evaluation in degree zero after applying mapFunctor is applying the original functor after evaluation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.mapFunctorCompEvalIso_hom_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {e : C ≌ C} {e' : D ≌ D} {F : Functor C D} (α : e.functor.comp F ≅ F.comp e'.functor) (X : e.IntSequence) : (mapFunctorCompEvalIso α).hom.app X = CategoryStruct.id (((mapFunctor α).comp eval).obj X)

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.mapFunctorCompEvalIso_inv_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {e : C ≌ C} {e' : D ≌ D} {F : Functor C D} (α : e.functor.comp F ≅ F.comp e'.functor) (X : e.IntSequence) : (mapFunctorCompEvalIso α).inv.app X = CategoryStruct.id ((eval.comp F).obj X)

def CategoryTheory.Equivalence.IntSequence.mapFunctorShiftIso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {e : C ≌ C} {e' : D ≌ D} {F : Functor C D} (α : e.functor.comp F ≅ F.comp e'.functor) (k : ℤ) : (shiftFunctor e.IntSequence k).comp (mapFunctor α) ≅ (mapFunctor α).comp (shiftFunctor e'.IntSequence k)

Applying an intertwining functor degreewise commutes with the reindexing shift.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.mapFunctorShiftIso_hom_app_f {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {e : C ≌ C} {e' : D ≌ D} {F : Functor C D} (α : e.functor.comp F ≅ F.comp e'.functor) (k : ℤ) (X : e.IntSequence) (n : ℤ) : ((mapFunctorShiftIso α k).hom.app X).f n = CategoryStruct.id (F.obj (X.X (n + k)))

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.mapFunctorShiftIso_inv_app_f {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {e : C ≌ C} {e' : D ≌ D} {F : Functor C D} (α : e.functor.comp F ≅ F.comp e'.functor) (k : ℤ) (X : e.IntSequence) (n : ℤ) : ((mapFunctorShiftIso α k).inv.app X).f n = CategoryStruct.id (F.obj (X.X (n + k)))

@[instance_reducible]

noncomputable instance CategoryTheory.Equivalence.IntSequence.mapFunctorCommShift {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {e : C ≌ C} {e' : D ≌ D} {F : Functor C D} (α : e.functor.comp F ≅ F.comp e'.functor) : (mapFunctor α).CommShift ℤ

The degreewise functor associated to an intertwining functor commutes coherently with reindexing.

Equations

• CategoryTheory.Equivalence.IntSequence.mapFunctorCommShift α = { commShiftIso := CategoryTheory.Equivalence.IntSequence.mapFunctorShiftIso α, commShiftIso_zero := ⋯, commShiftIso_add := ⋯ }

@[instance_reducible]

noncomputable def CategoryTheory.Functor.commShiftOfIntertwining {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (e : C ≌ C) (e' : D ≌ D) (α : e.functor.comp F ≅ F.comp e'.functor) : F.CommShift ℤ

A functor intertwining two autoequivalences commutes coherently with the integral shifts generated by those autoequivalences.

Equations

• F.commShiftOfIntertwining e e' α = CategoryTheory.Functor.CommShift.ofComp (CategoryTheory.Functor.CommShiftOfIntertwining.comparison✝ F α) ℤ

theorem CategoryTheory.Functor.commShiftOfIntertwining_iso_one {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (e : C ≌ C) (e' : D ≌ D) (α : e.functor.comp F ≅ F.comp e'.functor) : commShiftIso F 1 = isoWhiskerRight e.shiftFunctorOneIso F ≪≫ α ≪≫ F.isoWhiskerLeft e'.shiftFunctorOneIso.symm

At degree one, the coherent shift comparison recovers the supplied intertwining isomorphism.