Orbit categories of integral shifts

Let D be a preadditive category with an additive ℤ-shift and let n : ℤ. The orbit category D/[n] has the objects of D and hom groups

Hom_{D/[n]}(X, Y) = ⨁_{j : ℤ} Hom_D(X, Y⟦n * j⟧).

Homogeneous pieces f : X ⟶ Y⟦n * i⟧ and g : Y ⟶ Z⟦n * j⟧ compose to f ≫ g⟦n * i⟧' ≫ (Z⟦n * j⟧⟦n * i⟧ ≅ Z⟦n * (i + j)⟧), which is the composition ShiftedHom.comp of shifted morphisms; composition is extended biadditively to the direct sums. The coherence of shiftFunctorAdd' makes this associative.

This file constructs the orbit category with its preadditive structure, the additive and faithful projection D ⥤ D/[n] (the identity on objects and the degree-zero inclusion on morphisms), and the periodicity isomorphism [n] ⋙ π ≅ π. Its component at X is the identity of X⟦n⟧, read as a morphism X⟦n⟧ ⟶ X of degree 1, with inverse in degree -1. More generally X⟦n * i⟧ ≅ X in D/[n] for every i.

It also proves Keller's universal property. An additive functor G : D ⥤ E to a preadditive category with a periodicity isomorphism φ : [n] ⋙ G ≅ G descends to lift G φ : D/[n] ⥤ E, which sends a homogeneous piece f : X ⟶ Y⟦n * i⟧ to G.map f followed by the i-th power of φ at Y (CategoryTheory.Iso.periodicityZPow). The descent restricts to G along the projection and carries the periodicity isomorphism of the projection to φ, and every additive functor with these two properties is isomorphic to it.

Descent is compatible with composition. Postcomposing lift G φ with an additive functor H gives the descent of G ⋙ H. An additive functor F : D ⥤ D' commuting with the shifts induces map F : D/[n] ⥤ D'/[n], the descent of F followed by the projection; if F ⋙ G' ≅ G compatibly with periodicity isomorphisms, then map F followed by the descent of G' is the descent of G. This compares orbit functors defined on different categories, such as a homotopy category and its localization. On orbit hom groups map F is the direct sum of the maps f ↦ f.map F on homogeneous pieces, so it is bijective exactly when these are.

The orbit category is constructed rather than axiomatized: its hom groups are the displayed direct sums, so additive maps out of them are determined by their values on homogeneous pieces (DirectSum.addHom_ext, with TauCeti.OrbitCategory.homOf_def). Keller and Stai use it to compare bounded derived categories with periodic derived categories.

Main definitions

• TauCeti.OrbitCategory D n: the orbit category D/[n].
• TauCeti.OrbitCategory.homOf: the inclusion of a homogeneous piece into an orbit hom group.
• TauCeti.OrbitCategory.projection: the projection functor D ⥤ D/[n].
• TauCeti.OrbitCategory.shiftNatIso: the isomorphism [n * i] ⋙ π ≅ π.
• TauCeti.OrbitCategory.periodicity: the periodicity isomorphism [n] ⋙ π ≅ π.
• TauCeti.OrbitCategory.lift: the descent of an additive functor with a periodicity isomorphism.
• TauCeti.OrbitCategory.liftMap: the additive action of the descent on orbit hom groups.
• TauCeti.OrbitCategory.projectionCompLift: the descent restricts to the original functor.
• TauCeti.OrbitCategory.isoLift: any additive functor restricting to G compatibly with the periodicity isomorphisms is isomorphic to the descent.
• TauCeti.OrbitCategory.liftCompIso: lift G φ ⋙ H is the descent of G ⋙ H.
• TauCeti.OrbitCategory.map: the functor D/[n] ⥤ D'/[n] induced by a functor commuting with the shifts.
• TauCeti.OrbitCategory.mapCompLiftIso: descent along the induced functor map F.

Main results

