Graded exact categories

A graded exact category is a Quillen exact category equipped with a chosen internal grading shift {1}: an autoequivalence of the underlying additive category which is an isomorphism of exact categories, that is, whose functor and whose inverse are both conflation-exact. The shift is data, not a property, exactly as a pinning is: it is what gives the Grothendieck group of the category its ℤ-action [M] ↦ [M{1}].

Requiring the inverse to be conflation-exact is not automatic from requiring it of the functor. An autoequivalence can enlarge the class of conflations strictly, in which case its inverse does not induce the canonical inverse map on K₀. The theorem TauCeti.ExactStructure.isConflationExact_inverse_iff_reflectsConflations, proved alongside the transport of exact structures, identifies the extra hypothesis with reflection of conflations, which is the form in which it is usually checked.

Main definitions

• TauCeti.GradedExactStructure: an exact structure together with a conflation-exact autoequivalence, the grading shift.
• TauCeti.GradedExactStructure.split and TauCeti.GradedExactStructure.abelian: the split exact structure and the canonical exact structure of an abelian category are graded by an arbitrary additive autoequivalence, no compatibility being needed in either case.
• TauCeti.GradedConflationExact: a graded conflation-exact functor, namely a conflation-exact functor together with a chosen commutation isomorphism with the two grading shifts.
• TauCeti.GradedExactEquiv: a graded exact equivalence, namely an equivalence whose functor and whose inverse are conflation-exact, carrying such a commutation isomorphism.

Main results

• TauCeti.GradedExactStructure.conflation_shift_iff: a short complex is a conflation exactly when its shift is.

References

• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1–69, https://arxiv.org/abs/0811.1480, Section 2, for the exact structures which the grading shift is required here to preserve and to reflect.
• TauCetiRoadmap/GrothendieckEulerForms/README.md, Layer 2, which fixes the normalization [M{1}] = q[M] used downstream and requires the shift to be part of the data of a graded exact category.

structure TauCeti.GradedExactStructure (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] extends TauCeti.ExactStructure C : Type (max u₁ v₁)

A graded exact structure on an additive category: a Quillen exact structure together with a chosen autoequivalence {1}, the grading shift, whose functor and whose inverse both preserve the distinguished conflations.

The shift is data. Conflation-exactness of both directions supplies mutually inverse maps on Grothendieck groups induced by the shift and its inverse; see TauCeti.ExactStructure.isConflationExact_inverse_iff_reflectsConflations for the reformulation of the second hypothesis as reflection of conflations.

• Conflation : CategoryTheory.ObjectProperty (CategoryTheory.ShortComplex C)
• isKernelCokernelPair (S : CategoryTheory.ShortComplex C) : self.Conflation S → IsKernelCokernelPair S
• isClosedUnderIsomorphisms : self.Conflation.IsClosedUnderIsomorphisms
• isInflation_id (X : C) : self.IsInflation (CategoryTheory.CategoryStruct.id X)
• isDeflation_id (X : C) : self.IsDeflation (CategoryTheory.CategoryStruct.id X)
• isInflation_comp {X Y Z : C} (i : X ⟶ Y) (j : Y ⟶ Z) : self.IsInflation i → self.IsInflation j → self.IsInflation (CategoryTheory.CategoryStruct.comp i j)
• isDeflation_comp {X Y Z : C} (p : X ⟶ Y) (q : Y ⟶ Z) : self.IsDeflation p → self.IsDeflation q → self.IsDeflation (CategoryTheory.CategoryStruct.comp p q)
• hasPushouts_inflations : self.inflations.HasPushouts
• isStableUnderCobaseChange_inflations : self.inflations.IsStableUnderCobaseChange
• hasPullbacks_deflations : self.deflations.HasPullbacks
• isStableUnderBaseChange_deflations : self.deflations.IsStableUnderBaseChange
• shift : C ≌ C

  The grading shift {1}, an autoequivalence of the underlying additive category.

• shift_additive : self.shift.functor.Additive

  The grading shift is an additive functor.

• shift_exact : self.IsConflationExact self.toExactStructure self.shift.functor

  The grading shift preserves the distinguished conflations.

• shift_inverse_exact : self.IsConflationExact self.toExactStructure self.shift.inverse

  The inverse grading shift preserves the distinguished conflations.

theorem TauCeti.GradedExactStructure.shift_reflectsConflations {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) : E.ReflectsConflations E.toExactStructure E.shift.functor

The grading shift of a graded exact structure reflects conflations.

