The shift by ℤ generated by an autoequivalence

An autoequivalence e : C ≌ C determines a shift of C by ℤ whose shift by 1 is e.functor and whose shift by -1 is a quasi-inverse of e.functor. The shift functors are, up to isomorphism, the powers of e; the content of the construction is the coherence of the isomorphisms X⟦a + b⟧ ≅ X⟦a⟧⟦b⟧, which is not automatic when the powers of e are formed by iterated composition.

We obtain the coherence by strictification. An e.IntSequence is a family of objects X n, n : ℤ, together with isomorphisms e (X n) ≅ X (n + 1). On these sequences reindexing X ↦ (n ↦ X (n + k)) is a shift by ℤ whose coherence isomorphisms are identities up to eqToHom, so the axioms hold componentwise. Evaluation in degree zero is an equivalence from sequences to C: every object of C occurs as a degree-zero term, and a specified degree-zero morphism extends uniquely to a morphism of sequences. The reindexing shift is transported along this equivalence with Mathlib's HasShift.induced. Reindexing by one corresponds to e.functor under evaluation, which identifies the shift by one.

The sequence and functor definitions are exposed so their generated component lemmas and dependent functor fields can reduce in Lean's module system.

This is how the suspension autoequivalence of the stable category of a Frobenius exact category becomes the shift of that category.

Main definitions

• CategoryTheory.Equivalence.IntSequence: ℤ-indexed sequences of objects linked by e.
• CategoryTheory.Equivalence.IntSequence.eval: evaluation of a sequence in degree zero, an equivalence of categories.
• CategoryTheory.Equivalence.hasShift: the shift of C by ℤ generated by e.
• CategoryTheory.Equivalence.evalCommShift: evaluation commutes with the generated shift.
• CategoryTheory.Equivalence.shiftFunctorOneIso: its shift by 1 is e.functor.
• CategoryTheory.Equivalence.shiftFunctorNegOneIso: its shift by -1 is any quasi-inverse of e.functor.

Main results

• CategoryTheory.Equivalence.shiftFunctor_additive: when C is preadditive and e.functor is additive, every shift functor is additive.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2, where the suspension of a Frobenius stable category is the translation functor.

structure CategoryTheory.Equivalence.IntSequence {C : Type u} [Category.{v, u} C] (e : C ≌ C) : Type (max u v)

A ℤ-indexed sequence of objects of C in which each term is identified with the image under e of the previous one. The identifications are indexed by pairs n, m with n + 1 = m, so that reindexing a sequence needs no transport along equalities of indices.

• X : ℤ → C

  The term in degree n.

• iso (n m : ℤ) (h : n + 1 = m) : e.functor.obj (self.X n) ≅ self.X m

  The identification of e (X n) with the next term X m, where n + 1 = m.

structure CategoryTheory.Equivalence.IntSequence.Hom {C : Type u} [Category.{v, u} C] {e : C ≌ C} (X Y : e.IntSequence) : Type v

A morphism of e-sequences: a family of morphisms of the terms commuting with the identifications e (X n) ≅ X (n + 1).

• f (n : ℤ) : X.X n ⟶ Y.X n

  The component in degree n.

• comm (n m : ℤ) (h : n + 1 = m) : CategoryStruct.comp (e.functor.map (self.f n)) (Y.iso n m h).hom = CategoryStruct.comp (X.iso n m h).hom (self.f m)

theorem CategoryTheory.Equivalence.IntSequence.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {e : C ≌ C} {X Y : e.IntSequence} {x y : X.Hom Y} : x = y ↔ x.f = y.f

theorem CategoryTheory.Equivalence.IntSequence.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {e : C ≌ C} {X Y : e.IntSequence} {x y : X.Hom Y} (f : x.f = y.f) : x = y

theorem CategoryTheory.Equivalence.IntSequence.Hom.comm_assoc {C : Type u} [Category.{v, u} C] {e : C ≌ C} {X Y : e.IntSequence} (self : X.Hom Y) (n m : ℤ) (h : n + 1 = m) {Z : C} (h✝ : Y.X m ⟶ Z) : CategoryStruct.comp (e.functor.map (self.f n)) (CategoryStruct.comp (Y.iso n m h).hom h✝) = CategoryStruct.comp (X.iso n m h).hom (CategoryStruct.comp (self.f m) h✝)

@[instance_reducible]

instance CategoryTheory.Equivalence.IntSequence.instCategory {C : Type u} [Category.{v, u} C] {e : C ≌ C} : Category.{v, max u v} e.IntSequence

Equations

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

