The shift functor on H⁰

dg-enhancements-e6. IsPretriangulated.exists_shift says every object has a shift in every degree, as an existential. This file makes a choice, and shows the choice assembles into a functor H⁰ C ⥤ H⁰ C for each n.

The choice does not matter, and that is a theorem rather than a hope

shiftObj and shiftWitness are Classical.choice applied to exists_shift, so nothing about them is canonical on the nose. What makes them usable is IsShiftBy.compare_comp_compare: any two shifts of X by n are canonically isomorphic in Z⁰. So a different choice gives a naturally isomorphic functor, and IsShiftBy.mapShift_compare says the comparison is natural without a diagram to chase.

Descent to H⁰

The action on morphisms is IsShiftBy.mapShift, and it descends because it is additive (mapShift_add), preserves cocycles (mapShift_mem_cocycles) and preserves coboundaries (mapShift_mem_coboundaries). The descent argument is the one DGFunctor.h0 already uses, down to the leftRel_apply idiom.

Free degrees, and why

shiftFunctorAddIso' carries its target degree nm as a variable with n + m = nm as a hypothesis, rather than fixing it at n + m. Every coherence identity for a shift functor compares an object indexed by n + 0, 0 + n or (a + b) + c against one indexed by n, n or a + (b + c). Those indices are propositionally but not definitionally equal, so ShiftMkCore bridges them with eqToHom -- and with the degree fixed there is no way to normalise that eqToHom away. With the degree free, obtain rfl : nm = n eliminates a variable, the eqToHom acquires equal endpoints, and eqToHom_refl finishes it. Mathlib carries CochainComplex.shiftFunctorAdd' for exactly this reason.

What is proved, and what is not

All three of ShiftMkCore's coherence identities are proved here, in that general form: shiftFunctorAddIso'_hom_app_zero_right, ..._zero_left, and shiftFunctorAddIso'_assoc. The last one reduces, by compare_trans and mapShift_compare_comp', to compare from the chosen shift by m₁ + m₂ + m₃ to a threefold composite, and the two threefold composites have equal hom fields by comp'_assoc_hom.

The later computation lemmas identify Mathlib's additive and commutative shift comparisons with these same IsShiftBy.compare witnesses. They are the bridge used by compatibility proofs without replacing the existing HasShift instance.

So HasShift (H0 C) ℤ is an instance, not an aspiration: hasShift at the foot of this file. What dg-enhancements-e6 still owes after it is the transport theorem itself, IsPretriangulated C → Pretriangulated (H0 C), whose remaining clauses are the six fields of Pretriangulated rather than anything about the shift.

noncomputable def CategoryTheory.IsPretriangulated.shiftObj (C : Type u) [DGCategory C] [IsPretriangulated C] (X : C) (n : ℤ) : C

A chosen shift of X by n.

Equations

• CategoryTheory.IsPretriangulated.shiftObj C X n = ⋯.choose

noncomputable def CategoryTheory.IsPretriangulated.shiftWitness (C : Type u) [DGCategory C] [IsPretriangulated C] (X : C) (n : ℤ) : IsShiftBy X n (shiftObj C X n)

The witness that the chosen object really is a shift.

Equations

• CategoryTheory.IsPretriangulated.shiftWitness C X n = ⋯.some

noncomputable def CategoryTheory.H0.shiftFunctor (C : Type u) [DGCategory C] [IsPretriangulated C] (n : ℤ) : Functor (H0 C) (H0 C)

The shift functor on H⁰, at a fixed degree.

Quotient.map's well-definedness obligation is discharged exactly as in DGFunctor.h0: the relation is QuotientAddGroup.leftRel, so the hypothesis arrives as -f₁ + f₂ ∈ coboundaries and mapShiftHom's additivity turns mapShift_mem_coboundaries into what is needed.

Equations

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

@[simp]

theorem CategoryTheory.H0.shiftFunctor_map_mk (C : Type u) [DGCategory C] [IsPretriangulated C] (n : ℤ) {X Y : H0 C} (f : ↥(cocycles (of C X) (of C Y))) : (shiftFunctor C n).map ↑f = ↑⟨(IsPretriangulated.shiftWitness C (of C X) n).mapShift (IsPretriangulated.shiftWitness C (of C Y) n) ↑f, ⋯⟩

How the shift functor acts on a class. The computation rule simp needs before any square involving shiftFunctor will close.

instance CategoryTheory.H0.shiftFunctor_additive (C : Type u) [DGCategory C] [IsPretriangulated C] (n : ℤ) : (shiftFunctor C n).Additive

The shift functor is additive: mapShift is additive on representatives, and the quotient map is a group homomorphism.