• TauCeti.OrbitCategory.homOf_comp_homOf: homogeneous pieces compose by ShiftedHom.comp.
• TauCeti.OrbitCategory.lift_map_homOf: the descent on homogeneous pieces.
• TauCeti.OrbitCategory.lift_map_periodicity_hom_app: the descent carries the periodicity isomorphism of the projection to φ.
• TauCeti.OrbitCategory.map_map_homOf: the induced functor on homogeneous pieces.
• TauCeti.OrbitCategory.map_map_periodicity_hom_app: the induced functor carries the periodicity isomorphism of the projection to the shift comparison followed by periodicity.
• TauCeti.OrbitCategory.map_map_bijective_iff: the induced functor is bijective on orbit morphisms exactly when F is bijective on shifted morphisms of every multiple of n.

References

• B. Keller, On triangulated orbit categories, Documenta Mathematica 10 (2005), 551–581, Section 1.
• T. Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3.3.

structure TauCeti.OrbitCategory (D : Type u) [CategoryTheory.Category.{v, u} D] (n : ℤ) : Type u

The orbit category D/[n] of a category with an integral shift. Its objects are those of D; the wrapper keeps the orbit category and D apart for instance resolution. The morphisms are constructed in the Category instance below, when D is preadditive with an additive shift.

• obj : D

  The underlying object of D.

@[reducible, inline]

abbrev TauCeti.OrbitCategory.Hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] {n : ℤ} (X Y : OrbitCategory D n) : Type v

The orbit hom group ⨁_{j : ℤ} Hom_D(X, Y⟦n * j⟧).

@[instance_reducible]

noncomputable instance TauCeti.OrbitCategory.instCategoryStruct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} : CategoryTheory.CategoryStruct.{v, u} (OrbitCategory D n)

@[instance_reducible]

instance TauCeti.OrbitCategory.instAddCommGroupHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} (X Y : OrbitCategory D n) : AddCommGroup (X ⟶ Y)

@[instance_reducible]

noncomputable instance TauCeti.OrbitCategory.instCategory {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} : CategoryTheory.Category.{v, u} (OrbitCategory D n)

@[instance_reducible]

instance TauCeti.OrbitCategory.instPreadditive {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} : CategoryTheory.Preadditive (OrbitCategory D n)