theorem TauCeti.GradedExactStructure.shift_inverse_reflectsConflations {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) : E.ReflectsConflations E.toExactStructure E.shift.inverse

The inverse grading shift of a graded exact structure reflects conflations.

@[simp]

theorem TauCeti.GradedExactStructure.conflation_shift_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (S : CategoryTheory.ShortComplex C) : E.Conflation (S.map E.shift.functor) ↔ E.Conflation S

A short complex is a conflation exactly when its shift is. This is the precise sense in which the grading shift is an isomorphism of exact categories.

@[simp]

theorem TauCeti.GradedExactStructure.conflation_shift_inverse_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (S : CategoryTheory.ShortComplex C) : E.Conflation (S.map E.shift.inverse) ↔ E.Conflation S

A short complex is a conflation exactly when its inverse shift is.

def TauCeti.GradedExactStructure.ofReflects {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (e : C ≌ C) [e.functor.Additive] (he : E.IsConflationExact E e.functor) (hr : E.ReflectsConflations E e.functor) : GradedExactStructure C

Build a graded exact structure from a shift which both preserves and reflects conflations. This is the form in which the hypothesis is usually available.

Equations

• TauCeti.GradedExactStructure.ofReflects E e he hr = { toExactStructure := E, shift := e, shift_additive := inst✝, shift_exact := he, shift_inverse_exact := ⋯ }

@[simp]

theorem TauCeti.GradedExactStructure.ofReflects_toExactStructure {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (e : C ≌ C) [e.functor.Additive] (he : E.IsConflationExact E e.functor) (hr : E.ReflectsConflations E e.functor) : (ofReflects E e he hr).toExactStructure = E

@[simp]

theorem TauCeti.GradedExactStructure.ofReflects_shift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (e : C ≌ C) [e.functor.Additive] (he : E.IsConflationExact E e.functor) (hr : E.ReflectsConflations E e.functor) : (ofReflects E e he hr).shift = e

noncomputable def TauCeti.GradedExactStructure.split (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (e : C ≌ C) [e.functor.Additive] : GradedExactStructure C

The split exact structure, graded by an arbitrary additive autoequivalence: every additive functor preserves split conflations, so no compatibility between the shift and the exact structure has to be checked.

Equations

• TauCeti.GradedExactStructure.split C e = { toExactStructure := TauCeti.ExactStructure.split C, shift := e, shift_additive := inst✝, shift_exact := ⋯, shift_inverse_exact := ⋯ }

@[simp]

theorem TauCeti.GradedExactStructure.split_toExactStructure {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (e : C ≌ C) [e.functor.Additive] : (split C e).toExactStructure = ExactStructure.split C

@[simp]

theorem TauCeti.GradedExactStructure.split_shift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (e : C ≌ C) [e.functor.Additive] : (split C e).shift = e

noncomputable def TauCeti.GradedExactStructure.abelian (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Abelian A] (e : A ≌ A) [e.functor.Additive] : GradedExactStructure A

The canonical exact structure of an abelian category, graded by an arbitrary additive autoequivalence: an equivalence preserves all finite limits and colimits, so again no compatibility has to be checked.

Equations

• TauCeti.GradedExactStructure.abelian A e = { toExactStructure := TauCeti.ExactStructure.abelian A, shift := e, shift_additive := inst✝, shift_exact := ⋯, shift_inverse_exact := ⋯ }

@[simp]

theorem TauCeti.GradedExactStructure.abelian_toExactStructure {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Abelian A] (e : A ≌ A) [e.functor.Additive] : (abelian A e).toExactStructure = ExactStructure.abelian A

@[simp]

theorem TauCeti.GradedExactStructure.abelian_shift {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Abelian A] (e : A ≌ A) [e.functor.Additive] : (abelian A e).shift = e

structure TauCeti.GradedConflationExact {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : GradedExactStructure C) (E' : GradedExactStructure D) (F : CategoryTheory.Functor C D) [F.Additive] : Type (max u₁ v₂)

A graded conflation-exact functor between graded exact categories: a conflation-exact functor together with a chosen isomorphism commuting it with the two grading shifts.

The commutation isomorphism is data rather than a property, since the induced ℤ-equivariance of the map on Grothendieck groups is proved from it.

• isConflationExact : E.IsConflationExact E'.toExactStructure F

  The underlying functor is conflation-exact.

• commShift : E.shift.functor.comp F ≅ F.comp E'.shift.functor

  The chosen isomorphism commuting the functor with the two grading shifts.

def TauCeti.GradedConflationExact.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) : GradedConflationExact E E (CategoryTheory.Functor.id C)

The identity functor is graded conflation-exact.

Equations

• TauCeti.GradedConflationExact.id E = { isConflationExact := ⋯, commShift := E.shift.functor.rightUnitor ≪≫ E.shift.functor.leftUnitor.symm }

@[simp]

theorem TauCeti.GradedConflationExact.id_commShift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) : (GradedConflationExact.id E).commShift = E.shift.functor.rightUnitor ≪≫ E.shift.functor.leftUnitor.symm

The shift-commutation isomorphism of the identity graded conflation-exact functor.

def TauCeti.GradedConflationExact.comp {C : Type u₁} {D : Type u₂} {K : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.Category.{v₃, u₃} K] [CategoryTheory.Preadditive K] [CategoryTheory.Limits.HasZeroObject K] [CategoryTheory.Limits.HasBinaryBiproducts K] {E : GradedExactStructure C} {E' : GradedExactStructure D} {E'' : GradedExactStructure K} {F : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D K} [F.Additive] [H.Additive] (h : GradedConflationExact E E' F) (h' : GradedConflationExact E' E'' H) : GradedConflationExact E E'' (F.comp H)

A composite of graded conflation-exact functors is graded conflation-exact, for the composed commutation isomorphism.

Equations

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

@[simp]

theorem TauCeti.GradedConflationExact.comp_commShift {C : Type u₁} {D : Type u₂} {K : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.Category.{v₃, u₃} K] [CategoryTheory.Preadditive K] [CategoryTheory.Limits.HasZeroObject K] [CategoryTheory.Limits.HasBinaryBiproducts K] {E : GradedExactStructure C} {E' : GradedExactStructure D} {E'' : GradedExactStructure K} {F : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D K} [F.Additive] [H.Additive] (h : GradedConflationExact E E' F) (h' : GradedConflationExact E' E'' H) : (h.comp h').commShift = (E.shift.functor.associator F H).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight h.commShift H ≪≫ F.associator E'.shift.functor H ≪≫ F.isoWhiskerLeft h'.commShift ≪≫ (F.associator H E''.shift.functor).symm

The shift-commutation isomorphism of a composite graded conflation-exact functor.

structure TauCeti.GradedExactEquiv {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : GradedExactStructure C) (E' : GradedExactStructure D) : Type (max (max (max u₁ u₂) v₁) v₂)

A graded exact equivalence between graded exact categories: an equivalence of the underlying additive categories whose functor and whose inverse are both conflation-exact, together with a chosen isomorphism commuting the functor with the two grading shifts.

Conflation-exactness of the inverse is again an extra hypothesis, for the reason recorded on TauCeti.GradedExactStructure: it supplies the inverse map on Grothendieck groups induced by the inverse functor.

• equiv : C ≌ D

  The underlying equivalence of the additive categories.

• functor_additive : self.equiv.functor.Additive

  The underlying equivalence is additive.

• isConflationExact : E.IsConflationExact E'.toExactStructure self.equiv.functor

  The equivalence is conflation-exact.

• inverse_isConflationExact : E'.IsConflationExact E.toExactStructure self.equiv.inverse

  The inverse equivalence is conflation-exact.

• commShift : E.shift.functor.comp self.equiv.functor ≅ self.equiv.functor.comp E'.shift.functor

  The chosen isomorphism commuting the equivalence with the two grading shifts.

def TauCeti.GradedExactEquiv.toGradedConflationExact {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : GradedExactStructure C} {E' : GradedExactStructure D} (h : GradedExactEquiv E E') : GradedConflationExact E E' h.equiv.functor

The graded conflation-exact functor underlying a graded exact equivalence.

Equations

• h.toGradedConflationExact = { isConflationExact := ⋯, commShift := h.commShift }

@[simp]

theorem TauCeti.GradedExactEquiv.toGradedConflationExact_commShift {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : GradedExactStructure C} {E' : GradedExactStructure D} (h : GradedExactEquiv E E') : h.toGradedConflationExact.commShift = h.commShift

Passing to the underlying graded conflation-exact functor preserves the commutation isomorphism.

def TauCeti.GradedExactEquiv.refl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) : GradedExactEquiv E E

The identity equivalence is a graded exact equivalence.

Equations

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

@[simp]

theorem TauCeti.GradedExactEquiv.refl_equiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) : (GradedExactEquiv.refl E).equiv = CategoryTheory.Equivalence.refl

The equivalence underlying the identity graded exact equivalence.

@[simp]

theorem TauCeti.GradedExactEquiv.refl_commShift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) : (GradedExactEquiv.refl E).commShift ≍ E.shift.functor.rightUnitor ≪≫ E.shift.functor.leftUnitor.symm

The shift-commutation isomorphism of the identity graded exact equivalence.

def TauCeti.GradedExactEquiv.symm {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : GradedExactStructure C} {E' : GradedExactStructure D} (h : GradedExactEquiv E E') : GradedExactEquiv E' E

The inverse of a graded exact equivalence is a graded exact equivalence.

Equations

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

@[simp]

theorem TauCeti.GradedExactEquiv.symm_equiv {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : GradedExactStructure C} {E' : GradedExactStructure D} (h : GradedExactEquiv E E') : h.symm.equiv = h.equiv.symm

The equivalence underlying the inverse of a graded exact equivalence.

@[simp]

theorem TauCeti.GradedExactEquiv.symm_commShift {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : GradedExactStructure C} {E' : GradedExactStructure D} (h : GradedExactEquiv E E') : h.symm.commShift ≍ (E'.shift.functor.comp h.equiv.inverse).leftUnitor.symm ≪≫ CategoryTheory.Functor.isoWhiskerRight h.equiv.counitIso.symm (E'.shift.functor.comp h.equiv.inverse) ≪≫ h.equiv.inverse.associator h.equiv.functor (E'.shift.functor.comp h.equiv.inverse) ≪≫ h.equiv.inverse.isoWhiskerLeft (h.equiv.functor.associator E'.shift.functor h.equiv.inverse).symm ≪≫ h.equiv.inverse.isoWhiskerLeft (CategoryTheory.Functor.isoWhiskerRight h.commShift.symm h.equiv.inverse) ≪≫ h.equiv.inverse.isoWhiskerLeft (E.shift.functor.associator h.equiv.functor h.equiv.inverse) ≪≫ (h.equiv.inverse.associator E.shift.functor (h.equiv.functor.comp h.equiv.inverse)).symm ≪≫ (h.equiv.inverse.comp E.shift.functor).isoWhiskerLeft h.equiv.unitIso.symm ≪≫ h.equiv.inverse.associator E.shift.functor (CategoryTheory.Functor.id C) ≪≫ h.equiv.inverse.isoWhiskerLeft E.shift.functor.rightUnitor

The shift-commutation isomorphism of the inverse of a graded exact equivalence.

def TauCeti.GradedExactEquiv.trans {C : Type u₁} {D : Type u₂} {K : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.Category.{v₃, u₃} K] [CategoryTheory.Preadditive K] [CategoryTheory.Limits.HasZeroObject K] [CategoryTheory.Limits.HasBinaryBiproducts K] {E : GradedExactStructure C} {E' : GradedExactStructure D} {E'' : GradedExactStructure K} (h : GradedExactEquiv E E') (h' : GradedExactEquiv E' E'') : GradedExactEquiv E E''

A composite of graded exact equivalences is a graded exact equivalence, for the composed commutation isomorphism.

Equations

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

@[simp]

theorem TauCeti.GradedExactEquiv.trans_equiv {C : Type u₁} {D : Type u₂} {K : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.Category.{v₃, u₃} K] [CategoryTheory.Preadditive K] [CategoryTheory.Limits.HasZeroObject K] [CategoryTheory.Limits.HasBinaryBiproducts K] {E : GradedExactStructure C} {E' : GradedExactStructure D} {E'' : GradedExactStructure K} (h : GradedExactEquiv E E') (h' : GradedExactEquiv E' E'') : (h.trans h').equiv = h.equiv.trans h'.equiv

The equivalence underlying a composite of graded exact equivalences.

@[simp]

theorem TauCeti.GradedExactEquiv.trans_commShift {C : Type u₁} {D : Type u₂} {K : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.Category.{v₃, u₃} K] [CategoryTheory.Preadditive K] [CategoryTheory.Limits.HasZeroObject K] [CategoryTheory.Limits.HasBinaryBiproducts K] {E : GradedExactStructure C} {E' : GradedExactStructure D} {E'' : GradedExactStructure K} (h : GradedExactEquiv E E') (h' : GradedExactEquiv E' E'') : (h.trans h').commShift ≍ (E.shift.functor.associator h.equiv.functor h'.equiv.functor).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight h.commShift h'.equiv.functor ≪≫ h.equiv.functor.associator E'.shift.functor h'.equiv.functor ≪≫ h.equiv.functor.isoWhiskerLeft h'.commShift ≪≫ (h.equiv.functor.associator h'.equiv.functor E''.shift.functor).symm

The shift-commutation isomorphism of a composite graded exact equivalence.