cohomology of the shift is shift of the cohomology

Stream: Is there code for X?

[Kevin Buzzard]

Richard Hill asked me this in our last London Learning Lean meeting:

import Mathlib

variable (C : CochainComplex Ab ℤ)

example : C⟦(2 : ℤ)⟧.homology n ≅ C.homology (n + 2) := by
 sorry

Is this easy with our current definitions?

[Joël Riou]

This is in the file Algebra.Homology.HomotopyCategory.ShiftSequence.

[Adam Topaz]

import Mathlib

variable (C : CochainComplex Ab ℤ)

open CategoryTheory

noncomputable
example : C⟦(2 : ℤ)⟧.homology n ≅ C.homology (n + 2) :=
  CochainComplex.ShiftSequence.shiftIso _ _ _ _ (Int.add_comm _ _) |>.app _

[Adam Topaz]

Probably just beyond what exact? can currently do :-/

[Kevin Buzzard]

But not beyond #Is there code for X? ! Thanks a lot!

[Joël Riou]

The preferred phrasing should be:

open HomologicalComplex
noncomputable example {A : Type*} [Category A] [Abelian A] (C : CochainComplex A ℤ) (n : ℤ) :
    C⟦(2 : ℤ)⟧.homology n ≅ C.homology (n + 2) :=
  ((homologyFunctor _ _ 0).shiftIso _ _ _ (add_comm 2 n)).app C

[Joël Riou]

The notion Functor.ShiftSequence which is used here is not in the mathematical literature. It means that we attach to the functor homologyFunctor _ _ 0 : CochainComplex Ab ℤ ⥤ Ab the whole series of functors homologyFunctor _ _ n : CochainComplex Ab ℤ ⥤ Ab for all n : ℤ and we record isomorphisms about their behaviour with respect to the shift functors (and compatibilities of these isomorphisms). This is particularly useful in the triangulated context (e.g. the homotopy category, or the derived category): when we have a homological functor like F : DerivedCategory A ⥤ C, we should get long exact sequences like FX ⟶ FY ⟶ FZ ⟶ F(X⟦1⟧) for any distinguished triangle, but in the case F := DerivedCategory.homologyFunctor _ 0, that very exact sequence is H^0 X ⟶ H^0 Y ⟶ H^0 Z ⟶ H^0(X⟦1⟧). The use of this Functor.ShiftSequence structure allows to get a better looking long exact sequence ... ⟶ H^0 X ⟶ H^0 Y ⟶ H^0 Z ⟶ H^1 X ⟶ ....

[Richard Hill]

Thanks, that's really useful.