def TauCeti.OrbitCategory.homOf {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {X Y : D} (i : ℤ) : CategoryTheory.ShiftedHom X Y (n * i) →+ ({ obj := X } ⟶ { obj := Y })

The inclusion of the homogeneous piece of degree i, the morphisms X ⟶ Y⟦n * i⟧ of D, into the orbit hom group from X to Y.

theorem TauCeti.OrbitCategory.homOf_def {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {X Y : D} (i : ℤ) : homOf i = DirectSum.of (fun (j : ℤ) => CategoryTheory.ShiftedHom X Y (n * j)) i

homOf i is the inclusion DirectSum.of of the summand of degree i.

@[simp]

theorem TauCeti.OrbitCategory.toAddMonoid_homOf {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {X Y : D} {A : Type u_1} [AddCommMonoid A] (φ : (j : ℤ) → CategoryTheory.ShiftedHom X Y (n * j) →+ A) (i : ℤ) (f : CategoryTheory.ShiftedHom X Y (n * i)) : (DirectSum.toAddMonoid φ) ((homOf i) f) = (φ i) f

An additive map out of an orbit hom group defined summand by summand sends a homogeneous piece to the value of the corresponding summand.

theorem TauCeti.OrbitCategory.homOf_comp_homOf_eq {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {X Y Z : D} {i j k : ℤ} (h : i + j = k) (f : CategoryTheory.ShiftedHom X Y (n * i)) (g : CategoryTheory.ShiftedHom Y Z (n * j)) : CategoryTheory.CategoryStruct.comp ((homOf i) f) ((homOf j) g) = (homOf k) (f.comp g ⋯)

@[simp]

theorem TauCeti.OrbitCategory.homOf_comp_homOf {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {X Y Z : D} {i j : ℤ} (f : CategoryTheory.ShiftedHom X Y (n * i)) (g : CategoryTheory.ShiftedHom Y Z (n * j)) : CategoryTheory.CategoryStruct.comp ((homOf i) f) ((homOf j) g) = (homOf (i + j)) (f.comp g ⋯)

Homogeneous pieces compose by the composition of shifted morphisms, adding degrees. This has low priority so that the degree-zero special cases below, which avoid indices 0 + j, apply first.

theorem TauCeti.OrbitCategory.id_def {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} (X : D) : CategoryTheory.CategoryStruct.id { obj := X } = (homOf 0) (CategoryTheory.ShiftedHom.mk₀ (n * 0) ⋯ (CategoryTheory.CategoryStruct.id X))

@[simp]

theorem TauCeti.OrbitCategory.homOf_mk₀_comp_homOf {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {X Y Z : D} {j : ℤ} (f : X ⟶ Y) (g : CategoryTheory.ShiftedHom Y Z (n * j)) : CategoryTheory.CategoryStruct.comp ((homOf 0) (CategoryTheory.ShiftedHom.mk₀ (n * 0) ⋯ f)) ((homOf j) g) = (homOf j) (CategoryTheory.CategoryStruct.comp f g)

Precomposition with a degree-zero piece is composition in D.

@[simp]

theorem TauCeti.OrbitCategory.homOf_comp_homOf_mk₀ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {X Y Z : D} {i : ℤ} (f : CategoryTheory.ShiftedHom X Y (n * i)) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((homOf i) f) ((homOf 0) (CategoryTheory.ShiftedHom.mk₀ (n * 0) ⋯ g)) = (homOf i) (CategoryTheory.CategoryStruct.comp f (g⟦n * i⟧'))

Postcomposition with a degree-zero piece shifts it into the degree of the first piece.

@[reducible, inline]

noncomputable abbrev TauCeti.OrbitCategory.projection {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} : CategoryTheory.Functor D (OrbitCategory D n)

The projection D ⥤ D/[n]: the identity on objects and the degree-zero inclusion on morphisms.

theorem TauCeti.OrbitCategory.projection_map {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {X Y : D} (f : X ⟶ Y) : projection.map f = (homOf 0) (CategoryTheory.ShiftedHom.mk₀ (n * 0) ⋯ f)

instance TauCeti.OrbitCategory.instAdditiveProjection {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} : projection.Additive

instance TauCeti.OrbitCategory.instFaithfulProjection {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} : projection.Faithful

def TauCeti.OrbitCategory.shiftIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} (X : D) (m i : ℤ) (h : n * i = m) : projection.obj (X⟦m⟧) ≅ projection.obj X

For m = n * i, the objects X⟦m⟧ and X are isomorphic in the orbit category: the identity of X⟦m⟧ is a homogeneous morphism X⟦m⟧ ⟶ X of degree i. Its inverse has degree -i.

@[simp]

theorem TauCeti.OrbitCategory.shiftIso_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} (X : D) (m i : ℤ) (h : n * i = m) : (shiftIso X m i h).hom = (homOf i) (CategoryTheory.eqToHom ⋯)

@[simp]

theorem TauCeti.OrbitCategory.shiftIso_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} (X : D) (m i : ℤ) (h : n * i = m) : (shiftIso X m i h).inv = (homOf (-i)) ((CategoryTheory.shiftFunctorCompIsoId D m (n * -i) ⋯).inv.app X)

noncomputable def TauCeti.OrbitCategory.shiftNatIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} (m i : ℤ) (h : n * i = m) : (CategoryTheory.shiftFunctor D m).comp projection ≅ projection

For m = n * i, the shift by m becomes isomorphic to the identity in the orbit category, with components shiftIso.

@[simp]

theorem TauCeti.OrbitCategory.shiftNatIso_hom_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} (m i : ℤ) (h : n * i = m) (X : D) : (shiftNatIso m i h).hom.app X = (shiftIso X m i h).hom

@[simp]

theorem TauCeti.OrbitCategory.shiftNatIso_inv_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} (m i : ℤ) (h : n * i = m) (X : D) : (shiftNatIso m i h).inv.app X = (shiftIso X m i h).inv

@[reducible, inline]

noncomputable abbrev TauCeti.OrbitCategory.periodicity {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} : (CategoryTheory.shiftFunctor D n).comp projection ≅ projection

The periodicity isomorphism [n] ⋙ π ≅ π of the projection to the orbit category. Its component at X is the identity of X⟦n⟧, viewed as a morphism X⟦n⟧ ⟶ X of degree 1.

theorem TauCeti.OrbitCategory.homOf_eq_projection_map_comp_shiftIso_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {X Y : D} (i : ℤ) (f : CategoryTheory.ShiftedHom X Y (n * i)) : (homOf i) f = CategoryTheory.CategoryStruct.comp (projection.map f) (shiftIso Y (n * i) i ⋯).hom

A homogeneous piece f : X ⟶ Y⟦n * i⟧ is the projection of f followed by the shift isomorphism Y⟦n * i⟧ ≅ Y of the orbit category.

theorem TauCeti.OrbitCategory.shiftIso_hom_eq_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} (X : D) {m₁ m₂ m i j k : ℤ} (h₁ : n * i = m₁) (h₂ : n * j = m₂) (h : n * k = m) (hk : i + j = k) : (shiftIso X m k h).hom = CategoryTheory.CategoryStruct.comp (projection.map ((CategoryTheory.shiftFunctorAdd' D m₁ m₂ m ⋯).hom.app X)) (CategoryTheory.CategoryStruct.comp (shiftIso (X⟦m₁⟧) m₂ j h₂).hom (shiftIso X m₁ i h₁).hom)

The shift isomorphism of X⟦n * k⟧ in the orbit category, for k = i + j, is the composite of the projection of X⟦n * k⟧ ≅ X⟦n * i⟧⟦n * j⟧ with the shift isomorphisms of X⟦n * i⟧ and of X.

theorem TauCeti.OrbitCategory.hom_induction_on {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {X Y : OrbitCategory D n} {motive : (X ⟶ Y) → Prop} (f : X ⟶ Y) (zero : motive 0) (homOf : ∀ (i : ℤ) (g : CategoryTheory.ShiftedHom X.obj Y.obj (n * i)), motive ((homOf i) g)) (add : ∀ (f₁ f₂ : X ⟶ Y), motive f₁ → motive f₂ → motive (f₁ + f₂)) : motive f

Induction principle for morphisms of the orbit category: a property of morphisms that holds for 0 and for every homogeneous piece, and is closed under addition, holds for every morphism.

def TauCeti.OrbitCategory.liftMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) (X Y : OrbitCategory D n) : (X ⟶ Y) →+ (G.obj X.obj ⟶ G.obj Y.obj)

The action on morphisms of the descent lift G φ: the additive map sending a homogeneous piece f : X ⟶ Y⟦n * i⟧ of degree i to G.map f followed by the i-th power φ.periodicityZPow i of the periodicity isomorphism at Y.

@[simp]

theorem TauCeti.OrbitCategory.liftMap_homOf {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) {X Y : D} (i : ℤ) (f : CategoryTheory.ShiftedHom X Y (n * i)) : (liftMap G φ { obj := X } { obj := Y }) ((homOf i) f) = CategoryTheory.CategoryStruct.comp (G.map f) ((φ.periodicityZPow i).hom.app Y)

The additive map liftMap G φ on a homogeneous piece.

@[implicit_reducible]

def TauCeti.OrbitCategory.lift {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) : CategoryTheory.Functor (OrbitCategory D n) E

Keller's descent of an additive functor G with a periodicity isomorphism φ : [n] ⋙ G ≅ G to the orbit category D/[n]. It is G on objects, and acts on morphisms by liftMap G φ.

@[simp]

theorem TauCeti.OrbitCategory.lift_obj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) (X : OrbitCategory D n) : (lift G φ).obj X = G.obj X.obj

@[simp]

theorem TauCeti.OrbitCategory.lift_map_homOf {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) {X Y : D} (i : ℤ) (f : CategoryTheory.ShiftedHom X Y (n * i)) : (lift G φ).map ((homOf i) f) = CategoryTheory.CategoryStruct.comp (G.map f) ((φ.periodicityZPow i).hom.app Y)

The descent sends a homogeneous piece f : X ⟶ Y⟦n * i⟧ to G.map f followed by the i-th power of the periodicity isomorphism at Y.

instance TauCeti.OrbitCategory.instAdditiveLift {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) : (lift G φ).Additive

theorem TauCeti.OrbitCategory.lift_map_projection_map {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) {X Y : D} (f : X ⟶ Y) : (lift G φ).map (projection.map f) = G.map f

The descent sends the projection of a morphism f of D to G.map f.

@[simp]

theorem TauCeti.OrbitCategory.lift_map_homOf_mk₀ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) {X Y : D} (f : X ⟶ Y) : (lift G φ).map ((homOf 0) (CategoryTheory.ShiftedHom.mk₀ (n * 0) ⋯ f)) = G.map f

The descent sends a degree-zero piece f : X ⟶ Y to G.map f. This is lift_map_projection_map in the form simp sees, since simp unfolds the reducible projection.map f to this piece.

noncomputable def TauCeti.OrbitCategory.projectionCompLift {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) : projection.comp (lift G φ) ≅ G

The descent restricts to G along the projection.

@[simp]

theorem TauCeti.OrbitCategory.projectionCompLift_hom_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) (X : D) : (projectionCompLift G φ).hom.app X = CategoryTheory.CategoryStruct.id ((projection.comp (lift G φ)).obj X)

@[simp]

theorem TauCeti.OrbitCategory.projectionCompLift_inv_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) (X : D) : (projectionCompLift G φ).inv.app X = CategoryTheory.CategoryStruct.id (G.obj X)

theorem TauCeti.OrbitCategory.lift_map_periodicity_hom_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) (X : D) : (lift G φ).map (periodicity.hom.app X) = φ.hom.app X