noncomputable def CategoryTheory.H0.compareIso {C : Type u} [DGCategory C] {X Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (t : IsShiftBy X n Y') : (have this := Y; this) ≅ have this := Y'; this

Two shifts of the same object by the same degree, compared as an isomorphism in H⁰. The inverse is the comparison the other way, and compare_comp_compare is both triangle identities.

Equations

• CategoryTheory.H0.compareIso s t = { hom := ↑⟨s.compare t, ⋯⟩, inv := ↑⟨t.compare s, ⋯⟩, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def CategoryTheory.H0.shiftFunctorZeroIso (C : Type u) [DGCategory C] [IsPretriangulated C] : shiftFunctor C 0 ≅ Functor.id (H0 C)

shiftFunctor C 0 is the identity, up to natural isomorphism.

Naturality is IsShiftBy.mapShift_compare together with IsShiftBy.mapShift_self: shifting by zero does nothing to a morphism, and the comparison of two shifts is natural for free.

Equations

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

noncomputable def CategoryTheory.H0.shiftCompWitness' (C : Type u) [DGCategory C] [IsPretriangulated C] (X : C) (n m nm : ℤ) (hnm : n + m = nm) : IsShiftBy X nm (IsPretriangulated.shiftObj C (IsPretriangulated.shiftObj C X n) m)

The chosen shift by n followed by the chosen shift by m, as a shift by nm. The degree is a free variable for the reason IsShiftBy.comp' records: the coherence identities compare n + 0, 0 + n and (a + b) + c against n, n and a + (b + c), and only a free degree can be substed.

Equations

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

noncomputable def CategoryTheory.H0.shiftFunctorAddIso' (C : Type u) [DGCategory C] [IsPretriangulated C] (n m nm : ℤ) (hnm : n + m = nm) : shiftFunctor C nm ≅ (shiftFunctor C n).comp (shiftFunctor C m)

shiftFunctor C nm is shiftFunctor C n ⋙ shiftFunctor C m whenever n + m = nm, up to natural isomorphism.

Naturality is IsShiftBy.mapShift_compare followed by IsShiftBy.mapShift_comp'_shift, in the same shape as the degree-zero case: mapShift along a composite shift is mapShift twice, so the square is two rewrites and no diagram.

Equations

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

noncomputable def CategoryTheory.H0.shiftCompWitness (C : Type u) [DGCategory C] [IsPretriangulated C] (X : C) (n m : ℤ) : IsShiftBy X (n + m) (IsPretriangulated.shiftObj C (IsPretriangulated.shiftObj C X n) m)

The chosen shift by n followed by the chosen shift by m, at the definitional degree.

Equations

• CategoryTheory.H0.shiftCompWitness C X n m = CategoryTheory.H0.shiftCompWitness' C X n m (n + m) ⋯

noncomputable def CategoryTheory.H0.shiftFunctorAddIso (C : Type u) [DGCategory C] [IsPretriangulated C] (n m : ℤ) : shiftFunctor C (n + m) ≅ (shiftFunctor C n).comp (shiftFunctor C m)

shiftFunctorAddIso' at the definitional degree.

Equations

• CategoryTheory.H0.shiftFunctorAddIso C n m = CategoryTheory.H0.shiftFunctorAddIso' C n m (n + m) ⋯

theorem CategoryTheory.H0.shiftFunctorAddIso'_hom_app_zero_right (C : Type u) [DGCategory C] [IsPretriangulated C] (n nm : ℤ) (hnm : n + 0 = nm) (X : H0 C) : (shiftFunctorAddIso' C n 0 nm hnm).hom.app X = CategoryStruct.comp (eqToHom ⋯) ((shiftFunctorZeroIso C).inv.app ((shiftFunctor C n).obj X))

ShiftMkCore.add_zero_hom_app, in the general form where the target degree is free.

The free degree is the whole point: obtain rfl : nm = n eliminates a variable, which is exactly what n + 0 = n does not allow. Once it is gone the eqToHom has equal endpoints and collapses to the identity, and both sides reduce to (shiftWitness C (shiftObj C X n) 0).hom -- the left by inv_hom on the outer shift, the right by self_inv.

theorem CategoryTheory.H0.shiftFunctorAddIso'_hom_app_zero_left (C : Type u) [DGCategory C] [IsPretriangulated C] (n nm : ℤ) (hnm : 0 + n = nm) (X : H0 C) : (shiftFunctorAddIso' C 0 n nm hnm).hom.app X = CategoryStruct.comp (eqToHom ⋯) ((shiftFunctor C n).map ((shiftFunctorZeroIso C).inv.app X))

ShiftMkCore.zero_add_hom_app, in the general form where the target degree is free.

Same shape as the right-handed case, with one extra step: the right-hand side applies shiftFunctor to a comparison, and mapShift_compare_comp' turns that into a comparison of composites. What is left is that prefixing a shift with the zero shift does not change its inverse, which is comp'_self_left_inv.

theorem CategoryTheory.H0.shiftFunctorAddIso'_hom_app_congr (C : Type u) [DGCategory C] [IsPretriangulated C] (n m nm nm' : ℤ) (h : n + m = nm) (h' : n + m = nm') (X : H0 C) : (shiftFunctorAddIso' C n m nm h).hom.app X = CategoryStruct.comp (eqToHom ⋯) ((shiftFunctorAddIso' C n m nm' h').hom.app X)