theorem CategoryTheory.Equivalence.IntSequence.hom_ext {C : Type u} [Category.{v, u} C] {e : C ≌ C} {X Y : e.IntSequence} {φ ψ : X ⟶ Y} (h : ∀ (n : ℤ), φ.f n = ψ.f n) : φ = ψ

theorem CategoryTheory.Equivalence.IntSequence.hom_ext_iff {C : Type u} [Category.{v, u} C] {e : C ≌ C} {X Y : e.IntSequence} {φ ψ : X ⟶ Y} : φ = ψ ↔ ∀ (n : ℤ), φ.f n = ψ.f n

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.id_f {C : Type u} [Category.{v, u} C] {e : C ≌ C} (X : e.IntSequence) (n : ℤ) : (CategoryStruct.id X).f n = CategoryStruct.id (X.X n)

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.comp_f {C : Type u} [Category.{v, u} C] {e : C ≌ C} {X Y Z : e.IntSequence} (φ : X ⟶ Y) (ψ : Y ⟶ Z) (n : ℤ) : (CategoryStruct.comp φ ψ).f n = CategoryStruct.comp (φ.f n) (ψ.f n)

theorem CategoryTheory.Equivalence.IntSequence.comp_f_assoc {C : Type u} [Category.{v, u} C] {e : C ≌ C} {X Y Z : e.IntSequence} (φ : X ⟶ Y) (ψ : Y ⟶ Z) (n : ℤ) {Z✝ : C} (h : Z.X n ⟶ Z✝) : CategoryStruct.comp ((CategoryStruct.comp φ ψ).f n) h = CategoryStruct.comp (φ.f n) (CategoryStruct.comp (ψ.f n) h)

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.eqToHom_f {C : Type u} [Category.{v, u} C] {e : C ≌ C} {X Y : e.IntSequence} (h : X = Y) (n : ℤ) : (eqToHom h).f n = eqToHom ⋯

theorem CategoryTheory.Equivalence.IntSequence.Hom.f_comp_iso_inv {C : Type u} [Category.{v, u} C] {e : C ≌ C} {X Y : e.IntSequence} (φ : X ⟶ Y) (n m : ℤ) (h : n + 1 = m) : CategoryStruct.comp (φ.f m) (Y.iso n m h).inv = CategoryStruct.comp (X.iso n m h).inv (e.functor.map (φ.f n))

The compatibility of a morphism of sequences with the inverse identifications.

theorem CategoryTheory.Equivalence.IntSequence.Hom.f_comp_iso_inv_assoc {C : Type u} [Category.{v, u} C] {e : C ≌ C} {X Y : e.IntSequence} (φ : X ⟶ Y) (n m : ℤ) (h : n + 1 = m) {Z : C} (h✝ : e.functor.obj (Y.X n) ⟶ Z) : CategoryStruct.comp (φ.f m) (CategoryStruct.comp (Y.iso n m h).inv h✝) = CategoryStruct.comp (X.iso n m h).inv (CategoryStruct.comp (e.functor.map (φ.f n)) h✝)

The compatibility of a morphism of sequences with the inverse identifications.