The descent carries the periodicity isomorphism of the projection to φ.

noncomputable def TauCeti.OrbitCategory.isoLift {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] {G : CategoryTheory.Functor D E} [G.Additive] {φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G} (F : CategoryTheory.Functor (OrbitCategory D n) E) [F.Additive] (e : projection.comp F ≅ G) (he : ∀ (X : D), CategoryTheory.CategoryStruct.comp (F.map (periodicity.hom.app X)) (e.hom.app X) = CategoryTheory.CategoryStruct.comp (e.hom.app (X⟦n⟧)) (φ.hom.app X)) : F ≅ lift G φ

Uniqueness in Keller's universal property: an additive functor F out of the orbit category whose restriction along the projection is identified with G by e, compatibly with the periodicity isomorphisms, is isomorphic to the descent lift G φ, by e on components.

@[simp]

theorem TauCeti.OrbitCategory.isoLift_hom_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] {G : CategoryTheory.Functor D E} [G.Additive] {φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G} (F : CategoryTheory.Functor (OrbitCategory D n) E) [F.Additive] (e : projection.comp F ≅ G) (he : ∀ (X : D), CategoryTheory.CategoryStruct.comp (F.map (periodicity.hom.app X)) (e.hom.app X) = CategoryTheory.CategoryStruct.comp (e.hom.app (X⟦n⟧)) (φ.hom.app X)) (X : D) : (isoLift F e he).hom.app { obj := X } = e.hom.app X

