cohomology complex

[DanGrayson]

I noticed this, @tpannila :

  Definition CohomologyComplex (C : (ComplexPreCat_AbelianPreCat A hs)) :
    ComplexPreCat_AbelianPreCat A hs.
  Proof.
    cbn in *.
    use mk_Complex.
    - intros i.
      exact (Abelian.Cokernel (KernelIn to_Zero (Abelian.Kernel (Diff C i)) _ _
                                        (CohomologyComplex_KernelIn_eq C i))).
    - intros i. exact (ZeroArrow (to_Zero) _ _).
    - intros i. cbn. apply ZeroArrow_comp_left.
  Defined.

Here A is an Abelian category and this definition construct a chain complex whose objects are the cohomology objects of C and whose differentials are all 0. Rather than simulating a graded object of C with a chain complex of C whose differentials are 0, I suggest introducing the notion of graded object directly.

[tpannila]

@DanGrayson , I think this is a good idea. Can you do it? At the moment, I'm trying to formalize t-structure stuff and thus I don't have time to do it anytime soon.

[DanGrayson]

I'm going to be working on other stuff, too. But this issue is visible, and eventually someone will want to do it.

Random thought: is there a good reason to make a category whose objects are graded objects? We could just define for each integer n the cohomology functor H^n from complexes in A to A, and deal with them directly.

[vladimirias]

It might make sense to have the definition of a complex as a graded object with a differential instead of a family of objects. This will remove the need to worry about things such as that X ((n + 1) + 1) is not the same type as X (n + 2).

On Feb 24, 2017, at 8:50 AM, Daniel R. Grayson notifications@github.com wrote:

I'm going to be working on other stuff, too. But this issue is visible, and eventually someone will want to do it.

Random thought: is there a good reason to make a category whose objects are graded objects? We could just define for each integer n the cohomology functor H^n from complexes in A to A, and deal with them directly.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/UniMath/UniMath/issues/604#issuecomment-282295566, or mute the thread https://github.com/notifications/unsubscribe-auth/AAZ4S-f5-B5Ga1SCdG55ASEQbuiGDZMpks5rfuAygaJpZM4MKFGj.

[tpannila]

Sorry, I have thought of this idea more and now I think it is bad. In homological algebra one should never forget the complex structure. The idea of homological algebra is that things should be defined at the level of complexes, see for example derived functors. Even in the case of cohomology complex, I think one should not forget complex structure, so that taking cohomology complex is an operation on complexes.

[DanGrayson]

No, the point of taking cohomology is exactly to lose the complex structure. There is no complex structure to retain. Your reference to derived functors would only make sense if cohomology were compatible with distinguished triangles, but it's not.

[DanGrayson]

Re: "It might make sense to have the definition of a complex as a graded object with a differential instead of a family of objects. This will remove the need to worry about things such as that X ((n + 1) + 1) is not the same type as X (n + 2)."

I don't understand that. Can you explain?