theorem CategoryTheory.Equivalence.IntSequence.Hom.f_eq {C : Type u} [Category.{v, u} C] {e : C ≌ C} {X Y : e.IntSequence} (φ : X ⟶ Y) {n n' : ℤ} (h : n = n') : φ.f n = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (φ.f n') (eqToHom ⋯))

A morphism of sequences, transported along an equality of indices.

Reindexing

def CategoryTheory.Equivalence.IntSequence.comap {C : Type u} [Category.{v, u} C] {e : C ≌ C} (X : e.IntSequence) (g : ℤ → ℤ) (hg : ∀ (n m : ℤ), n + 1 = m → g n + 1 = g m) : e.IntSequence

The sequence n ↦ X (g n), for an index map g compatible with successors.

Equations

• X.comap g hg = { X := fun (n : ℤ) => X.X (g n), iso := fun (n m : ℤ) (h : n + 1 = m) => X.iso (g n) (g m) ⋯ }

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.comap_X {C : Type u} [Category.{v, u} C] {e : C ≌ C} (X : e.IntSequence) (g : ℤ → ℤ) (hg : ∀ (n m : ℤ), n + 1 = m → g n + 1 = g m) (n : ℤ) : (X.comap g hg).X n = X.X (g n)

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.comap_iso {C : Type u} [Category.{v, u} C] {e : C ≌ C} (X : e.IntSequence) (g : ℤ → ℤ) (hg : ∀ (n m : ℤ), n + 1 = m → g n + 1 = g m) (n m : ℤ) (h : n + 1 = m) : (X.comap g hg).iso n m h = X.iso (g n) (g m) ⋯

theorem CategoryTheory.Equivalence.IntSequence.comap_congr {C : Type u} [Category.{v, u} C] {e : C ≌ C} (X : e.IntSequence) {g g' : ℤ → ℤ} (h : g = g') (hg : ∀ (n m : ℤ), n + 1 = m → g n + 1 = g m) (hg' : ∀ (n m : ℤ), n + 1 = m → g' n + 1 = g' m) : X.comap g hg = X.comap g' hg'

Pulling back along equal index maps gives equal sequences.

def CategoryTheory.Equivalence.IntSequence.reindex {C : Type u} [Category.{v, u} C] {e : C ≌ C} (k : ℤ) : Functor e.IntSequence e.IntSequence

Reindexing sequences by k: the term in degree n of the reindexed sequence is the term in degree n + k. This is the shift by k of IntSequence e.

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.reindex_obj {C : Type u} [Category.{v, u} C] {e : C ≌ C} (k : ℤ) (X : e.IntSequence) : (reindex k).obj X = X.comap (fun (x : ℤ) => x + k) ⋯

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.reindex_map_f {C : Type u} [Category.{v, u} C] {e : C ≌ C} (k : ℤ) {X✝ Y✝ : e.IntSequence} (φ : X✝ ⟶ Y✝) (n : ℤ) : ((reindex k).map φ).f n = φ.f (n + k)

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.reindex_obj_X {C : Type u} [Category.{v, u} C] {e : C ≌ C} (k : ℤ) (X : e.IntSequence) (n : ℤ) : ((reindex k).obj X).X n = X.X (n + k)

theorem CategoryTheory.Equivalence.IntSequence.reindex_obj_zero {C : Type u} [Category.{v, u} C] {e : C ≌ C} (X : e.IntSequence) : (reindex 0).obj X = X

theorem CategoryTheory.Equivalence.IntSequence.reindex_obj_add {C : Type u} [Category.{v, u} C] {e : C ≌ C} (a b : ℤ) (X : e.IntSequence) : (reindex (a + b)).obj X = (reindex b).obj ((reindex a).obj X)

theorem CategoryTheory.Equivalence.IntSequence.reindex_zero {C : Type u} [Category.{v, u} C] {e : C ≌ C} : reindex 0 = Functor.id e.IntSequence

Reindexing by zero is the identity functor.

theorem CategoryTheory.Equivalence.IntSequence.reindex_add {C : Type u} [Category.{v, u} C] {e : C ≌ C} (a b : ℤ) : reindex (a + b) = (reindex a).comp (reindex b)

Reindexing by a + b is reindexing by a followed by reindexing by b.

@[instance_reducible]

instance CategoryTheory.Equivalence.IntSequence.instHasShiftInt {C : Type u} [Category.{v, u} C] {e : C ≌ C} : HasShift e.IntSequence ℤ

The shift of e-sequences by ℤ, given by reindexing. It is strict: its structure isomorphisms are identities up to eqToHom.

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.shiftFunctor_eq_reindex {C : Type u} [Category.{v, u} C] {e : C ≌ C} (k : ℤ) : shiftFunctor e.IntSequence k = reindex k

The shift functor on integer sequences is reindexing.

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.shiftFunctorZero_hom_app_f {C : Type u} [Category.{v, u} C] {e : C ≌ C} (X : e.IntSequence) (n : ℤ) : ((shiftFunctorZero e.IntSequence ℤ).hom.app X).f n = eqToHom ⋯

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.shiftFunctorZero_inv_app_f {C : Type u} [Category.{v, u} C] {e : C ≌ C} (X : e.IntSequence) (n : ℤ) : ((shiftFunctorZero e.IntSequence ℤ).inv.app X).f n = eqToHom ⋯

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.shiftFunctorAdd_hom_app_f {C : Type u} [Category.{v, u} C] {e : C ≌ C} (a b : ℤ) (X : e.IntSequence) (n : ℤ) : ((shiftFunctorAdd e.IntSequence a b).hom.app X).f n = eqToHom ⋯

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.shiftFunctorAdd_inv_app_f {C : Type u} [Category.{v, u} C] {e : C ≌ C} (a b : ℤ) (X : e.IntSequence) (n : ℤ) : ((shiftFunctorAdd e.IntSequence a b).inv.app X).f n = eqToHom ⋯

Evaluation in degree zero

def CategoryTheory.Equivalence.IntSequence.eval {C : Type u} [Category.{v, u} C] {e : C ≌ C} : Functor e.IntSequence C

Evaluation of a sequence in degree zero. It is an equivalence of categories: every object of C occurs as a degree-zero term, and each degree-zero morphism extends uniquely to a morphism of sequences.

Equations

• CategoryTheory.Equivalence.IntSequence.eval = { obj := fun (X : e.IntSequence) => X.X 0, map := fun {X Y : e.IntSequence} (φ : X ⟶ Y) => φ.f 0, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.eval_map {C : Type u} [Category.{v, u} C] {e : C ≌ C} {X✝ Y✝ : e.IntSequence} (φ : X✝ ⟶ Y✝) : eval.map φ = φ.f 0

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.eval_obj {C : Type u} [Category.{v, u} C] {e : C ≌ C} (X : e.IntSequence) : eval.obj X = X.X 0

theorem CategoryTheory.Equivalence.IntSequence.hom_ext_of_f_zero {C : Type u} [Category.{v, u} C] {e : C ≌ C} {X Y : e.IntSequence} {φ ψ : X ⟶ Y} (h : φ.f 0 = ψ.f 0) : φ = ψ

A morphism of sequences is determined by its component in degree zero.

instance CategoryTheory.Equivalence.IntSequence.instFaithfulEval {C : Type u} [Category.{v, u} C] {e : C ≌ C} : eval.Faithful

instance CategoryTheory.Equivalence.IntSequence.instFullEval {C : Type u} [Category.{v, u} C] {e : C ≌ C} : eval.Full

instance CategoryTheory.Equivalence.IntSequence.instEssSurjEval {C : Type u} [Category.{v, u} C] {e : C ≌ C} : eval.EssSurj

instance CategoryTheory.Equivalence.IntSequence.instIsEquivalenceEval {C : Type u} [Category.{v, u} C] {e : C ≌ C} : eval.IsEquivalence

def CategoryTheory.Equivalence.IntSequence.reindexOneCompEvalIso {C : Type u} [Category.{v, u} C] {e : C ≌ C} : (reindex 1).comp eval ≅ eval.comp e.functor

Reindexing by one corresponds to e.functor under evaluation in degree zero.

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.reindexOneCompEvalIso_hom_app {C : Type u} [Category.{v, u} C] {e : C ≌ C} (X : e.IntSequence) : reindexOneCompEvalIso.hom.app X = (X.iso 0 1 ⋯).inv

@[simp]

theorem CategoryTheory.Equivalence.IntSequence.reindexOneCompEvalIso_inv_app {C : Type u} [Category.{v, u} C] {e : C ≌ C} (X : e.IntSequence) : reindexOneCompEvalIso.inv.app X = (X.iso 0 1 ⋯).hom

@[instance_reducible]

noncomputable def CategoryTheory.Equivalence.hasShift {C : Type u} [Category.{v, u} C] (e : C ≌ C) : HasShift C ℤ

The shift of C by ℤ generated by the autoequivalence e: the reindexing shift of e-sequences, transported along evaluation in degree zero. Up to isomorphism, the shift by 1 is e.functor (Equivalence.shiftFunctorOneIso) and the shift by -1 is a quasi-inverse of e.functor (Equivalence.shiftFunctorNegOneIso).

Equations

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

@[instance_reducible]

noncomputable def CategoryTheory.Equivalence.evalCommShift {C : Type u} [Category.{v, u} C] (e : C ≌ C) : IntSequence.eval.CommShift ℤ

Evaluation in degree zero commutes with the shift generated by an autoequivalence.

Equations

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

noncomputable def CategoryTheory.Equivalence.shiftFunctorOneIso {C : Type u} [Category.{v, u} C] (e : C ≌ C) : shiftFunctor C 1 ≅ e.functor

The shift by 1 generated by e is e.functor.

Equations

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

theorem CategoryTheory.Equivalence.evalCommShiftIso_one {C : Type u} [Category.{v, u} C] (e : C ≌ C) : Functor.commShiftIso IntSequence.eval 1 ≪≫ IntSequence.eval.isoWhiskerLeft e.shiftFunctorOneIso = IntSequence.reindexOneCompEvalIso

Evaluation identifies the degree-one shift comparison with the sequence structure map.

noncomputable def CategoryTheory.Equivalence.shiftFunctorNegOneIso {C : Type u} [Category.{v, u} C] (e : C ≌ C) {G : Functor C C} (ε : G.comp e.functor ≅ Functor.id C) : shiftFunctor C (-1) ≅ G

The shift by -1 generated by e is any functor G with G ⋙ e.functor ≅ 𝟭 C, for instance e.inverse through the counit of e.

Equations

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

theorem CategoryTheory.Equivalence.shiftFunctor_additive {C : Type u} [Category.{v, u} C] (e : C ≌ C) [Preadditive C] [e.functor.Additive] (n : ℤ) : (shiftFunctor C n).Additive

When C is preadditive and e.functor is additive, every shift functor generated by e is additive.