Two shiftFunctorAddIso' at propositionally equal target degrees differ by the eqToHom between them. This is the bridge from the free-degree lemmas to ShiftMkCore's fields, whose degrees are fixed.

theorem CategoryTheory.H0.shiftFunctorAddIso'_assoc (C : Type u) [DGCategory C] [IsPretriangulated C] (m₁ m₂ m₃ m₁₂ m₂₃ m₁₂₃ : ℤ) (h₁₂ : m₁ + m₂ = m₁₂) (h₂₃ : m₂ + m₃ = m₂₃) (h : m₁₂ + m₃ = m₁₂₃) (X : H0 C) : CategoryStruct.comp ((shiftFunctorAddIso' C m₁₂ m₃ m₁₂₃ h).hom.app X) ((shiftFunctor C m₃).map ((shiftFunctorAddIso' C m₁ m₂ m₁₂ h₁₂).hom.app X)) = CategoryStruct.comp ((shiftFunctorAddIso' C m₁ m₂₃ m₁₂₃ ⋯).hom.app X) ((shiftFunctorAddIso' C m₂ m₃ m₂₃ h₂₃).hom.app ((shiftFunctor C m₁).obj X))

ShiftMkCore.assoc_hom_app, in the general form where every degree is free.

With the degrees free there is no eqToHom at all -- both sides are indexed by m₁₂₃ -- and the identity reduces to three moves with no diagram chase: mapShift_compare_comp' turns the functor applied to a comparison into a comparison of composites, compare_trans and compare_comp'_right collapse each side to a single comparison out of the chosen shift, and comp'_assoc_hom observes that the two threefold composites carry the same element.

noncomputable def CategoryTheory.H0.shiftMkCore (C : Type u) [DGCategory C] [IsPretriangulated C] : ShiftMkCore (H0 C) ℤ

Everything HasShift needs, assembled.

Equations

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

@[implicit_reducible]

noncomputable instance CategoryTheory.H0.hasShift (C : Type u) [DGCategory C] [IsPretriangulated C] : HasShift (H0 C) ℤ

H⁰ of a pretriangulated dg category has a shift by ℤ.

This is the second clause of a Pretriangulated structure, and the one dg-enhancements-e6 was sized around.

Equations

• CategoryTheory.H0.hasShift C = CategoryTheory.hasShiftMk (CategoryTheory.H0 C) ℤ (CategoryTheory.H0.shiftMkCore C)

theorem CategoryTheory.H0.shiftFunctorZero_eq (C : Type u) [DGCategory C] [IsPretriangulated C] : shiftFunctorZero (H0 C) ℤ = shiftFunctorZeroIso C

The ambient shiftFunctorZero is the comparison this file built. hasShiftMk records ShiftMkCore.zero as the shiftFunctorZero of the resulting HasShift, so this is ShiftMkCore.shiftFunctorZero_eq read back through shiftMkCore.

theorem CategoryTheory.H0.shiftFunctorAdd_eq (C : Type u) [DGCategory C] [IsPretriangulated C] (a b : ℤ) : shiftFunctorAdd (H0 C) a b = shiftFunctorAddIso C a b

The ambient shiftFunctorAdd is the comparison this file built.

theorem CategoryTheory.H0.shiftFunctorAdd'_eq_shiftFunctorAddIso' (C : Type u) [DGCategory C] [IsPretriangulated C] (a b ab : ℤ) (h : a + b = ab) : shiftFunctorAdd' (H0 C) a b ab h = shiftFunctorAddIso' C a b ab h

The ambient additive-shift comparison at a propositionally equal target degree is the free-degree comparison constructed from dg shift witnesses.

theorem CategoryTheory.H0.shiftFunctorCompIsoId_hom_app (C : Type u) [DGCategory C] [IsPretriangulated C] (n m : ℤ) (h : n + m = 0) (X : H0 C) : (shiftFunctorCompIsoId (H0 C) n m h).hom.app X = homMk ⟨(shiftCompWitness' C (of C X) n m 0 h).compare (IsShiftBy.self (of C X)), ⋯⟩

The cancellation comparison for two opposite shifts is the direct comparison from their composite dg shift witness to the unshifted object.

This exposes the representative used by Mathlib's shiftFunctorCompIsoId for the HasShift structure constructed above. It is the component-level bridge needed when a rotated triangle cancels an explicit pair of shifts.

@[simp]

theorem CategoryTheory.H0.shiftFunctorComm_hom_app (C : Type u) [DGCategory C] [IsPretriangulated C] (a b : ℤ) (X : H0 C) : (shiftFunctorComm (H0 C) a b).hom.app X = homMk ⟨(shiftCompWitness' C (of C X) a b (a + b) ⋯).compare (shiftCompWitness' C (of C X) b a (a + b) ⋯), ⋯⟩

On H⁰, the interchange of two shifts is the canonical comparison between the two composite dg shift witnesses.