@[simp]

theorem TauCeti.OrbitCategory.isoLift_inv_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] {G : CategoryTheory.Functor D E} [G.Additive] {φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G} (F : CategoryTheory.Functor (OrbitCategory D n) E) [F.Additive] (e : projection.comp F ≅ G) (he : ∀ (X : D), CategoryTheory.CategoryStruct.comp (F.map (periodicity.hom.app X)) (e.hom.app X) = CategoryTheory.CategoryStruct.comp (e.hom.app (X⟦n⟧)) (φ.hom.app X)) (X : D) : (isoLift F e he).inv.app { obj := X } = e.inv.app X

noncomputable def TauCeti.OrbitCategory.liftCompIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) {E' : Type u_1} [CategoryTheory.Category.{u_2, u_1} E'] [CategoryTheory.Preadditive E'] (H : CategoryTheory.Functor E E') [H.Additive] : (lift G φ).comp H ≅ lift (G.comp H) (((CategoryTheory.shiftFunctor D n).associator G H).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight φ H)

Postcomposing the descent lift G φ with an additive functor H gives the descent of G ⋙ H along the image of φ under H.

@[simp]

theorem TauCeti.OrbitCategory.liftCompIso_hom_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) {E' : Type u_1} [CategoryTheory.Category.{u_2, u_1} E'] [CategoryTheory.Preadditive E'] (H : CategoryTheory.Functor E E') [H.Additive] (X : D) : (liftCompIso G φ H).hom.app { obj := X } = CategoryTheory.CategoryStruct.id (H.obj (G.obj X))

@[simp]

theorem TauCeti.OrbitCategory.liftCompIso_inv_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [G.Additive] (φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G) {E' : Type u_1} [CategoryTheory.Category.{u_2, u_1} E'] [CategoryTheory.Preadditive E'] (H : CategoryTheory.Functor E E') [H.Additive] (X : D) : (liftCompIso G φ H).inv.app { obj := X } = CategoryTheory.CategoryStruct.id (H.obj (G.obj X))

noncomputable def TauCeti.OrbitCategory.mapPeriodicity {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.HasShift D ℤ] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.CommShift ℤ] : (CategoryTheory.shiftFunctor D n).comp (F.comp projection) ≅ F.comp projection

The periodicity isomorphism [n] ⋙ F ⋙ π ≅ F ⋙ π of a functor commuting with the shifts, followed by the projection to the orbit category: the shift comparison of F followed by the periodicity isomorphism of the projection.

@[simp]

theorem TauCeti.OrbitCategory.mapPeriodicity_hom_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.HasShift D ℤ] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.CommShift ℤ] (X : D) : (mapPeriodicity F).hom.app X = CategoryTheory.CategoryStruct.comp (projection.map ((CategoryTheory.Functor.commShiftIso F n).hom.app X)) (periodicity.hom.app (F.obj X))

The component of mapPeriodicity F at X: the projected shift comparison of F followed by the periodicity isomorphism of the projection from D'.

@[implicit_reducible]

noncomputable def TauCeti.OrbitCategory.map {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.Additive] [F.CommShift ℤ] : CategoryTheory.Functor (OrbitCategory D n) (OrbitCategory D' n)

The functor D/[n] ⥤ D'/[n] induced on orbit categories by an additive functor commuting with the shifts: the descent of F followed by the projection.

@[simp]

theorem TauCeti.OrbitCategory.map_obj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.Additive] [F.CommShift ℤ] (X : OrbitCategory D n) : (map F).obj X = { obj := F.obj X.obj }

instance TauCeti.OrbitCategory.instAdditiveMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.Additive] [F.CommShift ℤ] : (map F).Additive

theorem TauCeti.OrbitCategory.map_map_projection_map {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.Additive] [F.CommShift ℤ] {X Y : D} (f : X ⟶ Y) : (map F).map (projection.map f) = projection.map (F.map f)

The induced functor sends the projection of a morphism f to the projection of F.map f.

theorem TauCeti.OrbitCategory.map_map_periodicity_hom_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.Additive] [F.CommShift ℤ] (X : D) : (map F).map (periodicity.hom.app X) = CategoryTheory.CategoryStruct.comp (projection.map ((CategoryTheory.Functor.commShiftIso F n).hom.app X)) (periodicity.hom.app (F.obj X))

The induced functor sends the periodicity isomorphism of the projection from D to the projected shift comparison of F followed by the periodicity isomorphism of the projection from D'.

@[simp]

theorem TauCeti.OrbitCategory.map_map_homOf {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.Additive] [F.CommShift ℤ] {X Y : D} (i : ℤ) (f : CategoryTheory.ShiftedHom X Y (n * i)) : (map F).map ((homOf i) f) = (homOf i) (f.map F)

The induced functor sends a homogeneous piece f : X ⟶ Y⟦n * i⟧ to the homogeneous piece f.map F, that is F.map f followed by the shift comparison of F at Y.

theorem TauCeti.OrbitCategory.map_map_eq_directSumMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.Additive] [F.CommShift ℤ] {X Y : D} (f : { obj := X } ⟶ { obj := Y }) : (map F).map f = (DirectSum.map fun (j : ℤ) => AddMonoidHom.mk' (fun (g : CategoryTheory.ShiftedHom X Y (n * j)) => g.map F) ⋯) f

On the orbit hom group from X to Y, the induced functor is the direct sum, over the degrees j, of the maps f ↦ f.map F on the homogeneous pieces f : X ⟶ Y⟦n * j⟧.

theorem TauCeti.OrbitCategory.map_map_bijective_iff {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.Additive] [F.CommShift ℤ] {X Y : D} : Function.Bijective (map F).map ↔ ∀ (j : ℤ), Function.Bijective fun (f : CategoryTheory.ShiftedHom X Y (n * j)) => f.map F

The induced functor is bijective on the orbit morphisms from X to Y exactly when F is bijective on the shifted morphisms X ⟶ Y⟦n * j⟧ of every degree j.

theorem TauCeti.OrbitCategory.lift_map_map_periodicity_hom_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.Additive] [F.CommShift ℤ] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] [CategoryTheory.Preadditive E] {G' : CategoryTheory.Functor D' E} [G'.Additive] {φ' : (CategoryTheory.shiftFunctor D' n).comp G' ≅ G'} (X : D) : (lift G' φ').map ((map F).map (periodicity.hom.app X)) = CategoryTheory.CategoryStruct.comp (G'.map ((CategoryTheory.Functor.commShiftIso F n).hom.app X)) (φ'.hom.app (F.obj X))

The descent of G' sends the image under map F of the periodicity isomorphism of the projection from D to the shift comparison of F followed by φ'.

noncomputable def TauCeti.OrbitCategory.mapCompLiftIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.Additive] [F.CommShift ℤ] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] [CategoryTheory.Preadditive E] {G : CategoryTheory.Functor D E} [G.Additive] {φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G} {G' : CategoryTheory.Functor D' E} [G'.Additive] {φ' : (CategoryTheory.shiftFunctor D' n).comp G' ≅ G'} (e : F.comp G' ≅ G) (he : ∀ (X : D), CategoryTheory.CategoryStruct.comp (G'.map ((CategoryTheory.Functor.commShiftIso F n).hom.app X)) (CategoryTheory.CategoryStruct.comp (φ'.hom.app (F.obj X)) (e.hom.app X)) = CategoryTheory.CategoryStruct.comp (e.hom.app (X⟦n⟧)) (φ.hom.app X)) : (map F).comp (lift G' φ') ≅ lift G φ

Descent along the induced functor on orbit categories. If e : F ⋙ G' ≅ G carries the periodicity isomorphism φ' of G', transported along the shift comparison of F, to the periodicity isomorphism φ of G, then the induced functor followed by the descent of G' is the descent of G, by e on components.

@[simp]

theorem TauCeti.OrbitCategory.mapCompLiftIso_hom_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.Additive] [F.CommShift ℤ] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] [CategoryTheory.Preadditive E] {G : CategoryTheory.Functor D E} [G.Additive] {φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G} {G' : CategoryTheory.Functor D' E} [G'.Additive] {φ' : (CategoryTheory.shiftFunctor D' n).comp G' ≅ G'} (e : F.comp G' ≅ G) (he : ∀ (X : D), CategoryTheory.CategoryStruct.comp (G'.map ((CategoryTheory.Functor.commShiftIso F n).hom.app X)) (CategoryTheory.CategoryStruct.comp (φ'.hom.app (F.obj X)) (e.hom.app X)) = CategoryTheory.CategoryStruct.comp (e.hom.app (X⟦n⟧)) (φ.hom.app X)) (X : D) : (mapCompLiftIso F e he).hom.app { obj := X } = e.hom.app X

@[simp]

theorem TauCeti.OrbitCategory.mapCompLiftIso_inv_app {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D a).Additive] {n : ℤ} {D' : Type u'} [CategoryTheory.Category.{v', u'} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (a : ℤ), (CategoryTheory.shiftFunctor D' a).Additive] (F : CategoryTheory.Functor D D') [F.Additive] [F.CommShift ℤ] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] [CategoryTheory.Preadditive E] {G : CategoryTheory.Functor D E} [G.Additive] {φ : (CategoryTheory.shiftFunctor D n).comp G ≅ G} {G' : CategoryTheory.Functor D' E} [G'.Additive] {φ' : (CategoryTheory.shiftFunctor D' n).comp G' ≅ G'} (e : F.comp G' ≅ G) (he : ∀ (X : D), CategoryTheory.CategoryStruct.comp (G'.map ((CategoryTheory.Functor.commShiftIso F n).hom.app X)) (CategoryTheory.CategoryStruct.comp (φ'.hom.app (F.obj X)) (e.hom.app X)) = CategoryTheory.CategoryStruct.comp (e.hom.app (X⟦n⟧)) (φ.hom.app X)) (X : D) : (mapCompLiftIso F e he).inv.app { obj := X } = e.inv.app X